let n be Nat; :: thesis: ( 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 that
A2: n < 29 and
A3: 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 )
A1: 1 < n by A3, INT_2:def 4;
A4: ( 1 + 1 < n + 1 & n < 28 + 1 ) by A1, A2, XREAL_1:6;

per cases ( ( 2 <= n & n < 5 ) or ( 5 <= n & n <= 27 + 1 ) ) by A4, 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 A3, Lm2; :: thesis: verum

end;

suppose A5: ( 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 A5;

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 A3, 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 A3, 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 A3, Lm4, NAT_1:9; :: thesis: verum

end;

end;

end;

end;