let k be Nat; :: thesis: ( k < 841 implies for n being Nat st n * n <= k & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 holds
n = 23 )
assume A1: k < 841 ; :: thesis: for n being Nat st n * n <= k & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 holds
n = 23
let n be Nat; :: thesis: ( n * n <= k & n is prime & not n = 2 & not n = 3 & not n = 5 & not n = 7 & not n = 11 & not n = 13 & not n = 17 & not n = 19 implies n = 23 )
assume that
A3: n * n <= k and
A4: n is prime ; :: thesis: ( n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 )
n * n < 29 * 29 by A1, A3, XXREAL_0:2;
then n < 29 by Th1;
hence ( n = 2 or n = 3 or n = 5 or n = 7 or n = 11 or n = 13 or n = 17 or n = 19 or n = 23 ) by A4, Lm5; :: thesis: verum