Step | Hyp | Ref
| Expression |
1 | | elnnuz 12814 |
. . 3
โข (๐ โ โ โ ๐ โ
(โคโฅโ1)) |
2 | | ax-1 6 |
. . . 4
โข
(โ๐ โ
โ (๐ < ๐ โง ๐ โค (2 ยท ๐)) โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
3 | | 6nn0 12441 |
. . . . . . . . . . . . . . . . 17
โข 6 โ
โ0 |
4 | | 4nn0 12439 |
. . . . . . . . . . . . . . . . 17
โข 4 โ
โ0 |
5 | 3, 4 | deccl 12640 |
. . . . . . . . . . . . . . . 16
โข ;64 โ
โ0 |
6 | 5 | nn0rei 12431 |
. . . . . . . . . . . . . . 15
โข ;64 โ โ |
7 | 6 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ;83)
โ ;64 โ
โ) |
8 | | 8nn0 12443 |
. . . . . . . . . . . . . . . . 17
โข 8 โ
โ0 |
9 | | 3nn0 12438 |
. . . . . . . . . . . . . . . . 17
โข 3 โ
โ0 |
10 | 8, 9 | deccl 12640 |
. . . . . . . . . . . . . . . 16
โข ;83 โ
โ0 |
11 | 10 | nn0rei 12431 |
. . . . . . . . . . . . . . 15
โข ;83 โ โ |
12 | 11 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ;83)
โ ;83 โ
โ) |
13 | | eluzelre 12781 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ;83)
โ ๐ โ
โ) |
14 | | 4lt10 12761 |
. . . . . . . . . . . . . . . 16
โข 4 <
;10 |
15 | | 6lt8 12353 |
. . . . . . . . . . . . . . . 16
โข 6 <
8 |
16 | 3, 8, 4, 9, 14, 15 | decltc 12654 |
. . . . . . . . . . . . . . 15
โข ;64 < ;83 |
17 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ;83)
โ ;64 < ;83) |
18 | | eluzle 12783 |
. . . . . . . . . . . . . 14
โข (๐ โ
(โคโฅโ;83)
โ ;83 โค ๐) |
19 | 7, 12, 13, 17, 18 | ltletrd 11322 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ;83)
โ ;64 < ๐) |
20 | | ltnle 11241 |
. . . . . . . . . . . . . 14
โข ((;64 โ โ โง ๐ โ โ) โ (;64 < ๐ โ ยฌ ๐ โค ;64)) |
21 | 6, 13, 20 | sylancr 588 |
. . . . . . . . . . . . 13
โข (๐ โ
(โคโฅโ;83)
โ (;64 < ๐ โ ยฌ ๐ โค ;64)) |
22 | 19, 21 | mpbid 231 |
. . . . . . . . . . . 12
โข (๐ โ
(โคโฅโ;83)
โ ยฌ ๐ โค ;64) |
23 | 22 | pm2.21d 121 |
. . . . . . . . . . 11
โข (๐ โ
(โคโฅโ;83)
โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
24 | | 83prm 17002 |
. . . . . . . . . . 11
โข ;83 โ โ |
25 | 4, 9 | deccl 12640 |
. . . . . . . . . . 11
โข ;43 โ
โ0 |
26 | | 2nn0 12437 |
. . . . . . . . . . . 12
โข 2 โ
โ0 |
27 | | eqid 2737 |
. . . . . . . . . . . 12
โข ;43 = ;43 |
28 | | 4t2e8 12328 |
. . . . . . . . . . . 12
โข (4
ยท 2) = 8 |
29 | | 3t2e6 12326 |
. . . . . . . . . . . 12
โข (3
ยท 2) = 6 |
30 | 26, 4, 9, 27, 28, 29 | decmul1 12689 |
. . . . . . . . . . 11
โข (;43 ยท 2) = ;86 |
31 | | 3lt10 12762 |
. . . . . . . . . . . 12
โข 3 <
;10 |
32 | | 4lt8 12355 |
. . . . . . . . . . . 12
โข 4 <
8 |
33 | 4, 8, 9, 9, 31, 32 | decltc 12654 |
. . . . . . . . . . 11
โข ;43 < ;83 |
34 | | 6nn 12249 |
. . . . . . . . . . . . 13
โข 6 โ
โ |
35 | | 3lt6 12343 |
. . . . . . . . . . . . 13
โข 3 <
6 |
36 | 8, 9, 34, 35 | declt 12653 |
. . . . . . . . . . . 12
โข ;83 < ;86 |
37 | 36 | orci 864 |
. . . . . . . . . . 11
โข (;83 < ;86 โจ ;83 = ;86) |
38 | 2, 23, 24, 25, 30, 33, 37 | bpos1lem 26646 |
. . . . . . . . . 10
โข (๐ โ
(โคโฅโ;43)
โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
39 | | 43prm 17001 |
. . . . . . . . . 10
โข ;43 โ โ |
40 | 26, 9 | deccl 12640 |
. . . . . . . . . 10
โข ;23 โ
โ0 |
41 | | eqid 2737 |
. . . . . . . . . . 11
โข ;23 = ;23 |
42 | | 2t2e4 12324 |
. . . . . . . . . . 11
โข (2
ยท 2) = 4 |
43 | 26, 26, 9, 41, 42, 29 | decmul1 12689 |
. . . . . . . . . 10
โข (;23 ยท 2) = ;46 |
44 | | 2lt4 12335 |
. . . . . . . . . . 11
โข 2 <
4 |
45 | 26, 4, 9, 9, 31, 44 | decltc 12654 |
. . . . . . . . . 10
โข ;23 < ;43 |
46 | 4, 9, 34, 35 | declt 12653 |
. . . . . . . . . . 11
โข ;43 < ;46 |
47 | 46 | orci 864 |
. . . . . . . . . 10
โข (;43 < ;46 โจ ;43 = ;46) |
48 | 2, 38, 39, 40, 43, 45, 47 | bpos1lem 26646 |
. . . . . . . . 9
โข (๐ โ
(โคโฅโ;23)
โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
49 | | 23prm 16998 |
. . . . . . . . 9
โข ;23 โ โ |
50 | | 1nn0 12436 |
. . . . . . . . . 10
โข 1 โ
โ0 |
51 | 50, 9 | deccl 12640 |
. . . . . . . . 9
โข ;13 โ
โ0 |
52 | | eqid 2737 |
. . . . . . . . . 10
โข ;13 = ;13 |
53 | | 2cn 12235 |
. . . . . . . . . . 11
โข 2 โ
โ |
54 | 53 | mulid2i 11167 |
. . . . . . . . . 10
โข (1
ยท 2) = 2 |
55 | 26, 50, 9, 52, 54, 29 | decmul1 12689 |
. . . . . . . . 9
โข (;13 ยท 2) = ;26 |
56 | | 1lt2 12331 |
. . . . . . . . . 10
โข 1 <
2 |
57 | 50, 26, 9, 9, 31, 56 | decltc 12654 |
. . . . . . . . 9
โข ;13 < ;23 |
58 | 26, 9, 34, 35 | declt 12653 |
. . . . . . . . . 10
โข ;23 < ;26 |
59 | 58 | orci 864 |
. . . . . . . . 9
โข (;23 < ;26 โจ ;23 = ;26) |
60 | 2, 48, 49, 51, 55, 57, 59 | bpos1lem 26646 |
. . . . . . . 8
โข (๐ โ
(โคโฅโ;13)
โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
61 | | 13prm 16995 |
. . . . . . . 8
โข ;13 โ โ |
62 | | 7nn0 12442 |
. . . . . . . 8
โข 7 โ
โ0 |
63 | | 7t2e14 12734 |
. . . . . . . 8
โข (7
ยท 2) = ;14 |
64 | | 1nn 12171 |
. . . . . . . . 9
โข 1 โ
โ |
65 | | 7lt10 12758 |
. . . . . . . . 9
โข 7 <
;10 |
66 | 64, 9, 62, 65 | declti 12663 |
. . . . . . . 8
โข 7 <
;13 |
67 | | 4nn 12243 |
. . . . . . . . . 10
โข 4 โ
โ |
68 | | 3lt4 12334 |
. . . . . . . . . 10
โข 3 <
4 |
69 | 50, 9, 67, 68 | declt 12653 |
. . . . . . . . 9
โข ;13 < ;14 |
70 | 69 | orci 864 |
. . . . . . . 8
โข (;13 < ;14 โจ ;13 = ;14) |
71 | 2, 60, 61, 62, 63, 66, 70 | bpos1lem 26646 |
. . . . . . 7
โข (๐ โ
(โคโฅโ7) โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
72 | | 7prm 16990 |
. . . . . . 7
โข 7 โ
โ |
73 | | 5nn0 12440 |
. . . . . . 7
โข 5 โ
โ0 |
74 | | 5t2e10 12725 |
. . . . . . 7
โข (5
ยท 2) = ;10 |
75 | | 5lt7 12347 |
. . . . . . 7
โข 5 <
7 |
76 | 65 | orci 864 |
. . . . . . 7
โข (7 <
;10 โจ 7 = ;10) |
77 | 2, 71, 72, 73, 74, 75, 76 | bpos1lem 26646 |
. . . . . 6
โข (๐ โ
(โคโฅโ5) โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
78 | | 5prm 16988 |
. . . . . 6
โข 5 โ
โ |
79 | | 3lt5 12338 |
. . . . . 6
โข 3 <
5 |
80 | | 5lt6 12341 |
. . . . . . 7
โข 5 <
6 |
81 | 80 | orci 864 |
. . . . . 6
โข (5 < 6
โจ 5 = 6) |
82 | 2, 77, 78, 9, 29, 79, 81 | bpos1lem 26646 |
. . . . 5
โข (๐ โ
(โคโฅโ3) โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
83 | | 3prm 16577 |
. . . . 5
โข 3 โ
โ |
84 | | 2lt3 12332 |
. . . . 5
โข 2 <
3 |
85 | 68 | orci 864 |
. . . . 5
โข (3 < 4
โจ 3 = 4) |
86 | 2, 82, 83, 26, 42, 84, 85 | bpos1lem 26646 |
. . . 4
โข (๐ โ
(โคโฅโ2) โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
87 | | 2prm 16575 |
. . . 4
โข 2 โ
โ |
88 | | eqid 2737 |
. . . . 5
โข 2 =
2 |
89 | 88 | olci 865 |
. . . 4
โข (2 < 2
โจ 2 = 2) |
90 | 2, 86, 87, 50, 54, 56, 89 | bpos1lem 26646 |
. . 3
โข (๐ โ
(โคโฅโ1) โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
91 | 1, 90 | sylbi 216 |
. 2
โข (๐ โ โ โ (๐ โค ;64 โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐)))) |
92 | 91 | imp 408 |
1
โข ((๐ โ โ โง ๐ โค ;64) โ โ๐ โ โ (๐ < ๐ โง ๐ โค (2 ยท ๐))) |