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

Theorem 1259lem4 15776
Description: Lemma for 1259prm 15778. 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 11137 . 2 2 ∈ ℕ
2 6nn0 11265 . . . 4 6 ∈ ℕ0
3 2nn0 11261 . . . 4 2 ∈ ℕ0
42, 3deccl 11464 . . 3 62 ∈ ℕ0
5 9nn0 11268 . . 3 9 ∈ ℕ0
64, 5deccl 11464 . 2 629 ∈ ℕ0
7 0z 11340 . 2 0 ∈ ℤ
8 1nn 10983 . 2 1 ∈ ℕ
9 1nn0 11260 . 2 1 ∈ ℕ0
109, 3deccl 11464 . . . . . . 7 12 ∈ ℕ0
11 5nn0 11264 . . . . . . 7 5 ∈ ℕ0
1210, 11deccl 11464 . . . . . 6 125 ∈ ℕ0
13 8nn0 11267 . . . . . 6 8 ∈ ℕ0
1412, 13deccl 11464 . . . . 5 1258 ∈ ℕ0
1514nn0cni 11256 . . . 4 1258 ∈ ℂ
16 ax-1cn 9946 . . . 4 1 ∈ ℂ
17 1259prm.1 . . . . 5 𝑁 = 1259
18 8p1e9 11110 . . . . . 6 (8 + 1) = 9
19 eqid 2621 . . . . . 6 1258 = 1258
2012, 13, 18, 19decsuc 11487 . . . . 5 (1258 + 1) = 1259
2117, 20eqtr4i 2646 . . . 4 𝑁 = (1258 + 1)
2215, 16, 21mvrraddi 10250 . . 3 (𝑁 − 1) = 1258
2322, 14eqeltri 2694 . 2 (𝑁 − 1) ∈ ℕ0
24 9nn 11144 . . . . 5 9 ∈ ℕ
2512, 24decnncl 11470 . . . 4 1259 ∈ ℕ
2617, 25eqeltri 2694 . . 3 𝑁 ∈ ℕ
272, 9deccl 11464 . . . 4 61 ∈ ℕ0
2827, 3deccl 11464 . . 3 612 ∈ ℕ0
29 3nn0 11262 . . . . 5 3 ∈ ℕ0
30 4nn0 11263 . . . . 5 4 ∈ ℕ0
3129, 30deccl 11464 . . . 4 34 ∈ ℕ0
3231nn0zi 11354 . . 3 34 ∈ ℤ
3329, 3deccl 11464 . . . 4 32 ∈ ℕ0
3433, 30deccl 11464 . . 3 324 ∈ ℕ0
35 7nn0 11266 . . . 4 7 ∈ ℕ0
369, 35deccl 11464 . . 3 17 ∈ ℕ0
379, 29deccl 11464 . . . 4 13 ∈ ℕ0
3837, 2deccl 11464 . . 3 136 ∈ ℕ0
39 0nn0 11259 . . . . . 6 0 ∈ ℕ0
4029, 39deccl 11464 . . . . 5 30 ∈ ℕ0
4140, 2deccl 11464 . . . 4 306 ∈ ℕ0
42 8nn 11143 . . . . 5 8 ∈ ℕ
439, 42decnncl 11470 . . . 4 18 ∈ ℕ
4410, 30deccl 11464 . . . . 5 124 ∈ ℕ0
4544, 9deccl 11464 . . . 4 1241 ∈ ℕ0
469, 11deccl 11464 . . . . . 6 15 ∈ ℕ0
4746, 29deccl 11464 . . . . 5 153 ∈ ℕ0
48 1z 11359 . . . . 5 1 ∈ ℤ
4911, 39deccl 11464 . . . . 5 50 ∈ ℕ0
5046, 3deccl 11464 . . . . . 6 152 ∈ ℕ0
513, 11deccl 11464 . . . . . 6 25 ∈ ℕ0
5235, 2deccl 11464 . . . . . . 7 76 ∈ ℕ0
53171259lem3 15775 . . . . . . 7 ((2↑76) mod 𝑁) = (5 mod 𝑁)
54 eqid 2621 . . . . . . . 8 76 = 76
55 4p1e5 11106 . . . . . . . . 9 (4 + 1) = 5
56 7cn 11056 . . . . . . . . . 10 7 ∈ ℂ
57 2cn 11043 . . . . . . . . . 10 2 ∈ ℂ
58 7t2e14 11600 . . . . . . . . . 10 (7 · 2) = 14
5956, 57, 58mulcomli 9999 . . . . . . . . 9 (2 · 7) = 14
609, 30, 55, 59decsuc 11487 . . . . . . . 8 ((2 · 7) + 1) = 15
61 6cn 11054 . . . . . . . . 9 6 ∈ ℂ
62 6t2e12 11593 . . . . . . . . 9 (6 · 2) = 12
6361, 57, 62mulcomli 9999 . . . . . . . 8 (2 · 6) = 12
643, 35, 2, 54, 3, 9, 60, 63decmul2c 11541 . . . . . . 7 (2 · 76) = 152
6551nn0cni 11256 . . . . . . . . 9 25 ∈ ℂ
6665addid2i 10176 . . . . . . . 8 (0 + 25) = 25
6726nncni 10982 . . . . . . . . . 10 𝑁 ∈ ℂ
6867mul02i 10177 . . . . . . . . 9 (0 · 𝑁) = 0
6968oveq1i 6620 . . . . . . . 8 ((0 · 𝑁) + 25) = (0 + 25)
70 5t5e25 11591 . . . . . . . 8 (5 · 5) = 25
7166, 69, 703eqtr4i 2653 . . . . . . 7 ((0 · 𝑁) + 25) = (5 · 5)
7226, 1, 52, 7, 11, 51, 53, 64, 71mod2xi 15708 . . . . . 6 ((2↑152) mod 𝑁) = (25 mod 𝑁)
73 2p1e3 11103 . . . . . . 7 (2 + 1) = 3
74 eqid 2621 . . . . . . 7 152 = 152
7546, 3, 73, 74decsuc 11487 . . . . . 6 (152 + 1) = 153
7649nn0cni 11256 . . . . . . . 8 50 ∈ ℂ
7776addid2i 10176 . . . . . . 7 (0 + 50) = 50
7868oveq1i 6620 . . . . . . 7 ((0 · 𝑁) + 50) = (0 + 50)
79 eqid 2621 . . . . . . . 8 25 = 25
80 2t2e4 11129 . . . . . . . . . 10 (2 · 2) = 4
8180oveq1i 6620 . . . . . . . . 9 ((2 · 2) + 1) = (4 + 1)
8281, 55eqtri 2643 . . . . . . . 8 ((2 · 2) + 1) = 5
83 5t2e10 11586 . . . . . . . 8 (5 · 2) = 10
843, 3, 11, 79, 39, 9, 82, 83decmul1c 11539 . . . . . . 7 (25 · 2) = 50
8577, 78, 843eqtr4i 2653 . . . . . 6 ((0 · 𝑁) + 50) = (25 · 2)
8626, 1, 50, 7, 51, 49, 72, 75, 85modxp1i 15709 . . . . 5 ((2↑153) mod 𝑁) = (50 mod 𝑁)
87 eqid 2621 . . . . . 6 153 = 153
88 eqid 2621 . . . . . . . . 9 15 = 15
8957mulid1i 9994 . . . . . . . . . . 11 (2 · 1) = 2
9089oveq1i 6620 . . . . . . . . . 10 ((2 · 1) + 1) = (2 + 1)
9190, 73eqtri 2643 . . . . . . . . 9 ((2 · 1) + 1) = 3
92 5cn 11052 . . . . . . . . . 10 5 ∈ ℂ
9392, 57, 83mulcomli 9999 . . . . . . . . 9 (2 · 5) = 10
943, 9, 11, 88, 39, 9, 91, 93decmul2c 11541 . . . . . . . 8 (2 · 15) = 30
9594oveq1i 6620 . . . . . . 7 ((2 · 15) + 0) = (30 + 0)
9640nn0cni 11256 . . . . . . . 8 30 ∈ ℂ
9796addid1i 10175 . . . . . . 7 (30 + 0) = 30
9895, 97eqtri 2643 . . . . . 6 ((2 · 15) + 0) = 30
99 3cn 11047 . . . . . . . 8 3 ∈ ℂ
100 3t2e6 11131 . . . . . . . 8 (3 · 2) = 6
10199, 57, 100mulcomli 9999 . . . . . . 7 (2 · 3) = 6
1022dec0h 11474 . . . . . . 7 6 = 06
103101, 102eqtri 2643 . . . . . 6 (2 · 3) = 06
1043, 46, 29, 87, 2, 39, 98, 103decmul2c 11541 . . . . 5 (2 · 153) = 306
10567mulid2i 9995 . . . . . . . 8 (1 · 𝑁) = 𝑁
106105, 17eqtri 2643 . . . . . . 7 (1 · 𝑁) = 1259
107 eqid 2621 . . . . . . 7 1241 = 1241
1083, 30deccl 11464 . . . . . . . 8 24 ∈ ℕ0
109 eqid 2621 . . . . . . . . 9 24 = 24
1103, 30, 55, 109decsuc 11487 . . . . . . . 8 (24 + 1) = 25
111 eqid 2621 . . . . . . . . 9 125 = 125
112 eqid 2621 . . . . . . . . 9 124 = 124
113 eqid 2621 . . . . . . . . . 10 12 = 12
114 1p1e2 11086 . . . . . . . . . 10 (1 + 1) = 2
115 2p2e4 11096 . . . . . . . . . 10 (2 + 2) = 4
1169, 3, 9, 3, 113, 113, 114, 115decadd 11522 . . . . . . . . 9 (12 + 12) = 24
117 5p4e9 11119 . . . . . . . . 9 (5 + 4) = 9
11810, 11, 10, 30, 111, 112, 116, 117decadd 11522 . . . . . . . 8 (125 + 124) = 249
119108, 110, 118decsucc 11502 . . . . . . 7 ((125 + 124) + 1) = 250
120 9p1e10 11448 . . . . . . 7 (9 + 1) = 10
12112, 5, 44, 9, 106, 107, 119, 120decaddc2 11527 . . . . . 6 ((1 · 𝑁) + 1241) = 2500
122 eqid 2621 . . . . . . 7 50 = 50
12392mul02i 10177 . . . . . . . . . 10 (0 · 5) = 0
12411, 11, 39, 122, 39, 70, 123decmul1 11537 . . . . . . . . 9 (50 · 5) = 250
125124oveq1i 6620 . . . . . . . 8 ((50 · 5) + 0) = (250 + 0)
12651, 39deccl 11464 . . . . . . . . . 10 250 ∈ ℕ0
127126nn0cni 11256 . . . . . . . . 9 250 ∈ ℂ
128127addid1i 10175 . . . . . . . 8 (250 + 0) = 250
129125, 128eqtri 2643 . . . . . . 7 ((50 · 5) + 0) = 250
13076mul01i 10178 . . . . . . . 8 (50 · 0) = 0
13139dec0h 11474 . . . . . . . 8 0 = 00
132130, 131eqtri 2643 . . . . . . 7 (50 · 0) = 00
13349, 11, 39, 122, 39, 39, 129, 132decmul2c 11541 . . . . . 6 (50 · 50) = 2500
134121, 133eqtr4i 2646 . . . . 5 ((1 · 𝑁) + 1241) = (50 · 50)
13526, 1, 47, 48, 49, 45, 86, 104, 134mod2xi 15708 . . . 4 ((2↑306) mod 𝑁) = (1241 mod 𝑁)
136 eqid 2621 . . . . 5 306 = 306
137 eqid 2621 . . . . . 6 30 = 30
1389dec0h 11474 . . . . . 6 1 = 01
139 00id 10163 . . . . . . . 8 (0 + 0) = 0
140101, 139oveq12i 6622 . . . . . . 7 ((2 · 3) + (0 + 0)) = (6 + 0)
14161addid1i 10175 . . . . . . 7 (6 + 0) = 6
142140, 141eqtri 2643 . . . . . 6 ((2 · 3) + (0 + 0)) = 6
14357mul01i 10178 . . . . . . . 8 (2 · 0) = 0
144143oveq1i 6620 . . . . . . 7 ((2 · 0) + 1) = (0 + 1)
145 0p1e1 11084 . . . . . . 7 (0 + 1) = 1
146144, 145, 1383eqtri 2647 . . . . . 6 ((2 · 0) + 1) = 01
14729, 39, 39, 9, 137, 138, 3, 9, 39, 142, 146decma2c 11520 . . . . 5 ((2 · 30) + 1) = 61
1483, 40, 2, 136, 3, 9, 147, 63decmul2c 11541 . . . 4 (2 · 306) = 612
149 eqid 2621 . . . . . 6 18 = 18
15010, 30, 55, 112decsuc 11487 . . . . . 6 (124 + 1) = 125
151 8cn 11058 . . . . . . 7 8 ∈ ℂ
152151, 16, 18addcomli 10180 . . . . . 6 (1 + 8) = 9
15344, 9, 9, 13, 107, 149, 150, 152decadd 11522 . . . . 5 (1241 + 18) = 1259
154153, 17eqtr4i 2646 . . . 4 (1241 + 18) = 𝑁
15534nn0cni 11256 . . . . . 6 324 ∈ ℂ
156155addid2i 10176 . . . . 5 (0 + 324) = 324
15768oveq1i 6620 . . . . 5 ((0 · 𝑁) + 324) = (0 + 324)
1589, 13deccl 11464 . . . . . 6 18 ∈ ℕ0
1599, 30deccl 11464 . . . . . 6 14 ∈ ℕ0
160 eqid 2621 . . . . . . 7 14 = 14
16116mulid1i 9994 . . . . . . . . 9 (1 · 1) = 1
162161, 114oveq12i 6622 . . . . . . . 8 ((1 · 1) + (1 + 1)) = (1 + 2)
163 1p2e3 11104 . . . . . . . 8 (1 + 2) = 3
164162, 163eqtri 2643 . . . . . . 7 ((1 · 1) + (1 + 1)) = 3
165151mulid1i 9994 . . . . . . . . 9 (8 · 1) = 8
166165oveq1i 6620 . . . . . . . 8 ((8 · 1) + 4) = (8 + 4)
167 8p4e12 11566 . . . . . . . 8 (8 + 4) = 12
168166, 167eqtri 2643 . . . . . . 7 ((8 · 1) + 4) = 12
1699, 13, 9, 30, 149, 160, 9, 3, 9, 164, 168decmac 11518 . . . . . 6 ((18 · 1) + 14) = 32
170151mulid2i 9995 . . . . . . . . 9 (1 · 8) = 8
171170oveq1i 6620 . . . . . . . 8 ((1 · 8) + 6) = (8 + 6)
172 8p6e14 11568 . . . . . . . 8 (8 + 6) = 14
173171, 172eqtri 2643 . . . . . . 7 ((1 · 8) + 6) = 14
174 8t8e64 11614 . . . . . . 7 (8 · 8) = 64
17513, 9, 13, 149, 30, 2, 173, 174decmul1c 11539 . . . . . 6 (18 · 8) = 144
176158, 9, 13, 149, 30, 159, 169, 175decmul2c 11541 . . . . 5 (18 · 18) = 324
177156, 157, 1763eqtr4i 2653 . . . 4 ((0 · 𝑁) + 324) = (18 · 18)
1781, 41, 7, 43, 34, 45, 135, 148, 154, 177mod2xnegi 15710 . . 3 ((2↑612) mod 𝑁) = (324 mod 𝑁)
179171259lem1 15773 . . 3 ((2↑17) mod 𝑁) = (136 mod 𝑁)
180 eqid 2621 . . . 4 612 = 612
181 eqid 2621 . . . 4 17 = 17
182 eqid 2621 . . . . 5 61 = 61
1832, 9, 114, 182decsuc 11487 . . . 4 (61 + 1) = 62
184 7p2e9 11124 . . . . 5 (7 + 2) = 9
18556, 57, 184addcomli 10180 . . . 4 (2 + 7) = 9
18627, 3, 9, 35, 180, 181, 183, 185decadd 11522 . . 3 (612 + 17) = 629
18729, 9deccl 11464 . . . . 5 31 ∈ ℕ0
188 eqid 2621 . . . . . . 7 31 = 31
189 3p2e5 11112 . . . . . . . . 9 (3 + 2) = 5
19099, 57, 189addcomli 10180 . . . . . . . 8 (2 + 3) = 5
1919, 3, 29, 113, 190decaddi 11531 . . . . . . 7 (12 + 3) = 15
192 5p1e6 11107 . . . . . . 7 (5 + 1) = 6
19310, 11, 29, 9, 111, 188, 191, 192decadd 11522 . . . . . 6 (125 + 31) = 156
194114oveq1i 6620 . . . . . . . . 9 ((1 + 1) + 1) = (2 + 1)
195194, 73eqtri 2643 . . . . . . . 8 ((1 + 1) + 1) = 3
196 7p5e12 11559 . . . . . . . . 9 (7 + 5) = 12
19756, 92, 196addcomli 10180 . . . . . . . 8 (5 + 7) = 12
1989, 11, 9, 35, 88, 181, 195, 3, 197decaddc 11524 . . . . . . 7 (15 + 17) = 32
199 eqid 2621 . . . . . . . 8 34 = 34
200 7p3e10 11555 . . . . . . . . 9 (7 + 3) = 10
20156, 99, 200addcomli 10180 . . . . . . . 8 (3 + 7) = 10
20299mulid1i 9994 . . . . . . . . . 10 (3 · 1) = 3
20316addid1i 10175 . . . . . . . . . 10 (1 + 0) = 1
204202, 203oveq12i 6622 . . . . . . . . 9 ((3 · 1) + (1 + 0)) = (3 + 1)
205 3p1e4 11105 . . . . . . . . 9 (3 + 1) = 4
206204, 205eqtri 2643 . . . . . . . 8 ((3 · 1) + (1 + 0)) = 4
207 4cn 11050 . . . . . . . . . . 11 4 ∈ ℂ
208207mulid1i 9994 . . . . . . . . . 10 (4 · 1) = 4
209208oveq1i 6620 . . . . . . . . 9 ((4 · 1) + 0) = (4 + 0)
210207addid1i 10175 . . . . . . . . 9 (4 + 0) = 4
21130dec0h 11474 . . . . . . . . 9 4 = 04
212209, 210, 2113eqtri 2647 . . . . . . . 8 ((4 · 1) + 0) = 04
21329, 30, 9, 39, 199, 201, 9, 30, 39, 206, 212decmac 11518 . . . . . . 7 ((34 · 1) + (3 + 7)) = 44
2143dec0h 11474 . . . . . . . 8 2 = 02
215100, 145oveq12i 6622 . . . . . . . . 9 ((3 · 2) + (0 + 1)) = (6 + 1)
216 6p1e7 11108 . . . . . . . . 9 (6 + 1) = 7
217215, 216eqtri 2643 . . . . . . . 8 ((3 · 2) + (0 + 1)) = 7
218 4t2e8 11133 . . . . . . . . . 10 (4 · 2) = 8
219218oveq1i 6620 . . . . . . . . 9 ((4 · 2) + 2) = (8 + 2)
220 8p2e10 11562 . . . . . . . . 9 (8 + 2) = 10
221219, 220eqtri 2643 . . . . . . . 8 ((4 · 2) + 2) = 10
22229, 30, 39, 3, 199, 214, 3, 39, 9, 217, 221decmac 11518 . . . . . . 7 ((34 · 2) + 2) = 70
2239, 3, 29, 3, 113, 198, 31, 39, 35, 213, 222decma2c 11520 . . . . . 6 ((34 · 12) + (15 + 17)) = 440
224 5t3e15 11587 . . . . . . . . 9 (5 · 3) = 15
22592, 99, 224mulcomli 9999 . . . . . . . 8 (3 · 5) = 15
226 5p2e7 11117 . . . . . . . 8 (5 + 2) = 7
2279, 11, 3, 225, 226decaddi 11531 . . . . . . 7 ((3 · 5) + 2) = 17
228 5t4e20 11589 . . . . . . . . 9 (5 · 4) = 20
22992, 207, 228mulcomli 9999 . . . . . . . 8 (4 · 5) = 20
23061addid2i 10176 . . . . . . . 8 (0 + 6) = 6
2313, 39, 2, 229, 230decaddi 11531 . . . . . . 7 ((4 · 5) + 6) = 26
23229, 30, 2, 199, 11, 2, 3, 227, 231decrmac 11529 . . . . . 6 ((34 · 5) + 6) = 176
23310, 11, 46, 2, 111, 193, 31, 2, 36, 223, 232decma2c 11520 . . . . 5 ((34 · 125) + (125 + 31)) = 4406
234 9cn 11060 . . . . . . . 8 9 ∈ ℂ
235 9t3e27 11616 . . . . . . . 8 (9 · 3) = 27
236234, 99, 235mulcomli 9999 . . . . . . 7 (3 · 9) = 27
237 7p4e11 11557 . . . . . . 7 (7 + 4) = 11
2383, 35, 30, 236, 73, 9, 237decaddci 11532 . . . . . 6 ((3 · 9) + 4) = 31
239 9t4e36 11617 . . . . . . . 8 (9 · 4) = 36
240234, 207, 239mulcomli 9999 . . . . . . 7 (4 · 9) = 36
241151, 61, 172addcomli 10180 . . . . . . 7 (6 + 8) = 14
24229, 2, 13, 240, 205, 30, 241decaddci 11532 . . . . . 6 ((4 · 9) + 8) = 44
24329, 30, 13, 199, 5, 30, 30, 238, 242decrmac 11529 . . . . 5 ((34 · 9) + 8) = 314
24412, 5, 12, 13, 17, 22, 31, 30, 187, 233, 243decma2c 11520 . . . 4 ((34 · 𝑁) + (𝑁 − 1)) = 44064
245 eqid 2621 . . . . 5 136 = 136
2469, 5deccl 11464 . . . . . 6 19 ∈ ℕ0
247246, 30deccl 11464 . . . . 5 194 ∈ ℕ0
248 eqid 2621 . . . . . 6 13 = 13
249 eqid 2621 . . . . . 6 194 = 194
2505, 35deccl 11464 . . . . . 6 97 ∈ ℕ0
2519, 9deccl 11464 . . . . . . 7 11 ∈ ℕ0
252 eqid 2621 . . . . . . 7 324 = 324
253 eqid 2621 . . . . . . . 8 19 = 19
254 eqid 2621 . . . . . . . 8 97 = 97
255234, 16, 120addcomli 10180 . . . . . . . . 9 (1 + 9) = 10
2569, 39, 145, 255decsuc 11487 . . . . . . . 8 ((1 + 9) + 1) = 11
257 9p7e16 11577 . . . . . . . 8 (9 + 7) = 16
2589, 5, 5, 35, 253, 254, 256, 2, 257decaddc 11524 . . . . . . 7 (19 + 97) = 116
259 eqid 2621 . . . . . . . 8 32 = 32
260 eqid 2621 . . . . . . . . 9 11 = 11
2619, 9, 114, 260decsuc 11487 . . . . . . . 8 (11 + 1) = 12
26289oveq1i 6620 . . . . . . . . 9 ((2 · 1) + 2) = (2 + 2)
263262, 115, 2113eqtri 2647 . . . . . . . 8 ((2 · 1) + 2) = 04
26429, 3, 9, 3, 259, 261, 9, 30, 39, 206, 263decmac 11518 . . . . . . 7 ((32 · 1) + (11 + 1)) = 44
265208oveq1i 6620 . . . . . . . 8 ((4 · 1) + 6) = (4 + 6)
266 6p4e10 11550 . . . . . . . . 9 (6 + 4) = 10
26761, 207, 266addcomli 10180 . . . . . . . 8 (4 + 6) = 10
268265, 267eqtri 2643 . . . . . . 7 ((4 · 1) + 6) = 10
26933, 30, 251, 2, 252, 258, 9, 39, 9, 264, 268decmac 11518 . . . . . 6 ((324 · 1) + (19 + 97)) = 440
270145, 138eqtri 2643 . . . . . . . 8 (0 + 1) = 01
271 3t3e9 11132 . . . . . . . . . 10 (3 · 3) = 9
272271, 139oveq12i 6622 . . . . . . . . 9 ((3 · 3) + (0 + 0)) = (9 + 0)
273234addid1i 10175 . . . . . . . . 9 (9 + 0) = 9
274272, 273eqtri 2643 . . . . . . . 8 ((3 · 3) + (0 + 0)) = 9
275101oveq1i 6620 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
27635dec0h 11474 . . . . . . . . 9 7 = 07
277275, 216, 2763eqtri 2647 . . . . . . . 8 ((2 · 3) + 1) = 07
27829, 3, 39, 9, 259, 270, 29, 35, 39, 274, 277decmac 11518 . . . . . . 7 ((32 · 3) + (0 + 1)) = 97
279 4t3e12 11584 . . . . . . . 8 (4 · 3) = 12
280 4p2e6 11114 . . . . . . . . 9 (4 + 2) = 6
281207, 57, 280addcomli 10180 . . . . . . . 8 (2 + 4) = 6
2829, 3, 30, 279, 281decaddi 11531 . . . . . . 7 ((4 · 3) + 4) = 16
28333, 30, 39, 30, 252, 211, 29, 2, 9, 278, 282decmac 11518 . . . . . 6 ((324 · 3) + 4) = 976
2849, 29, 246, 30, 248, 249, 34, 2, 250, 269, 283decma2c 11520 . . . . 5 ((324 · 13) + 194) = 4406
285 6t3e18 11594 . . . . . . . . 9 (6 · 3) = 18
28661, 99, 285mulcomli 9999 . . . . . . . 8 (3 · 6) = 18
2879, 13, 18, 286decsuc 11487 . . . . . . 7 ((3 · 6) + 1) = 19
2889, 3, 3, 63, 115decaddi 11531 . . . . . . 7 ((2 · 6) + 2) = 14
28929, 3, 3, 259, 2, 30, 9, 287, 288decrmac 11529 . . . . . 6 ((32 · 6) + 2) = 194
290 6t4e24 11595 . . . . . . 7 (6 · 4) = 24
29161, 207, 290mulcomli 9999 . . . . . 6 (4 · 6) = 24
2922, 33, 30, 252, 30, 3, 289, 291decmul1c 11539 . . . . 5 (324 · 6) = 1944
29334, 37, 2, 245, 30, 247, 284, 292decmul2c 11541 . . . 4 (324 · 136) = 44064
294244, 293eqtr4i 2646 . . 3 ((34 · 𝑁) + (𝑁 − 1)) = (324 · 136)
29526, 1, 28, 32, 34, 23, 36, 38, 178, 179, 186, 294modxai 15707 . 2 ((2↑629) mod 𝑁) = ((𝑁 − 1) mod 𝑁)
296 eqid 2621 . . . 4 629 = 629
297 eqid 2621 . . . . 5 62 = 62
298139oveq2i 6621 . . . . . 6 ((2 · 6) + (0 + 0)) = ((2 · 6) + 0)
29963oveq1i 6620 . . . . . 6 ((2 · 6) + 0) = (12 + 0)
30010nn0cni 11256 . . . . . . 7 12 ∈ ℂ
301300addid1i 10175 . . . . . 6 (12 + 0) = 12
302298, 299, 3013eqtri 2647 . . . . 5 ((2 · 6) + (0 + 0)) = 12
30311dec0h 11474 . . . . . 6 5 = 05
30481, 55, 3033eqtri 2647 . . . . 5 ((2 · 2) + 1) = 05
3052, 3, 39, 9, 297, 138, 3, 11, 39, 302, 304decma2c 11520 . . . 4 ((2 · 62) + 1) = 125
306 9t2e18 11615 . . . . 5 (9 · 2) = 18
307234, 57, 306mulcomli 9999 . . . 4 (2 · 9) = 18
3083, 4, 5, 296, 13, 9, 305, 307decmul2c 11541 . . 3 (2 · 629) = 1258
309308, 22eqtr4i 2646 . 2 (2 · 629) = (𝑁 − 1)
310 npcan 10242 . . 3 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
31167, 16, 310mp2an 707 . 2 ((𝑁 − 1) + 1) = 𝑁
31268oveq1i 6620 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
313145, 312, 1613eqtr4i 2653 . 2 ((0 · 𝑁) + 1) = (1 · 1)
3141, 6, 7, 8, 9, 23, 295, 309, 311, 313mod2xnegi 15710 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wcel 1987  (class class class)co 6610  cc 9886  0cc0 9888  1c1 9889   + caddc 9891   · cmul 9893  cmin 10218  cn 10972  2c2 11022  3c3 11023  4c4 11024  5c5 11025  6c6 11026  7c7 11027  8c8 11028  9c9 11029  0cn0 11244  cdc 11445   mod cmo 12616  cexp 12808
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9944  ax-resscn 9945  ax-1cn 9946  ax-icn 9947  ax-addcl 9948  ax-addrcl 9949  ax-mulcl 9950  ax-mulrcl 9951  ax-mulcom 9952  ax-addass 9953  ax-mulass 9954  ax-distr 9955  ax-i2m1 9956  ax-1ne0 9957  ax-1rid 9958  ax-rnegex 9959  ax-rrecex 9960  ax-cnre 9961  ax-pre-lttri 9962  ax-pre-lttrn 9963  ax-pre-ltadd 9964  ax-pre-mulgt0 9965  ax-pre-sup 9966
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-er 7694  df-en 7908  df-dom 7909  df-sdom 7910  df-sup 8300  df-inf 8301  df-pnf 10028  df-mnf 10029  df-xr 10030  df-ltxr 10031  df-le 10032  df-sub 10220  df-neg 10221  df-div 10637  df-nn 10973  df-2 11031  df-3 11032  df-4 11033  df-5 11034  df-6 11035  df-7 11036  df-8 11037  df-9 11038  df-n0 11245  df-z 11330  df-dec 11446  df-uz 11640  df-rp 11785  df-fl 12541  df-mod 12617  df-seq 12750  df-exp 12809
This theorem is referenced by:  1259prm  15778
  Copyright terms: Public domain W3C validator