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

Theorem 1259lem4 17108
Description: Lemma for 1259prm 17110. 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 12321 . 2 2 ∈ ℕ
2 6nn0 12529 . . . 4 6 ∈ ℕ0
3 2nn0 12525 . . . 4 2 ∈ ℕ0
42, 3deccl 12728 . . 3 62 ∈ ℕ0
5 9nn0 12532 . . 3 9 ∈ ℕ0
64, 5deccl 12728 . 2 629 ∈ ℕ0
7 0z 12605 . 2 0 ∈ ℤ
8 1nn 12259 . 2 1 ∈ ℕ
9 1nn0 12524 . 2 1 ∈ ℕ0
109, 3deccl 12728 . . . . . . 7 12 ∈ ℕ0
11 5nn0 12528 . . . . . . 7 5 ∈ ℕ0
1210, 11deccl 12728 . . . . . 6 125 ∈ ℕ0
13 8nn0 12531 . . . . . 6 8 ∈ ℕ0
1412, 13deccl 12728 . . . . 5 1258 ∈ ℕ0
1514nn0cni 12520 . . . 4 1258 ∈ ℂ
16 ax-1cn 11202 . . . 4 1 ∈ ℂ
17 1259prm.1 . . . . 5 𝑁 = 1259
18 8p1e9 12398 . . . . . 6 (8 + 1) = 9
19 eqid 2727 . . . . . 6 1258 = 1258
2012, 13, 18, 19decsuc 12744 . . . . 5 (1258 + 1) = 1259
2117, 20eqtr4i 2758 . . . 4 𝑁 = (1258 + 1)
2215, 16, 21mvrraddi 11513 . . 3 (𝑁 − 1) = 1258
2322, 14eqeltri 2824 . 2 (𝑁 − 1) ∈ ℕ0
24 9nn 12346 . . . . 5 9 ∈ ℕ
2512, 24decnncl 12733 . . . 4 1259 ∈ ℕ
2617, 25eqeltri 2824 . . 3 𝑁 ∈ ℕ
272, 9deccl 12728 . . . 4 61 ∈ ℕ0
2827, 3deccl 12728 . . 3 612 ∈ ℕ0
29 3nn0 12526 . . . . 5 3 ∈ ℕ0
30 4nn0 12527 . . . . 5 4 ∈ ℕ0
3129, 30deccl 12728 . . . 4 34 ∈ ℕ0
3231nn0zi 12623 . . 3 34 ∈ ℤ
3329, 3deccl 12728 . . . 4 32 ∈ ℕ0
3433, 30deccl 12728 . . 3 324 ∈ ℕ0
35 7nn0 12530 . . . 4 7 ∈ ℕ0
369, 35deccl 12728 . . 3 17 ∈ ℕ0
379, 29deccl 12728 . . . 4 13 ∈ ℕ0
3837, 2deccl 12728 . . 3 136 ∈ ℕ0
39 0nn0 12523 . . . . . 6 0 ∈ ℕ0
4029, 39deccl 12728 . . . . 5 30 ∈ ℕ0
4140, 2deccl 12728 . . . 4 306 ∈ ℕ0
42 8nn 12343 . . . . 5 8 ∈ ℕ
439, 42decnncl 12733 . . . 4 18 ∈ ℕ
4410, 30deccl 12728 . . . . 5 124 ∈ ℕ0
4544, 9deccl 12728 . . . 4 1241 ∈ ℕ0
469, 11deccl 12728 . . . . . 6 15 ∈ ℕ0
4746, 29deccl 12728 . . . . 5 153 ∈ ℕ0
48 1z 12628 . . . . 5 1 ∈ ℤ
4911, 39deccl 12728 . . . . 5 50 ∈ ℕ0
5046, 3deccl 12728 . . . . . 6 152 ∈ ℕ0
513, 11deccl 12728 . . . . . 6 25 ∈ ℕ0
5235, 2deccl 12728 . . . . . . 7 76 ∈ ℕ0
53171259lem3 17107 . . . . . . 7 ((2↑76) mod 𝑁) = (5 mod 𝑁)
54 eqid 2727 . . . . . . . 8 76 = 76
55 4p1e5 12394 . . . . . . . . 9 (4 + 1) = 5
56 7cn 12342 . . . . . . . . . 10 7 ∈ ℂ
57 2cn 12323 . . . . . . . . . 10 2 ∈ ℂ
58 7t2e14 12822 . . . . . . . . . 10 (7 · 2) = 14
5956, 57, 58mulcomli 11259 . . . . . . . . 9 (2 · 7) = 14
609, 30, 55, 59decsuc 12744 . . . . . . . 8 ((2 · 7) + 1) = 15
61 6cn 12339 . . . . . . . . 9 6 ∈ ℂ
62 6t2e12 12817 . . . . . . . . 9 (6 · 2) = 12
6361, 57, 62mulcomli 11259 . . . . . . . 8 (2 · 6) = 12
643, 35, 2, 54, 3, 9, 60, 63decmul2c 12779 . . . . . . 7 (2 · 76) = 152
6551nn0cni 12520 . . . . . . . . 9 25 ∈ ℂ
6665addlidi 11438 . . . . . . . 8 (0 + 25) = 25
6726nncni 12258 . . . . . . . . . 10 𝑁 ∈ ℂ
6867mul02i 11439 . . . . . . . . 9 (0 · 𝑁) = 0
6968oveq1i 7434 . . . . . . . 8 ((0 · 𝑁) + 25) = (0 + 25)
70 5t5e25 12816 . . . . . . . 8 (5 · 5) = 25
7166, 69, 703eqtr4i 2765 . . . . . . 7 ((0 · 𝑁) + 25) = (5 · 5)
7226, 1, 52, 7, 11, 51, 53, 64, 71mod2xi 17043 . . . . . 6 ((2↑152) mod 𝑁) = (25 mod 𝑁)
73 2p1e3 12390 . . . . . . 7 (2 + 1) = 3
74 eqid 2727 . . . . . . 7 152 = 152
7546, 3, 73, 74decsuc 12744 . . . . . 6 (152 + 1) = 153
7649nn0cni 12520 . . . . . . . 8 50 ∈ ℂ
7776addlidi 11438 . . . . . . 7 (0 + 50) = 50
7868oveq1i 7434 . . . . . . 7 ((0 · 𝑁) + 50) = (0 + 50)
79 eqid 2727 . . . . . . . 8 25 = 25
80 2t2e4 12412 . . . . . . . . . 10 (2 · 2) = 4
8180oveq1i 7434 . . . . . . . . 9 ((2 · 2) + 1) = (4 + 1)
8281, 55eqtri 2755 . . . . . . . 8 ((2 · 2) + 1) = 5
83 5t2e10 12813 . . . . . . . 8 (5 · 2) = 10
843, 3, 11, 79, 39, 9, 82, 83decmul1c 12778 . . . . . . 7 (25 · 2) = 50
8577, 78, 843eqtr4i 2765 . . . . . 6 ((0 · 𝑁) + 50) = (25 · 2)
8626, 1, 50, 7, 51, 49, 72, 75, 85modxp1i 17044 . . . . 5 ((2↑153) mod 𝑁) = (50 mod 𝑁)
87 eqid 2727 . . . . . 6 153 = 153
88 eqid 2727 . . . . . . . . 9 15 = 15
8957mulridi 11254 . . . . . . . . . . 11 (2 · 1) = 2
9089oveq1i 7434 . . . . . . . . . 10 ((2 · 1) + 1) = (2 + 1)
9190, 73eqtri 2755 . . . . . . . . 9 ((2 · 1) + 1) = 3
92 5cn 12336 . . . . . . . . . 10 5 ∈ ℂ
9392, 57, 83mulcomli 11259 . . . . . . . . 9 (2 · 5) = 10
943, 9, 11, 88, 39, 9, 91, 93decmul2c 12779 . . . . . . . 8 (2 · 15) = 30
9594oveq1i 7434 . . . . . . 7 ((2 · 15) + 0) = (30 + 0)
9640nn0cni 12520 . . . . . . . 8 30 ∈ ℂ
9796addridi 11437 . . . . . . 7 (30 + 0) = 30
9895, 97eqtri 2755 . . . . . 6 ((2 · 15) + 0) = 30
99 3cn 12329 . . . . . . . 8 3 ∈ ℂ
100 3t2e6 12414 . . . . . . . 8 (3 · 2) = 6
10199, 57, 100mulcomli 11259 . . . . . . 7 (2 · 3) = 6
1022dec0h 12735 . . . . . . 7 6 = 06
103101, 102eqtri 2755 . . . . . 6 (2 · 3) = 06
1043, 46, 29, 87, 2, 39, 98, 103decmul2c 12779 . . . . 5 (2 · 153) = 306
10567mullidi 11255 . . . . . . . 8 (1 · 𝑁) = 𝑁
106105, 17eqtri 2755 . . . . . . 7 (1 · 𝑁) = 1259
107 eqid 2727 . . . . . . 7 1241 = 1241
1083, 30deccl 12728 . . . . . . . 8 24 ∈ ℕ0
109 eqid 2727 . . . . . . . . 9 24 = 24
1103, 30, 55, 109decsuc 12744 . . . . . . . 8 (24 + 1) = 25
111 eqid 2727 . . . . . . . . 9 125 = 125
112 eqid 2727 . . . . . . . . 9 124 = 124
113 eqid 2727 . . . . . . . . . 10 12 = 12
114 1p1e2 12373 . . . . . . . . . 10 (1 + 1) = 2
115 2p2e4 12383 . . . . . . . . . 10 (2 + 2) = 4
1169, 3, 9, 3, 113, 113, 114, 115decadd 12767 . . . . . . . . 9 (12 + 12) = 24
117 5p4e9 12406 . . . . . . . . 9 (5 + 4) = 9
11810, 11, 10, 30, 111, 112, 116, 117decadd 12767 . . . . . . . 8 (125 + 124) = 249
119108, 110, 118decsucc 12754 . . . . . . 7 ((125 + 124) + 1) = 250
120 9p1e10 12715 . . . . . . 7 (9 + 1) = 10
12112, 5, 44, 9, 106, 107, 119, 120decaddc2 12769 . . . . . 6 ((1 · 𝑁) + 1241) = 2500
122 eqid 2727 . . . . . . 7 50 = 50
12392mul02i 11439 . . . . . . . . . 10 (0 · 5) = 0
12411, 11, 39, 122, 70, 123decmul1 12777 . . . . . . . . 9 (50 · 5) = 250
125124oveq1i 7434 . . . . . . . 8 ((50 · 5) + 0) = (250 + 0)
12651, 39deccl 12728 . . . . . . . . . 10 250 ∈ ℕ0
127126nn0cni 12520 . . . . . . . . 9 250 ∈ ℂ
128127addridi 11437 . . . . . . . 8 (250 + 0) = 250
129125, 128eqtri 2755 . . . . . . 7 ((50 · 5) + 0) = 250
13076mul01i 11440 . . . . . . . 8 (50 · 0) = 0
13139dec0h 12735 . . . . . . . 8 0 = 00
132130, 131eqtri 2755 . . . . . . 7 (50 · 0) = 00
13349, 11, 39, 122, 39, 39, 129, 132decmul2c 12779 . . . . . 6 (50 · 50) = 2500
134121, 133eqtr4i 2758 . . . . 5 ((1 · 𝑁) + 1241) = (50 · 50)
13526, 1, 47, 48, 49, 45, 86, 104, 134mod2xi 17043 . . . 4 ((2↑306) mod 𝑁) = (1241 mod 𝑁)
136 eqid 2727 . . . . 5 306 = 306
137 eqid 2727 . . . . . 6 30 = 30
1389dec0h 12735 . . . . . 6 1 = 01
139 00id 11425 . . . . . . . 8 (0 + 0) = 0
140101, 139oveq12i 7436 . . . . . . 7 ((2 · 3) + (0 + 0)) = (6 + 0)
14161addridi 11437 . . . . . . 7 (6 + 0) = 6
142140, 141eqtri 2755 . . . . . 6 ((2 · 3) + (0 + 0)) = 6
14357mul01i 11440 . . . . . . . 8 (2 · 0) = 0
144143oveq1i 7434 . . . . . . 7 ((2 · 0) + 1) = (0 + 1)
145 0p1e1 12370 . . . . . . 7 (0 + 1) = 1
146144, 145, 1383eqtri 2759 . . . . . 6 ((2 · 0) + 1) = 01
14729, 39, 39, 9, 137, 138, 3, 9, 39, 142, 146decma2c 12766 . . . . 5 ((2 · 30) + 1) = 61
1483, 40, 2, 136, 3, 9, 147, 63decmul2c 12779 . . . 4 (2 · 306) = 612
149 eqid 2727 . . . . . 6 18 = 18
15010, 30, 55, 112decsuc 12744 . . . . . 6 (124 + 1) = 125
151 8cn 12345 . . . . . . 7 8 ∈ ℂ
152151, 16, 18addcomli 11442 . . . . . 6 (1 + 8) = 9
15344, 9, 9, 13, 107, 149, 150, 152decadd 12767 . . . . 5 (1241 + 18) = 1259
154153, 17eqtr4i 2758 . . . 4 (1241 + 18) = 𝑁
15534nn0cni 12520 . . . . . 6 324 ∈ ℂ
156155addlidi 11438 . . . . 5 (0 + 324) = 324
15768oveq1i 7434 . . . . 5 ((0 · 𝑁) + 324) = (0 + 324)
1589, 13deccl 12728 . . . . . 6 18 ∈ ℕ0
1599, 30deccl 12728 . . . . . 6 14 ∈ ℕ0
160 eqid 2727 . . . . . . 7 14 = 14
16116mulridi 11254 . . . . . . . . 9 (1 · 1) = 1
162161, 114oveq12i 7436 . . . . . . . 8 ((1 · 1) + (1 + 1)) = (1 + 2)
163 1p2e3 12391 . . . . . . . 8 (1 + 2) = 3
164162, 163eqtri 2755 . . . . . . 7 ((1 · 1) + (1 + 1)) = 3
165151mulridi 11254 . . . . . . . . 9 (8 · 1) = 8
166165oveq1i 7434 . . . . . . . 8 ((8 · 1) + 4) = (8 + 4)
167 8p4e12 12795 . . . . . . . 8 (8 + 4) = 12
168166, 167eqtri 2755 . . . . . . 7 ((8 · 1) + 4) = 12
1699, 13, 9, 30, 149, 160, 9, 3, 9, 164, 168decmac 12765 . . . . . 6 ((18 · 1) + 14) = 32
170151mullidi 11255 . . . . . . . . 9 (1 · 8) = 8
171170oveq1i 7434 . . . . . . . 8 ((1 · 8) + 6) = (8 + 6)
172 8p6e14 12797 . . . . . . . 8 (8 + 6) = 14
173171, 172eqtri 2755 . . . . . . 7 ((1 · 8) + 6) = 14
174 8t8e64 12834 . . . . . . 7 (8 · 8) = 64
17513, 9, 13, 149, 30, 2, 173, 174decmul1c 12778 . . . . . 6 (18 · 8) = 144
176158, 9, 13, 149, 30, 159, 169, 175decmul2c 12779 . . . . 5 (18 · 18) = 324
177156, 157, 1763eqtr4i 2765 . . . 4 ((0 · 𝑁) + 324) = (18 · 18)
1781, 41, 7, 43, 34, 45, 135, 148, 154, 177mod2xnegi 17045 . . 3 ((2↑612) mod 𝑁) = (324 mod 𝑁)
179171259lem1 17105 . . 3 ((2↑17) mod 𝑁) = (136 mod 𝑁)
180 eqid 2727 . . . 4 612 = 612
181 eqid 2727 . . . 4 17 = 17
182 eqid 2727 . . . . 5 61 = 61
1832, 9, 114, 182decsuc 12744 . . . 4 (61 + 1) = 62
184 7p2e9 12409 . . . . 5 (7 + 2) = 9
18556, 57, 184addcomli 11442 . . . 4 (2 + 7) = 9
18627, 3, 9, 35, 180, 181, 183, 185decadd 12767 . . 3 (612 + 17) = 629
18729, 9deccl 12728 . . . . 5 31 ∈ ℕ0
188 eqid 2727 . . . . . . 7 31 = 31
189 3p2e5 12399 . . . . . . . . 9 (3 + 2) = 5
19099, 57, 189addcomli 11442 . . . . . . . 8 (2 + 3) = 5
1919, 3, 29, 113, 190decaddi 12773 . . . . . . 7 (12 + 3) = 15
192 5p1e6 12395 . . . . . . 7 (5 + 1) = 6
19310, 11, 29, 9, 111, 188, 191, 192decadd 12767 . . . . . 6 (125 + 31) = 156
194114oveq1i 7434 . . . . . . . . 9 ((1 + 1) + 1) = (2 + 1)
195194, 73eqtri 2755 . . . . . . . 8 ((1 + 1) + 1) = 3
196 7p5e12 12790 . . . . . . . . 9 (7 + 5) = 12
19756, 92, 196addcomli 11442 . . . . . . . 8 (5 + 7) = 12
1989, 11, 9, 35, 88, 181, 195, 3, 197decaddc 12768 . . . . . . 7 (15 + 17) = 32
199 eqid 2727 . . . . . . . 8 34 = 34
200 7p3e10 12788 . . . . . . . . 9 (7 + 3) = 10
20156, 99, 200addcomli 11442 . . . . . . . 8 (3 + 7) = 10
20299mulridi 11254 . . . . . . . . . 10 (3 · 1) = 3
20316addridi 11437 . . . . . . . . . 10 (1 + 0) = 1
204202, 203oveq12i 7436 . . . . . . . . 9 ((3 · 1) + (1 + 0)) = (3 + 1)
205 3p1e4 12393 . . . . . . . . 9 (3 + 1) = 4
206204, 205eqtri 2755 . . . . . . . 8 ((3 · 1) + (1 + 0)) = 4
207 4cn 12333 . . . . . . . . . . 11 4 ∈ ℂ
208207mulridi 11254 . . . . . . . . . 10 (4 · 1) = 4
209208oveq1i 7434 . . . . . . . . 9 ((4 · 1) + 0) = (4 + 0)
210207addridi 11437 . . . . . . . . 9 (4 + 0) = 4
21130dec0h 12735 . . . . . . . . 9 4 = 04
212209, 210, 2113eqtri 2759 . . . . . . . 8 ((4 · 1) + 0) = 04
21329, 30, 9, 39, 199, 201, 9, 30, 39, 206, 212decmac 12765 . . . . . . 7 ((34 · 1) + (3 + 7)) = 44
2143dec0h 12735 . . . . . . . 8 2 = 02
215100, 145oveq12i 7436 . . . . . . . . 9 ((3 · 2) + (0 + 1)) = (6 + 1)
216 6p1e7 12396 . . . . . . . . 9 (6 + 1) = 7
217215, 216eqtri 2755 . . . . . . . 8 ((3 · 2) + (0 + 1)) = 7
218 4t2e8 12416 . . . . . . . . . 10 (4 · 2) = 8
219218oveq1i 7434 . . . . . . . . 9 ((4 · 2) + 2) = (8 + 2)
220 8p2e10 12793 . . . . . . . . 9 (8 + 2) = 10
221219, 220eqtri 2755 . . . . . . . 8 ((4 · 2) + 2) = 10
22229, 30, 39, 3, 199, 214, 3, 39, 9, 217, 221decmac 12765 . . . . . . 7 ((34 · 2) + 2) = 70
2239, 3, 29, 3, 113, 198, 31, 39, 35, 213, 222decma2c 12766 . . . . . 6 ((34 · 12) + (15 + 17)) = 440
224 5t3e15 12814 . . . . . . . . 9 (5 · 3) = 15
22592, 99, 224mulcomli 11259 . . . . . . . 8 (3 · 5) = 15
226 5p2e7 12404 . . . . . . . 8 (5 + 2) = 7
2279, 11, 3, 225, 226decaddi 12773 . . . . . . 7 ((3 · 5) + 2) = 17
228 5t4e20 12815 . . . . . . . . 9 (5 · 4) = 20
22992, 207, 228mulcomli 11259 . . . . . . . 8 (4 · 5) = 20
23061addlidi 11438 . . . . . . . 8 (0 + 6) = 6
2313, 39, 2, 229, 230decaddi 12773 . . . . . . 7 ((4 · 5) + 6) = 26
23229, 30, 2, 199, 11, 2, 3, 227, 231decrmac 12771 . . . . . 6 ((34 · 5) + 6) = 176
23310, 11, 46, 2, 111, 193, 31, 2, 36, 223, 232decma2c 12766 . . . . 5 ((34 · 125) + (125 + 31)) = 4406
234 9cn 12348 . . . . . . . 8 9 ∈ ℂ
235 9t3e27 12836 . . . . . . . 8 (9 · 3) = 27
236234, 99, 235mulcomli 11259 . . . . . . 7 (3 · 9) = 27
237 7p4e11 12789 . . . . . . 7 (7 + 4) = 11
2383, 35, 30, 236, 73, 9, 237decaddci 12774 . . . . . 6 ((3 · 9) + 4) = 31
239 9t4e36 12837 . . . . . . . 8 (9 · 4) = 36
240234, 207, 239mulcomli 11259 . . . . . . 7 (4 · 9) = 36
241151, 61, 172addcomli 11442 . . . . . . 7 (6 + 8) = 14
24229, 2, 13, 240, 205, 30, 241decaddci 12774 . . . . . 6 ((4 · 9) + 8) = 44
24329, 30, 13, 199, 5, 30, 30, 238, 242decrmac 12771 . . . . 5 ((34 · 9) + 8) = 314
24412, 5, 12, 13, 17, 22, 31, 30, 187, 233, 243decma2c 12766 . . . 4 ((34 · 𝑁) + (𝑁 − 1)) = 44064
245 eqid 2727 . . . . 5 136 = 136
2469, 5deccl 12728 . . . . . 6 19 ∈ ℕ0
247246, 30deccl 12728 . . . . 5 194 ∈ ℕ0
248 eqid 2727 . . . . . 6 13 = 13
249 eqid 2727 . . . . . 6 194 = 194
2505, 35deccl 12728 . . . . . 6 97 ∈ ℕ0
2519, 9deccl 12728 . . . . . . 7 11 ∈ ℕ0
252 eqid 2727 . . . . . . 7 324 = 324
253 eqid 2727 . . . . . . . 8 19 = 19
254 eqid 2727 . . . . . . . 8 97 = 97
255234, 16, 120addcomli 11442 . . . . . . . . 9 (1 + 9) = 10
2569, 39, 145, 255decsuc 12744 . . . . . . . 8 ((1 + 9) + 1) = 11
257 9p7e16 12805 . . . . . . . 8 (9 + 7) = 16
2589, 5, 5, 35, 253, 254, 256, 2, 257decaddc 12768 . . . . . . 7 (19 + 97) = 116
259 eqid 2727 . . . . . . . 8 32 = 32
260 eqid 2727 . . . . . . . . 9 11 = 11
2619, 9, 114, 260decsuc 12744 . . . . . . . 8 (11 + 1) = 12
26289oveq1i 7434 . . . . . . . . 9 ((2 · 1) + 2) = (2 + 2)
263262, 115, 2113eqtri 2759 . . . . . . . 8 ((2 · 1) + 2) = 04
26429, 3, 9, 3, 259, 261, 9, 30, 39, 206, 263decmac 12765 . . . . . . 7 ((32 · 1) + (11 + 1)) = 44
265208oveq1i 7434 . . . . . . . 8 ((4 · 1) + 6) = (4 + 6)
266 6p4e10 12785 . . . . . . . . 9 (6 + 4) = 10
26761, 207, 266addcomli 11442 . . . . . . . 8 (4 + 6) = 10
268265, 267eqtri 2755 . . . . . . 7 ((4 · 1) + 6) = 10
26933, 30, 251, 2, 252, 258, 9, 39, 9, 264, 268decmac 12765 . . . . . 6 ((324 · 1) + (19 + 97)) = 440
270145, 138eqtri 2755 . . . . . . . 8 (0 + 1) = 01
271 3t3e9 12415 . . . . . . . . . 10 (3 · 3) = 9
272271, 139oveq12i 7436 . . . . . . . . 9 ((3 · 3) + (0 + 0)) = (9 + 0)
273234addridi 11437 . . . . . . . . 9 (9 + 0) = 9
274272, 273eqtri 2755 . . . . . . . 8 ((3 · 3) + (0 + 0)) = 9
275101oveq1i 7434 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
27635dec0h 12735 . . . . . . . . 9 7 = 07
277275, 216, 2763eqtri 2759 . . . . . . . 8 ((2 · 3) + 1) = 07
27829, 3, 39, 9, 259, 270, 29, 35, 39, 274, 277decmac 12765 . . . . . . 7 ((32 · 3) + (0 + 1)) = 97
279 4t3e12 12811 . . . . . . . 8 (4 · 3) = 12
280 4p2e6 12401 . . . . . . . . 9 (4 + 2) = 6
281207, 57, 280addcomli 11442 . . . . . . . 8 (2 + 4) = 6
2829, 3, 30, 279, 281decaddi 12773 . . . . . . 7 ((4 · 3) + 4) = 16
28333, 30, 39, 30, 252, 211, 29, 2, 9, 278, 282decmac 12765 . . . . . 6 ((324 · 3) + 4) = 976
2849, 29, 246, 30, 248, 249, 34, 2, 250, 269, 283decma2c 12766 . . . . 5 ((324 · 13) + 194) = 4406
285 6t3e18 12818 . . . . . . . . 9 (6 · 3) = 18
28661, 99, 285mulcomli 11259 . . . . . . . 8 (3 · 6) = 18
2879, 13, 18, 286decsuc 12744 . . . . . . 7 ((3 · 6) + 1) = 19
2889, 3, 3, 63, 115decaddi 12773 . . . . . . 7 ((2 · 6) + 2) = 14
28929, 3, 3, 259, 2, 30, 9, 287, 288decrmac 12771 . . . . . 6 ((32 · 6) + 2) = 194
290 6t4e24 12819 . . . . . . 7 (6 · 4) = 24
29161, 207, 290mulcomli 11259 . . . . . 6 (4 · 6) = 24
2922, 33, 30, 252, 30, 3, 289, 291decmul1c 12778 . . . . 5 (324 · 6) = 1944
29334, 37, 2, 245, 30, 247, 284, 292decmul2c 12779 . . . 4 (324 · 136) = 44064
294244, 293eqtr4i 2758 . . 3 ((34 · 𝑁) + (𝑁 − 1)) = (324 · 136)
29526, 1, 28, 32, 34, 23, 36, 38, 178, 179, 186, 294modxai 17042 . 2 ((2↑629) mod 𝑁) = ((𝑁 − 1) mod 𝑁)
296 eqid 2727 . . . 4 629 = 629
297 eqid 2727 . . . . 5 62 = 62
298139oveq2i 7435 . . . . . 6 ((2 · 6) + (0 + 0)) = ((2 · 6) + 0)
29963oveq1i 7434 . . . . . 6 ((2 · 6) + 0) = (12 + 0)
30010nn0cni 12520 . . . . . . 7 12 ∈ ℂ
301300addridi 11437 . . . . . 6 (12 + 0) = 12
302298, 299, 3013eqtri 2759 . . . . 5 ((2 · 6) + (0 + 0)) = 12
30311dec0h 12735 . . . . . 6 5 = 05
30481, 55, 3033eqtri 2759 . . . . 5 ((2 · 2) + 1) = 05
3052, 3, 39, 9, 297, 138, 3, 11, 39, 302, 304decma2c 12766 . . . 4 ((2 · 62) + 1) = 125
306 9t2e18 12835 . . . . 5 (9 · 2) = 18
307234, 57, 306mulcomli 11259 . . . 4 (2 · 9) = 18
3083, 4, 5, 296, 13, 9, 305, 307decmul2c 12779 . . 3 (2 · 629) = 1258
309308, 22eqtr4i 2758 . 2 (2 · 629) = (𝑁 − 1)
310 npcan 11505 . . 3 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
31167, 16, 310mp2an 690 . 2 ((𝑁 − 1) + 1) = 𝑁
31268oveq1i 7434 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
313145, 312, 1613eqtr4i 2765 . 2 ((0 · 𝑁) + 1) = (1 · 1)
3141, 6, 7, 8, 9, 23, 295, 309, 311, 313mod2xnegi 17045 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  wcel 2098  (class class class)co 7424  cc 11142  0cc0 11144  1c1 11145   + caddc 11147   · cmul 11149  cmin 11480  cn 12248  2c2 12303  3c3 12304  4c4 12305  5c5 12306  6c6 12307  7c7 12308  8c8 12309  9c9 12310  0cn0 12508  cdc 12713   mod cmo 13872  cexp 14064
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 2698  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221  ax-pre-sup 11222
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 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-iun 5000  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7875  df-2nd 7998  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-er 8729  df-en 8969  df-dom 8970  df-sdom 8971  df-sup 9471  df-inf 9472  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317  df-9 12318  df-n0 12509  df-z 12595  df-dec 12714  df-uz 12859  df-rp 13013  df-fl 13795  df-mod 13873  df-seq 14005  df-exp 14065
This theorem is referenced by:  1259prm  17110
  Copyright terms: Public domain W3C validator