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 A2: ( 1 < n & n * n <= k & n is prime ) ; :: thesis: ( n = 2 or n = 3 )
then n * n < 5 * 5 by A1, XXREAL_0:2;
then n < 5 by Th1;
hence ( n = 2 or n = 3 ) by A2, Lm2; :: thesis: verum