let n be Element of NAT ; :: thesis: ( 1 < n & n < 29 & 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 A1: ( 1 < n & n < 29 & 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 )
then A2: ( 1 + 1 < n + 1 & n < 28 + 1 ) by XREAL_1:8;

per cases ( ( 2 <= n & n < 5 ) or ( 5 <= n & n <= 27 + 1 ) ) by A2, NAT_1:13;

suppose ( 2 <= n & n < 5 ) ; :: 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 )

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 A1, Lm2; :: thesis: verum

end;

suppose A3: ( 5 <= n & n <= 27 + 1 ) ; :: 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 )

per cases ( ( 5 <= n & n <= 12 + 1 ) or ( 13 <= n & n <= 20 + 1 ) or ( 21 <= n & n <= 27 + 1 ) ) by A3;

suppose ( 5 <= n & n <= 12 + 1 ) ; :: 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 )

then ( ( 5 <= n & n <= 5 + 1 ) or ( 6 <= n & n <= 6 + 1 ) or ( 7 <= n & n <= 7 + 1 ) or ( 8 <= n & n <= 8 + 1 ) or ( 9 <= n & n <= 9 + 1 ) or ( 10 <= n & n <= 10 + 1 ) or ( 11 <= n & n <= 11 + 1 ) or ( 12 <= n & n <= 12 + 1 ) ) ;
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 A1, Lm4, NAT_1:9; :: thesis: verum

end;

suppose ( 13 <= n & n <= 20 + 1 ) ; :: 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 )

then ( ( 13 <= n & n <= 13 + 1 ) or ( 14 <= n & n <= 14 + 1 ) or ( 15 <= n & n <= 15 + 1 ) or ( 16 <= n & n <= 16 + 1 ) or ( 17 <= n & n <= 17 + 1 ) or ( 18 <= n & n <= 18 + 1 ) or ( 19 <= n & n <= 19 + 1 ) or ( 20 <= n & n <= 20 + 1 ) ) ;
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 A1, Lm4, NAT_1:9; :: thesis: verum

end;

suppose ( 21 <= n & n <= 27 + 1 ) ; :: 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 )

then ( ( 21 <= n & n <= 21 + 1 ) or ( 22 <= n & n <= 22 + 1 ) or ( 23 <= n & n <= 23 + 1 ) or ( 24 <= n & n <= 24 + 1 ) or ( 25 <= n & n <= 25 + 1 ) or ( 26 <= n & n <= 26 + 1 ) or ( 27 <= n & n <= 27 + 1 ) ) ;
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 A1, Lm4, NAT_1:9; :: thesis: verum

end;

end;

end;

end;