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 & sqrt p = i / n & ( for i1 being Integer
for n1 being Element of NAT st n1 <> 0 & sqrt p = i1 / n1 holds
n <= n1 ) ) by RAT_1:25;
A4: i = (sqrt p) * n by A3, XCMPLX_1:88;
( sqrt p >= 0 & n >= 0 ) by SQUARE_1:def 4;
then i >= 0 by A4;
then reconsider m = i as Element of NAT by INT_1:16;
A5: m ^2 = ((sqrt p) ^2 ) * (n ^2 ) by A4
.= 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
A6: m = p * m1 by NAT_D:def 3;
n ^2 = (p * (p * (m1 ^2 ))) / p by A2, A5, A6, 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
A7: n = p * n1 by NAT_D:def 3;
A8: n1 <> 0 by A3, A7;
A9: m1 / n1 = sqrt p by A2, A3, A6, A7, XCMPLX_1:92;
p * n1 > 1 * n1 by A2, A8, XREAL_1:100;
hence contradiction by A3, A7, A8, A9; :: thesis: verum