Gersting page103_example14

hughmcguire

Proof of the following formula: 

(∀n≥1)[(∑(2i-1) for i=1 to n) = n²]

(#) Comments Suppositions and derivations Theorem and subgoals
    We presuppose the following:  
(1)   
(∀f,v,x)[(∑ f for v = x to x) = f◀(v := x)]
 
(2)   
(∀f,v,x,y)
  [(∑ f for v = x to y+1)
    =
   (∑ f for v = x to y) + f◀(v := y + 1)]
 
(3)   
(∀x,y,z)[x(y + z) = xy + xz]
 
(4)   
(∀x,y)[(x + y)² = x² + 2xy + y²]
 
(5)   
(∀x,y,z)[x + (y + z) = (x + y) + z]
 
       
      We start working with the formula being proved
as follows:
(6)     
(∀n≥1)[(∑(2i-1) for i=1 to n) = n²]
      Well, invoking stepwise induction, we should prove the following:
(7)     
(∑ (2i - 1) for i = 1 to 1) = 1²
  ∧
(∀n)
  ((∑ (2i - 1) for i = 1 to n) = n²  ∧  n ≥ 1
     ⇒
   (∑ (2i - 1) for i = 1 to (n+1)) = (n+1)²)
          ≡      by simplifying
(8)     
(∑ (2i - 1) for i = 1 to 1) = 1
  ∧
(∀n)
  ((∑ (2i - 1) for i = 1 to n) = n²  ∧  n ≥ 1
     ⇒
   (∑ (2i - 1) for i = 1 to (n+1)) = (n+1)²)
      We'll handle that formula's subparts
in separate cases (below):
    Assigning "y := 1" in formula (4) yields:  
(9)   
(∀x)[(x+1)² = x² + 2x·1 + 1²]
 
        ≡      by simplifying  
(10)   
(∀x)[(x+1)² = x² + 2x + 1]
 
       
      Case 1:
(11)     
(∑ (2i - 1) for i = 1 to 1) = 1
          ≡      by (1) with "f := 2i-1, v := i, x := 1"
(12)     
[(2i-1)◀(i := 1)] = 1
          ≡      by simplifying
(13)     
true
      That concludes the proof for this case.
       
      Case 2:
(14)     
(∀n)
  ((∑ (2i - 1) for i = 1 to n) = n²  ∧  n ≥ 1
     ⇒
   (∑ (2i - 1) for i = 1 to (n+1)) = (n+1)²)
      Well, let an arbitrary value "k" be given;
then we should prove the following:
(15)     
(∑ (2i - 1) for i = 1 to k) = k²  ∧  k ≥ 1
  ⇒
(∑ (2i - 1) for i = 1 to (k+1)) = (k+1)²
    We'll assume that formula's antecedents:  
(16)   
(∑ (2i - 1) for i = 1 to k) = k²
 
    and also:  
(17)  [unused] 
k ≥ 1
 
      and we'll work on proving the consequent:
(18)     
(∑ (2i - 1) for i = 1 to (k+1)) = (k+1)²
       
      We'll work on transforming the left-hand side of formula (18)
to the right-hand side as follows:
(19)     
∑ (2i - 1) for i = 1 to (k+1)
          =      by (2) with "f := 2i-1, v := i, x := 1, y := k"
(20)     
(∑ (2i - 1) for i = 1 to k) + (2i-1)◀(i := k + 1)
          =      by simplifying
(21)     
(∑ (2i - 1) for i = 1 to k) + (2(k+1) - 1)
          =      by (16)
(22)     
k² + (2(k+1) - 1)
          =      by (3) with "x := 2, y := k, z := 1"
(23)     
k² + ((2k + 2·1) - 1)
          =      by simplifying
(24)     
k² + (2k + 1)
          =      by (5) with "x := k², y := 2k, z := 1"
(25)     
(k² + (2k)) + 1
          =      by (10) with "x := k"
(26)     
(k+1)²
      And that satisfies our earlier goal (18); i.e. we have:
(27)     
true
      That concludes this part of the proof.
       
      Thus, the theorem that was given is true in all cases.

identification:
1206471675838
1206471232189
443649