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

Theorem 1259lem4 17172
Description: Lemma for 1259prm 17174. 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 12340 . 2 2 ∈ ℕ
2 6nn0 12549 . . . 4 6 ∈ ℕ0
3 2nn0 12545 . . . 4 2 ∈ ℕ0
42, 3deccl 12750 . . 3 62 ∈ ℕ0
5 9nn0 12552 . . 3 9 ∈ ℕ0
64, 5deccl 12750 . 2 629 ∈ ℕ0
7 0z 12626 . 2 0 ∈ ℤ
8 1nn 12278 . 2 1 ∈ ℕ
9 1nn0 12544 . 2 1 ∈ ℕ0
109, 3deccl 12750 . . . . . . 7 12 ∈ ℕ0
11 5nn0 12548 . . . . . . 7 5 ∈ ℕ0
1210, 11deccl 12750 . . . . . 6 125 ∈ ℕ0
13 8nn0 12551 . . . . . 6 8 ∈ ℕ0
1412, 13deccl 12750 . . . . 5 1258 ∈ ℕ0
1514nn0cni 12540 . . . 4 1258 ∈ ℂ
16 ax-1cn 11214 . . . 4 1 ∈ ℂ
17 1259prm.1 . . . . 5 𝑁 = 1259
18 8p1e9 12417 . . . . . 6 (8 + 1) = 9
19 eqid 2736 . . . . . 6 1258 = 1258
2012, 13, 18, 19decsuc 12766 . . . . 5 (1258 + 1) = 1259
2117, 20eqtr4i 2767 . . . 4 𝑁 = (1258 + 1)
2215, 16, 21mvrraddi 11526 . . 3 (𝑁 − 1) = 1258
2322, 14eqeltri 2836 . 2 (𝑁 − 1) ∈ ℕ0
24 9nn 12365 . . . . 5 9 ∈ ℕ
2512, 24decnncl 12755 . . . 4 1259 ∈ ℕ
2617, 25eqeltri 2836 . . 3 𝑁 ∈ ℕ
272, 9deccl 12750 . . . 4 61 ∈ ℕ0
2827, 3deccl 12750 . . 3 612 ∈ ℕ0
29 3nn0 12546 . . . . 5 3 ∈ ℕ0
30 4nn0 12547 . . . . 5 4 ∈ ℕ0
3129, 30deccl 12750 . . . 4 34 ∈ ℕ0
3231nn0zi 12644 . . 3 34 ∈ ℤ
3329, 3deccl 12750 . . . 4 32 ∈ ℕ0
3433, 30deccl 12750 . . 3 324 ∈ ℕ0
35 7nn0 12550 . . . 4 7 ∈ ℕ0
369, 35deccl 12750 . . 3 17 ∈ ℕ0
379, 29deccl 12750 . . . 4 13 ∈ ℕ0
3837, 2deccl 12750 . . 3 136 ∈ ℕ0
39 0nn0 12543 . . . . . 6 0 ∈ ℕ0
4029, 39deccl 12750 . . . . 5 30 ∈ ℕ0
4140, 2deccl 12750 . . . 4 306 ∈ ℕ0
42 8nn 12362 . . . . 5 8 ∈ ℕ
439, 42decnncl 12755 . . . 4 18 ∈ ℕ
4410, 30deccl 12750 . . . . 5 124 ∈ ℕ0
4544, 9deccl 12750 . . . 4 1241 ∈ ℕ0
469, 11deccl 12750 . . . . . 6 15 ∈ ℕ0
4746, 29deccl 12750 . . . . 5 153 ∈ ℕ0
48 1z 12649 . . . . 5 1 ∈ ℤ
4911, 39deccl 12750 . . . . 5 50 ∈ ℕ0
5046, 3deccl 12750 . . . . . 6 152 ∈ ℕ0
513, 11deccl 12750 . . . . . 6 25 ∈ ℕ0
5235, 2deccl 12750 . . . . . . 7 76 ∈ ℕ0
53171259lem3 17171 . . . . . . 7 ((2↑76) mod 𝑁) = (5 mod 𝑁)
54 eqid 2736 . . . . . . . 8 76 = 76
55 4p1e5 12413 . . . . . . . . 9 (4 + 1) = 5
56 7cn 12361 . . . . . . . . . 10 7 ∈ ℂ
57 2cn 12342 . . . . . . . . . 10 2 ∈ ℂ
58 7t2e14 12844 . . . . . . . . . 10 (7 · 2) = 14
5956, 57, 58mulcomli 11271 . . . . . . . . 9 (2 · 7) = 14
609, 30, 55, 59decsuc 12766 . . . . . . . 8 ((2 · 7) + 1) = 15
61 6cn 12358 . . . . . . . . 9 6 ∈ ℂ
62 6t2e12 12839 . . . . . . . . 9 (6 · 2) = 12
6361, 57, 62mulcomli 11271 . . . . . . . 8 (2 · 6) = 12
643, 35, 2, 54, 3, 9, 60, 63decmul2c 12801 . . . . . . 7 (2 · 76) = 152
6551nn0cni 12540 . . . . . . . . 9 25 ∈ ℂ
6665addlidi 11450 . . . . . . . 8 (0 + 25) = 25
6726nncni 12277 . . . . . . . . . 10 𝑁 ∈ ℂ
6867mul02i 11451 . . . . . . . . 9 (0 · 𝑁) = 0
6968oveq1i 7442 . . . . . . . 8 ((0 · 𝑁) + 25) = (0 + 25)
70 5t5e25 12838 . . . . . . . 8 (5 · 5) = 25
7166, 69, 703eqtr4i 2774 . . . . . . 7 ((0 · 𝑁) + 25) = (5 · 5)
7226, 1, 52, 7, 11, 51, 53, 64, 71mod2xi 17108 . . . . . 6 ((2↑152) mod 𝑁) = (25 mod 𝑁)
73 2p1e3 12409 . . . . . . 7 (2 + 1) = 3
74 eqid 2736 . . . . . . 7 152 = 152
7546, 3, 73, 74decsuc 12766 . . . . . 6 (152 + 1) = 153
7649nn0cni 12540 . . . . . . . 8 50 ∈ ℂ
7776addlidi 11450 . . . . . . 7 (0 + 50) = 50
7868oveq1i 7442 . . . . . . 7 ((0 · 𝑁) + 50) = (0 + 50)
79 eqid 2736 . . . . . . . 8 25 = 25
80 2t2e4 12431 . . . . . . . . . 10 (2 · 2) = 4
8180oveq1i 7442 . . . . . . . . 9 ((2 · 2) + 1) = (4 + 1)
8281, 55eqtri 2764 . . . . . . . 8 ((2 · 2) + 1) = 5
83 5t2e10 12835 . . . . . . . 8 (5 · 2) = 10
843, 3, 11, 79, 39, 9, 82, 83decmul1c 12800 . . . . . . 7 (25 · 2) = 50
8577, 78, 843eqtr4i 2774 . . . . . 6 ((0 · 𝑁) + 50) = (25 · 2)
8626, 1, 50, 7, 51, 49, 72, 75, 85modxp1i 17109 . . . . 5 ((2↑153) mod 𝑁) = (50 mod 𝑁)
87 eqid 2736 . . . . . 6 153 = 153
88 eqid 2736 . . . . . . . . 9 15 = 15
8957mulridi 11266 . . . . . . . . . . 11 (2 · 1) = 2
9089oveq1i 7442 . . . . . . . . . 10 ((2 · 1) + 1) = (2 + 1)
9190, 73eqtri 2764 . . . . . . . . 9 ((2 · 1) + 1) = 3
92 5cn 12355 . . . . . . . . . 10 5 ∈ ℂ
9392, 57, 83mulcomli 11271 . . . . . . . . 9 (2 · 5) = 10
943, 9, 11, 88, 39, 9, 91, 93decmul2c 12801 . . . . . . . 8 (2 · 15) = 30
9594oveq1i 7442 . . . . . . 7 ((2 · 15) + 0) = (30 + 0)
9640nn0cni 12540 . . . . . . . 8 30 ∈ ℂ
9796addridi 11449 . . . . . . 7 (30 + 0) = 30
9895, 97eqtri 2764 . . . . . 6 ((2 · 15) + 0) = 30
99 3cn 12348 . . . . . . . 8 3 ∈ ℂ
100 3t2e6 12433 . . . . . . . 8 (3 · 2) = 6
10199, 57, 100mulcomli 11271 . . . . . . 7 (2 · 3) = 6
1022dec0h 12757 . . . . . . 7 6 = 06
103101, 102eqtri 2764 . . . . . 6 (2 · 3) = 06
1043, 46, 29, 87, 2, 39, 98, 103decmul2c 12801 . . . . 5 (2 · 153) = 306
10567mullidi 11267 . . . . . . . 8 (1 · 𝑁) = 𝑁
106105, 17eqtri 2764 . . . . . . 7 (1 · 𝑁) = 1259
107 eqid 2736 . . . . . . 7 1241 = 1241
1083, 30deccl 12750 . . . . . . . 8 24 ∈ ℕ0
109 eqid 2736 . . . . . . . . 9 24 = 24
1103, 30, 55, 109decsuc 12766 . . . . . . . 8 (24 + 1) = 25
111 eqid 2736 . . . . . . . . 9 125 = 125
112 eqid 2736 . . . . . . . . 9 124 = 124
113 eqid 2736 . . . . . . . . . 10 12 = 12
114 1p1e2 12392 . . . . . . . . . 10 (1 + 1) = 2
115 2p2e4 12402 . . . . . . . . . 10 (2 + 2) = 4
1169, 3, 9, 3, 113, 113, 114, 115decadd 12789 . . . . . . . . 9 (12 + 12) = 24
117 5p4e9 12425 . . . . . . . . 9 (5 + 4) = 9
11810, 11, 10, 30, 111, 112, 116, 117decadd 12789 . . . . . . . 8 (125 + 124) = 249
119108, 110, 118decsucc 12776 . . . . . . 7 ((125 + 124) + 1) = 250
120 9p1e10 12737 . . . . . . 7 (9 + 1) = 10
12112, 5, 44, 9, 106, 107, 119, 120decaddc2 12791 . . . . . 6 ((1 · 𝑁) + 1241) = 2500
122 eqid 2736 . . . . . . 7 50 = 50
12392mul02i 11451 . . . . . . . . . 10 (0 · 5) = 0
12411, 11, 39, 122, 70, 123decmul1 12799 . . . . . . . . 9 (50 · 5) = 250
125124oveq1i 7442 . . . . . . . 8 ((50 · 5) + 0) = (250 + 0)
12651, 39deccl 12750 . . . . . . . . . 10 250 ∈ ℕ0
127126nn0cni 12540 . . . . . . . . 9 250 ∈ ℂ
128127addridi 11449 . . . . . . . 8 (250 + 0) = 250
129125, 128eqtri 2764 . . . . . . 7 ((50 · 5) + 0) = 250
13076mul01i 11452 . . . . . . . 8 (50 · 0) = 0
13139dec0h 12757 . . . . . . . 8 0 = 00
132130, 131eqtri 2764 . . . . . . 7 (50 · 0) = 00
13349, 11, 39, 122, 39, 39, 129, 132decmul2c 12801 . . . . . 6 (50 · 50) = 2500
134121, 133eqtr4i 2767 . . . . 5 ((1 · 𝑁) + 1241) = (50 · 50)
13526, 1, 47, 48, 49, 45, 86, 104, 134mod2xi 17108 . . . 4 ((2↑306) mod 𝑁) = (1241 mod 𝑁)
136 eqid 2736 . . . . 5 306 = 306
137 eqid 2736 . . . . . 6 30 = 30
1389dec0h 12757 . . . . . 6 1 = 01
139 00id 11437 . . . . . . . 8 (0 + 0) = 0
140101, 139oveq12i 7444 . . . . . . 7 ((2 · 3) + (0 + 0)) = (6 + 0)
14161addridi 11449 . . . . . . 7 (6 + 0) = 6
142140, 141eqtri 2764 . . . . . 6 ((2 · 3) + (0 + 0)) = 6
14357mul01i 11452 . . . . . . . 8 (2 · 0) = 0
144143oveq1i 7442 . . . . . . 7 ((2 · 0) + 1) = (0 + 1)
145 0p1e1 12389 . . . . . . 7 (0 + 1) = 1
146144, 145, 1383eqtri 2768 . . . . . 6 ((2 · 0) + 1) = 01
14729, 39, 39, 9, 137, 138, 3, 9, 39, 142, 146decma2c 12788 . . . . 5 ((2 · 30) + 1) = 61
1483, 40, 2, 136, 3, 9, 147, 63decmul2c 12801 . . . 4 (2 · 306) = 612
149 eqid 2736 . . . . . 6 18 = 18
15010, 30, 55, 112decsuc 12766 . . . . . 6 (124 + 1) = 125
151 8cn 12364 . . . . . . 7 8 ∈ ℂ
152151, 16, 18addcomli 11454 . . . . . 6 (1 + 8) = 9
15344, 9, 9, 13, 107, 149, 150, 152decadd 12789 . . . . 5 (1241 + 18) = 1259
154153, 17eqtr4i 2767 . . . 4 (1241 + 18) = 𝑁
15534nn0cni 12540 . . . . . 6 324 ∈ ℂ
156155addlidi 11450 . . . . 5 (0 + 324) = 324
15768oveq1i 7442 . . . . 5 ((0 · 𝑁) + 324) = (0 + 324)
1589, 13deccl 12750 . . . . . 6 18 ∈ ℕ0
1599, 30deccl 12750 . . . . . 6 14 ∈ ℕ0
160 eqid 2736 . . . . . . 7 14 = 14
16116mulridi 11266 . . . . . . . . 9 (1 · 1) = 1
162161, 114oveq12i 7444 . . . . . . . 8 ((1 · 1) + (1 + 1)) = (1 + 2)
163 1p2e3 12410 . . . . . . . 8 (1 + 2) = 3
164162, 163eqtri 2764 . . . . . . 7 ((1 · 1) + (1 + 1)) = 3
165151mulridi 11266 . . . . . . . . 9 (8 · 1) = 8
166165oveq1i 7442 . . . . . . . 8 ((8 · 1) + 4) = (8 + 4)
167 8p4e12 12817 . . . . . . . 8 (8 + 4) = 12
168166, 167eqtri 2764 . . . . . . 7 ((8 · 1) + 4) = 12
1699, 13, 9, 30, 149, 160, 9, 3, 9, 164, 168decmac 12787 . . . . . 6 ((18 · 1) + 14) = 32
170151mullidi 11267 . . . . . . . . 9 (1 · 8) = 8
171170oveq1i 7442 . . . . . . . 8 ((1 · 8) + 6) = (8 + 6)
172 8p6e14 12819 . . . . . . . 8 (8 + 6) = 14
173171, 172eqtri 2764 . . . . . . 7 ((1 · 8) + 6) = 14
174 8t8e64 12856 . . . . . . 7 (8 · 8) = 64
17513, 9, 13, 149, 30, 2, 173, 174decmul1c 12800 . . . . . 6 (18 · 8) = 144
176158, 9, 13, 149, 30, 159, 169, 175decmul2c 12801 . . . . 5 (18 · 18) = 324
177156, 157, 1763eqtr4i 2774 . . . 4 ((0 · 𝑁) + 324) = (18 · 18)
1781, 41, 7, 43, 34, 45, 135, 148, 154, 177mod2xnegi 17110 . . 3 ((2↑612) mod 𝑁) = (324 mod 𝑁)
179171259lem1 17169 . . 3 ((2↑17) mod 𝑁) = (136 mod 𝑁)
180 eqid 2736 . . . 4 612 = 612
181 eqid 2736 . . . 4 17 = 17
182 eqid 2736 . . . . 5 61 = 61
1832, 9, 114, 182decsuc 12766 . . . 4 (61 + 1) = 62
184 7p2e9 12428 . . . . 5 (7 + 2) = 9
18556, 57, 184addcomli 11454 . . . 4 (2 + 7) = 9
18627, 3, 9, 35, 180, 181, 183, 185decadd 12789 . . 3 (612 + 17) = 629
18729, 9deccl 12750 . . . . 5 31 ∈ ℕ0
188 eqid 2736 . . . . . . 7 31 = 31
189 3p2e5 12418 . . . . . . . . 9 (3 + 2) = 5
19099, 57, 189addcomli 11454 . . . . . . . 8 (2 + 3) = 5
1919, 3, 29, 113, 190decaddi 12795 . . . . . . 7 (12 + 3) = 15
192 5p1e6 12414 . . . . . . 7 (5 + 1) = 6
19310, 11, 29, 9, 111, 188, 191, 192decadd 12789 . . . . . 6 (125 + 31) = 156
194114oveq1i 7442 . . . . . . . . 9 ((1 + 1) + 1) = (2 + 1)
195194, 73eqtri 2764 . . . . . . . 8 ((1 + 1) + 1) = 3
196 7p5e12 12812 . . . . . . . . 9 (7 + 5) = 12
19756, 92, 196addcomli 11454 . . . . . . . 8 (5 + 7) = 12
1989, 11, 9, 35, 88, 181, 195, 3, 197decaddc 12790 . . . . . . 7 (15 + 17) = 32
199 eqid 2736 . . . . . . . 8 34 = 34
200 7p3e10 12810 . . . . . . . . 9 (7 + 3) = 10
20156, 99, 200addcomli 11454 . . . . . . . 8 (3 + 7) = 10
20299mulridi 11266 . . . . . . . . . 10 (3 · 1) = 3
20316addridi 11449 . . . . . . . . . 10 (1 + 0) = 1
204202, 203oveq12i 7444 . . . . . . . . 9 ((3 · 1) + (1 + 0)) = (3 + 1)
205 3p1e4 12412 . . . . . . . . 9 (3 + 1) = 4
206204, 205eqtri 2764 . . . . . . . 8 ((3 · 1) + (1 + 0)) = 4
207 4cn 12352 . . . . . . . . . . 11 4 ∈ ℂ
208207mulridi 11266 . . . . . . . . . 10 (4 · 1) = 4
209208oveq1i 7442 . . . . . . . . 9 ((4 · 1) + 0) = (4 + 0)
210207addridi 11449 . . . . . . . . 9 (4 + 0) = 4
21130dec0h 12757 . . . . . . . . 9 4 = 04
212209, 210, 2113eqtri 2768 . . . . . . . 8 ((4 · 1) + 0) = 04
21329, 30, 9, 39, 199, 201, 9, 30, 39, 206, 212decmac 12787 . . . . . . 7 ((34 · 1) + (3 + 7)) = 44
2143dec0h 12757 . . . . . . . 8 2 = 02
215100, 145oveq12i 7444 . . . . . . . . 9 ((3 · 2) + (0 + 1)) = (6 + 1)
216 6p1e7 12415 . . . . . . . . 9 (6 + 1) = 7
217215, 216eqtri 2764 . . . . . . . 8 ((3 · 2) + (0 + 1)) = 7
218 4t2e8 12435 . . . . . . . . . 10 (4 · 2) = 8
219218oveq1i 7442 . . . . . . . . 9 ((4 · 2) + 2) = (8 + 2)
220 8p2e10 12815 . . . . . . . . 9 (8 + 2) = 10
221219, 220eqtri 2764 . . . . . . . 8 ((4 · 2) + 2) = 10
22229, 30, 39, 3, 199, 214, 3, 39, 9, 217, 221decmac 12787 . . . . . . 7 ((34 · 2) + 2) = 70
2239, 3, 29, 3, 113, 198, 31, 39, 35, 213, 222decma2c 12788 . . . . . 6 ((34 · 12) + (15 + 17)) = 440
224 5t3e15 12836 . . . . . . . . 9 (5 · 3) = 15
22592, 99, 224mulcomli 11271 . . . . . . . 8 (3 · 5) = 15
226 5p2e7 12423 . . . . . . . 8 (5 + 2) = 7
2279, 11, 3, 225, 226decaddi 12795 . . . . . . 7 ((3 · 5) + 2) = 17
228 5t4e20 12837 . . . . . . . . 9 (5 · 4) = 20
22992, 207, 228mulcomli 11271 . . . . . . . 8 (4 · 5) = 20
23061addlidi 11450 . . . . . . . 8 (0 + 6) = 6
2313, 39, 2, 229, 230decaddi 12795 . . . . . . 7 ((4 · 5) + 6) = 26
23229, 30, 2, 199, 11, 2, 3, 227, 231decrmac 12793 . . . . . 6 ((34 · 5) + 6) = 176
23310, 11, 46, 2, 111, 193, 31, 2, 36, 223, 232decma2c 12788 . . . . 5 ((34 · 125) + (125 + 31)) = 4406
234 9cn 12367 . . . . . . . 8 9 ∈ ℂ
235 9t3e27 12858 . . . . . . . 8 (9 · 3) = 27
236234, 99, 235mulcomli 11271 . . . . . . 7 (3 · 9) = 27
237 7p4e11 12811 . . . . . . 7 (7 + 4) = 11
2383, 35, 30, 236, 73, 9, 237decaddci 12796 . . . . . 6 ((3 · 9) + 4) = 31
239 9t4e36 12859 . . . . . . . 8 (9 · 4) = 36
240234, 207, 239mulcomli 11271 . . . . . . 7 (4 · 9) = 36
241151, 61, 172addcomli 11454 . . . . . . 7 (6 + 8) = 14
24229, 2, 13, 240, 205, 30, 241decaddci 12796 . . . . . 6 ((4 · 9) + 8) = 44
24329, 30, 13, 199, 5, 30, 30, 238, 242decrmac 12793 . . . . 5 ((34 · 9) + 8) = 314
24412, 5, 12, 13, 17, 22, 31, 30, 187, 233, 243decma2c 12788 . . . 4 ((34 · 𝑁) + (𝑁 − 1)) = 44064
245 eqid 2736 . . . . 5 136 = 136
2469, 5deccl 12750 . . . . . 6 19 ∈ ℕ0
247246, 30deccl 12750 . . . . 5 194 ∈ ℕ0
248 eqid 2736 . . . . . 6 13 = 13
249 eqid 2736 . . . . . 6 194 = 194
2505, 35deccl 12750 . . . . . 6 97 ∈ ℕ0
2519, 9deccl 12750 . . . . . . 7 11 ∈ ℕ0
252 eqid 2736 . . . . . . 7 324 = 324
253 eqid 2736 . . . . . . . 8 19 = 19
254 eqid 2736 . . . . . . . 8 97 = 97
255234, 16, 120addcomli 11454 . . . . . . . . 9 (1 + 9) = 10
2569, 39, 145, 255decsuc 12766 . . . . . . . 8 ((1 + 9) + 1) = 11
257 9p7e16 12827 . . . . . . . 8 (9 + 7) = 16
2589, 5, 5, 35, 253, 254, 256, 2, 257decaddc 12790 . . . . . . 7 (19 + 97) = 116
259 eqid 2736 . . . . . . . 8 32 = 32
260 eqid 2736 . . . . . . . . 9 11 = 11
2619, 9, 114, 260decsuc 12766 . . . . . . . 8 (11 + 1) = 12
26289oveq1i 7442 . . . . . . . . 9 ((2 · 1) + 2) = (2 + 2)
263262, 115, 2113eqtri 2768 . . . . . . . 8 ((2 · 1) + 2) = 04
26429, 3, 9, 3, 259, 261, 9, 30, 39, 206, 263decmac 12787 . . . . . . 7 ((32 · 1) + (11 + 1)) = 44
265208oveq1i 7442 . . . . . . . 8 ((4 · 1) + 6) = (4 + 6)
266 6p4e10 12807 . . . . . . . . 9 (6 + 4) = 10
26761, 207, 266addcomli 11454 . . . . . . . 8 (4 + 6) = 10
268265, 267eqtri 2764 . . . . . . 7 ((4 · 1) + 6) = 10
26933, 30, 251, 2, 252, 258, 9, 39, 9, 264, 268decmac 12787 . . . . . 6 ((324 · 1) + (19 + 97)) = 440
270145, 138eqtri 2764 . . . . . . . 8 (0 + 1) = 01
271 3t3e9 12434 . . . . . . . . . 10 (3 · 3) = 9
272271, 139oveq12i 7444 . . . . . . . . 9 ((3 · 3) + (0 + 0)) = (9 + 0)
273234addridi 11449 . . . . . . . . 9 (9 + 0) = 9
274272, 273eqtri 2764 . . . . . . . 8 ((3 · 3) + (0 + 0)) = 9
275101oveq1i 7442 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
27635dec0h 12757 . . . . . . . . 9 7 = 07
277275, 216, 2763eqtri 2768 . . . . . . . 8 ((2 · 3) + 1) = 07
27829, 3, 39, 9, 259, 270, 29, 35, 39, 274, 277decmac 12787 . . . . . . 7 ((32 · 3) + (0 + 1)) = 97
279 4t3e12 12833 . . . . . . . 8 (4 · 3) = 12
280 4p2e6 12420 . . . . . . . . 9 (4 + 2) = 6
281207, 57, 280addcomli 11454 . . . . . . . 8 (2 + 4) = 6
2829, 3, 30, 279, 281decaddi 12795 . . . . . . 7 ((4 · 3) + 4) = 16
28333, 30, 39, 30, 252, 211, 29, 2, 9, 278, 282decmac 12787 . . . . . 6 ((324 · 3) + 4) = 976
2849, 29, 246, 30, 248, 249, 34, 2, 250, 269, 283decma2c 12788 . . . . 5 ((324 · 13) + 194) = 4406
285 6t3e18 12840 . . . . . . . . 9 (6 · 3) = 18
28661, 99, 285mulcomli 11271 . . . . . . . 8 (3 · 6) = 18
2879, 13, 18, 286decsuc 12766 . . . . . . 7 ((3 · 6) + 1) = 19
2889, 3, 3, 63, 115decaddi 12795 . . . . . . 7 ((2 · 6) + 2) = 14
28929, 3, 3, 259, 2, 30, 9, 287, 288decrmac 12793 . . . . . 6 ((32 · 6) + 2) = 194
290 6t4e24 12841 . . . . . . 7 (6 · 4) = 24
29161, 207, 290mulcomli 11271 . . . . . 6 (4 · 6) = 24
2922, 33, 30, 252, 30, 3, 289, 291decmul1c 12800 . . . . 5 (324 · 6) = 1944
29334, 37, 2, 245, 30, 247, 284, 292decmul2c 12801 . . . 4 (324 · 136) = 44064
294244, 293eqtr4i 2767 . . 3 ((34 · 𝑁) + (𝑁 − 1)) = (324 · 136)
29526, 1, 28, 32, 34, 23, 36, 38, 178, 179, 186, 294modxai 17107 . 2 ((2↑629) mod 𝑁) = ((𝑁 − 1) mod 𝑁)
296 eqid 2736 . . . 4 629 = 629
297 eqid 2736 . . . . 5 62 = 62
298139oveq2i 7443 . . . . . 6 ((2 · 6) + (0 + 0)) = ((2 · 6) + 0)
29963oveq1i 7442 . . . . . 6 ((2 · 6) + 0) = (12 + 0)
30010nn0cni 12540 . . . . . . 7 12 ∈ ℂ
301300addridi 11449 . . . . . 6 (12 + 0) = 12
302298, 299, 3013eqtri 2768 . . . . 5 ((2 · 6) + (0 + 0)) = 12
30311dec0h 12757 . . . . . 6 5 = 05
30481, 55, 3033eqtri 2768 . . . . 5 ((2 · 2) + 1) = 05
3052, 3, 39, 9, 297, 138, 3, 11, 39, 302, 304decma2c 12788 . . . 4 ((2 · 62) + 1) = 125
306 9t2e18 12857 . . . . 5 (9 · 2) = 18
307234, 57, 306mulcomli 11271 . . . 4 (2 · 9) = 18
3083, 4, 5, 296, 13, 9, 305, 307decmul2c 12801 . . 3 (2 · 629) = 1258
309308, 22eqtr4i 2767 . 2 (2 · 629) = (𝑁 − 1)
310 npcan 11518 . . 3 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
31167, 16, 310mp2an 692 . 2 ((𝑁 − 1) + 1) = 𝑁
31268oveq1i 7442 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
313145, 312, 1613eqtr4i 2774 . 2 ((0 · 𝑁) + 1) = (1 · 1)
3141, 6, 7, 8, 9, 23, 295, 309, 311, 313mod2xnegi 17110 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1539  wcel 2107  (class class class)co 7432  cc 11154  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161  cmin 11493  cn 12267  2c2 12322  3c3 12323  4c4 12324  5c5 12325  6c6 12326  7c7 12327  8c8 12328  9c9 12329  0cn0 12528  cdc 12735   mod cmo 13910  cexp 14103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-2nd 8016  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-er 8746  df-en 8987  df-dom 8988  df-sdom 8989  df-sup 9483  df-inf 9484  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12529  df-z 12616  df-dec 12736  df-uz 12880  df-rp 13036  df-fl 13833  df-mod 13911  df-seq 14044  df-exp 14104
This theorem is referenced by:  1259prm  17174
  Copyright terms: Public domain W3C validator