Epp page150_to_151

hughmcguire

Proof of the following formula: 

∀x∀y∀z[x|y ∧ y|z → x|z]

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

identification:
1206632113217
1206631887089
226128