environ
vocabulary SQUARE_1,IRRAT_1,ARYTM_3,RAT_1,INT_1;
constructors NAT_1,PREPOWER,PEPIN,MEMBERED;
notations XCMPLX_0,XREAL_0,INT_1,NAT_1,RAT_1,SQUARE_1,IRRAT_1;
registrations XREAL_0,INT_1,MEMBERED;
theorems INT_1,SQUARE_1,REAL_2,INT_2,XCMPLX_1,NAT_1,RAT_1,NEWTON;
requirements ARITHM,REAL,NUMERALS,SUBSET;
begin
theorem
sqrt 2 is irrational
proof
assume sqrt 2 is rational;
then consider i being Integer, n being Nat such that
W1: n<>0 and
W2: sqrt 2=i/n and
W3: for i1 being Integer, n1 being Nat st n1<>0 & sqrt 2=i1/n1 holds n<=n1
by RAT_1:25;
A5: i=sqrt 2*n by W1,XCMPLX_1:88,W2;
C: sqrt 2>=0 & n>0 by W1,NAT_1:19,SQUARE_1:93;
then i>=0 by A5,REAL_2:121;
then reconsider m = i as Nat by INT_1:16;
A6: m*m = n*n*(sqrt 2*sqrt 2) by A5
.= n*n*(sqrt 2)^2 by SQUARE_1:def 3
.= 2*(n*n) by SQUARE_1:def 4;
then 2 divides m*m by NAT_1:def 3;
then 2 divides m by INT_2:44,NEWTON:98;
then consider m1 being Nat such that
W4: m=2*m1 by NAT_1:def 3;
m1*m1*2*2 = m1*(m1*2)*2
.= 2*(n*n) by W4,A6,XCMPLX_1:4;
then 2*(m1*m1) = n*n by XCMPLX_1:5;
then 2 divides n*n by NAT_1:def 3;
then 2 divides n by INT_2:44,NEWTON:98;
then consider n1 being Nat such that
W5: n=2*n1 by NAT_1:def 3;
A10: m1/n1 = sqrt 2 by W4,W5,XCMPLX_1:92,W2;
A11: n1>0 by W5,C,REAL_2:123;
then 2*n1>1*n1 by REAL_2:199;
hence contradiction by A10,W5,A11,W3;
end;