Step | Hyp | Ref
| Expression |
1 | | prmlem2.n |
. 2
โข ๐ โ โ |
2 | | prmlem2.gt |
. 2
โข 1 <
๐ |
3 | | prmlem2.2 |
. 2
โข ยฌ 2
โฅ ๐ |
4 | | prmlem2.3 |
. 2
โข ยฌ 3
โฅ ๐ |
5 | | eluzelre 12830 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ
(โคโฅโ;29)
โ ๐ฅ โ
โ) |
6 | 5 | resqcld 14087 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ
(โคโฅโ;29)
โ (๐ฅโ2) โ
โ) |
7 | | eluzle 12832 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ โ
(โคโฅโ;29)
โ ;29 โค ๐ฅ) |
8 | | 2nn0 12486 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 2 โ
โ0 |
9 | | 9nn0 12493 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 9 โ
โ0 |
10 | 8, 9 | deccl 12689 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ;29 โ
โ0 |
11 | 10 | nn0rei 12480 |
. . . . . . . . . . . . . . . . . . . . 21
โข ;29 โ โ |
12 | 10 | nn0ge0i 12496 |
. . . . . . . . . . . . . . . . . . . . 21
โข 0 โค
;29 |
13 | | le2sq2 14097 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((;29 โ โ โง 0 โค ;29) โง (๐ฅ โ โ โง ;29 โค ๐ฅ)) โ (;29โ2) โค (๐ฅโ2)) |
14 | 11, 12, 13 | mpanl12 701 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ฅ โ โ โง ;29 โค ๐ฅ) โ (;29โ2) โค (๐ฅโ2)) |
15 | 5, 7, 14 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ โ
(โคโฅโ;29)
โ (;29โ2) โค (๐ฅโ2)) |
16 | 1 | nnrei 12218 |
. . . . . . . . . . . . . . . . . . . 20
โข ๐ โ โ |
17 | 11 | resqcli 14147 |
. . . . . . . . . . . . . . . . . . . 20
โข (;29โ2) โ
โ |
18 | | prmlem2.lt |
. . . . . . . . . . . . . . . . . . . . . 22
โข ๐ < ;;841 |
19 | 10 | nn0cni 12481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ;29 โ โ |
20 | 19 | sqvali 14141 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (;29โ2) = (;29 ยท ;29) |
21 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ;29 = ;29 |
22 | | 1nn0 12485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข 1 โ
โ0 |
23 | | 6nn0 12490 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 6 โ
โ0 |
24 | 8, 23 | deccl 12689 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ;26 โ
โ0 |
25 | | 5nn0 12489 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 5 โ
โ0 |
26 | | 8nn0 12492 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 8 โ
โ0 |
27 | 19 | 2timesi 12347 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (2
ยท ;29) = (;29 + ;29) |
28 | | 2p2e4 12344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
โข (2 + 2) =
4 |
29 | 28 | oveq1i 7416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข ((2 + 2)
+ 1) = (4 + 1) |
30 | | 4p1e5 12355 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
โข (4 + 1) =
5 |
31 | 29, 30 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข ((2 + 2)
+ 1) = 5 |
32 | | 9p9e18 12768 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (9 + 9) =
;18 |
33 | 8, 9, 8, 9, 21, 21, 31, 26, 32 | decaddc 12729 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (;29 + ;29) = ;58 |
34 | 27, 33 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (2
ยท ;29) = ;58 |
35 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ;26 = ;26 |
36 | | 5p2e7 12365 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
โข (5 + 2) =
7 |
37 | 36 | oveq1i 7416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข ((5 + 2)
+ 1) = (7 + 1) |
38 | | 7p1e8 12358 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (7 + 1) =
8 |
39 | 37, 38 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((5 + 2)
+ 1) = 8 |
40 | | 4nn0 12488 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข 4 โ
โ0 |
41 | | 8p6e14 12758 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (8 + 6) =
;14 |
42 | 25, 26, 8, 23, 34, 35, 39, 40, 41 | decaddc 12729 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข ((2
ยท ;29) + ;26) = ;84 |
43 | | 9t2e18 12796 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (9
ยท 2) = ;18 |
44 | | 1p1e2 12334 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (1 + 1) =
2 |
45 | | 8p8e16 12760 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
โข (8 + 8) =
;16 |
46 | 22, 26, 26, 43, 44, 23, 45 | decaddci 12735 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข ((9
ยท 2) + 8) = ;26 |
47 | | 9t9e81 12803 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
โข (9
ยท 9) = ;81 |
48 | 9, 8, 9, 21, 22, 26, 46, 47 | decmul2c 12740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข (9
ยท ;29) = ;;261 |
49 | 10, 8, 9, 21, 22, 24, 42, 48 | decmul1c 12739 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (;29 ยท ;29) = ;;841 |
50 | 20, 49 | eqtri 2761 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (;29โ2) = ;;841 |
51 | 18, 50 | breqtrri 5175 |
. . . . . . . . . . . . . . . . . . . . 21
โข ๐ < (;29โ2) |
52 | | ltletr 11303 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โ โง (;29โ2) โ โ โง (๐ฅโ2) โ โ) โ
((๐ < (;29โ2) โง (;29โ2) โค (๐ฅโ2)) โ ๐ < (๐ฅโ2))) |
53 | 51, 52 | mpani 695 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โ โ โง (;29โ2) โ โ โง (๐ฅโ2) โ โ) โ
((;29โ2) โค (๐ฅโ2) โ ๐ < (๐ฅโ2))) |
54 | 16, 17, 53 | mp3an12 1452 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ฅโ2) โ โ โ
((;29โ2) โค (๐ฅโ2) โ ๐ < (๐ฅโ2))) |
55 | 6, 15, 54 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ
(โคโฅโ;29)
โ ๐ < (๐ฅโ2)) |
56 | | ltnle 11290 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โ โ โง (๐ฅโ2) โ โ) โ
(๐ < (๐ฅโ2) โ ยฌ (๐ฅโ2) โค ๐)) |
57 | 16, 6, 56 | sylancr 588 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ โ
(โคโฅโ;29)
โ (๐ < (๐ฅโ2) โ ยฌ (๐ฅโ2) โค ๐)) |
58 | 55, 57 | mpbid 231 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ โ
(โคโฅโ;29)
โ ยฌ (๐ฅโ2)
โค ๐) |
59 | 58 | pm2.21d 121 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ
(โคโฅโ;29)
โ ((๐ฅโ2) โค
๐ โ ยฌ ๐ฅ โฅ ๐)) |
60 | 59 | adantld 492 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โ
(โคโฅโ;29)
โ ((๐ฅ โ (โ
โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
61 | 60 | adantl 483 |
. . . . . . . . . . . . . 14
โข ((ยฌ 2
โฅ ;29 โง ๐ฅ โ
(โคโฅโ;29)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
62 | | 9nn 12307 |
. . . . . . . . . . . . . . . 16
โข 9 โ
โ |
63 | | 3nn 12288 |
. . . . . . . . . . . . . . . 16
โข 3 โ
โ |
64 | | 1lt9 12415 |
. . . . . . . . . . . . . . . 16
โข 1 <
9 |
65 | | 1lt3 12382 |
. . . . . . . . . . . . . . . 16
โข 1 <
3 |
66 | | 9t3e27 12797 |
. . . . . . . . . . . . . . . 16
โข (9
ยท 3) = ;27 |
67 | 62, 63, 64, 65, 66 | nprmi 16623 |
. . . . . . . . . . . . . . 15
โข ยฌ
;27 โ
โ |
68 | 67 | pm2.21i 119 |
. . . . . . . . . . . . . 14
โข (;27 โ โ โ ยฌ ;27 โฅ ๐) |
69 | | 7nn0 12491 |
. . . . . . . . . . . . . . 15
โข 7 โ
โ0 |
70 | | eqid 2733 |
. . . . . . . . . . . . . . 15
โข ;27 = ;27 |
71 | | 7p2e9 12370 |
. . . . . . . . . . . . . . 15
โข (7 + 2) =
9 |
72 | 8, 69, 8, 70, 71 | decaddi 12734 |
. . . . . . . . . . . . . 14
โข (;27 + 2) = ;29 |
73 | 61, 68, 72 | prmlem0 17036 |
. . . . . . . . . . . . 13
โข ((ยฌ 2
โฅ ;27 โง ๐ฅ โ
(โคโฅโ;27)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
74 | | 5nn 12295 |
. . . . . . . . . . . . . . 15
โข 5 โ
โ |
75 | | 1lt5 12389 |
. . . . . . . . . . . . . . 15
โข 1 <
5 |
76 | | 5t5e25 12777 |
. . . . . . . . . . . . . . 15
โข (5
ยท 5) = ;25 |
77 | 74, 74, 75, 75, 76 | nprmi 16623 |
. . . . . . . . . . . . . 14
โข ยฌ
;25 โ
โ |
78 | 77 | pm2.21i 119 |
. . . . . . . . . . . . 13
โข (;25 โ โ โ ยฌ ;25 โฅ ๐) |
79 | | eqid 2733 |
. . . . . . . . . . . . . 14
โข ;25 = ;25 |
80 | 8, 25, 8, 79, 36 | decaddi 12734 |
. . . . . . . . . . . . 13
โข (;25 + 2) = ;27 |
81 | 73, 78, 80 | prmlem0 17036 |
. . . . . . . . . . . 12
โข ((ยฌ 2
โฅ ;25 โง ๐ฅ โ
(โคโฅโ;25)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
82 | | prmlem2.23 |
. . . . . . . . . . . . 13
โข ยฌ
;23 โฅ ๐ |
83 | 82 | a1i 11 |
. . . . . . . . . . . 12
โข (;23 โ โ โ ยฌ ;23 โฅ ๐) |
84 | | 3nn0 12487 |
. . . . . . . . . . . . 13
โข 3 โ
โ0 |
85 | | eqid 2733 |
. . . . . . . . . . . . 13
โข ;23 = ;23 |
86 | | 3p2e5 12360 |
. . . . . . . . . . . . 13
โข (3 + 2) =
5 |
87 | 8, 84, 8, 85, 86 | decaddi 12734 |
. . . . . . . . . . . 12
โข (;23 + 2) = ;25 |
88 | 81, 83, 87 | prmlem0 17036 |
. . . . . . . . . . 11
โข ((ยฌ 2
โฅ ;23 โง ๐ฅ โ
(โคโฅโ;23)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
89 | | 7nn 12301 |
. . . . . . . . . . . . 13
โข 7 โ
โ |
90 | | 1lt7 12400 |
. . . . . . . . . . . . 13
โข 1 <
7 |
91 | | 7t3e21 12784 |
. . . . . . . . . . . . 13
โข (7
ยท 3) = ;21 |
92 | 89, 63, 90, 65, 91 | nprmi 16623 |
. . . . . . . . . . . 12
โข ยฌ
;21 โ
โ |
93 | 92 | pm2.21i 119 |
. . . . . . . . . . 11
โข (;21 โ โ โ ยฌ ;21 โฅ ๐) |
94 | | eqid 2733 |
. . . . . . . . . . . 12
โข ;21 = ;21 |
95 | | 1p2e3 12352 |
. . . . . . . . . . . 12
โข (1 + 2) =
3 |
96 | 8, 22, 8, 94, 95 | decaddi 12734 |
. . . . . . . . . . 11
โข (;21 + 2) = ;23 |
97 | 88, 93, 96 | prmlem0 17036 |
. . . . . . . . . 10
โข ((ยฌ 2
โฅ ;21 โง ๐ฅ โ
(โคโฅโ;21)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
98 | | prmlem2.19 |
. . . . . . . . . . 11
โข ยฌ
;19 โฅ ๐ |
99 | 98 | a1i 11 |
. . . . . . . . . 10
โข (;19 โ โ โ ยฌ ;19 โฅ ๐) |
100 | | eqid 2733 |
. . . . . . . . . . 11
โข ;19 = ;19 |
101 | | 9p2e11 12761 |
. . . . . . . . . . 11
โข (9 + 2) =
;11 |
102 | 22, 9, 8, 100, 44, 22, 101 | decaddci 12735 |
. . . . . . . . . 10
โข (;19 + 2) = ;21 |
103 | 97, 99, 102 | prmlem0 17036 |
. . . . . . . . 9
โข ((ยฌ 2
โฅ ;19 โง ๐ฅ โ
(โคโฅโ;19)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
104 | | prmlem2.17 |
. . . . . . . . . 10
โข ยฌ
;17 โฅ ๐ |
105 | 104 | a1i 11 |
. . . . . . . . 9
โข (;17 โ โ โ ยฌ ;17 โฅ ๐) |
106 | | eqid 2733 |
. . . . . . . . . 10
โข ;17 = ;17 |
107 | 22, 69, 8, 106, 71 | decaddi 12734 |
. . . . . . . . 9
โข (;17 + 2) = ;19 |
108 | 103, 105,
107 | prmlem0 17036 |
. . . . . . . 8
โข ((ยฌ 2
โฅ ;17 โง ๐ฅ โ
(โคโฅโ;17)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
109 | | 5t3e15 12775 |
. . . . . . . . . 10
โข (5
ยท 3) = ;15 |
110 | 74, 63, 75, 65, 109 | nprmi 16623 |
. . . . . . . . 9
โข ยฌ
;15 โ
โ |
111 | 110 | pm2.21i 119 |
. . . . . . . 8
โข (;15 โ โ โ ยฌ ;15 โฅ ๐) |
112 | | eqid 2733 |
. . . . . . . . 9
โข ;15 = ;15 |
113 | 22, 25, 8, 112, 36 | decaddi 12734 |
. . . . . . . 8
โข (;15 + 2) = ;17 |
114 | 108, 111,
113 | prmlem0 17036 |
. . . . . . 7
โข ((ยฌ 2
โฅ ;15 โง ๐ฅ โ
(โคโฅโ;15)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
115 | | prmlem2.13 |
. . . . . . . 8
โข ยฌ
;13 โฅ ๐ |
116 | 115 | a1i 11 |
. . . . . . 7
โข (;13 โ โ โ ยฌ ;13 โฅ ๐) |
117 | | eqid 2733 |
. . . . . . . 8
โข ;13 = ;13 |
118 | 22, 84, 8, 117, 86 | decaddi 12734 |
. . . . . . 7
โข (;13 + 2) = ;15 |
119 | 114, 116,
118 | prmlem0 17036 |
. . . . . 6
โข ((ยฌ 2
โฅ ;13 โง ๐ฅ โ
(โคโฅโ;13)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
120 | | prmlem2.11 |
. . . . . . 7
โข ยฌ
;11 โฅ ๐ |
121 | 120 | a1i 11 |
. . . . . 6
โข (;11 โ โ โ ยฌ ;11 โฅ ๐) |
122 | | eqid 2733 |
. . . . . . 7
โข ;11 = ;11 |
123 | 22, 22, 8, 122, 95 | decaddi 12734 |
. . . . . 6
โข (;11 + 2) = ;13 |
124 | 119, 121,
123 | prmlem0 17036 |
. . . . 5
โข ((ยฌ 2
โฅ ;11 โง ๐ฅ โ
(โคโฅโ;11)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
125 | | 9nprm 17043 |
. . . . . 6
โข ยฌ 9
โ โ |
126 | 125 | pm2.21i 119 |
. . . . 5
โข (9 โ
โ โ ยฌ 9 โฅ ๐) |
127 | 124, 126,
101 | prmlem0 17036 |
. . . 4
โข ((ยฌ 2
โฅ 9 โง ๐ฅ โ
(โคโฅโ9)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
128 | | prmlem2.7 |
. . . . 5
โข ยฌ 7
โฅ ๐ |
129 | 128 | a1i 11 |
. . . 4
โข (7 โ
โ โ ยฌ 7 โฅ ๐) |
130 | 127, 129,
71 | prmlem0 17036 |
. . 3
โข ((ยฌ 2
โฅ 7 โง ๐ฅ โ
(โคโฅโ7)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
131 | | prmlem2.5 |
. . . 4
โข ยฌ 5
โฅ ๐ |
132 | 131 | a1i 11 |
. . 3
โข (5 โ
โ โ ยฌ 5 โฅ ๐) |
133 | 130, 132,
36 | prmlem0 17036 |
. 2
โข ((ยฌ 2
โฅ 5 โง ๐ฅ โ
(โคโฅโ5)) โ ((๐ฅ โ (โ โ {2}) โง (๐ฅโ2) โค ๐) โ ยฌ ๐ฅ โฅ ๐)) |
134 | 1, 2, 3, 4, 133 | prmlem1a 17037 |
1
โข ๐ โ โ |