let p be Nat; :: thesis: ( p is prime implies sqrt p is irrational )
assume A1: p is prime ; :: thesis: sqrt p is irrational
then A2: p > 1 by INT_2:def 4;
assume sqrt p is rational ; :: thesis: contradiction
then consider i being Integer, n being Nat such that
A3: n <> 0 and
A4: sqrt p = i / n and
A5: for i1 being Integer
for n1 being Nat st n1 <> 0 & sqrt p = i1 / n1 holds
n <= n1 by RAT_1:9;
A6: i = (sqrt p) * n by A3, A4, XCMPLX_1:87;
sqrt p >= 0 by SQUARE_1:def 2;
then reconsider m = i as Element of NAT by A6, INT_1:3;
A7: m ^2 = ((sqrt p) ^2) * (n ^2) by A6
.= p * (n ^2) by SQUARE_1:def 2 ;
then p divides m ^2 by NAT_D:def 3;
then p divides m by A1, NEWTON:80;
then consider m1 being Nat such that
A8: m = p * m1 by NAT_D:def 3;
n ^2 = (p * (p * (m1 ^2))) / p by A2, A7, A8, XCMPLX_1:89
.= p * (m1 ^2) by A2, XCMPLX_1:89 ;
then p divides n ^2 by NAT_D:def 3;
then p divides n by A1, NEWTON:80;
then consider n1 being Nat such that
A9: n = p * n1 by NAT_D:def 3;
reconsider n1 = n1 as Element of NAT by ORDINAL1:def 12;
A10: m1 / n1 = sqrt p by A2, A4, A8, A9, XCMPLX_1:91;
A11: n1 <> 0 by A3, A9;
then p * n1 > 1 * n1 by A2, XREAL_1:98;
hence contradiction by A5, A9, A11, A10; :: thesis: verum