Sundstrom page242_theorem5.9

hughmcguire

Proof of the following formula: 

(∀n>1)[n is prime  or  n is a_product_of_primes]

(#) Comments Suppositions and derivations Theorem and subgoals
    We presuppose the following:  
(1)  [unused] 
(∀x)
  (x > 1
     →
   ¬[x is prime]
     →
   (∃y,z)
     [x = y·z
        and
      1 < y  ≤  x - 1
        and
      1 < z  ≤  x - 1])
 
(2)   
(∀x)
  [x is prime  or  x is not prime]
 
(3)   
(∀x)
  (x > 1
     →
   x is not prime
     →
   (∃y,z)
     [x = y·z
        and
      1 < y  ≤  x - 1
        and
      1 < z  ≤  x - 1])
 
(4)   
(∀x,y,z)
  [x > y  ∧  x ≤ z
     ↔
   y < x  ≤  z]
 
(5)   
(∀x)
  (x is a_product_of_primes
     means
   (∃y,z)
     [x = y·z
        and
      (y is prime
         or
       y is a_product_of_primes)
       and
      (z is prime
         or
       z is a_product_of_primes)])
 
       
      We start working with the formula being proved
as follows:
(6)     
(∀n>1)[n is prime  or  n is a_product_of_primes]
      Well, invoking strong induction, we should prove the following:
(7)     
(∀n)
  [(∀m)
     [m > 1  ∧  m ≤ n
        ⇒
      m is prime  or  m is a_product_of_primes]
     ∧
   (n + 1) > 1
     ⇒
   (n + 1) is prime  or  (n + 1) is a_product_of_primes]
          ≡      by simplifying
(8)     
(∀n)
  [(∀m)
     [m > 1  ∧  m ≤ n
        ⇒
      m is prime  or  m is a_product_of_primes]
     ∧
   n > 0
     ⇒
   (n + 1) is prime  or  (n + 1) is a_product_of_primes]
      Well, let an arbitrary value "k" be given;
then we should prove the following:
(9)     
(∀m)
  [m > 1  ∧  m ≤ k
     ⇒
   m is prime  or  m is a_product_of_primes]
  ∧
k > 0
  ⇒
(k + 1) is prime  or  (k + 1) is a_product_of_primes
    We'll assume that formula's antecedents:  
(10)   
(∀m)
  [m > 1  ∧  m ≤ k
     ⇒
   m is prime
     or
   m is a_product_of_primes]
 
    and also:  
(11)   
k > 0
 
      and we'll work on proving a consequent:
(12)     
(k + 1) is prime
      or alternatively:
(13)     
(k + 1) is a_product_of_primes
          ≡      by (5) with "x := k+1"
(14)     
(∃y,z)
  [(k + 1) = y·z
     and
   (y is prime  or  y is a_product_of_primes)
    and
   (z is prime  or  z is a_product_of_primes)]
      Removing that variable quantification
clarifies that to prove that formula,
it will suffice to find values for the variables.
(15)     
(k + 1) = y·z
  and
(y is prime  or  y is a_product_of_primes)
 and
(z is prime  or  z is a_product_of_primes)
    Assigning "(∀x)
   [x is prime  or  x is not prime] := k+1" in formula (2) yields: 		 
(16)   
(k + 1) is prime
  or
(k + 1) is not prime
 
    Applying simple algebra to formula (11) yields:formula (11) yields:  
(17)   
k + 1  >  1
 
        ↓      by (3) with "x := k+1"  
(18)   
(k + 1) is not prime
  →
(∃y,z)
  [(k + 1) = y·z  and  1 < y  ≤  k
     and
   1 < z  ≤  k]
 
    Applying the equivalence in formula (4)
to the selection in formula (10)
with "x := m, y := 1, z := k"
yields: 		 
(19)   
(∀m)
  [[1 < m  ≤  k]
     ⇒
   m is prime
     or
   m is a_product_of_primes]
 
       
    We'll handle formula (16)'s components
in separate subparts of this proof, as follows: 		 
    Case 1:  
(20)   
(k + 1) is prime
 
          ↓      by (12)
(21)     
true
      That concludes this part of the proof.
       
    Case 2:  
(22)   
(k + 1) is not prime
 
        ↓      by (18)  
(23)   
(∃y,z)
  [(k + 1) = y·z  and  1 < y  ≤  k
     and
   1 < z  ≤  k]
 
    That formula indicates there exists
some value say "a" satisfying that
quantified formula, i.e.: 		 
(24)   
(∃z)
  [(k + 1) = a·z  and  1 < a  ≤  k
     and
   1 < z  ≤  k]
 
    That formula indicates there exists
some value say "b" satisfying that
quantified formula, i.e.: 		 
(25)   
(k + 1) = a·b  and  1 < a  ≤  k
  and
1 < b  ≤  k
 
    That formula can be separated into three
alternative suppositions/derivations; first: 		 
(26)   
(k + 1) = a·b
 
    and also:  
(27)   
1 < a  ≤  k
 
    and also:  
(28)   
1 < b  ≤  k
 
        ↓      by (19) with "m := b"  
(29)   
b is prime
  or
b is a_product_of_primes
 
    Applying formula (19) to formula (27)
with "m := a"
yields: 		 
(30)   
a is prime
  or
a is a_product_of_primes
 
      Applying formula (26) to formula (15)
with "y := a, z := b"
yields:
(31)     
true and (a is prime  or  a is a_product_of_primes)
 and
(b is prime  or  b is a_product_of_primes)
          ≡      by simplifying
(32)     
(a is prime  or  a is a_product_of_primes)
 and
(b is prime  or  b is a_product_of_primes)
          ↓      by (30)
(33)     
true and (b is prime  or  b is a_product_of_primes)
          ≡      by simplifying
(34)     
b is prime  or  b is a_product_of_primes
          ≡      by (29)
(35)     
true
      That concludes this part of the proof.
       
      Thus, the theorem that was given is true,
by the above partitioning of this proof into subparts.

identification:
1216528457455
1216491183778
37273677