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

Theorem 1259lem4 17112
Description: Lemma for 1259prm 17114. 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 12325 . 2 2 ∈ ℕ
2 6nn0 12533 . . . 4 6 ∈ ℕ0
3 2nn0 12529 . . . 4 2 ∈ ℕ0
42, 3deccl 12732 . . 3 62 ∈ ℕ0
5 9nn0 12536 . . 3 9 ∈ ℕ0
64, 5deccl 12732 . 2 629 ∈ ℕ0
7 0z 12609 . 2 0 ∈ ℤ
8 1nn 12263 . 2 1 ∈ ℕ
9 1nn0 12528 . 2 1 ∈ ℕ0
109, 3deccl 12732 . . . . . . 7 12 ∈ ℕ0
11 5nn0 12532 . . . . . . 7 5 ∈ ℕ0
1210, 11deccl 12732 . . . . . 6 125 ∈ ℕ0
13 8nn0 12535 . . . . . 6 8 ∈ ℕ0
1412, 13deccl 12732 . . . . 5 1258 ∈ ℕ0
1514nn0cni 12524 . . . 4 1258 ∈ ℂ
16 ax-1cn 11206 . . . 4 1 ∈ ℂ
17 1259prm.1 . . . . 5 𝑁 = 1259
18 8p1e9 12402 . . . . . 6 (8 + 1) = 9
19 eqid 2728 . . . . . 6 1258 = 1258
2012, 13, 18, 19decsuc 12748 . . . . 5 (1258 + 1) = 1259
2117, 20eqtr4i 2759 . . . 4 𝑁 = (1258 + 1)
2215, 16, 21mvrraddi 11517 . . 3 (𝑁 − 1) = 1258
2322, 14eqeltri 2825 . 2 (𝑁 − 1) ∈ ℕ0
24 9nn 12350 . . . . 5 9 ∈ ℕ
2512, 24decnncl 12737 . . . 4 1259 ∈ ℕ
2617, 25eqeltri 2825 . . 3 𝑁 ∈ ℕ
272, 9deccl 12732 . . . 4 61 ∈ ℕ0
2827, 3deccl 12732 . . 3 612 ∈ ℕ0
29 3nn0 12530 . . . . 5 3 ∈ ℕ0
30 4nn0 12531 . . . . 5 4 ∈ ℕ0
3129, 30deccl 12732 . . . 4 34 ∈ ℕ0
3231nn0zi 12627 . . 3 34 ∈ ℤ
3329, 3deccl 12732 . . . 4 32 ∈ ℕ0
3433, 30deccl 12732 . . 3 324 ∈ ℕ0
35 7nn0 12534 . . . 4 7 ∈ ℕ0
369, 35deccl 12732 . . 3 17 ∈ ℕ0
379, 29deccl 12732 . . . 4 13 ∈ ℕ0
3837, 2deccl 12732 . . 3 136 ∈ ℕ0
39 0nn0 12527 . . . . . 6 0 ∈ ℕ0
4029, 39deccl 12732 . . . . 5 30 ∈ ℕ0
4140, 2deccl 12732 . . . 4 306 ∈ ℕ0
42 8nn 12347 . . . . 5 8 ∈ ℕ
439, 42decnncl 12737 . . . 4 18 ∈ ℕ
4410, 30deccl 12732 . . . . 5 124 ∈ ℕ0
4544, 9deccl 12732 . . . 4 1241 ∈ ℕ0
469, 11deccl 12732 . . . . . 6 15 ∈ ℕ0
4746, 29deccl 12732 . . . . 5 153 ∈ ℕ0
48 1z 12632 . . . . 5 1 ∈ ℤ
4911, 39deccl 12732 . . . . 5 50 ∈ ℕ0
5046, 3deccl 12732 . . . . . 6 152 ∈ ℕ0
513, 11deccl 12732 . . . . . 6 25 ∈ ℕ0
5235, 2deccl 12732 . . . . . . 7 76 ∈ ℕ0
53171259lem3 17111 . . . . . . 7 ((2↑76) mod 𝑁) = (5 mod 𝑁)
54 eqid 2728 . . . . . . . 8 76 = 76
55 4p1e5 12398 . . . . . . . . 9 (4 + 1) = 5
56 7cn 12346 . . . . . . . . . 10 7 ∈ ℂ
57 2cn 12327 . . . . . . . . . 10 2 ∈ ℂ
58 7t2e14 12826 . . . . . . . . . 10 (7 · 2) = 14
5956, 57, 58mulcomli 11263 . . . . . . . . 9 (2 · 7) = 14
609, 30, 55, 59decsuc 12748 . . . . . . . 8 ((2 · 7) + 1) = 15
61 6cn 12343 . . . . . . . . 9 6 ∈ ℂ
62 6t2e12 12821 . . . . . . . . 9 (6 · 2) = 12
6361, 57, 62mulcomli 11263 . . . . . . . 8 (2 · 6) = 12
643, 35, 2, 54, 3, 9, 60, 63decmul2c 12783 . . . . . . 7 (2 · 76) = 152
6551nn0cni 12524 . . . . . . . . 9 25 ∈ ℂ
6665addlidi 11442 . . . . . . . 8 (0 + 25) = 25
6726nncni 12262 . . . . . . . . . 10 𝑁 ∈ ℂ
6867mul02i 11443 . . . . . . . . 9 (0 · 𝑁) = 0
6968oveq1i 7436 . . . . . . . 8 ((0 · 𝑁) + 25) = (0 + 25)
70 5t5e25 12820 . . . . . . . 8 (5 · 5) = 25
7166, 69, 703eqtr4i 2766 . . . . . . 7 ((0 · 𝑁) + 25) = (5 · 5)
7226, 1, 52, 7, 11, 51, 53, 64, 71mod2xi 17047 . . . . . 6 ((2↑152) mod 𝑁) = (25 mod 𝑁)
73 2p1e3 12394 . . . . . . 7 (2 + 1) = 3
74 eqid 2728 . . . . . . 7 152 = 152
7546, 3, 73, 74decsuc 12748 . . . . . 6 (152 + 1) = 153
7649nn0cni 12524 . . . . . . . 8 50 ∈ ℂ
7776addlidi 11442 . . . . . . 7 (0 + 50) = 50
7868oveq1i 7436 . . . . . . 7 ((0 · 𝑁) + 50) = (0 + 50)
79 eqid 2728 . . . . . . . 8 25 = 25
80 2t2e4 12416 . . . . . . . . . 10 (2 · 2) = 4
8180oveq1i 7436 . . . . . . . . 9 ((2 · 2) + 1) = (4 + 1)
8281, 55eqtri 2756 . . . . . . . 8 ((2 · 2) + 1) = 5
83 5t2e10 12817 . . . . . . . 8 (5 · 2) = 10
843, 3, 11, 79, 39, 9, 82, 83decmul1c 12782 . . . . . . 7 (25 · 2) = 50
8577, 78, 843eqtr4i 2766 . . . . . 6 ((0 · 𝑁) + 50) = (25 · 2)
8626, 1, 50, 7, 51, 49, 72, 75, 85modxp1i 17048 . . . . 5 ((2↑153) mod 𝑁) = (50 mod 𝑁)
87 eqid 2728 . . . . . 6 153 = 153
88 eqid 2728 . . . . . . . . 9 15 = 15
8957mulridi 11258 . . . . . . . . . . 11 (2 · 1) = 2
9089oveq1i 7436 . . . . . . . . . 10 ((2 · 1) + 1) = (2 + 1)
9190, 73eqtri 2756 . . . . . . . . 9 ((2 · 1) + 1) = 3
92 5cn 12340 . . . . . . . . . 10 5 ∈ ℂ
9392, 57, 83mulcomli 11263 . . . . . . . . 9 (2 · 5) = 10
943, 9, 11, 88, 39, 9, 91, 93decmul2c 12783 . . . . . . . 8 (2 · 15) = 30
9594oveq1i 7436 . . . . . . 7 ((2 · 15) + 0) = (30 + 0)
9640nn0cni 12524 . . . . . . . 8 30 ∈ ℂ
9796addridi 11441 . . . . . . 7 (30 + 0) = 30
9895, 97eqtri 2756 . . . . . 6 ((2 · 15) + 0) = 30
99 3cn 12333 . . . . . . . 8 3 ∈ ℂ
100 3t2e6 12418 . . . . . . . 8 (3 · 2) = 6
10199, 57, 100mulcomli 11263 . . . . . . 7 (2 · 3) = 6
1022dec0h 12739 . . . . . . 7 6 = 06
103101, 102eqtri 2756 . . . . . 6 (2 · 3) = 06
1043, 46, 29, 87, 2, 39, 98, 103decmul2c 12783 . . . . 5 (2 · 153) = 306
10567mullidi 11259 . . . . . . . 8 (1 · 𝑁) = 𝑁
106105, 17eqtri 2756 . . . . . . 7 (1 · 𝑁) = 1259
107 eqid 2728 . . . . . . 7 1241 = 1241
1083, 30deccl 12732 . . . . . . . 8 24 ∈ ℕ0
109 eqid 2728 . . . . . . . . 9 24 = 24
1103, 30, 55, 109decsuc 12748 . . . . . . . 8 (24 + 1) = 25
111 eqid 2728 . . . . . . . . 9 125 = 125
112 eqid 2728 . . . . . . . . 9 124 = 124
113 eqid 2728 . . . . . . . . . 10 12 = 12
114 1p1e2 12377 . . . . . . . . . 10 (1 + 1) = 2
115 2p2e4 12387 . . . . . . . . . 10 (2 + 2) = 4
1169, 3, 9, 3, 113, 113, 114, 115decadd 12771 . . . . . . . . 9 (12 + 12) = 24
117 5p4e9 12410 . . . . . . . . 9 (5 + 4) = 9
11810, 11, 10, 30, 111, 112, 116, 117decadd 12771 . . . . . . . 8 (125 + 124) = 249
119108, 110, 118decsucc 12758 . . . . . . 7 ((125 + 124) + 1) = 250
120 9p1e10 12719 . . . . . . 7 (9 + 1) = 10
12112, 5, 44, 9, 106, 107, 119, 120decaddc2 12773 . . . . . 6 ((1 · 𝑁) + 1241) = 2500
122 eqid 2728 . . . . . . 7 50 = 50
12392mul02i 11443 . . . . . . . . . 10 (0 · 5) = 0
12411, 11, 39, 122, 70, 123decmul1 12781 . . . . . . . . 9 (50 · 5) = 250
125124oveq1i 7436 . . . . . . . 8 ((50 · 5) + 0) = (250 + 0)
12651, 39deccl 12732 . . . . . . . . . 10 250 ∈ ℕ0
127126nn0cni 12524 . . . . . . . . 9 250 ∈ ℂ
128127addridi 11441 . . . . . . . 8 (250 + 0) = 250
129125, 128eqtri 2756 . . . . . . 7 ((50 · 5) + 0) = 250
13076mul01i 11444 . . . . . . . 8 (50 · 0) = 0
13139dec0h 12739 . . . . . . . 8 0 = 00
132130, 131eqtri 2756 . . . . . . 7 (50 · 0) = 00
13349, 11, 39, 122, 39, 39, 129, 132decmul2c 12783 . . . . . 6 (50 · 50) = 2500
134121, 133eqtr4i 2759 . . . . 5 ((1 · 𝑁) + 1241) = (50 · 50)
13526, 1, 47, 48, 49, 45, 86, 104, 134mod2xi 17047 . . . 4 ((2↑306) mod 𝑁) = (1241 mod 𝑁)
136 eqid 2728 . . . . 5 306 = 306
137 eqid 2728 . . . . . 6 30 = 30
1389dec0h 12739 . . . . . 6 1 = 01
139 00id 11429 . . . . . . . 8 (0 + 0) = 0
140101, 139oveq12i 7438 . . . . . . 7 ((2 · 3) + (0 + 0)) = (6 + 0)
14161addridi 11441 . . . . . . 7 (6 + 0) = 6
142140, 141eqtri 2756 . . . . . 6 ((2 · 3) + (0 + 0)) = 6
14357mul01i 11444 . . . . . . . 8 (2 · 0) = 0
144143oveq1i 7436 . . . . . . 7 ((2 · 0) + 1) = (0 + 1)
145 0p1e1 12374 . . . . . . 7 (0 + 1) = 1
146144, 145, 1383eqtri 2760 . . . . . 6 ((2 · 0) + 1) = 01
14729, 39, 39, 9, 137, 138, 3, 9, 39, 142, 146decma2c 12770 . . . . 5 ((2 · 30) + 1) = 61
1483, 40, 2, 136, 3, 9, 147, 63decmul2c 12783 . . . 4 (2 · 306) = 612
149 eqid 2728 . . . . . 6 18 = 18
15010, 30, 55, 112decsuc 12748 . . . . . 6 (124 + 1) = 125
151 8cn 12349 . . . . . . 7 8 ∈ ℂ
152151, 16, 18addcomli 11446 . . . . . 6 (1 + 8) = 9
15344, 9, 9, 13, 107, 149, 150, 152decadd 12771 . . . . 5 (1241 + 18) = 1259
154153, 17eqtr4i 2759 . . . 4 (1241 + 18) = 𝑁
15534nn0cni 12524 . . . . . 6 324 ∈ ℂ
156155addlidi 11442 . . . . 5 (0 + 324) = 324
15768oveq1i 7436 . . . . 5 ((0 · 𝑁) + 324) = (0 + 324)
1589, 13deccl 12732 . . . . . 6 18 ∈ ℕ0
1599, 30deccl 12732 . . . . . 6 14 ∈ ℕ0
160 eqid 2728 . . . . . . 7 14 = 14
16116mulridi 11258 . . . . . . . . 9 (1 · 1) = 1
162161, 114oveq12i 7438 . . . . . . . 8 ((1 · 1) + (1 + 1)) = (1 + 2)
163 1p2e3 12395 . . . . . . . 8 (1 + 2) = 3
164162, 163eqtri 2756 . . . . . . 7 ((1 · 1) + (1 + 1)) = 3
165151mulridi 11258 . . . . . . . . 9 (8 · 1) = 8
166165oveq1i 7436 . . . . . . . 8 ((8 · 1) + 4) = (8 + 4)
167 8p4e12 12799 . . . . . . . 8 (8 + 4) = 12
168166, 167eqtri 2756 . . . . . . 7 ((8 · 1) + 4) = 12
1699, 13, 9, 30, 149, 160, 9, 3, 9, 164, 168decmac 12769 . . . . . 6 ((18 · 1) + 14) = 32
170151mullidi 11259 . . . . . . . . 9 (1 · 8) = 8
171170oveq1i 7436 . . . . . . . 8 ((1 · 8) + 6) = (8 + 6)
172 8p6e14 12801 . . . . . . . 8 (8 + 6) = 14
173171, 172eqtri 2756 . . . . . . 7 ((1 · 8) + 6) = 14
174 8t8e64 12838 . . . . . . 7 (8 · 8) = 64
17513, 9, 13, 149, 30, 2, 173, 174decmul1c 12782 . . . . . 6 (18 · 8) = 144
176158, 9, 13, 149, 30, 159, 169, 175decmul2c 12783 . . . . 5 (18 · 18) = 324
177156, 157, 1763eqtr4i 2766 . . . 4 ((0 · 𝑁) + 324) = (18 · 18)
1781, 41, 7, 43, 34, 45, 135, 148, 154, 177mod2xnegi 17049 . . 3 ((2↑612) mod 𝑁) = (324 mod 𝑁)
179171259lem1 17109 . . 3 ((2↑17) mod 𝑁) = (136 mod 𝑁)
180 eqid 2728 . . . 4 612 = 612
181 eqid 2728 . . . 4 17 = 17
182 eqid 2728 . . . . 5 61 = 61
1832, 9, 114, 182decsuc 12748 . . . 4 (61 + 1) = 62
184 7p2e9 12413 . . . . 5 (7 + 2) = 9
18556, 57, 184addcomli 11446 . . . 4 (2 + 7) = 9
18627, 3, 9, 35, 180, 181, 183, 185decadd 12771 . . 3 (612 + 17) = 629
18729, 9deccl 12732 . . . . 5 31 ∈ ℕ0
188 eqid 2728 . . . . . . 7 31 = 31
189 3p2e5 12403 . . . . . . . . 9 (3 + 2) = 5
19099, 57, 189addcomli 11446 . . . . . . . 8 (2 + 3) = 5
1919, 3, 29, 113, 190decaddi 12777 . . . . . . 7 (12 + 3) = 15
192 5p1e6 12399 . . . . . . 7 (5 + 1) = 6
19310, 11, 29, 9, 111, 188, 191, 192decadd 12771 . . . . . 6 (125 + 31) = 156
194114oveq1i 7436 . . . . . . . . 9 ((1 + 1) + 1) = (2 + 1)
195194, 73eqtri 2756 . . . . . . . 8 ((1 + 1) + 1) = 3
196 7p5e12 12794 . . . . . . . . 9 (7 + 5) = 12
19756, 92, 196addcomli 11446 . . . . . . . 8 (5 + 7) = 12
1989, 11, 9, 35, 88, 181, 195, 3, 197decaddc 12772 . . . . . . 7 (15 + 17) = 32
199 eqid 2728 . . . . . . . 8 34 = 34
200 7p3e10 12792 . . . . . . . . 9 (7 + 3) = 10
20156, 99, 200addcomli 11446 . . . . . . . 8 (3 + 7) = 10
20299mulridi 11258 . . . . . . . . . 10 (3 · 1) = 3
20316addridi 11441 . . . . . . . . . 10 (1 + 0) = 1
204202, 203oveq12i 7438 . . . . . . . . 9 ((3 · 1) + (1 + 0)) = (3 + 1)
205 3p1e4 12397 . . . . . . . . 9 (3 + 1) = 4
206204, 205eqtri 2756 . . . . . . . 8 ((3 · 1) + (1 + 0)) = 4
207 4cn 12337 . . . . . . . . . . 11 4 ∈ ℂ
208207mulridi 11258 . . . . . . . . . 10 (4 · 1) = 4
209208oveq1i 7436 . . . . . . . . 9 ((4 · 1) + 0) = (4 + 0)
210207addridi 11441 . . . . . . . . 9 (4 + 0) = 4
21130dec0h 12739 . . . . . . . . 9 4 = 04
212209, 210, 2113eqtri 2760 . . . . . . . 8 ((4 · 1) + 0) = 04
21329, 30, 9, 39, 199, 201, 9, 30, 39, 206, 212decmac 12769 . . . . . . 7 ((34 · 1) + (3 + 7)) = 44
2143dec0h 12739 . . . . . . . 8 2 = 02
215100, 145oveq12i 7438 . . . . . . . . 9 ((3 · 2) + (0 + 1)) = (6 + 1)
216 6p1e7 12400 . . . . . . . . 9 (6 + 1) = 7
217215, 216eqtri 2756 . . . . . . . 8 ((3 · 2) + (0 + 1)) = 7
218 4t2e8 12420 . . . . . . . . . 10 (4 · 2) = 8
219218oveq1i 7436 . . . . . . . . 9 ((4 · 2) + 2) = (8 + 2)
220 8p2e10 12797 . . . . . . . . 9 (8 + 2) = 10
221219, 220eqtri 2756 . . . . . . . 8 ((4 · 2) + 2) = 10
22229, 30, 39, 3, 199, 214, 3, 39, 9, 217, 221decmac 12769 . . . . . . 7 ((34 · 2) + 2) = 70
2239, 3, 29, 3, 113, 198, 31, 39, 35, 213, 222decma2c 12770 . . . . . 6 ((34 · 12) + (15 + 17)) = 440
224 5t3e15 12818 . . . . . . . . 9 (5 · 3) = 15
22592, 99, 224mulcomli 11263 . . . . . . . 8 (3 · 5) = 15
226 5p2e7 12408 . . . . . . . 8 (5 + 2) = 7
2279, 11, 3, 225, 226decaddi 12777 . . . . . . 7 ((3 · 5) + 2) = 17
228 5t4e20 12819 . . . . . . . . 9 (5 · 4) = 20
22992, 207, 228mulcomli 11263 . . . . . . . 8 (4 · 5) = 20
23061addlidi 11442 . . . . . . . 8 (0 + 6) = 6
2313, 39, 2, 229, 230decaddi 12777 . . . . . . 7 ((4 · 5) + 6) = 26
23229, 30, 2, 199, 11, 2, 3, 227, 231decrmac 12775 . . . . . 6 ((34 · 5) + 6) = 176
23310, 11, 46, 2, 111, 193, 31, 2, 36, 223, 232decma2c 12770 . . . . 5 ((34 · 125) + (125 + 31)) = 4406
234 9cn 12352 . . . . . . . 8 9 ∈ ℂ
235 9t3e27 12840 . . . . . . . 8 (9 · 3) = 27
236234, 99, 235mulcomli 11263 . . . . . . 7 (3 · 9) = 27
237 7p4e11 12793 . . . . . . 7 (7 + 4) = 11
2383, 35, 30, 236, 73, 9, 237decaddci 12778 . . . . . 6 ((3 · 9) + 4) = 31
239 9t4e36 12841 . . . . . . . 8 (9 · 4) = 36
240234, 207, 239mulcomli 11263 . . . . . . 7 (4 · 9) = 36
241151, 61, 172addcomli 11446 . . . . . . 7 (6 + 8) = 14
24229, 2, 13, 240, 205, 30, 241decaddci 12778 . . . . . 6 ((4 · 9) + 8) = 44
24329, 30, 13, 199, 5, 30, 30, 238, 242decrmac 12775 . . . . 5 ((34 · 9) + 8) = 314
24412, 5, 12, 13, 17, 22, 31, 30, 187, 233, 243decma2c 12770 . . . 4 ((34 · 𝑁) + (𝑁 − 1)) = 44064
245 eqid 2728 . . . . 5 136 = 136
2469, 5deccl 12732 . . . . . 6 19 ∈ ℕ0
247246, 30deccl 12732 . . . . 5 194 ∈ ℕ0
248 eqid 2728 . . . . . 6 13 = 13
249 eqid 2728 . . . . . 6 194 = 194
2505, 35deccl 12732 . . . . . 6 97 ∈ ℕ0
2519, 9deccl 12732 . . . . . . 7 11 ∈ ℕ0
252 eqid 2728 . . . . . . 7 324 = 324
253 eqid 2728 . . . . . . . 8 19 = 19
254 eqid 2728 . . . . . . . 8 97 = 97
255234, 16, 120addcomli 11446 . . . . . . . . 9 (1 + 9) = 10
2569, 39, 145, 255decsuc 12748 . . . . . . . 8 ((1 + 9) + 1) = 11
257 9p7e16 12809 . . . . . . . 8 (9 + 7) = 16
2589, 5, 5, 35, 253, 254, 256, 2, 257decaddc 12772 . . . . . . 7 (19 + 97) = 116
259 eqid 2728 . . . . . . . 8 32 = 32
260 eqid 2728 . . . . . . . . 9 11 = 11
2619, 9, 114, 260decsuc 12748 . . . . . . . 8 (11 + 1) = 12
26289oveq1i 7436 . . . . . . . . 9 ((2 · 1) + 2) = (2 + 2)
263262, 115, 2113eqtri 2760 . . . . . . . 8 ((2 · 1) + 2) = 04
26429, 3, 9, 3, 259, 261, 9, 30, 39, 206, 263decmac 12769 . . . . . . 7 ((32 · 1) + (11 + 1)) = 44
265208oveq1i 7436 . . . . . . . 8 ((4 · 1) + 6) = (4 + 6)
266 6p4e10 12789 . . . . . . . . 9 (6 + 4) = 10
26761, 207, 266addcomli 11446 . . . . . . . 8 (4 + 6) = 10
268265, 267eqtri 2756 . . . . . . 7 ((4 · 1) + 6) = 10
26933, 30, 251, 2, 252, 258, 9, 39, 9, 264, 268decmac 12769 . . . . . 6 ((324 · 1) + (19 + 97)) = 440
270145, 138eqtri 2756 . . . . . . . 8 (0 + 1) = 01
271 3t3e9 12419 . . . . . . . . . 10 (3 · 3) = 9
272271, 139oveq12i 7438 . . . . . . . . 9 ((3 · 3) + (0 + 0)) = (9 + 0)
273234addridi 11441 . . . . . . . . 9 (9 + 0) = 9
274272, 273eqtri 2756 . . . . . . . 8 ((3 · 3) + (0 + 0)) = 9
275101oveq1i 7436 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
27635dec0h 12739 . . . . . . . . 9 7 = 07
277275, 216, 2763eqtri 2760 . . . . . . . 8 ((2 · 3) + 1) = 07
27829, 3, 39, 9, 259, 270, 29, 35, 39, 274, 277decmac 12769 . . . . . . 7 ((32 · 3) + (0 + 1)) = 97
279 4t3e12 12815 . . . . . . . 8 (4 · 3) = 12
280 4p2e6 12405 . . . . . . . . 9 (4 + 2) = 6
281207, 57, 280addcomli 11446 . . . . . . . 8 (2 + 4) = 6
2829, 3, 30, 279, 281decaddi 12777 . . . . . . 7 ((4 · 3) + 4) = 16
28333, 30, 39, 30, 252, 211, 29, 2, 9, 278, 282decmac 12769 . . . . . 6 ((324 · 3) + 4) = 976
2849, 29, 246, 30, 248, 249, 34, 2, 250, 269, 283decma2c 12770 . . . . 5 ((324 · 13) + 194) = 4406
285 6t3e18 12822 . . . . . . . . 9 (6 · 3) = 18
28661, 99, 285mulcomli 11263 . . . . . . . 8 (3 · 6) = 18
2879, 13, 18, 286decsuc 12748 . . . . . . 7 ((3 · 6) + 1) = 19
2889, 3, 3, 63, 115decaddi 12777 . . . . . . 7 ((2 · 6) + 2) = 14
28929, 3, 3, 259, 2, 30, 9, 287, 288decrmac 12775 . . . . . 6 ((32 · 6) + 2) = 194
290 6t4e24 12823 . . . . . . 7 (6 · 4) = 24
29161, 207, 290mulcomli 11263 . . . . . 6 (4 · 6) = 24
2922, 33, 30, 252, 30, 3, 289, 291decmul1c 12782 . . . . 5 (324 · 6) = 1944
29334, 37, 2, 245, 30, 247, 284, 292decmul2c 12783 . . . 4 (324 · 136) = 44064
294244, 293eqtr4i 2759 . . 3 ((34 · 𝑁) + (𝑁 − 1)) = (324 · 136)
29526, 1, 28, 32, 34, 23, 36, 38, 178, 179, 186, 294modxai 17046 . 2 ((2↑629) mod 𝑁) = ((𝑁 − 1) mod 𝑁)
296 eqid 2728 . . . 4 629 = 629
297 eqid 2728 . . . . 5 62 = 62
298139oveq2i 7437 . . . . . 6 ((2 · 6) + (0 + 0)) = ((2 · 6) + 0)
29963oveq1i 7436 . . . . . 6 ((2 · 6) + 0) = (12 + 0)
30010nn0cni 12524 . . . . . . 7 12 ∈ ℂ
301300addridi 11441 . . . . . 6 (12 + 0) = 12
302298, 299, 3013eqtri 2760 . . . . 5 ((2 · 6) + (0 + 0)) = 12
30311dec0h 12739 . . . . . 6 5 = 05
30481, 55, 3033eqtri 2760 . . . . 5 ((2 · 2) + 1) = 05
3052, 3, 39, 9, 297, 138, 3, 11, 39, 302, 304decma2c 12770 . . . 4 ((2 · 62) + 1) = 125
306 9t2e18 12839 . . . . 5 (9 · 2) = 18
307234, 57, 306mulcomli 11263 . . . 4 (2 · 9) = 18
3083, 4, 5, 296, 13, 9, 305, 307decmul2c 12783 . . 3 (2 · 629) = 1258
309308, 22eqtr4i 2759 . 2 (2 · 629) = (𝑁 − 1)
310 npcan 11509 . . 3 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
31167, 16, 310mp2an 690 . 2 ((𝑁 − 1) + 1) = 𝑁
31268oveq1i 7436 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
313145, 312, 1613eqtr4i 2766 . 2 ((0 · 𝑁) + 1) = (1 · 1)
3141, 6, 7, 8, 9, 23, 295, 309, 311, 313mod2xnegi 17049 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  wcel 2098  (class class class)co 7426  cc 11146  0cc0 11148  1c1 11149   + caddc 11151   · cmul 11153  cmin 11484  cn 12252  2c2 12307  3c3 12308  4c4 12309  5c5 12310  6c6 12311  7c7 12312  8c8 12313  9c9 12314  0cn0 12512  cdc 12717   mod cmo 13876  cexp 14068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7879  df-2nd 8002  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-er 8733  df-en 8973  df-dom 8974  df-sdom 8975  df-sup 9475  df-inf 9476  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-z 12599  df-dec 12718  df-uz 12863  df-rp 13017  df-fl 13799  df-mod 13877  df-seq 14009  df-exp 14069
This theorem is referenced by:  1259prm  17114
  Copyright terms: Public domain W3C validator