let p be Element of 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 5;
assume not sqrt p is irrational ; :: thesis: contradiction
then consider i being Integer, n being Element of NAT such that
A3: n <> 0 and
A4: sqrt p = i / n and
A5: for i1 being Integer
for n1 being Element of NAT st n1 <> 0 & sqrt p = i1 / n1 holds
n <= n1 by RAT_1:25;
A6: i = (sqrt p) * n by A3, A4, XCMPLX_1:88;
sqrt p >= 0 by SQUARE_1:def 4;
then reconsider m = i as Element of NAT by A6, INT_1:16;
A7: m ^2 = ((sqrt p) ^2 ) * (n ^2 ) by A6
.= p * (n ^2 ) by SQUARE_1:def 4 ;
then p divides m ^2 by NAT_D:def 3;
then p divides m by A1, NEWTON:98;
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:90
.= p * (m1 ^2 ) by A2, XCMPLX_1:90 ;
then p divides n ^2 by NAT_D:def 3;
then p divides n by A1, NEWTON:98;
then consider n1 being Nat such that
A9: n = p * n1 by NAT_D:def 3;
A10: m1 / n1 = sqrt p by A2, A4, A8, A9, XCMPLX_1:92;
A11: n1 <> 0 by A3, A9;
then p * n1 > 1 * n1 by A2, XREAL_1:100;
hence contradiction by A5, A9, A11, A10; :: thesis: verum