1. Mathematical Induction

Definition 1.1. Mathematical induction is a method of mathematical proof typically used to establish a given statement for all natural numbers p(n). It is a form of direct proof, and it is done in two steps: base case, inductive step.

The first step, known as the base case, is to prove the given statement for the first natural number. The second step, known as the inductive step, is to prove that the given statement for any one natural number implies the given statement for the next natural number. From these two steps, mathematical induction is the rule from which we infer that the given statement is established for all natural numbers.

Let us consider example of p(n) which is :

1 + 3 + 5 + ... + (2n - 1) = (n^2)

It is convenient to talk about a statement p(n). For n=1, p(1) says that 1 = (1^2) which is incidentally true. For n=2, p(2) says that 1 + 3 = (2^2) which is true, p(3) means that 1 + 3 + 5 = (3^2) which is also true. And so on... These particular cases are obtained by substituting specific values 1, 2, 3 for n into p(n).

Assume you want to prove that for some statement p, p(n) is true for all n starting with n = 1. How to do this ?

Have you heard of the "infinite line of dominos effect"?

Step 1. The first domino falls
Step 2. When any domino falls, the next domino falls, so ... all dominos will fall!

That is how Mathematical Induction works.

In the world of numbers we say:

Let p(n) denote the statement involving the integer variable n. The Principle of Mathematical Induction states:

If p(1) is true and, for each integer k ⩾ 1, p(k+1) is true whenever p(k) is true then p(n) is true for all n ⩾ 1 .

Therefore if we divide it into steps we get:

Step 1 is usually easy, we just have to prove it is true for n=1.

Step 2 is best done this way:
				• Assume it is true for n=k;
				• Prove it is true for n=k+1 (we can use the n=k case as a fact.).

Consider examples below.

(*Kludge b could not be a local var *)
m1[]:=DynamicModule[{s,eq,term,sum,s1,s2,s3,s4,s5,s6},

Dynamic@Panel@Column[{

Button["Again",
{{term, sum},s}=RandomChoice@eq;
],

"Prove by induction: "<>If[s==s5,"",s["step 0"]<>If[s==s6," > ",If[s==s3,"(n times) = ","="]]]<>s["sum 0"]<>If[s==s5," is divisible by "<>s["step 0"],""]<>If[s==s6," for all n ⩾ "<>s["n0"]," for all n ∈ (SubPlus[ℕ])"],
"Proof:",
Spacer[100],
"Step 1: n=1",
s["sum 1"]<>"="<>s["step 1"]<>If[s==s5," is divisible by "<>s["step 0"],""],
If[s==s4,"1 =  1"],
Spacer[100],
"Step 2:",
"Assume that it is true for n=k:",
If[s==s5,
s["sum n"]<>" is divisible by "<>s["step 0"]<>"\n"<>s["sum n"]<>" = "<>s["step 0"]<>"m, where m is positive integer."<>"      (•)"
,
s["step n"]<>If[s==s6," > "," = "]<>s["sum n"]<>"      (•)"],

"\nProve that it is true for n=k+1: ",
If[s==s6,
s["sum n+1"]<>" = "<>s["step all"]<>"\n"
,
If[s==s5,
s["sum n+1"]<>" = "<>s["step all"]<>" = ("<>s["step n"]<>") + "<>s["step all2"]
,
s["step n+1"]<>
If[s==s4,
s["step all"]
,
"=("<>s["step n"]<>") + "<>s["term n+1"]<>" = \[VerticalSeparator] from (•) \[VerticalSeparator] ="]
]
],
If[s==s6,Plot[{(k-1)^2 - 2, 0} , {k,-7, 7},PlotLegends->{"(k-1)^2 - 2","0"}],If[s==s5,"",If[s==s4,"","=("<>s["sum n"]<>")+"<>s["term n+1"]]]],

If[s==s6,"",If[s==s5,"","\nNote that after appropriate transformation of above result, we get that: "]],
If[s==s6,"",If[s==s5,"",If[s==s4,s["step all2"],"("<>s["sum n"]<>")+"<>s["term n+1"]]<>" = " <>s["sum n+1"]]],

If[s==s6,"",If[s==s5,"",If[s==  s4 ,"","\nWe can also consider delta of sums for k+1 terms and k terms, to check if difference is exactly k+1 element:"]]],
If[s==s6,"",If[s==s5,"",If[s== s4 ,"",s["delta sum"]<>"="<>s["Expand delta sum"]<>"="]]],
If[s==s6,"",If[s==s5,"",If[s== s4 ,"","="<>s["delta sum EXP"]]]],

"\nTherefore, the proof is complete since it has been shown to be true for n = 1, n = k, and n = k + 1, so",
If[s==s5,"",s["step 0"]<>If[s==s6," > ",If[s==s3,"(n times) = ","="]]]<>s["sum 0"]<>If[s==s5," is divisible by "<>s["step 0"],""]<>If[s==s6," for all n ⩾"<>s["n0"]," for all n ∈ (SubPlus[ℕ])"]
}],


Initialization:>(
eq={
{{k^2,k*(k+1)*(2*k+1)/6},s1},
{{k,k*(k+1)/2},s1},
{{k^3,(k*(k+1)/2)^2}, s1},
{{1,k}, s3},
{{2*k-1,k^2}, s1} ,(*FIXME: make another s1 fix the formatting *)
{{(2^(k-1)),2^k-1}, s2} ,(*s2*)
(*Anna new examples*)
{{k^3,(k^2)*((k+1)^2)/4},s1},
{{k*(k+1),k*(k+1)*(k+2)/3},s1},
(*{{1/((3k-2)*(3k+1)),k/(3k+1)},s1},*)
{{k*k!,(k+1)!-1},s1},
{{(k+1)*2^k,k*2^(k+1)},s1},
(*{{(-1^(k+1)*k^2),(((-1)^(k+1))*k*(k+1))/2},s1},*) (*FIXME fix the formatting(-1) *)
{{1/(k*(k+1)),k/(k+1)},s1},
(*examples Derivative*)
{{"(d/dx)[(x^n)]",k*"x"^(k-1)},s4} ,
(*examples "divisible by"*)
{{3,k^3 + 2k},s5},
(*examples with inequality*)
{{(2^k),(k^2)},s6}

};

{{term, sum},s}=RandomChoice@eq;
s6:=<|
(*first line*)
"n0"->ToString[5,TraditionalForm],
"step 0"->StringReplace[ToString[ToString[term,TraditionalForm],TraditionalForm],"k"->"n"],
"sum 0"->StringReplace[ToString[sum,TraditionalForm],"k"->"n"],
(*rest*)
"step 1"->ToString[(term/.(k->"1")),TraditionalForm],
"sum 1"->ToString[(sum/.(k->"1")),TraditionalForm],

"step n"->ToString[ToString[term,TraditionalForm],TraditionalForm],

"term n"->ToString[term,TraditionalForm],
"term n+1"->ToString[term/.(k->(k+1)),TraditionalForm],

(*Step n+1*)
"step n+1"->ToString[Sum[StringReplace[ToString[term,TraditionalForm],{"k"->ToString@(i)}], {i,1,3}]+"... + "<>ToString[term/.{k->"k"},TraditionalForm]<>"+"<>ToString[term/.{k->"(k+1)"},TraditionalForm],TraditionalForm],

(*Sum n *)
"sum n"->ToString[sum,TraditionalForm],
"sum n EXP"->sum,


(*Sum n + 1 *)
"sum n+1"->ToString[(sum/.{k->(k+1)}),TraditionalForm],
"sum n+1 EXP"->(sum/.{k->(k+1)}),

"step all" -> "(2^k)2 > |from (•)| > 2\!\(\*SuperscriptBox[\(k\), \(\(2\)\(\\ \)\)]\) > (k+1\!\(\*SuperscriptBox[\()\), \(\(2\)\(\\ \\ \)\)]\) \n The last inequality holds since \n 2\!\(\*SuperscriptBox[\(k\), \(\(2\)\(\\ \)\)]\) - (k+1\!\(\*SuperscriptBox[\()\), \(\(2\)\(\\ \\ \)\)]\) = (k-1\!\(\*SuperscriptBox[\()\), \(\(2\)\(\\ \\ \)\)]\)- 2 > 0 , whenever k ⩾ 5.",

(* Subtranct Sum n+1 - Sum n*)
"delta sum"->ToString[ToString[(sum/.{k->"(k+1)"}),TraditionalForm]<>" - ("<>ToString[sum/.{k-> "k"},TraditionalForm]<>")", TraditionalForm],

"delta sum EXP"->ToString[Simplify[(sum/.{k->(k+1)})-sum],TraditionalForm],
(* Expand and simplify Subtranct Sum n+1 - Sum n*)

"Expand delta sum"->ToString[ToString[Expand@(sum/.{k->(k+1)}),TraditionalForm]<>" - ("<>ToString[Expand@(sum),TraditionalForm]<>")",TraditionalForm],


"Expand delta sum EXP"->Expand[(sum/.{k->(k+1)})-sum]
|>;


s5:=<|
(*first line*)
"step 0"->ToString[term,TraditionalForm],
"sum 0"->StringReplace[ToString[sum,TraditionalForm],"k"->"n"],
(*rest*)
"step 1"->ToString[(term/.(k->"1")),TraditionalForm],
"sum 1"->ToString[(sum/.(k->"1")),TraditionalForm],

"step n"->ToString[sum,TraditionalForm],

"term n"->ToString[term,TraditionalForm],
"term n+1"->ToString[term/.(k->(k+1)),TraditionalForm],

(*Step n+1*)
"step n+1"->ToString[Sum[StringReplace[ToString[term,TraditionalForm],{"k"->ToString@(i)}], {i,1,3}]+"... + "<>ToString[term/.{k->"k"},TraditionalForm]<>"+"<>ToString[term/.{k->"(k+1)"},TraditionalForm],TraditionalForm],

(*Sum n *)
"sum n"->ToString[sum,TraditionalForm],
"sum n EXP"->sum,


(*Sum n + 1 *)
"sum n+1"->ToString[(sum/.{k->(k+1)}),TraditionalForm],
"sum n+1 EXP"->(sum/.{k->(k+1)}),

"step all" -> ToString[Expand@(sum/.{k->(k+1)}),TraditionalForm],
"step all2"->" 3(k^2) + 3k +3 = \[VerticalSeparator] from (•) \[VerticalSeparator] =\n= 3m + 3((k^2) + k + 1) is  divisible by 3",


(* Subtranct Sum n+1 - Sum n*)
"delta sum"->ToString[ToString[(sum/.{k->"(k+1)"}),TraditionalForm]<>" - ("<>ToString[sum/.{k-> "k"},TraditionalForm]<>")", TraditionalForm],

"delta sum EXP"->ToString[Simplify[(sum/.{k->(k+1)})-sum],TraditionalForm],
(* Expand and simplify Subtranct Sum n+1 - Sum n*)

"Expand delta sum"->ToString[ToString[Expand@(sum/.{k->(k+1)}),TraditionalForm]<>" - ("<>ToString[Expand@(sum),TraditionalForm]<>")",TraditionalForm],


"Expand delta sum EXP"->Expand[(sum/.{k->(k+1)})-sum]
|>;


s4:=<|
(*first line*)
"step 0"->StringReplace[ToString[ToString[term,TraditionalForm],TraditionalForm],"k"->"n"],
"sum 0"->StringReplace[ToString[sum,TraditionalForm],"k"->"n"],
(*rest*)
"step 1"->ToString["(d/dx)[(x^1)]",TraditionalForm],
"sum 1"->ToString[(sum/.(k->"1")),TraditionalForm],

"step n"->"(d/dx)[(x^k)]",

"term n"->ToString[term,TraditionalForm],
"term n+1"->ToString[term/.(k->(k+1)),TraditionalForm],

(*Step n+1*)
"step n+1"->"(d/dx)[(x^(k + 1))]",
"step all" ->" = (d/dx)[(x^k)x] = |(d/dx)[fg] = f'g + fg' | = ((d/dx)[(x^k)])x + (x^k)((d/dx)[x]) = |from (•)| =\n= \!\(\*SuperscriptBox[\(kx\), \(\(k\)\(-\)\(1\)\(\\ \)\)]\)x + (x^k) = (x^k)(k+1)" ,
"step all2" -> "(x^k)(k+1)",

(*Sum n *)
"sum n"->ToString[sum,TraditionalForm],
"sum n EXP"->sum,


(*Sum n + 1 *)
"sum n+1"->ToString[(sum/.{k->(k+1)}),TraditionalForm],
"sum n+1 EXP"->(sum/.{k->(k+1)}),
(* Subtranct Sum n+1 - Sum n*)
"delta sum"->ToString[ToString[(sum/.{k->"(k+1)"}),TraditionalForm]<>" - ("<>ToString[sum/.{k-> "k"},TraditionalForm]<>")", TraditionalForm],

"delta sum EXP"->ToString[Simplify[(sum/.{k->(k+1)})-sum],TraditionalForm],
(* Expand and simplify Subtranct Sum n+1 - Sum n*)

"Expand delta sum"->ToString[ToString[ToString[Expand@(sum/.{k->(k+1)}),TraditionalForm]<>" - ("<>ToString[Expand@(sum),TraditionalForm],TraditionalForm]<>")",TraditionalForm],


"Expand delta sum EXP"->Expand[(sum/.{k->(k+1)})-sum]
|>;


s1:=<|
(*first line*)
"step 0"->StringReplace[ToString[Sum[StringReplace[ToString[term,TraditionalForm],{"k"->ToString@i}], {i,1,3}]+"... + "<>ToString[term,TraditionalForm],TraditionalForm],"k"->"n"],
"sum 0"->StringReplace[ToString[sum,TraditionalForm],"k"->"n"],
(*rest*)
"step 1"->ToString[(term/.(k->"1")),TraditionalForm],
"sum 1"->ToString[(sum/.(k->"1")),TraditionalForm],

"step n"->ToString[Sum[StringReplace[ToString[term,TraditionalForm],{"k"->ToString@i}], {i,1,3}]+"... + "<>ToString[term,TraditionalForm],TraditionalForm],

"term n"->ToString[term,TraditionalForm],
"term n+1"->ToString[term/.(k->(k+1)),TraditionalForm],

(*Step n+1*)
"step n+1"->ToString[Sum[StringReplace[ToString[term,TraditionalForm],{"k"->ToString@(i)}], {i,1,3}]+"... + "<>ToString[term/.{k->"k"},TraditionalForm]<>"+"<>ToString[term/.{k->"(k+1)"},TraditionalForm],TraditionalForm],

(*Sum n *)
"sum n"->ToString[sum,TraditionalForm],
"sum n EXP"->sum,


(*Sum n + 1 *)
"sum n+1"->ToString[(sum/.{k->(k+1)}),TraditionalForm],
"sum n+1 EXP"->(sum/.{k->(k+1)}),


(* Subtranct Sum n+1 - Sum n*)
"delta sum"->ToString[ToString[(sum/.{k->"(k+1)"}),TraditionalForm]<>" - ("<>ToString[sum/.{k-> "k"},TraditionalForm]<>")", TraditionalForm],

"delta sum EXP"->ToString[Simplify[(sum/.{k->(k+1)})-sum],TraditionalForm],
(* Expand and simplify Subtranct Sum n+1 - Sum n*)

"Expand delta sum"->ToString[ToString[Expand@(sum/.{k->(k+1)}),TraditionalForm]<>" - ("<>ToString[Expand@(sum),TraditionalForm]<>")",TraditionalForm],


"Expand delta sum EXP"->Expand[(sum/.{k->(k+1)})-sum]
|>;



s2:=<|
(*for n *)

(*first line*)
"step 0"->StringReplace[ToString[Sum[StringReplace[ToString[term,TraditionalForm],{"k - 1"->ToString@(i-1)}], {i,1,3}]+"... + "<>StringReplace[ToString[term,TraditionalForm],{"k - 1"->("k-1")}],TraditionalForm],"k"->"n"],
"sum 0"->StringReplace[ToString[sum,TraditionalForm],"k"->"n"],
(*rest*)

"step 1"->ToString[(term/.(k->"1")),TraditionalForm],
"sum 1"->ToString[(sum/.(k->"1")),TraditionalForm],

"step n"->ToString[Sum[StringReplace[ToString[term,TraditionalForm],{"k - 1"->ToString@(i-1)}], {i,1,3}]+"... + "(*<>ToString[term,TraditionalForm]<>" + "*)<>StringReplace[ToString[term,TraditionalForm],{"k - 1"->("k-1")}],TraditionalForm],

"term n"->ToString[term,TraditionalForm],
"term n+1"->ToString[term/.(k->(k+1)),TraditionalForm],

(*Step n+1*)
"step n+1"->ToString[Sum[StringReplace[ToString[term,TraditionalForm],{"k - 1"->ToString@(i-1)}], {i,1,3}]+"... + "<>StringReplace[ToString[term,TraditionalForm],{"k - 1"->("k")}],TraditionalForm],


(*Sum n *)
"sum n"->ToString[sum,TraditionalForm],
"sum n EXP"->sum,


(*Sum n + 1 *)
"sum n+1"->ToString[(sum/.{k->(k+1)}),TraditionalForm],
"sum n+1 EXP"->(sum/.{k->(k+1)}),


(* Subtranct Sum n+1 - Sum n*)
"delta sum"->ToString[ToString[ToString[(sum/.{k->(k+1)}),TraditionalForm]<>" - ("<>ToString[sum,TraditionalForm], TraditionalForm]<>")",TraditionalForm],

"delta sum EXP"->ToString[Simplify[(sum/.{k->(k+1)})-sum],TraditionalForm],
(* Expand and simplify Subtranct Sum n+1 - Sum n*)

"Expand delta sum"->ToString[ToString[Expand@(sum/.{k->(k+1)}),TraditionalForm]<>" - ("<>ToString[Expand@sum,TraditionalForm]<>")",TraditionalForm],


"Expand delta sum EXP"->Expand[(sum/.{k->(k+1)})-sum]
|>;




s3:=<|
(*first line*)
"step 0"->StringReplace[ToString["1 + 1 + 1 + ... + "<>ToString[term,TraditionalForm],TraditionalForm],"k"->"n"],
"sum 0"->StringReplace[ToString[sum,TraditionalForm],"k"->"n"],
(*rest*)
"step 1"->ToString[(term/.(k->"1")),TraditionalForm],
"sum 1"->ToString[(sum/.(k->"1")),TraditionalForm],

"step n"->ToString["1 + 1 + 1 ... + "<>ToString[term,TraditionalForm],TraditionalForm],

"term n"->ToString[term,TraditionalForm],
"term n+1"->ToString[term/.(k->(k+1)),TraditionalForm],

(*Step n+1*)
"step n+1"->ToString["1 + 1 + 1 + ... + "<>ToString[term/.{k->"k"},TraditionalForm]<>"+"<>ToString[term/.{k->"(k+1)"},TraditionalForm],TraditionalForm],

(*Sum n *)
"sum n"->ToString[sum,TraditionalForm],
"sum n EXP"->sum,


(*Sum n + 1 *)
"sum n+1"->ToString[(sum/.{k->(k+1)}),TraditionalForm],
"sum n+1 EXP"->(sum/.{k->(k+1)}),


(* Subtranct Sum n+1 - Sum n*)
"delta sum"->ToString[ToString[(sum/.{k->"(k+1)"}),TraditionalForm]<>" - ("<>ToString[sum/.{k-> "k"},TraditionalForm]<>")", TraditionalForm],

"delta sum EXP"->ToString[Simplify[(sum/.{k->(k+1)})-sum],TraditionalForm],
(* Expand and simplify Subtranct Sum n+1 - Sum n*)

"Expand delta sum"->ToString[ToString[ToString[Expand@(sum/.{k->(k+1)}),TraditionalForm]<>" - ("<>ToString[Expand@(sum),TraditionalForm],TraditionalForm]<>")",TraditionalForm],


"Expand delta sum EXP"->Expand[(sum/.{k->(k+1)})-sum]
|>;



)

]

m1[]

Let us repeat once again why exactly we can assume that our statment is true for n=k? We are relying on the Domino Effect. We are asking if any domino falls will the next one fall? So we take it as a fact (temporarily) that the “n=k” domino falls and see if that means the “n=k+1” domino will also fall.

Generally we can distinguish two main variations in our principle.

The first covers statements that are true for all integers beyond a certain value (such as (2^n)> (n^2) which is true for all n ⩾ 5, therefore (Subscript[n, 0])=5 in this case):

If p((Subscript[n, 0])) is true and, for each integer k ⩾ (Subscript[n, 0]) , p(k+1) is true whenever p(k) is true then p(n) is true for all n ⩾ (Subscript[n, 0]) .

There is also a stronger form of mathematical induction which states the following:

If p(1) is true and, for each integer  k ⩾ 1  the statements  p(1), p(2),...,p(k) imply the statement p(k+1) then p(n) is true for all n ⩾ 1 .