:: 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 INT_1, SQUARE_1, MATRIX_2, IRRAT_1, RAT_1, ARYTM_3, ABSVALUE,
   SEQM_3, FINSET_1;
 notations INT_1, NAT_1, SQUARE_1, XXREAL_0, ABIAN, RAT_1, IRRAT_1, XCMPLX_0,
   INT_2, SEQM_3, FINSET_1, REAL_1, PEPIN;
 constructors INT_1, NAT_1, SQUARE_1, XXREAL_0, ABIAN, RAT_1, IRRAT_1,XCMPLX_0, 
    INT_2, SEQM_3, FINSET_1, PEPIN;
 requirements SUBSET, NUMERALS, ARITHM, BOOLE, REAL;
 registrations XREAL_0, REAL_1, NAT_1, INT_1;
begin


Lemma:  for m,n being Nat holds m^2 = 2*n^2 implies m = 0 & n = 0 
 proof
   let m,n being Nat;
   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 P[m];
     then consider n being Nat such that
     m^2 = 2*n^2 & m > 0;
     m^2 is even ;
::>            *4
     m is even;
::>          *4
     consider k being Nat such that m = 2*k;
::>                                       *4
     2*n^2 = m^2
::>            *4
          .= 4*k^2;
::>              *4
     then n^2 = 2*k^2;
     m > 0 implies m^2 > 0 & n^2 > 0 & n > 0;
::>                                        *4,4,4
     then P[n];
::>          *4,4
     m^2 = n^2 + n^2;
::>                *4
     n^2 + n^2 >  n^2;
::>                 *4
     then m^2 > n^2;
::>               *4
     then m > n;
::>           *4
     take m' = n;
     thus thesis;
::>            *4,4
   end;
   A2: for k being Nat holds not P[k]
   proof
     not ex q being Seq_of_Nat st q is infinite decreasing by Claim;
::>                                                         *4
     hence thesis;
::>             *4
   end;
   assume A0: m^2 = 2*n^2;
   per cases by A0; 
   suppose B1: m <> 0;
     then m > 0;
::>           *4
     then P[m] by B1;
::>             *4
     then contradiction by A2;
     hence thesis;
   end; 
   suppose S1: m = 0;
     then n = 0;
::>           *4
     thus thesis by S1;
::>               *4
   end; 
 end; 
  
Corollary:  sqrt 2 is irrational 
  proof 
    assume sqrt 2 is rational;
    then ex p,q being Integer st
    q <> 0 & sqrt 2 = p/q;
::>                     *4
    then consider m,n being Integer such that
    A0: sqrt 2 = m/n and m = abs m & n = abs n & n <> 0;
::>                                                   *4
    m^2 = 2*n^2;
::>           *4
    n = 0 by Lemma;
::>        *4
    hence contradiction;
::>                   *4
  end;
  
::> 4: This inference is not accepted