let k be Element of NAT ; :: thesis: ( k < 25 implies for n being Element of NAT st 1 < n & n * n <= k & n is prime & not n = 2 holds
n = 3 )
assume A1: k < 25 ; :: thesis: for n being Element of NAT st 1 < n & n * n <= k & n is prime & not n = 2 holds
n = 3
let n be Element of NAT ; :: thesis: ( 1 < n & n * n <= k & n is prime & not n = 2 implies n = 3 )
assume that
A2: 1 < n and
A3: n * n <= k and
A4: n is prime ; :: thesis: ( n = 2 or n = 3 )
n * n < 5 * 5 by A1, A3, XXREAL_0:2;
then n < 5 by Th1;
hence ( n = 2 or n = 3 ) by A2, A4, Lm2; :: thesis: verum