let p be Prime; :: thesis: ( not p < 23 or p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 )
assume p < 23 ; :: thesis: ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 )
then ( 1 + 1 < p + 1 & p < 22 + 1 ) by XREAL_1:6, INT_2:def 4;
per cases then ( ( 2 <= p & p < 19 ) or ( 19 <= p & p <= 19 + 1 ) or ( 20 <= p & p <= 20 + 1 ) or ( 21 <= p & p <= 21 + 1 ) ) by NAT_1:13;
suppose ( 2 <= p & p < 19 ) ; :: thesis: ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 )
hence ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 ) by Th13; :: thesis: verum
end;
suppose ( 19 <= p & p <= 19 + 1 ) ; :: thesis: ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 )
hence ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 ) by XPRIMES0:20, NAT_1:9; :: thesis: verum
end;
suppose ( 20 <= p & p <= 20 + 1 ) ; :: thesis: ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 )
hence ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 ) by XPRIMES0:20, XPRIMES0:21, NAT_1:9; :: thesis: verum
end;
suppose ( 21 <= p & p <= 21 + 1 ) ; :: thesis: ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 )
hence ( p = 2 or p = 3 or p = 5 or p = 7 or p = 11 or p = 13 or p = 17 or p = 19 ) by XPRIMES0:21, XPRIMES0:22, NAT_1:9; :: thesis: verum
end;
end;