:: This file is verified with the system version:
:: Mizar verifier= 7.8.03,MML = 4.76.959
::
:: Created by Krzysztof Retel {retel@macs.hw.ac.uk}


environ
 vocabularies SQUARE_1, IRRAT_1, RAT_1, MATRIX_2, INT_1, ARYTM_3, ABSVALUE,
    FINSET_1, SEQM_3, XREAL_0, ARYTM;
 notations INT_1, SQUARE_1, IRRAT_1, XCMPLX_0, RAT_1, REAL_1, ABIAN,
    PEPIN, INT_2, FINSET_1, SEQM_3, XXREAL_0, XREAL_0, NAT_1, SUBSET_1,
    NUMBERS, ORDINAL1;
 constructors NAT_1, SQUARE_1, IRRAT_1, XCMPLX_0, RAT_1, ABIAN, INT_1,
    PEPIN, INT_2, FINSET_1, SEQM_3, XXREAL_0, XREAL_0,SUBSET_1;
 requirements SUBSET, NUMERALS, ARITHM, BOOLE, REAL;
 registrations XREAL_0, REAL_1, NAT_1, INT_1;
 theorems ABIAN,PYTHTRIP,SQUARE_1,XCMPLX_1,REAL_1,NAT_1,INT_1,
    RAT_1,REAL_2,XREAL_1, ORDINAL1;
 schemes NAT_1;
begin
  
Lemma:  
 for m,n being Nat holds m^2 = 2*n^2 implies m = 0 & n = 0
 proof
   defpred P[Nat] means ex n being Nat st $1^2 = 2*n^2 & $1 > 0;
   Claim: for m being Nat holds P[m] implies ex m' being Nat st m' < m & P[m']
   proof
     let m being Nat;
     assume B0: P[m];
     then consider n being Nat such that
     B1: m^2 = 2*n^2 &  m > 0;
     m^2 is even by ABIAN:def 1,B1;
     then m is even by PYTHTRIP:2;
     then consider k being Integer such that
     B2: m = 2*k by ABIAN:def 1;
     2*n^2 = m^2 by B1
          .= 2^2*k^2 by B2,SQUARE_1:68
          .= (2*2)*k^2 by SQUARE_1:def 3
          .= 4*k^2;
     then B3: n^2 = 2*k^2;
     m^2 > 0 by SQUARE_1:74,B0;
     then (2*n^2)/2 > 0/2 by B1,REAL_1:73;
     then B6: n^2 > 0;
     then n <> 0 by SQUARE_1:60,B1;
     then B8: n > 0 by NAT_1:3;
     0 <= k
     proof
       assume not thesis;
       then k < 0;
       then 2*k < 2*0 by XREAL_1:70;
       hence contradiction by B2,B1;
     end;
     then k is Element of NAT by INT_1:16;
     then reconsider k as Nat;
     C0: n^2 = 2*k^2 & n > 0 by B3,B8;
     then C1: P[n];
     0+n^2 < n^2 + n^2 by B6,XREAL_1:10;
     then m^2 = n^2 + n^2 & n^2 + n^2 > n^2 by B1;
     then m^2 > n^2 ;
     then sqrt m^2 > sqrt n^2 by B6,SQUARE_1:95;
     then 0 <= m & sqrt m^2 > n by B1,C0,SQUARE_1:89;
     then C2: m > n by SQUARE_1:89;
     take m' = n;
     thus thesis by C1,C2;
   end;
   A2: for k being Nat holds not P[k]
   proof
     let k be Nat;
     assume S0: not thesis;
     then S1: ex k being Nat st P[k];
     then consider aa being Nat such that B1: P[aa];
     reconsider aa as Element of NAT by ORDINAL1:def 13;
     P[aa] by B1;
     then S11: ex k being Element of NAT st P[k];
     S2: for k being Nat st k <> 0 & P[k] holds
     ex n being Nat st n < k & P[n] by Claim;
     S22: for k being Element of NAT st k <> 0 & P[k] holds
     ex n being Element of NAT st n < k & P[n]
     proof
       let k be Element of NAT;
       assume that T0: k <> 0 and T1: P[k];
       ex n being Nat st n < k & P[n] by T0,T1,S2;
       consider n being Nat such that
       T2: n < k & P[n] by T0,T1,S2;
       take n;
       reconsider n as Element of NAT by ORDINAL1:def 13;
       n < k & P[n] by T2;
       hence thesis;
     end;
     P[0] from NAT_1:sch 7(S11,S22);
     hence contradiction;
   end;
   let m,n being Nat;
   assume A0: m^2 = 2*n^2;
   per cases by A0;
   suppose B1: m^2 = 2*n^2 & m <> 0;
     then m > 0 by NAT_1:3;
     then P[m] by B1;
     then contradiction by A2;
     hence thesis;
   end;
   suppose S1: m^2 = 2*n^2 & m = 0;
     then 0 = 2*n^2 by SQUARE_1:60;
     then 0 = n*n by SQUARE_1:def 3;
     then 0 = n by XCMPLX_1:6;
     hence thesis by S1;
   end;
 end;
  
Corollary1:
  sqrt 2 is irrational
  proof
    assume sqrt 2 is rational;
    then consider m being Integer, n being Element of NAT such that
    A0: n <> 0 & sqrt 2 = m/n by RAT_1:24;
    A1: m = sqrt 2 * n by A0,XCMPLX_1:88;
    A2: m/n >= 0 by A0, SQUARE_1:def 4;
    then n >= 0 by NAT_1:3;
    then m >= 0 by A2,A1,REAL_2:121,A0;
    then m is Element of NAT by INT_1:16;
    then reconsider m as Nat;
    reconsider n as Nat;
    m^2 = (sqrt 2)^2*n^2 by A1,SQUARE_1:68
       .=2*n^2 by SQUARE_1:def 4;
    then m = 0 & n = 0 by Lemma;
    hence contradiction by A0;
  end;