let k be Nat; ( 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
; 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; ( 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
; ( 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; verum