helphome pageduck scriptspecificationfirst proof pagepage 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
    ,
    and try to get contradiction.
  • 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.
    Click here to see its proof.
  • 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.
    Click here to see its proof.
  • 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).
    Click here to see its proof.
  • In the following hypothesis
        ( M  N  : NzNat  ) gcd(M + M , N + N) > (s 0) ,
    let M  = n4 and N  = n3 , we get
        gcd(n4 + n4 , n3 + n3) > (s 0) ,
  • Then we apply equation gcd(n4 + n4 , n3 + n3) = 1 to the hypothesis
        gcd(n4 + n4 , n3 + n3) > (s 0) ,
    and get
        false ,

And thus the main goal is proved.

BOBJ proof scoreLeft    Up    Down    Right   
 

       This page was generated by Kumo on Tue Feb 13 19:36:15 PST 2001.