helphome pageduck scriptspecificationfirst proof pagepage 1 1

A Lemma About GCD


We want to prove
( M  N  : NzNat  ) gcd(M + M , N + N) > (s 0) .
We take the following steps:
  • We introduce the lemma
      ( N  M  : Nat  ) (M + N) - N = M.
    Click here to see its proof.
  • We use induction on M and N to prove this goal. For this, we use the following induction scheme:
    to prove an assertion P on the sort(s) NzNat NzNat , we can do the following:
              base case:   prove P(1 , 1) .
              induction case:   assume P(m , n) ,  prove P(m + n , n)  for m and n .
              induction case:   assume P(m , n) ,  prove P(m , m + n)  for m and n .
    1. Base case: prove gcd(2 * 1 , 2 * 1) > 1 .
      • We show gcd(2 * 1 , 2 * 1) > 1 by reduction.
    2. Induction case: assume gcd(m + m , n + n) > (s 0) , prove gcd(2 * (m + n) , 2 * n) > 1 .
      • We introduce the lemma
          ( M  : Nat  )
               (N  : Nat  )
                          M = 2 * N
                     or
                          M = (2 * N) + 1.
        Click here to see its proof.
      • We introduce the lemma
          ( M  : Nat  )
               ( K  : NzNat  ) (M + K) > M.
        Click here to see its proof.
      • We show gcd(2 * (m + n) , 2 * n) > 1 by reduction.
    3. Induction case: assume gcd(2 * m , 2 * n) > 1 , prove gcd(2 * m , 2 * (m + n)) > 1 .
      • We introduce the lemma
          ( M  : Nat  )
               (N  : Nat  )
                          M = 2 * N
                     or
                          M = (2 * N) + 1.
        Click here to see its proof.
      • We introduce the lemma
          ( M  : Nat  )
               ( K  : NzNat  ) (M + K) > M.
        Click here to see its proof.
      • We show gcd(2 * m , 2 * (m + n)) > 1 by reduction.

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:13 PST 2001.