let n be Nat; :: thesis: ( n < 31 & 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 & not n = 23 implies n = 29 )
assume that
A1: n < 31 and
A2: 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 or n = 29 )
A3: ( 1 + 1 < n + 1 & n < 30 + 1 ) by A2, A1, XREAL_1:6;

per cases ( ( 2 <= n & n < 5 ) or ( 5 <= n & n <= 29 + 1 ) ) by A3, 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 or n = 29 )

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 or n = 29 ) by A2, NAT_4:59; :: thesis: verum

end;

suppose A4: ( 5 <= n & n <= 29 + 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 or n = 29 )

per cases ( ( 5 <= n & n <= 9 + 1 ) or ( 10 <= n & n <= 15 + 1 ) or ( 16 <= n & n <= 20 + 1 ) or ( 21 <= n & n <= 27 + 1 ) or ( 28 <= n & n <= 29 + 1 ) ) by A4;

suppose ( 5 <= n & n <= 9 + 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 or n = 29 )

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 ) ) ;
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 or n = 29 ) by A2, NAT_4:57, NAT_1:9; :: thesis: verum

end;

suppose ( 10 <= n & n <= 15 + 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 or n = 29 )

then ( ( 10 <= n & n <= 10 + 1 ) or ( 11 <= n & n <= 11 + 1 ) or ( 12 <= n & n <= 12 + 1 ) or ( 13 <= n & n <= 13 + 1 ) or ( 14 <= n & n <= 14 + 1 ) or ( 15 <= n & n <= 15 + 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 or n = 29 ) by A2, NAT_4:57, NAT_1:9; :: thesis: verum

end;

suppose ( 16 <= 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 or n = 29 )

then ( ( 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 or n = 29 ) by A2, Lm1, Lm2, 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 or n = 29 )

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 or n = 29 ) by A2, NAT_4:58, NAT_1:9; :: thesis: verum

end;

suppose ( 28 <= n & n <= 29 + 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 or n = 29 )

then ( ( 28 <= n & n <= 28 + 1 ) or ( 29 <= n & n <= 29 + 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 or n = 29 ) by A2, NAT_4:58, Th10, NAT_1:9; :: thesis: verum

end;

end;

end;

end;