Epp page113_middle

hughmcguire

Proof of the following formula: 

even(m) ∧ even(n) → even(m + n)

(#)   Suppositions and derivations Theorem and subgoals
    We presuppose the following:  
(1)   
∀x[even(x) ↔ ∃k(x = 2k)]
 
(2)   
(∀x,y,z)[xy + xz = x(y + z)]
 
       
      We start working with the formula being proved
as follows:
(3)     
even(m) ∧ even(n) → even(m + n)
    We'll assume that formula's antecedents:  
(4)   
even(m)
 
    and also:  
(5)   
even(n)
 
      and we'll work on proving the consequent:
(6)     
even(m+n)
          ≡      by (1) with "x := m+n"
(7)     
∃k((m + n) = 2k)
      Removing that variable quantification
clarifies that to prove that formula,
it will suffice to find a value for the variable.
(8)     
(m + n) = 2k
    Applying the equivalence in formula (1)
to formula (4)
with "x := m"
yields: 		 
(9)   
∃k(m = 2k)
 
    That formula indicates there exists
some value say "r" satisfying that
quantified formula, i.e.: 		 
(10)   
m = 2r
 
    Applying the equivalence in formula (1)
to formula (5)
with "x := n"
yields: 		 
(11)   
∃k(n = 2k)
 
    That formula indicates there exists
some value say "s" satisfying that
quantified formula, i.e.: 		 
(12)   
n = 2s
 
       
      We'll work on transforming the left-hand side of formula (8)
to the right-hand side as follows:
(13)     
m + n
          =      by (10)
(14)     
(2r) + n
          =      by (12)
(15)     
(2r) + (2s)
          =      by (2) with "x := 2, y := r, z := s"
(16)     
2(r+s)
      And that satisfies our earlier goal (8)
with "k := r + s"; i.e. we have:
(17)     
true
      That concludes this part of the proof.
       
      Thus, the theorem that was given is true.

identification:
1206475462213
1206475294606
167607