Proof of Theorem 1259lem5
Step | Hyp | Ref
| Expression |
1 | | 2nn 12046 |
. . . 4
⊢ 2 ∈
ℕ |
2 | | 3nn0 12251 |
. . . . 5
⊢ 3 ∈
ℕ0 |
3 | | 4nn0 12252 |
. . . . 5
⊢ 4 ∈
ℕ0 |
4 | 2, 3 | deccl 12452 |
. . . 4
⊢ ;34 ∈
ℕ0 |
5 | | nnexpcl 13795 |
. . . 4
⊢ ((2
∈ ℕ ∧ ;34 ∈
ℕ0) → (2↑;34) ∈ ℕ) |
6 | 1, 4, 5 | mp2an 689 |
. . 3
⊢
(2↑;34) ∈
ℕ |
7 | | nnm1nn0 12274 |
. . 3
⊢
((2↑;34) ∈
ℕ → ((2↑;34)
− 1) ∈ ℕ0) |
8 | 6, 7 | ax-mp 5 |
. 2
⊢
((2↑;34) − 1)
∈ ℕ0 |
9 | | 8nn0 12256 |
. . . 4
⊢ 8 ∈
ℕ0 |
10 | | 6nn0 12254 |
. . . 4
⊢ 6 ∈
ℕ0 |
11 | 9, 10 | deccl 12452 |
. . 3
⊢ ;86 ∈
ℕ0 |
12 | | 9nn0 12257 |
. . 3
⊢ 9 ∈
ℕ0 |
13 | 11, 12 | deccl 12452 |
. 2
⊢ ;;869 ∈ ℕ0 |
14 | | 1259prm.1 |
. . 3
⊢ 𝑁 = ;;;1259 |
15 | | 1nn0 12249 |
. . . . . 6
⊢ 1 ∈
ℕ0 |
16 | | 2nn0 12250 |
. . . . . 6
⊢ 2 ∈
ℕ0 |
17 | 15, 16 | deccl 12452 |
. . . . 5
⊢ ;12 ∈
ℕ0 |
18 | | 5nn0 12253 |
. . . . 5
⊢ 5 ∈
ℕ0 |
19 | 17, 18 | deccl 12452 |
. . . 4
⊢ ;;125 ∈ ℕ0 |
20 | | 9nn 12071 |
. . . 4
⊢ 9 ∈
ℕ |
21 | 19, 20 | decnncl 12457 |
. . 3
⊢ ;;;1259
∈ ℕ |
22 | 14, 21 | eqeltri 2835 |
. 2
⊢ 𝑁 ∈ ℕ |
23 | 14 | 1259lem2 16833 |
. . 3
⊢
((2↑;34) mod 𝑁) = (;;870
mod 𝑁) |
24 | | 6p1e7 12121 |
. . . . 5
⊢ (6 + 1) =
7 |
25 | | eqid 2738 |
. . . . 5
⊢ ;86 = ;86 |
26 | 9, 10, 24, 25 | decsuc 12468 |
. . . 4
⊢ (;86 + 1) = ;87 |
27 | | eqid 2738 |
. . . 4
⊢ ;;869 = ;;869 |
28 | 11, 26, 27 | decsucc 12478 |
. . 3
⊢ (;;869 + 1) = ;;870 |
29 | 22, 6, 15, 13, 23, 28 | modsubi 16773 |
. 2
⊢
(((2↑;34) − 1)
mod 𝑁) = (;;869 mod 𝑁) |
30 | 2, 12 | deccl 12452 |
. . . 4
⊢ ;39 ∈
ℕ0 |
31 | | 0nn0 12248 |
. . . 4
⊢ 0 ∈
ℕ0 |
32 | 30, 31 | deccl 12452 |
. . 3
⊢ ;;390 ∈ ℕ0 |
33 | 9, 12 | deccl 12452 |
. . . 4
⊢ ;89 ∈
ℕ0 |
34 | 16, 15 | deccl 12452 |
. . . . . 6
⊢ ;21 ∈
ℕ0 |
35 | 15, 2 | deccl 12452 |
. . . . . . 7
⊢ ;13 ∈
ℕ0 |
36 | 34 | nn0zi 12345 |
. . . . . . . . 9
⊢ ;21 ∈ ℤ |
37 | 35 | nn0zi 12345 |
. . . . . . . . 9
⊢ ;13 ∈ ℤ |
38 | | gcdcom 16220 |
. . . . . . . . 9
⊢ ((;21 ∈ ℤ ∧ ;13 ∈ ℤ) → (;21 gcd ;13) = (;13 gcd ;21)) |
39 | 36, 37, 38 | mp2an 689 |
. . . . . . . 8
⊢ (;21 gcd ;13) = (;13 gcd ;21) |
40 | | 3nn 12052 |
. . . . . . . . . . 11
⊢ 3 ∈
ℕ |
41 | 15, 40 | decnncl 12457 |
. . . . . . . . . 10
⊢ ;13 ∈ ℕ |
42 | | 8nn 12068 |
. . . . . . . . . 10
⊢ 8 ∈
ℕ |
43 | | eqid 2738 |
. . . . . . . . . . 11
⊢ ;13 = ;13 |
44 | 9 | dec0h 12459 |
. . . . . . . . . . 11
⊢ 8 = ;08 |
45 | | ax-1cn 10929 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℂ |
46 | 45 | mulid1i 10979 |
. . . . . . . . . . . . 13
⊢ (1
· 1) = 1 |
47 | 45 | addid2i 11163 |
. . . . . . . . . . . . 13
⊢ (0 + 1) =
1 |
48 | 46, 47 | oveq12i 7287 |
. . . . . . . . . . . 12
⊢ ((1
· 1) + (0 + 1)) = (1 + 1) |
49 | | 1p1e2 12098 |
. . . . . . . . . . . 12
⊢ (1 + 1) =
2 |
50 | 48, 49 | eqtri 2766 |
. . . . . . . . . . 11
⊢ ((1
· 1) + (0 + 1)) = 2 |
51 | | 3cn 12054 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℂ |
52 | 51 | mulid1i 10979 |
. . . . . . . . . . . . 13
⊢ (3
· 1) = 3 |
53 | 52 | oveq1i 7285 |
. . . . . . . . . . . 12
⊢ ((3
· 1) + 8) = (3 + 8) |
54 | | 8cn 12070 |
. . . . . . . . . . . . 13
⊢ 8 ∈
ℂ |
55 | | 8p3e11 12518 |
. . . . . . . . . . . . 13
⊢ (8 + 3) =
;11 |
56 | 54, 51, 55 | addcomli 11167 |
. . . . . . . . . . . 12
⊢ (3 + 8) =
;11 |
57 | 53, 56 | eqtri 2766 |
. . . . . . . . . . 11
⊢ ((3
· 1) + 8) = ;11 |
58 | 15, 2, 31, 9, 43, 44, 15, 15, 15, 50, 57 | decmac 12489 |
. . . . . . . . . 10
⊢ ((;13 · 1) + 8) = ;21 |
59 | | 1nn 11984 |
. . . . . . . . . . 11
⊢ 1 ∈
ℕ |
60 | | 8lt10 12569 |
. . . . . . . . . . 11
⊢ 8 <
;10 |
61 | 59, 2, 9, 60 | declti 12475 |
. . . . . . . . . 10
⊢ 8 <
;13 |
62 | 41, 15, 42, 58, 61 | ndvdsi 16121 |
. . . . . . . . 9
⊢ ¬
;13 ∥ ;21 |
63 | | 13prm 16817 |
. . . . . . . . . 10
⊢ ;13 ∈ ℙ |
64 | | coprm 16416 |
. . . . . . . . . 10
⊢ ((;13 ∈ ℙ ∧ ;21 ∈ ℤ) → (¬ ;13 ∥ ;21 ↔ (;13 gcd ;21) = 1)) |
65 | 63, 36, 64 | mp2an 689 |
. . . . . . . . 9
⊢ (¬
;13 ∥ ;21 ↔ (;13 gcd ;21) = 1) |
66 | 62, 65 | mpbi 229 |
. . . . . . . 8
⊢ (;13 gcd ;21) = 1 |
67 | 39, 66 | eqtri 2766 |
. . . . . . 7
⊢ (;21 gcd ;13) = 1 |
68 | | eqid 2738 |
. . . . . . . 8
⊢ ;21 = ;21 |
69 | | 2cn 12048 |
. . . . . . . . . . 11
⊢ 2 ∈
ℂ |
70 | 69 | mulid2i 10980 |
. . . . . . . . . 10
⊢ (1
· 2) = 2 |
71 | 45 | addid1i 11162 |
. . . . . . . . . 10
⊢ (1 + 0) =
1 |
72 | 70, 71 | oveq12i 7287 |
. . . . . . . . 9
⊢ ((1
· 2) + (1 + 0)) = (2 + 1) |
73 | | 2p1e3 12115 |
. . . . . . . . 9
⊢ (2 + 1) =
3 |
74 | 72, 73 | eqtri 2766 |
. . . . . . . 8
⊢ ((1
· 2) + (1 + 0)) = 3 |
75 | 46 | oveq1i 7285 |
. . . . . . . . 9
⊢ ((1
· 1) + 3) = (1 + 3) |
76 | | 3p1e4 12118 |
. . . . . . . . . 10
⊢ (3 + 1) =
4 |
77 | 51, 45, 76 | addcomli 11167 |
. . . . . . . . 9
⊢ (1 + 3) =
4 |
78 | 3 | dec0h 12459 |
. . . . . . . . 9
⊢ 4 = ;04 |
79 | 75, 77, 78 | 3eqtri 2770 |
. . . . . . . 8
⊢ ((1
· 1) + 3) = ;04 |
80 | 16, 15, 15, 2, 68, 43, 15, 3, 31, 74, 79 | decma2c 12490 |
. . . . . . 7
⊢ ((1
· ;21) + ;13) = ;34 |
81 | 15, 35, 34, 67, 80 | gcdi 16774 |
. . . . . 6
⊢ (;34 gcd ;21) = 1 |
82 | | eqid 2738 |
. . . . . . 7
⊢ ;34 = ;34 |
83 | | 3t2e6 12139 |
. . . . . . . . . 10
⊢ (3
· 2) = 6 |
84 | 51, 69, 83 | mulcomli 10984 |
. . . . . . . . 9
⊢ (2
· 3) = 6 |
85 | 69 | addid1i 11162 |
. . . . . . . . 9
⊢ (2 + 0) =
2 |
86 | 84, 85 | oveq12i 7287 |
. . . . . . . 8
⊢ ((2
· 3) + (2 + 0)) = (6 + 2) |
87 | | 6p2e8 12132 |
. . . . . . . 8
⊢ (6 + 2) =
8 |
88 | 86, 87 | eqtri 2766 |
. . . . . . 7
⊢ ((2
· 3) + (2 + 0)) = 8 |
89 | | 4cn 12058 |
. . . . . . . . . 10
⊢ 4 ∈
ℂ |
90 | | 4t2e8 12141 |
. . . . . . . . . 10
⊢ (4
· 2) = 8 |
91 | 89, 69, 90 | mulcomli 10984 |
. . . . . . . . 9
⊢ (2
· 4) = 8 |
92 | 91 | oveq1i 7285 |
. . . . . . . 8
⊢ ((2
· 4) + 1) = (8 + 1) |
93 | | 8p1e9 12123 |
. . . . . . . 8
⊢ (8 + 1) =
9 |
94 | 12 | dec0h 12459 |
. . . . . . . 8
⊢ 9 = ;09 |
95 | 92, 93, 94 | 3eqtri 2770 |
. . . . . . 7
⊢ ((2
· 4) + 1) = ;09 |
96 | 2, 3, 16, 15, 82, 68, 16, 12, 31, 88, 95 | decma2c 12490 |
. . . . . 6
⊢ ((2
· ;34) + ;21) = ;89 |
97 | 16, 34, 4, 81, 96 | gcdi 16774 |
. . . . 5
⊢ (;89 gcd ;34) = 1 |
98 | | eqid 2738 |
. . . . . 6
⊢ ;89 = ;89 |
99 | | 4p3e7 12127 |
. . . . . . . . 9
⊢ (4 + 3) =
7 |
100 | 89, 51, 99 | addcomli 11167 |
. . . . . . . 8
⊢ (3 + 4) =
7 |
101 | 100 | oveq2i 7286 |
. . . . . . 7
⊢ ((4
· 8) + (3 + 4)) = ((4 · 8) + 7) |
102 | | 7nn0 12255 |
. . . . . . . 8
⊢ 7 ∈
ℕ0 |
103 | | 8t4e32 12554 |
. . . . . . . . 9
⊢ (8
· 4) = ;32 |
104 | 54, 89, 103 | mulcomli 10984 |
. . . . . . . 8
⊢ (4
· 8) = ;32 |
105 | | 7cn 12067 |
. . . . . . . . 9
⊢ 7 ∈
ℂ |
106 | | 7p2e9 12134 |
. . . . . . . . 9
⊢ (7 + 2) =
9 |
107 | 105, 69, 106 | addcomli 11167 |
. . . . . . . 8
⊢ (2 + 7) =
9 |
108 | 2, 16, 102, 104, 107 | decaddi 12497 |
. . . . . . 7
⊢ ((4
· 8) + 7) = ;39 |
109 | 101, 108 | eqtri 2766 |
. . . . . 6
⊢ ((4
· 8) + (3 + 4)) = ;39 |
110 | | 9cn 12073 |
. . . . . . . 8
⊢ 9 ∈
ℂ |
111 | | 9t4e36 12561 |
. . . . . . . 8
⊢ (9
· 4) = ;36 |
112 | 110, 89, 111 | mulcomli 10984 |
. . . . . . 7
⊢ (4
· 9) = ;36 |
113 | | 6p4e10 12509 |
. . . . . . 7
⊢ (6 + 4) =
;10 |
114 | 2, 10, 3, 112, 76, 113 | decaddci2 12499 |
. . . . . 6
⊢ ((4
· 9) + 4) = ;40 |
115 | 9, 12, 2, 3, 98, 82, 3, 31, 3, 109, 114 | decma2c 12490 |
. . . . 5
⊢ ((4
· ;89) + ;34) = ;;390 |
116 | 3, 4, 33, 97, 115 | gcdi 16774 |
. . . 4
⊢ (;;390 gcd ;89) = 1 |
117 | | eqid 2738 |
. . . . 5
⊢ ;;390 = ;;390 |
118 | | eqid 2738 |
. . . . . 6
⊢ ;39 = ;39 |
119 | 54 | addid1i 11162 |
. . . . . . 7
⊢ (8 + 0) =
8 |
120 | 119, 44 | eqtri 2766 |
. . . . . 6
⊢ (8 + 0) =
;08 |
121 | 69 | addid2i 11163 |
. . . . . . . 8
⊢ (0 + 2) =
2 |
122 | 84, 121 | oveq12i 7287 |
. . . . . . 7
⊢ ((2
· 3) + (0 + 2)) = (6 + 2) |
123 | 122, 87 | eqtri 2766 |
. . . . . 6
⊢ ((2
· 3) + (0 + 2)) = 8 |
124 | | 9t2e18 12559 |
. . . . . . . 8
⊢ (9
· 2) = ;18 |
125 | 110, 69, 124 | mulcomli 10984 |
. . . . . . 7
⊢ (2
· 9) = ;18 |
126 | | 8p8e16 12523 |
. . . . . . 7
⊢ (8 + 8) =
;16 |
127 | 15, 9, 9, 125, 49, 10, 126 | decaddci 12498 |
. . . . . 6
⊢ ((2
· 9) + 8) = ;26 |
128 | 2, 12, 31, 9, 118, 120, 16, 10, 16, 123, 127 | decma2c 12490 |
. . . . 5
⊢ ((2
· ;39) + (8 + 0)) = ;86 |
129 | | 2t0e0 12142 |
. . . . . . 7
⊢ (2
· 0) = 0 |
130 | 129 | oveq1i 7285 |
. . . . . 6
⊢ ((2
· 0) + 9) = (0 + 9) |
131 | 110 | addid2i 11163 |
. . . . . 6
⊢ (0 + 9) =
9 |
132 | 130, 131,
94 | 3eqtri 2770 |
. . . . 5
⊢ ((2
· 0) + 9) = ;09 |
133 | 30, 31, 9, 12, 117, 98, 16, 12, 31, 128, 132 | decma2c 12490 |
. . . 4
⊢ ((2
· ;;390) + ;89) = ;;869 |
134 | 16, 33, 32, 116, 133 | gcdi 16774 |
. . 3
⊢ (;;869 gcd ;;390) =
1 |
135 | 30 | nn0cni 12245 |
. . . . . . 7
⊢ ;39 ∈ ℂ |
136 | 135 | addid1i 11162 |
. . . . . 6
⊢ (;39 + 0) = ;39 |
137 | 54 | mulid2i 10980 |
. . . . . . . 8
⊢ (1
· 8) = 8 |
138 | 137, 76 | oveq12i 7287 |
. . . . . . 7
⊢ ((1
· 8) + (3 + 1)) = (8 + 4) |
139 | | 8p4e12 12519 |
. . . . . . 7
⊢ (8 + 4) =
;12 |
140 | 138, 139 | eqtri 2766 |
. . . . . 6
⊢ ((1
· 8) + (3 + 1)) = ;12 |
141 | | 6cn 12064 |
. . . . . . . . 9
⊢ 6 ∈
ℂ |
142 | 141 | mulid2i 10980 |
. . . . . . . 8
⊢ (1
· 6) = 6 |
143 | 142 | oveq1i 7285 |
. . . . . . 7
⊢ ((1
· 6) + 9) = (6 + 9) |
144 | | 9p6e15 12528 |
. . . . . . . 8
⊢ (9 + 6) =
;15 |
145 | 110, 141,
144 | addcomli 11167 |
. . . . . . 7
⊢ (6 + 9) =
;15 |
146 | 143, 145 | eqtri 2766 |
. . . . . 6
⊢ ((1
· 6) + 9) = ;15 |
147 | 9, 10, 2, 12, 25, 136, 15, 18, 15, 140, 146 | decma2c 12490 |
. . . . 5
⊢ ((1
· ;86) + (;39 + 0)) = ;;125 |
148 | 110 | mulid2i 10980 |
. . . . . . 7
⊢ (1
· 9) = 9 |
149 | 148 | oveq1i 7285 |
. . . . . 6
⊢ ((1
· 9) + 0) = (9 + 0) |
150 | 110 | addid1i 11162 |
. . . . . 6
⊢ (9 + 0) =
9 |
151 | 149, 150,
94 | 3eqtri 2770 |
. . . . 5
⊢ ((1
· 9) + 0) = ;09 |
152 | 11, 12, 30, 31, 27, 117, 15, 12, 31, 147, 151 | decma2c 12490 |
. . . 4
⊢ ((1
· ;;869) + ;;390) =
;;;1259 |
153 | 152, 14 | eqtr4i 2769 |
. . 3
⊢ ((1
· ;;869) + ;;390) =
𝑁 |
154 | 15, 32, 13, 134, 153 | gcdi 16774 |
. 2
⊢ (𝑁 gcd ;;869) =
1 |
155 | 8, 13, 22, 29, 154 | gcdmodi 16775 |
1
⊢
(((2↑;34) − 1)
gcd 𝑁) = 1 |