page 1 1

The Square Root of 2 is Irrational

We want to prove the square root of 2 is irrational.

By the definition of rational number, we will show that there are no numbers   N   and   M   such that   2 * M * M = N * N   and   gcd(M, N) = 1   .

We want to prove
not (
(M  N  : NzNat  )
(2 * M) * M = N * N and gcd(M , N) = 1
) .
We take the following steps:
• We assume  (M  N  : NzNat  )       (2 * M) * M = N * N and gcd(M , N) = 1 ,
• By skolemization, we can get  (2 * n1) * n1 = n2 * n2 and gcd(n1 , n2) = 1
from the following hypothesis  (M  N  : NzNat  )       (2 * M) * M = N * N and gcd(M , N) = 1 .
• Then we decompose the hypothesis  (2 * n1) * n1 = n2 * n2 and gcd(n1 , n2) = 1 .
into the following 2 hypothese:
•  (2 * n1) * n1 = n2 * n2 .
•  gcd(n1 , n2) = 1 .
• We introduce the lemma  ( M  N  : Nat  )             (2 * M) * M = N * N       implies              (K  : Nat  ) N = 2 * K.
• By modus ponens , we get  (K  : Nat  ) n2 = 2 * K
from  ( M  N  : Nat  )             (2 * M) * M = N * N       implies              (K  : Nat  ) N = 2 * K
and  (2 * n1) * n1 = n2 * n2 .
• By skolemization, we can get  n2 = 2 * n3
from the following hypothesis  (K  : Nat  ) n2 = 2 * K .
• Then we apply equation n2 = 2 * n3 to the hypothesis  (2 * n1) * n1 = n2 * n2 ,
and get  (2 * n1) * n1 = ((n3 * n3) + (n3 * n3)) + ((n3 * n3) + (n3 * n3)) ,
• We reverse the equation
(2 * n1) * n1 = ((n3 * n3) + (n3 * n3)) + ((n3 * n3) + (n3 * n3)) ,
and get
((n3 * n3) + (n3 * n3)) + ((n3 * n3) + (n3 * n3)) = (2 * n1) * n1 ,
• We introduce the lemma  ( M  N  : Nat  )             2 * M = 2 * N       implies             M = N.
• By modus ponens , we get  (n3 * n3) + (n3 * n3) = n1 * n1
from  ( M  N  : Nat  )             2 * M = 2 * N       implies             M = N
and  ((n3 * n3) + (n3 * n3)) + ((n3 * n3) + (n3 * n3)) = (2 * n1) * n1 .
• By modus ponens , we get  (K  : Nat  ) n1 = 2 * K
from  ( M  N  : Nat  )             (2 * M) * M = N * N       implies              (K  : Nat  ) N = 2 * K
and  (n3 * n3) + (n3 * n3) = n1 * n1 .
• By skolemization, we can get  n1 = 2 * n4
from the following hypothesis  (K  : Nat  ) n1 = 2 * K .
• Then we apply equation n2 = 2 * n3 to the hypothesis  gcd(n1 , n2) = 1 ,
and get  gcd(n1 , n3 + n3) = 1 ,
• Then we apply equation n1 = 2 * n4 to the hypothesis  gcd(n1 , n3 + n3) = 1 ,
and get  gcd(n4 + n4 , n3 + n3) = 1 ,
• We introduce the lemma  ( M  N  : NzNat  ) gcd(M + M , N + N) > (s 0).