let a be even Nat; ( 1 < a & a <= 100 & not a = 2 & not a = 4 & not a = 6 & not a = 8 & not a = 10 & not a = 12 & not a = 14 & not a = 16 & not a = 18 & not a = 20 & not a = 22 & not a = 24 & not a = 26 & not a = 28 & not a = 30 & not a = 32 & not a = 34 & not a = 36 & not a = 38 & not a = 40 & not a = 42 & not a = 44 & not a = 46 & not a = 48 & not a = 50 & not a = 52 & not a = 54 & not a = 56 & not a = 58 & not a = 60 & not a = 62 & not a = 64 & not a = 66 & not a = 68 & not a = 70 & not a = 72 & not a = 74 & not a = 76 & not a = 78 & not a = 80 & not a = 82 & not a = 84 & not a = 86 & not a = 88 & not a = 90 & not a = 92 & not a = 94 & not a = 96 & not a = 98 implies a = 100 )
assume A1:
1 < a
; ( not a <= 100 or a = 2 or a = 4 or a = 6 or a = 8 or a = 10 or a = 12 or a = 14 or a = 16 or a = 18 or a = 20 or a = 22 or a = 24 or a = 26 or a = 28 or a = 30 or a = 32 or a = 34 or a = 36 or a = 38 or a = 40 or a = 42 or a = 44 or a = 46 or a = 48 or a = 50 or a = 52 or a = 54 or a = 56 or a = 58 or a = 60 or a = 62 or a = 64 or a = 66 or a = 68 or a = 70 or a = 72 or a = 74 or a = 76 or a = 78 or a = 80 or a = 82 or a = 84 or a = 86 or a = 88 or a = 90 or a = 92 or a = 94 or a = 96 or a = 98 or a = 100 )
assume
a <= 100
; ( a = 2 or a = 4 or a = 6 or a = 8 or a = 10 or a = 12 or a = 14 or a = 16 or a = 18 or a = 20 or a = 22 or a = 24 or a = 26 or a = 28 or a = 30 or a = 32 or a = 34 or a = 36 or a = 38 or a = 40 or a = 42 or a = 44 or a = 46 or a = 48 or a = 50 or a = 52 or a = 54 or a = 56 or a = 58 or a = 60 or a = 62 or a = 64 or a = 66 or a = 68 or a = 70 or a = 72 or a = 74 or a = 76 or a = 78 or a = 80 or a = 82 or a = 84 or a = 86 or a = 88 or a = 90 or a = 92 or a = 94 or a = 96 or a = 98 or a = 100 )
then A2:
not not a = 0 & ... & not a = 100
;
( 3 = (1 * 2) + 1 & 5 = (2 * 2) + 1 & 7 = (3 * 2) + 1 & 9 = (4 * 2) + 1 & 11 = (5 * 2) + 1 & 13 = (6 * 2) + 1 & 15 = (7 * 2) + 1 & 17 = (8 * 2) + 1 & 19 = (9 * 2) + 1 & 21 = (10 * 2) + 1 & 23 = (11 * 2) + 1 & 25 = (12 * 2) + 1 & 27 = (13 * 2) + 1 & 29 = (14 * 2) + 1 & 31 = (15 * 2) + 1 & 33 = (16 * 2) + 1 & 35 = (17 * 2) + 1 & 37 = (18 * 2) + 1 & 39 = (19 * 2) + 1 & 41 = (20 * 2) + 1 & 43 = (21 * 2) + 1 & 45 = (22 * 2) + 1 & 47 = (23 * 2) + 1 & 49 = (24 * 2) + 1 & 51 = (25 * 2) + 1 & 53 = (26 * 2) + 1 & 55 = (27 * 2) + 1 & 57 = (28 * 2) + 1 & 59 = (29 * 2) + 1 & 61 = (30 * 2) + 1 & 63 = (31 * 2) + 1 & 65 = (32 * 2) + 1 & 67 = (33 * 2) + 1 & 69 = (34 * 2) + 1 & 71 = (35 * 2) + 1 & 73 = (36 * 2) + 1 & 75 = (37 * 2) + 1 & 77 = (38 * 2) + 1 & 79 = (39 * 2) + 1 & 81 = (40 * 2) + 1 & 83 = (41 * 2) + 1 & 85 = (42 * 2) + 1 & 87 = (43 * 2) + 1 & 89 = (44 * 2) + 1 & 91 = (45 * 2) + 1 & 93 = (46 * 2) + 1 & 95 = (47 * 2) + 1 & 97 = (48 * 2) + 1 & 99 = (49 * 2) + 1 )
;
hence
( a = 2 or a = 4 or a = 6 or a = 8 or a = 10 or a = 12 or a = 14 or a = 16 or a = 18 or a = 20 or a = 22 or a = 24 or a = 26 or a = 28 or a = 30 or a = 32 or a = 34 or a = 36 or a = 38 or a = 40 or a = 42 or a = 44 or a = 46 or a = 48 or a = 50 or a = 52 or a = 54 or a = 56 or a = 58 or a = 60 or a = 62 or a = 64 or a = 66 or a = 68 or a = 70 or a = 72 or a = 74 or a = 76 or a = 78 or a = 80 or a = 82 or a = 84 or a = 86 or a = 88 or a = 90 or a = 92 or a = 94 or a = 96 or a = 98 or a = 100 )
by A1, A2; verum