assume ex r being Rational st r |^ 3 = 2 ; :: thesis:
then consider r being Rational such that
A1: r |^ 3 = 2 ;
consider i being Integer, n being Nat such that
A3: n <> 0 and
A4: r = i / n and
A5: for i1 being Integer
for n1 being Nat st n1 <> 0 & r = i1 / n1 holds
n <= n1 by RAT_1:9;
A6: i = r * n by A3, A4, XCMPLX_1:87;
r >= 0 by A1, lemcontr1;
then reconsider m = i as Element of NAT by A6, INT_1:3;
A7: m |^ 3 = 2 * (n |^ 3) by A1, A6, lemcontr2;
then m is even ;
then consider m1 being Nat such that
A8: m = 2 * m1 by ABIAN:def 2;
n |^ 3 = ((2 * m1) |^ 3) / 2 by A7, A8
.= ((2 |^ (2 + 1)) * (m1 |^ 3)) / 2 by lemcontr2
.= (((2 |^ 2) * 2) * (m1 |^ 3)) / 2 by NEWTON:6
.= (2 |^ (1 + 1)) * (m1 |^ 3)
.= ((2 |^ 1) * 2) * (m1 |^ 3) by NEWTON:6
.= 2 * ((2 |^ 1) * (m1 |^ 3)) ;
then n is even ;
then consider n1 being Nat such that
A9: n = 2 * n1 by ABIAN:def 2;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 12;
A10: m1 / n1 = r by A4, A8, A9, XCMPLX_1:91;
A11: n1 <> 0 by A3, A9;
then 2 * n1 > 1 * n1 by XREAL_1:98;
hence contradiction by A5, A9, A11, A10; :: thesis:

end;