ROOT_2_IRRAT
____________

*C root_2_irrat_begin         ************ ROOT_2_IRRAT ************
*T qrat_irreduc_witness_orig

Œ ขu:„. (ฃn:…. ฃd:…ทธ. u = n / d ’ CoPrime(n,d))
| 
BY (D 0 THENM InstLemma `qrat_witness` [Šu‹] ...a)
|
1. u: „
2. (ฃn:…. ฃd:…ทธ. u = n / d)
Œ (ฃn:…. ฃd:…ทธ. u = n / d ’ CoPrime(n,d))
| 
BY (D 2 THENM D 0 THENM ExRepD ...a)
|
2. n: …
3. d: …ทธ
4. u = n / d
Œ ฃn:…. ฃd:…ทธ. u = n / d ’ CoPrime(n,d)
| 
BY (Assert Šgcd(n;d) จ 0‹ 
|   THENM Assert Šd ต gcd(n;d) จ 0‹ 
|   THENM Inst [Šn ต gcd(n;d)‹;Šd ต gcd(n;d)‹] 0 ...a)
|\
| Œ gcd(n;d) จ 0
| | 
| BY (D 0 ...a)
| |
| 5. gcd(n;d) = 0
| ΠFalse
| | 
| BY (Sel (-1) (FLemma `gcd_zero_result` [5]) ...a)
| |
| 6. n = 0 ’ d = 0
| | 
| BY Auto
|\
| 5. gcd(n;d) จ 0
| Œ d ต gcd(n;d) จ 0
| | 
| BY (BLemma `div_zero_a` ...a)
| |\
| | Œ “(d = 0)
| | | 
| | BY Auto
|  \
|   Πgcd(n;d) | d
|   | 
|   BY (BLemma `gcd_is_divisor_2` ...a)
|\
| 5. gcd(n;d) จ 0
| 6. d ต gcd(n;d) จ 0
| Œ u = (n ต gcd(n;d)) / (d ต gcd(n;d))
| | 
| BY (RWH (RevLemmaWithC [`n',Šgcd(n;d)‹] `numq_factor_cancel`) 0 ...a)
| |
| Œ u = (gcd(n;d) * (n ต gcd(n;d))) / (gcd(n;d) * (d ต gcd(n;d)))
| | 
| BY (RWH (LemmaC `mul_com`) 0 ...a)
| |\
| | 7. gcd(n;d) * (d ต gcd(n;d)) = (d ต gcd(n;d)) * gcd(n;d)
| | Œ ...GenFormulaCondC: failed... gcd(n;d) * (d ต gcd(n;d))
| | |  = (d ต gcd(n;d)) * gcd(n;d)
| | | 
| | BY RemoveLabel THENM EqTypeCD 
| | |  THEN Try (Complete Auto)
| | |
| | Œ gcd(n;d) * (d ต gcd(n;d)) จ 0
| | | 
| | BY (BLemma `int_entire_a` ...)
|  \
|   Œ u = ((n ต gcd(n;d)) * gcd(n;d)) / ((d ต gcd(n;d)) * gcd(n;d))
|   | 
|   BY (RWH (GenLemmaC 1 `divides_iff_div_exact`) 0 ...a)
|   |\
|   | Πgcd(n;d) | n
|   | | 
|   | BY (BLemma `gcd_is_divisor_1` ...a)
|   |\
|   | Πgcd(n;d) | d
|   | | 
|   | BY (BLemma `gcd_is_divisor_2` ...a)
|   |\
|   | 7. (d ต gcd(n;d)) * gcd(n;d) = d
|   | Œ ...GenFormulaCondC: failed... (d ต gcd(n;d)) * gcd(n;d) = d
|   | | 
|   | BY (RemoveLabel THEN EqTypeCD ...)
|    \
|     Πu = n / d
|     | 
|     BY Auto
 \
  5. gcd(n;d) จ 0
  6. d ต gcd(n;d) จ 0
  Œ CoPrime(n ต gcd(n;d),d ต gcd(n;d))
  | 
  BY (Unfold `coprime` 0 ...a)
  |
  Œ GCD(n ต gcd(n;d);d ต gcd(n;d);1)
  | 
  BY (Using [`n',Šgcd(n;d)‹] (BLemma `gcd_p_mul_elim`)  ...a)
  |
  Œ GCD(gcd(n;d) * (n ต gcd(n;d));gcd(n;d) * (d ต gcd(n;d));gcd(n;d) * 1)
  | 
  BY (RWH IntSimpC 0 
  |   THENM RWH (GenLemmaC 1 `divides_iff_div_exact`) 0 ...a)
  |\
  | Πgcd(n;d) | n
  | | 
  | BY (BLemma `gcd_is_divisor_1` ...a)
  |\
  | Πgcd(n;d) | d
  | | 
  | BY (BLemma `gcd_is_divisor_2` ...a)
   \
    ΠGCD(n;d;gcd(n;d))
    | 
    BY (BLemma `gcd_sat_gcd_p` ...a)

*T qrat_irreduc_witness

Œ ขu:„. (ฃn:…. ฃd:…ทธ. u = n / d ’ CoPrime(n,d))
| 
BY (D 0 THENM InstLemma `qrat_witness` [Šu‹] 
|   THENM D 2 THENM D 0 THENM ExRepD ...a)
|
1. u: „
2. n: …
3. d: …ทธ
4. u = n / d
Œ ฃn:…. ฃd:…ทธ. u = n / d ’ CoPrime(n,d)
| 
BY % Facts to help type-checking % 
|   
|  (Assert Šgcd(n;d) จ 0‹ THENA 
|    (D 0 THENM Sel (-1) (FLemma `gcd_zero_result` [5]) ...)) 
|  THEN  
|  (Assert Šd ต gcd(n;d) จ 0‹ THENA 
|    (Backchain ``div_zero_a gcd_is_divisor_2`` ...)) 
|
5. gcd(n;d) จ 0
6. d ต gcd(n;d) จ 0
| 
BY (Inst [Šn ต gcd(n;d)‹;Šd ต gcd(n;d)‹] 0 ...a)
|\
| Œ u = (n ต gcd(n;d)) / (d ต gcd(n;d))
| | 
| BY (RWH (RevLemmaWithC [`n',Šgcd(n;d)‹] `numq_factor_cancel`) 0 ...a)
| |
| Œ u = (gcd(n;d) * (n ต gcd(n;d))) / (gcd(n;d) * (d ต gcd(n;d)))
| | 
| BY RWH (LemmaC `mul_com`) 0  
| |  THENM RWH (GenLemmaC 1 `divides_iff_div_exact`) 0  
| |  THENA Repeat  
| |    (Progress Auto 
| |     ORELSE (RemoveLabel THEN EqTypeCD) 
| |     ORELSE Backchain ``gcd_is_divisor_1 gcd_is_divisor_2 int_entire_a``)
| |
| Πu = n / d
| | 
| BY Auto
 \
  Œ CoPrime(n ต gcd(n;d),d ต gcd(n;d))
  | 
  BY Unfold `coprime` 0
  |
  Œ GCD(n ต gcd(n;d);d ต gcd(n;d);1)
  | 
  BY (Using [`n',Šgcd(n;d)‹] (BLemma `gcd_p_mul_elim`) 
  |   THENM RWH IntSimpC 0  ...a)
  |
  Œ GCD((n ต gcd(n;d)) * gcd(n;d);(d ต gcd(n;d)) * gcd(n;d);gcd(n;d))
  | 
  BY (RWH (GenLemmaC 1 `divides_iff_div_exact`) 0 
      THEN Backchain ``gcd_is_divisor_1 gcd_is_divisor_2 gcd_sat_gcd_p`` ...)

*T exists_zero_one_elim

Œ ขP:‚2 ฏฐ €. (ฃi:‚2. P[i]) ‡ˆ‰ P[0] ญ P[1]
| 
BY GenExRepD THENA Auto
|\
| 1. P: ‚2 ฏฐ €
| 2. i: ‚2
| 3. P[i]
| Œ P[0] ญ P[1]
| | 
| BY (Assert Ši = 0 ญ i = 1‹ ...a)
| |\
| | Œ i = 0 ญ i = 1
| | | 
| | BY SIAuto
|  \
|   4. i = 0 ญ i = 1
|   | 
|   BY D 4
|   |\
|   | 4. i = 0
|   | | 
|   | BY HypSubst 4 3 THENA Auto
|   | |
|   | 3. P[0]
|   | | 
|   | BY ProveProp THENA Auto
|    \
|     4. i = 1
|     | 
|     BY HypSubst 4 3 THENA Auto
|     |
|     3. P[1]
|     | 
|     BY (ProveProp ...)
|\
| 1. P: ‚2 ฏฐ €
| 2. P[0]
| Œ ฃi:‚2. P[i]
| | 
| BY (Inst [Š0‹] 0 ...)
 \
  1. P: ‚2 ฏฐ €
  2. P[1]
  Œ ฃi:‚2. P[i]
  | 
  BY (Inst [Š1‹] 0 ...)

*T two_div_square

Œ ขn:…. 2 | n * n ˆ‰ 2 | n
| 
BY (D 0 ...a)
|
1. n: …
Œ 2 | n * n ˆ‰ 2 | n
| 
BY Assert Šn * n = 0 mod 2 ˆ‰ n = 0 mod 2‹
|\
| Œ n * n = 0 mod 2 ˆ‰ n = 0 mod 2
| | 
| BY (D 0 ...a)
| |
| 2. n * n = 0 mod 2
| Πn = 0 mod 2
| | 
| BY (InstLemma `eqmod_exists` [Š2‹;Šn‹] ...a)
| |
| 3. ฃb:‚2. n = b mod 2
| | 
| BY (RWH (LemmaC `exists_zero_one_elim`) 3 ...a)
| |
| 3. n = 0 mod 2 ญ n = 1 mod 2
| | 
| BY D 3 THEN Auto
| |
| 3. n = 1 mod 2
| | 
| BY (FLemma `multiply_functionality_wrt_eqmod` [3;3] 
| |   THENM ArithSimp 4 ...a)
| |
| 4. n * n = 1 mod 2
| | 
| BY (FLemma `eqmod_unique` [2;4] ...a)
| |
| 5. 0 = 1
| | 
| BY Auto
 \
  2. n * n = 0 mod 2 ˆ‰ n = 0 mod 2
  | 
  BY (Unfold `eqmod` 2 THEN ArithSimp 2 ...)

*T root_2_irrat_over_int_orig

Œ “(ฃm,n:…. CoPrime(m,n) ’ m * m = 2 * n * n)
| 
BY (D 0 THENM ExRepD ...a)
|
1. m: …
2. n: …
3. CoPrime(m,n)
4. m * m = 2 * n * n
ΠFalse
| 
BY Assert Š2 | m‹
|\
| Π2 | m
| | 
| BY (BLemma `two_div_square` ...a)
| |
| Π2 | m * m
| | 
| BY Unfold `divides` 0
| |
| Œ ฃc:…. m * m = 2 * c
| | 
| BY (Inst [Šn * n‹] 0 ...)
 \
  5. 2 | m
  | 
  BY Assert Š2 | n‹
  |\
  | Π2 | n
  | | 
  | BY (BLemma `two_div_square` ...a)
  | |
  | Π2 | n * n
  | | 
  | BY All (Unfold `divides`) 
  | |  THEN ExRepD
  | |
  | 5. c: …
  | 6. m = 2 * c
  | Œ ฃc:…. n * n = 2 * c
  | | 
  | BY (With Šc * c‹ (D 0) ...)
  | |
  | Πn * n = 2 * c * c
  | | 
  | BY (RWW "6" 4 ...)
   \
    6. 2 | n
    | 
    BY (RWO "coprime_elim" 3 ...a)
    |
    3. ขc:…. c | m ˆ‰ c | n ˆ‰ c ~ 1
    | 
    BY (FHyp 3 [5;6] ...a)
    |
    7. 2 ~ 1
    | 
    BY (RWW "assoced_elim" 7 
        THENM D (-1) ...)

*T root_2_irrat_over_int

Œ “(ฃm,n:…. CoPrime(m,n) ’ m * m = 2 * n * n)
| 
BY (D 0 THENM ExRepD ...a)
|
1. m: …
2. n: …
3. CoPrime(m,n)
4. m * m = 2 * n * n
ΠFalse
| 
BY Assert Š2 | m‹
|\
| Π2 | m
| | 
| BY (BLemma `two_div_square` THENM Unfold `divides` 0 
|     THENM AutoInstConcl [] ...a)
 \
  5. 2 | m
  | 
  BY Assert Š2 | n‹
  |\
  | Π2 | n
  | | 
  | BY (BLemma `two_div_square` THENM All (Unfold `divides`) 
  |     THENM ExRepD THENM Inst [Šc * c‹] 0 
  |     THENM RWO "6" 4 ...)
   \
    6. 2 | n
    | 
    BY (RWO "coprime_elim" 3 THENM FHyp 3 [5;6] ...a)
    |
    3. ขc:…. c | m ˆ‰ c | n ˆ‰ c ~ 1
    7. 2 ~ 1
    | 
    BY (RWO "assoced_elim" 7 THENM D (-1) ...)

*T root_2_irrat_orig

Œ “(ฃu:„. u *ร u = 2 / 1)
| 
BY (D 0 THENM D (-1) ...a)
|
1. u: „
2. u *ร u = 2 / 1
ΠFalse
| 
BY (InstLemma `qrat_irreduc_witness` [Šu‹] 
|   THENM D (-1) 
|   THENM ExRepD ...a)
|
3. n: …
4. d: …ทธ
5. u = n / d
6. CoPrime(n,d)
| 
BY (RWW "5" 2 ...a)
|
2. n: …
3. d: …ทธ
4. u = n / d
5. CoPrime(n,d)
6. (n / d) *ร (n / d) = 2 / 1
| 
BY Unfolds ``mulq numq`` 6 
|  THENM AbReduce 6
|
6. [qnum(n;d) *q qnum(n;d)]ร = [2.]ร
| 
BY (RWW "eq_qrat_elim" 6 ...a)
|
6. qnum(n;d) *q qnum(n;d) ฌq 2.
| 
BY Unfolds ``qmul qequiv`` 6 
|  THENM AbReduce 6 
|  THENM (RWH IntSimpC 6 ...a)
|
6. n * n = 2 * d * d
| 
BY AssertLemma `root_2_irrat_over_int` [] 
|  THENM (D (-1))
|
Œ ฃm,n:…. CoPrime(m,n) ’ m * m = 2 * n * n
| 
BY (AutoInstConcl [5] ...)

*T root_2_irrat

Œ “(ฃu:„. u *ร u = 2 / 1)
| 
BY (D 0 THENM D (-1) ...a)
|
1. u: „
2. u *ร u = 2 / 1
ΠFalse
| 
BY (InstLemma `qrat_irreduc_witness` [Šu‹] 
|   THENM D (-1) THENM ExRepD 
|   THENM RWW "5" 2 THENM On [4;1] Thin ...a)
|
1. n: …
2. d: …ทธ
3. CoPrime(n,d)
4. (n / d) *ร (n / d) = 2 / 1
| 
BY (Unfolds ``mulq numq`` 4 THENM AbReduce 4  
|   THENM RWO "eq_qrat_elim" 4  
|   THENM Unfolds ``qmul qequiv`` 4 THENM AbReduce 4 
|   THENM RWH IntSimpC 4 ...a)
|
4. n * n = 2 * d * d
| 
BY AssertLemma `root_2_irrat_over_int` [] THENM D (-1)
|
Œ ฃm,n:…. CoPrime(m,n) ’ m * m = 2 * n * n
| 
BY (AutoInstConcl [] ...)

*C root_2_irrat_end           **************************************