MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1259lem4 Structured version   Visualization version   GIF version

Theorem 1259lem4 16048
Description: Lemma for 1259prm 16050. Calculate a power mod. In decimal, we calculate 2↑306 = (2↑76)↑4 · 4≡5↑4 · 4 = 2𝑁 − 18, 2↑612 = (2↑306)↑2≡18↑2 = 324, 2↑629 = 2↑612 · 2↑17≡324 · 136 = 35𝑁 − 1 and finally 2↑(𝑁 − 1) = (2↑629)↑2≡1↑2 = 1. (Contributed by Mario Carneiro, 22-Feb-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
Hypothesis
Ref Expression
1259prm.1 𝑁 = 1259
Assertion
Ref Expression
1259lem4 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)

Proof of Theorem 1259lem4
StepHypRef Expression
1 2nn 11387 . 2 2 ∈ ℕ
2 6nn0 11515 . . . 4 6 ∈ ℕ0
3 2nn0 11511 . . . 4 2 ∈ ℕ0
42, 3deccl 11714 . . 3 62 ∈ ℕ0
5 9nn0 11518 . . 3 9 ∈ ℕ0
64, 5deccl 11714 . 2 629 ∈ ℕ0
7 0z 11590 . 2 0 ∈ ℤ
8 1nn 11233 . 2 1 ∈ ℕ
9 1nn0 11510 . 2 1 ∈ ℕ0
109, 3deccl 11714 . . . . . . 7 12 ∈ ℕ0
11 5nn0 11514 . . . . . . 7 5 ∈ ℕ0
1210, 11deccl 11714 . . . . . 6 125 ∈ ℕ0
13 8nn0 11517 . . . . . 6 8 ∈ ℕ0
1412, 13deccl 11714 . . . . 5 1258 ∈ ℕ0
1514nn0cni 11506 . . . 4 1258 ∈ ℂ
16 ax-1cn 10196 . . . 4 1 ∈ ℂ
17 1259prm.1 . . . . 5 𝑁 = 1259
18 8p1e9 11360 . . . . . 6 (8 + 1) = 9
19 eqid 2771 . . . . . 6 1258 = 1258
2012, 13, 18, 19decsuc 11737 . . . . 5 (1258 + 1) = 1259
2117, 20eqtr4i 2796 . . . 4 𝑁 = (1258 + 1)
2215, 16, 21mvrraddi 10500 . . 3 (𝑁 − 1) = 1258
2322, 14eqeltri 2846 . 2 (𝑁 − 1) ∈ ℕ0
24 9nn 11394 . . . . 5 9 ∈ ℕ
2512, 24decnncl 11720 . . . 4 1259 ∈ ℕ
2617, 25eqeltri 2846 . . 3 𝑁 ∈ ℕ
272, 9deccl 11714 . . . 4 61 ∈ ℕ0
2827, 3deccl 11714 . . 3 612 ∈ ℕ0
29 3nn0 11512 . . . . 5 3 ∈ ℕ0
30 4nn0 11513 . . . . 5 4 ∈ ℕ0
3129, 30deccl 11714 . . . 4 34 ∈ ℕ0
3231nn0zi 11604 . . 3 34 ∈ ℤ
3329, 3deccl 11714 . . . 4 32 ∈ ℕ0
3433, 30deccl 11714 . . 3 324 ∈ ℕ0
35 7nn0 11516 . . . 4 7 ∈ ℕ0
369, 35deccl 11714 . . 3 17 ∈ ℕ0
379, 29deccl 11714 . . . 4 13 ∈ ℕ0
3837, 2deccl 11714 . . 3 136 ∈ ℕ0
39 0nn0 11509 . . . . . 6 0 ∈ ℕ0
4029, 39deccl 11714 . . . . 5 30 ∈ ℕ0
4140, 2deccl 11714 . . . 4 306 ∈ ℕ0
42 8nn 11393 . . . . 5 8 ∈ ℕ
439, 42decnncl 11720 . . . 4 18 ∈ ℕ
4410, 30deccl 11714 . . . . 5 124 ∈ ℕ0
4544, 9deccl 11714 . . . 4 1241 ∈ ℕ0
469, 11deccl 11714 . . . . . 6 15 ∈ ℕ0
4746, 29deccl 11714 . . . . 5 153 ∈ ℕ0
48 1z 11609 . . . . 5 1 ∈ ℤ
4911, 39deccl 11714 . . . . 5 50 ∈ ℕ0
5046, 3deccl 11714 . . . . . 6 152 ∈ ℕ0
513, 11deccl 11714 . . . . . 6 25 ∈ ℕ0
5235, 2deccl 11714 . . . . . . 7 76 ∈ ℕ0
53171259lem3 16047 . . . . . . 7 ((2↑76) mod 𝑁) = (5 mod 𝑁)
54 eqid 2771 . . . . . . . 8 76 = 76
55 4p1e5 11356 . . . . . . . . 9 (4 + 1) = 5
56 7cn 11306 . . . . . . . . . 10 7 ∈ ℂ
57 2cn 11293 . . . . . . . . . 10 2 ∈ ℂ
58 7t2e14 11849 . . . . . . . . . 10 (7 · 2) = 14
5956, 57, 58mulcomli 10249 . . . . . . . . 9 (2 · 7) = 14
609, 30, 55, 59decsuc 11737 . . . . . . . 8 ((2 · 7) + 1) = 15
61 6cn 11304 . . . . . . . . 9 6 ∈ ℂ
62 6t2e12 11842 . . . . . . . . 9 (6 · 2) = 12
6361, 57, 62mulcomli 10249 . . . . . . . 8 (2 · 6) = 12
643, 35, 2, 54, 3, 9, 60, 63decmul2c 11790 . . . . . . 7 (2 · 76) = 152
6551nn0cni 11506 . . . . . . . . 9 25 ∈ ℂ
6665addid2i 10426 . . . . . . . 8 (0 + 25) = 25
6726nncni 11232 . . . . . . . . . 10 𝑁 ∈ ℂ
6867mul02i 10427 . . . . . . . . 9 (0 · 𝑁) = 0
6968oveq1i 6803 . . . . . . . 8 ((0 · 𝑁) + 25) = (0 + 25)
70 5t5e25 11840 . . . . . . . 8 (5 · 5) = 25
7166, 69, 703eqtr4i 2803 . . . . . . 7 ((0 · 𝑁) + 25) = (5 · 5)
7226, 1, 52, 7, 11, 51, 53, 64, 71mod2xi 15980 . . . . . 6 ((2↑152) mod 𝑁) = (25 mod 𝑁)
73 2p1e3 11353 . . . . . . 7 (2 + 1) = 3
74 eqid 2771 . . . . . . 7 152 = 152
7546, 3, 73, 74decsuc 11737 . . . . . 6 (152 + 1) = 153
7649nn0cni 11506 . . . . . . . 8 50 ∈ ℂ
7776addid2i 10426 . . . . . . 7 (0 + 50) = 50
7868oveq1i 6803 . . . . . . 7 ((0 · 𝑁) + 50) = (0 + 50)
79 eqid 2771 . . . . . . . 8 25 = 25
80 2t2e4 11379 . . . . . . . . . 10 (2 · 2) = 4
8180oveq1i 6803 . . . . . . . . 9 ((2 · 2) + 1) = (4 + 1)
8281, 55eqtri 2793 . . . . . . . 8 ((2 · 2) + 1) = 5
83 5t2e10 11835 . . . . . . . 8 (5 · 2) = 10
843, 3, 11, 79, 39, 9, 82, 83decmul1c 11788 . . . . . . 7 (25 · 2) = 50
8577, 78, 843eqtr4i 2803 . . . . . 6 ((0 · 𝑁) + 50) = (25 · 2)
8626, 1, 50, 7, 51, 49, 72, 75, 85modxp1i 15981 . . . . 5 ((2↑153) mod 𝑁) = (50 mod 𝑁)
87 eqid 2771 . . . . . 6 153 = 153
88 eqid 2771 . . . . . . . . 9 15 = 15
8957mulid1i 10244 . . . . . . . . . . 11 (2 · 1) = 2
9089oveq1i 6803 . . . . . . . . . 10 ((2 · 1) + 1) = (2 + 1)
9190, 73eqtri 2793 . . . . . . . . 9 ((2 · 1) + 1) = 3
92 5cn 11302 . . . . . . . . . 10 5 ∈ ℂ
9392, 57, 83mulcomli 10249 . . . . . . . . 9 (2 · 5) = 10
943, 9, 11, 88, 39, 9, 91, 93decmul2c 11790 . . . . . . . 8 (2 · 15) = 30
9594oveq1i 6803 . . . . . . 7 ((2 · 15) + 0) = (30 + 0)
9640nn0cni 11506 . . . . . . . 8 30 ∈ ℂ
9796addid1i 10425 . . . . . . 7 (30 + 0) = 30
9895, 97eqtri 2793 . . . . . 6 ((2 · 15) + 0) = 30
99 3cn 11297 . . . . . . . 8 3 ∈ ℂ
100 3t2e6 11381 . . . . . . . 8 (3 · 2) = 6
10199, 57, 100mulcomli 10249 . . . . . . 7 (2 · 3) = 6
1022dec0h 11724 . . . . . . 7 6 = 06
103101, 102eqtri 2793 . . . . . 6 (2 · 3) = 06
1043, 46, 29, 87, 2, 39, 98, 103decmul2c 11790 . . . . 5 (2 · 153) = 306
10567mulid2i 10245 . . . . . . . 8 (1 · 𝑁) = 𝑁
106105, 17eqtri 2793 . . . . . . 7 (1 · 𝑁) = 1259
107 eqid 2771 . . . . . . 7 1241 = 1241
1083, 30deccl 11714 . . . . . . . 8 24 ∈ ℕ0
109 eqid 2771 . . . . . . . . 9 24 = 24
1103, 30, 55, 109decsuc 11737 . . . . . . . 8 (24 + 1) = 25
111 eqid 2771 . . . . . . . . 9 125 = 125
112 eqid 2771 . . . . . . . . 9 124 = 124
113 eqid 2771 . . . . . . . . . 10 12 = 12
114 1p1e2 11336 . . . . . . . . . 10 (1 + 1) = 2
115 2p2e4 11346 . . . . . . . . . 10 (2 + 2) = 4
1169, 3, 9, 3, 113, 113, 114, 115decadd 11771 . . . . . . . . 9 (12 + 12) = 24
117 5p4e9 11369 . . . . . . . . 9 (5 + 4) = 9
11810, 11, 10, 30, 111, 112, 116, 117decadd 11771 . . . . . . . 8 (125 + 124) = 249
119108, 110, 118decsucc 11752 . . . . . . 7 ((125 + 124) + 1) = 250
120 9p1e10 11698 . . . . . . 7 (9 + 1) = 10
12112, 5, 44, 9, 106, 107, 119, 120decaddc2 11776 . . . . . 6 ((1 · 𝑁) + 1241) = 2500
122 eqid 2771 . . . . . . 7 50 = 50
12392mul02i 10427 . . . . . . . . . 10 (0 · 5) = 0
12411, 11, 39, 122, 39, 70, 123decmul1 11786 . . . . . . . . 9 (50 · 5) = 250
125124oveq1i 6803 . . . . . . . 8 ((50 · 5) + 0) = (250 + 0)
12651, 39deccl 11714 . . . . . . . . . 10 250 ∈ ℕ0
127126nn0cni 11506 . . . . . . . . 9 250 ∈ ℂ
128127addid1i 10425 . . . . . . . 8 (250 + 0) = 250
129125, 128eqtri 2793 . . . . . . 7 ((50 · 5) + 0) = 250
13076mul01i 10428 . . . . . . . 8 (50 · 0) = 0
13139dec0h 11724 . . . . . . . 8 0 = 00
132130, 131eqtri 2793 . . . . . . 7 (50 · 0) = 00
13349, 11, 39, 122, 39, 39, 129, 132decmul2c 11790 . . . . . 6 (50 · 50) = 2500
134121, 133eqtr4i 2796 . . . . 5 ((1 · 𝑁) + 1241) = (50 · 50)
13526, 1, 47, 48, 49, 45, 86, 104, 134mod2xi 15980 . . . 4 ((2↑306) mod 𝑁) = (1241 mod 𝑁)
136 eqid 2771 . . . . 5 306 = 306
137 eqid 2771 . . . . . 6 30 = 30
1389dec0h 11724 . . . . . 6 1 = 01
139 00id 10413 . . . . . . . 8 (0 + 0) = 0
140101, 139oveq12i 6805 . . . . . . 7 ((2 · 3) + (0 + 0)) = (6 + 0)
14161addid1i 10425 . . . . . . 7 (6 + 0) = 6
142140, 141eqtri 2793 . . . . . 6 ((2 · 3) + (0 + 0)) = 6
14357mul01i 10428 . . . . . . . 8 (2 · 0) = 0
144143oveq1i 6803 . . . . . . 7 ((2 · 0) + 1) = (0 + 1)
145 0p1e1 11334 . . . . . . 7 (0 + 1) = 1
146144, 145, 1383eqtri 2797 . . . . . 6 ((2 · 0) + 1) = 01
14729, 39, 39, 9, 137, 138, 3, 9, 39, 142, 146decma2c 11769 . . . . 5 ((2 · 30) + 1) = 61
1483, 40, 2, 136, 3, 9, 147, 63decmul2c 11790 . . . 4 (2 · 306) = 612
149 eqid 2771 . . . . . 6 18 = 18
15010, 30, 55, 112decsuc 11737 . . . . . 6 (124 + 1) = 125
151 8cn 11308 . . . . . . 7 8 ∈ ℂ
152151, 16, 18addcomli 10430 . . . . . 6 (1 + 8) = 9
15344, 9, 9, 13, 107, 149, 150, 152decadd 11771 . . . . 5 (1241 + 18) = 1259
154153, 17eqtr4i 2796 . . . 4 (1241 + 18) = 𝑁
15534nn0cni 11506 . . . . . 6 324 ∈ ℂ
156155addid2i 10426 . . . . 5 (0 + 324) = 324
15768oveq1i 6803 . . . . 5 ((0 · 𝑁) + 324) = (0 + 324)
1589, 13deccl 11714 . . . . . 6 18 ∈ ℕ0
1599, 30deccl 11714 . . . . . 6 14 ∈ ℕ0
160 eqid 2771 . . . . . . 7 14 = 14
16116mulid1i 10244 . . . . . . . . 9 (1 · 1) = 1
162161, 114oveq12i 6805 . . . . . . . 8 ((1 · 1) + (1 + 1)) = (1 + 2)
163 1p2e3 11354 . . . . . . . 8 (1 + 2) = 3
164162, 163eqtri 2793 . . . . . . 7 ((1 · 1) + (1 + 1)) = 3
165151mulid1i 10244 . . . . . . . . 9 (8 · 1) = 8
166165oveq1i 6803 . . . . . . . 8 ((8 · 1) + 4) = (8 + 4)
167 8p4e12 11815 . . . . . . . 8 (8 + 4) = 12
168166, 167eqtri 2793 . . . . . . 7 ((8 · 1) + 4) = 12
1699, 13, 9, 30, 149, 160, 9, 3, 9, 164, 168decmac 11767 . . . . . 6 ((18 · 1) + 14) = 32
170151mulid2i 10245 . . . . . . . . 9 (1 · 8) = 8
171170oveq1i 6803 . . . . . . . 8 ((1 · 8) + 6) = (8 + 6)
172 8p6e14 11817 . . . . . . . 8 (8 + 6) = 14
173171, 172eqtri 2793 . . . . . . 7 ((1 · 8) + 6) = 14
174 8t8e64 11863 . . . . . . 7 (8 · 8) = 64
17513, 9, 13, 149, 30, 2, 173, 174decmul1c 11788 . . . . . 6 (18 · 8) = 144
176158, 9, 13, 149, 30, 159, 169, 175decmul2c 11790 . . . . 5 (18 · 18) = 324
177156, 157, 1763eqtr4i 2803 . . . 4 ((0 · 𝑁) + 324) = (18 · 18)
1781, 41, 7, 43, 34, 45, 135, 148, 154, 177mod2xnegi 15982 . . 3 ((2↑612) mod 𝑁) = (324 mod 𝑁)
179171259lem1 16045 . . 3 ((2↑17) mod 𝑁) = (136 mod 𝑁)
180 eqid 2771 . . . 4 612 = 612
181 eqid 2771 . . . 4 17 = 17
182 eqid 2771 . . . . 5 61 = 61
1832, 9, 114, 182decsuc 11737 . . . 4 (61 + 1) = 62
184 7p2e9 11374 . . . . 5 (7 + 2) = 9
18556, 57, 184addcomli 10430 . . . 4 (2 + 7) = 9
18627, 3, 9, 35, 180, 181, 183, 185decadd 11771 . . 3 (612 + 17) = 629
18729, 9deccl 11714 . . . . 5 31 ∈ ℕ0
188 eqid 2771 . . . . . . 7 31 = 31
189 3p2e5 11362 . . . . . . . . 9 (3 + 2) = 5
19099, 57, 189addcomli 10430 . . . . . . . 8 (2 + 3) = 5
1919, 3, 29, 113, 190decaddi 11780 . . . . . . 7 (12 + 3) = 15
192 5p1e6 11357 . . . . . . 7 (5 + 1) = 6
19310, 11, 29, 9, 111, 188, 191, 192decadd 11771 . . . . . 6 (125 + 31) = 156
194114oveq1i 6803 . . . . . . . . 9 ((1 + 1) + 1) = (2 + 1)
195194, 73eqtri 2793 . . . . . . . 8 ((1 + 1) + 1) = 3
196 7p5e12 11808 . . . . . . . . 9 (7 + 5) = 12
19756, 92, 196addcomli 10430 . . . . . . . 8 (5 + 7) = 12
1989, 11, 9, 35, 88, 181, 195, 3, 197decaddc 11773 . . . . . . 7 (15 + 17) = 32
199 eqid 2771 . . . . . . . 8 34 = 34
200 7p3e10 11804 . . . . . . . . 9 (7 + 3) = 10
20156, 99, 200addcomli 10430 . . . . . . . 8 (3 + 7) = 10
20299mulid1i 10244 . . . . . . . . . 10 (3 · 1) = 3
20316addid1i 10425 . . . . . . . . . 10 (1 + 0) = 1
204202, 203oveq12i 6805 . . . . . . . . 9 ((3 · 1) + (1 + 0)) = (3 + 1)
205 3p1e4 11355 . . . . . . . . 9 (3 + 1) = 4
206204, 205eqtri 2793 . . . . . . . 8 ((3 · 1) + (1 + 0)) = 4
207 4cn 11300 . . . . . . . . . . 11 4 ∈ ℂ
208207mulid1i 10244 . . . . . . . . . 10 (4 · 1) = 4
209208oveq1i 6803 . . . . . . . . 9 ((4 · 1) + 0) = (4 + 0)
210207addid1i 10425 . . . . . . . . 9 (4 + 0) = 4
21130dec0h 11724 . . . . . . . . 9 4 = 04
212209, 210, 2113eqtri 2797 . . . . . . . 8 ((4 · 1) + 0) = 04
21329, 30, 9, 39, 199, 201, 9, 30, 39, 206, 212decmac 11767 . . . . . . 7 ((34 · 1) + (3 + 7)) = 44
2143dec0h 11724 . . . . . . . 8 2 = 02
215100, 145oveq12i 6805 . . . . . . . . 9 ((3 · 2) + (0 + 1)) = (6 + 1)
216 6p1e7 11358 . . . . . . . . 9 (6 + 1) = 7
217215, 216eqtri 2793 . . . . . . . 8 ((3 · 2) + (0 + 1)) = 7
218 4t2e8 11383 . . . . . . . . . 10 (4 · 2) = 8
219218oveq1i 6803 . . . . . . . . 9 ((4 · 2) + 2) = (8 + 2)
220 8p2e10 11811 . . . . . . . . 9 (8 + 2) = 10
221219, 220eqtri 2793 . . . . . . . 8 ((4 · 2) + 2) = 10
22229, 30, 39, 3, 199, 214, 3, 39, 9, 217, 221decmac 11767 . . . . . . 7 ((34 · 2) + 2) = 70
2239, 3, 29, 3, 113, 198, 31, 39, 35, 213, 222decma2c 11769 . . . . . 6 ((34 · 12) + (15 + 17)) = 440
224 5t3e15 11836 . . . . . . . . 9 (5 · 3) = 15
22592, 99, 224mulcomli 10249 . . . . . . . 8 (3 · 5) = 15
226 5p2e7 11367 . . . . . . . 8 (5 + 2) = 7
2279, 11, 3, 225, 226decaddi 11780 . . . . . . 7 ((3 · 5) + 2) = 17
228 5t4e20 11838 . . . . . . . . 9 (5 · 4) = 20
22992, 207, 228mulcomli 10249 . . . . . . . 8 (4 · 5) = 20
23061addid2i 10426 . . . . . . . 8 (0 + 6) = 6
2313, 39, 2, 229, 230decaddi 11780 . . . . . . 7 ((4 · 5) + 6) = 26
23229, 30, 2, 199, 11, 2, 3, 227, 231decrmac 11778 . . . . . 6 ((34 · 5) + 6) = 176
23310, 11, 46, 2, 111, 193, 31, 2, 36, 223, 232decma2c 11769 . . . . 5 ((34 · 125) + (125 + 31)) = 4406
234 9cn 11310 . . . . . . . 8 9 ∈ ℂ
235 9t3e27 11865 . . . . . . . 8 (9 · 3) = 27
236234, 99, 235mulcomli 10249 . . . . . . 7 (3 · 9) = 27
237 7p4e11 11806 . . . . . . 7 (7 + 4) = 11
2383, 35, 30, 236, 73, 9, 237decaddci 11781 . . . . . 6 ((3 · 9) + 4) = 31
239 9t4e36 11866 . . . . . . . 8 (9 · 4) = 36
240234, 207, 239mulcomli 10249 . . . . . . 7 (4 · 9) = 36
241151, 61, 172addcomli 10430 . . . . . . 7 (6 + 8) = 14
24229, 2, 13, 240, 205, 30, 241decaddci 11781 . . . . . 6 ((4 · 9) + 8) = 44
24329, 30, 13, 199, 5, 30, 30, 238, 242decrmac 11778 . . . . 5 ((34 · 9) + 8) = 314
24412, 5, 12, 13, 17, 22, 31, 30, 187, 233, 243decma2c 11769 . . . 4 ((34 · 𝑁) + (𝑁 − 1)) = 44064
245 eqid 2771 . . . . 5 136 = 136
2469, 5deccl 11714 . . . . . 6 19 ∈ ℕ0
247246, 30deccl 11714 . . . . 5 194 ∈ ℕ0
248 eqid 2771 . . . . . 6 13 = 13
249 eqid 2771 . . . . . 6 194 = 194
2505, 35deccl 11714 . . . . . 6 97 ∈ ℕ0
2519, 9deccl 11714 . . . . . . 7 11 ∈ ℕ0
252 eqid 2771 . . . . . . 7 324 = 324
253 eqid 2771 . . . . . . . 8 19 = 19
254 eqid 2771 . . . . . . . 8 97 = 97
255234, 16, 120addcomli 10430 . . . . . . . . 9 (1 + 9) = 10
2569, 39, 145, 255decsuc 11737 . . . . . . . 8 ((1 + 9) + 1) = 11
257 9p7e16 11826 . . . . . . . 8 (9 + 7) = 16
2589, 5, 5, 35, 253, 254, 256, 2, 257decaddc 11773 . . . . . . 7 (19 + 97) = 116
259 eqid 2771 . . . . . . . 8 32 = 32
260 eqid 2771 . . . . . . . . 9 11 = 11
2619, 9, 114, 260decsuc 11737 . . . . . . . 8 (11 + 1) = 12
26289oveq1i 6803 . . . . . . . . 9 ((2 · 1) + 2) = (2 + 2)
263262, 115, 2113eqtri 2797 . . . . . . . 8 ((2 · 1) + 2) = 04
26429, 3, 9, 3, 259, 261, 9, 30, 39, 206, 263decmac 11767 . . . . . . 7 ((32 · 1) + (11 + 1)) = 44
265208oveq1i 6803 . . . . . . . 8 ((4 · 1) + 6) = (4 + 6)
266 6p4e10 11799 . . . . . . . . 9 (6 + 4) = 10
26761, 207, 266addcomli 10430 . . . . . . . 8 (4 + 6) = 10
268265, 267eqtri 2793 . . . . . . 7 ((4 · 1) + 6) = 10
26933, 30, 251, 2, 252, 258, 9, 39, 9, 264, 268decmac 11767 . . . . . 6 ((324 · 1) + (19 + 97)) = 440
270145, 138eqtri 2793 . . . . . . . 8 (0 + 1) = 01
271 3t3e9 11382 . . . . . . . . . 10 (3 · 3) = 9
272271, 139oveq12i 6805 . . . . . . . . 9 ((3 · 3) + (0 + 0)) = (9 + 0)
273234addid1i 10425 . . . . . . . . 9 (9 + 0) = 9
274272, 273eqtri 2793 . . . . . . . 8 ((3 · 3) + (0 + 0)) = 9
275101oveq1i 6803 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
27635dec0h 11724 . . . . . . . . 9 7 = 07
277275, 216, 2763eqtri 2797 . . . . . . . 8 ((2 · 3) + 1) = 07
27829, 3, 39, 9, 259, 270, 29, 35, 39, 274, 277decmac 11767 . . . . . . 7 ((32 · 3) + (0 + 1)) = 97
279 4t3e12 11833 . . . . . . . 8 (4 · 3) = 12
280 4p2e6 11364 . . . . . . . . 9 (4 + 2) = 6
281207, 57, 280addcomli 10430 . . . . . . . 8 (2 + 4) = 6
2829, 3, 30, 279, 281decaddi 11780 . . . . . . 7 ((4 · 3) + 4) = 16
28333, 30, 39, 30, 252, 211, 29, 2, 9, 278, 282decmac 11767 . . . . . 6 ((324 · 3) + 4) = 976
2849, 29, 246, 30, 248, 249, 34, 2, 250, 269, 283decma2c 11769 . . . . 5 ((324 · 13) + 194) = 4406
285 6t3e18 11843 . . . . . . . . 9 (6 · 3) = 18
28661, 99, 285mulcomli 10249 . . . . . . . 8 (3 · 6) = 18
2879, 13, 18, 286decsuc 11737 . . . . . . 7 ((3 · 6) + 1) = 19
2889, 3, 3, 63, 115decaddi 11780 . . . . . . 7 ((2 · 6) + 2) = 14
28929, 3, 3, 259, 2, 30, 9, 287, 288decrmac 11778 . . . . . 6 ((32 · 6) + 2) = 194
290 6t4e24 11844 . . . . . . 7 (6 · 4) = 24
29161, 207, 290mulcomli 10249 . . . . . 6 (4 · 6) = 24
2922, 33, 30, 252, 30, 3, 289, 291decmul1c 11788 . . . . 5 (324 · 6) = 1944
29334, 37, 2, 245, 30, 247, 284, 292decmul2c 11790 . . . 4 (324 · 136) = 44064
294244, 293eqtr4i 2796 . . 3 ((34 · 𝑁) + (𝑁 − 1)) = (324 · 136)
29526, 1, 28, 32, 34, 23, 36, 38, 178, 179, 186, 294modxai 15979 . 2 ((2↑629) mod 𝑁) = ((𝑁 − 1) mod 𝑁)
296 eqid 2771 . . . 4 629 = 629
297 eqid 2771 . . . . 5 62 = 62
298139oveq2i 6804 . . . . . 6 ((2 · 6) + (0 + 0)) = ((2 · 6) + 0)
29963oveq1i 6803 . . . . . 6 ((2 · 6) + 0) = (12 + 0)
30010nn0cni 11506 . . . . . . 7 12 ∈ ℂ
301300addid1i 10425 . . . . . 6 (12 + 0) = 12
302298, 299, 3013eqtri 2797 . . . . 5 ((2 · 6) + (0 + 0)) = 12
30311dec0h 11724 . . . . . 6 5 = 05
30481, 55, 3033eqtri 2797 . . . . 5 ((2 · 2) + 1) = 05
3052, 3, 39, 9, 297, 138, 3, 11, 39, 302, 304decma2c 11769 . . . 4 ((2 · 62) + 1) = 125
306 9t2e18 11864 . . . . 5 (9 · 2) = 18
307234, 57, 306mulcomli 10249 . . . 4 (2 · 9) = 18
3083, 4, 5, 296, 13, 9, 305, 307decmul2c 11790 . . 3 (2 · 629) = 1258
309308, 22eqtr4i 2796 . 2 (2 · 629) = (𝑁 − 1)
310 npcan 10492 . . 3 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
31167, 16, 310mp2an 672 . 2 ((𝑁 − 1) + 1) = 𝑁
31268oveq1i 6803 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
313145, 312, 1613eqtr4i 2803 . 2 ((0 · 𝑁) + 1) = (1 · 1)
3141, 6, 7, 8, 9, 23, 295, 309, 311, 313mod2xnegi 15982 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1631  wcel 2145  (class class class)co 6793  cc 10136  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143  cmin 10468  cn 11222  2c2 11272  3c3 11273  4c4 11274  5c5 11275  6c6 11276  7c7 11277  8c8 11278  9c9 11279  0cn0 11494  cdc 11695   mod cmo 12876  cexp 13067
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215  ax-pre-sup 10216
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-sup 8504  df-inf 8505  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-div 10887  df-nn 11223  df-2 11281  df-3 11282  df-4 11283  df-5 11284  df-6 11285  df-7 11286  df-8 11287  df-9 11288  df-n0 11495  df-z 11580  df-dec 11696  df-uz 11889  df-rp 12036  df-fl 12801  df-mod 12877  df-seq 13009  df-exp 13068
This theorem is referenced by:  1259prm  16050
  Copyright terms: Public domain W3C validator