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

Theorem 1259lem4 16206
 Description: Lemma for 1259prm 16208. 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 11424 . 2 2 ∈ ℕ
2 6nn0 11641 . . . 4 6 ∈ ℕ0
3 2nn0 11637 . . . 4 2 ∈ ℕ0
42, 3deccl 11836 . . 3 62 ∈ ℕ0
5 9nn0 11644 . . 3 9 ∈ ℕ0
64, 5deccl 11836 . 2 629 ∈ ℕ0
7 0z 11715 . 2 0 ∈ ℤ
8 1nn 11363 . 2 1 ∈ ℕ
9 1nn0 11636 . 2 1 ∈ ℕ0
109, 3deccl 11836 . . . . . . 7 12 ∈ ℕ0
11 5nn0 11640 . . . . . . 7 5 ∈ ℕ0
1210, 11deccl 11836 . . . . . 6 125 ∈ ℕ0
13 8nn0 11643 . . . . . 6 8 ∈ ℕ0
1412, 13deccl 11836 . . . . 5 1258 ∈ ℕ0
1514nn0cni 11631 . . . 4 1258 ∈ ℂ
16 ax-1cn 10310 . . . 4 1 ∈ ℂ
17 1259prm.1 . . . . 5 𝑁 = 1259
18 8p1e9 11508 . . . . . 6 (8 + 1) = 9
19 eqid 2825 . . . . . 6 1258 = 1258
2012, 13, 18, 19decsuc 11853 . . . . 5 (1258 + 1) = 1259
2117, 20eqtr4i 2852 . . . 4 𝑁 = (1258 + 1)
2215, 16, 21mvrraddi 10619 . . 3 (𝑁 − 1) = 1258
2322, 14eqeltri 2902 . 2 (𝑁 − 1) ∈ ℕ0
24 9nn 11455 . . . . 5 9 ∈ ℕ
2512, 24decnncl 11842 . . . 4 1259 ∈ ℕ
2617, 25eqeltri 2902 . . 3 𝑁 ∈ ℕ
272, 9deccl 11836 . . . 4 61 ∈ ℕ0
2827, 3deccl 11836 . . 3 612 ∈ ℕ0
29 3nn0 11638 . . . . 5 3 ∈ ℕ0
30 4nn0 11639 . . . . 5 4 ∈ ℕ0
3129, 30deccl 11836 . . . 4 34 ∈ ℕ0
3231nn0zi 11730 . . 3 34 ∈ ℤ
3329, 3deccl 11836 . . . 4 32 ∈ ℕ0
3433, 30deccl 11836 . . 3 324 ∈ ℕ0
35 7nn0 11642 . . . 4 7 ∈ ℕ0
369, 35deccl 11836 . . 3 17 ∈ ℕ0
379, 29deccl 11836 . . . 4 13 ∈ ℕ0
3837, 2deccl 11836 . . 3 136 ∈ ℕ0
39 0nn0 11635 . . . . . 6 0 ∈ ℕ0
4029, 39deccl 11836 . . . . 5 30 ∈ ℕ0
4140, 2deccl 11836 . . . 4 306 ∈ ℕ0
42 8nn 11451 . . . . 5 8 ∈ ℕ
439, 42decnncl 11842 . . . 4 18 ∈ ℕ
4410, 30deccl 11836 . . . . 5 124 ∈ ℕ0
4544, 9deccl 11836 . . . 4 1241 ∈ ℕ0
469, 11deccl 11836 . . . . . 6 15 ∈ ℕ0
4746, 29deccl 11836 . . . . 5 153 ∈ ℕ0
48 1z 11735 . . . . 5 1 ∈ ℤ
4911, 39deccl 11836 . . . . 5 50 ∈ ℕ0
5046, 3deccl 11836 . . . . . 6 152 ∈ ℕ0
513, 11deccl 11836 . . . . . 6 25 ∈ ℕ0
5235, 2deccl 11836 . . . . . . 7 76 ∈ ℕ0
53171259lem3 16205 . . . . . . 7 ((2↑76) mod 𝑁) = (5 mod 𝑁)
54 eqid 2825 . . . . . . . 8 76 = 76
55 4p1e5 11504 . . . . . . . . 9 (4 + 1) = 5
56 7cn 11449 . . . . . . . . . 10 7 ∈ ℂ
57 2cn 11426 . . . . . . . . . 10 2 ∈ ℂ
58 7t2e14 11932 . . . . . . . . . 10 (7 · 2) = 14
5956, 57, 58mulcomli 10366 . . . . . . . . 9 (2 · 7) = 14
609, 30, 55, 59decsuc 11853 . . . . . . . 8 ((2 · 7) + 1) = 15
61 6cn 11445 . . . . . . . . 9 6 ∈ ℂ
62 6t2e12 11927 . . . . . . . . 9 (6 · 2) = 12
6361, 57, 62mulcomli 10366 . . . . . . . 8 (2 · 6) = 12
643, 35, 2, 54, 3, 9, 60, 63decmul2c 11889 . . . . . . 7 (2 · 76) = 152
6551nn0cni 11631 . . . . . . . . 9 25 ∈ ℂ
6665addid2i 10543 . . . . . . . 8 (0 + 25) = 25
6726nncni 11361 . . . . . . . . . 10 𝑁 ∈ ℂ
6867mul02i 10544 . . . . . . . . 9 (0 · 𝑁) = 0
6968oveq1i 6915 . . . . . . . 8 ((0 · 𝑁) + 25) = (0 + 25)
70 5t5e25 11926 . . . . . . . 8 (5 · 5) = 25
7166, 69, 703eqtr4i 2859 . . . . . . 7 ((0 · 𝑁) + 25) = (5 · 5)
7226, 1, 52, 7, 11, 51, 53, 64, 71mod2xi 16144 . . . . . 6 ((2↑152) mod 𝑁) = (25 mod 𝑁)
73 2p1e3 11500 . . . . . . 7 (2 + 1) = 3
74 eqid 2825 . . . . . . 7 152 = 152
7546, 3, 73, 74decsuc 11853 . . . . . 6 (152 + 1) = 153
7649nn0cni 11631 . . . . . . . 8 50 ∈ ℂ
7776addid2i 10543 . . . . . . 7 (0 + 50) = 50
7868oveq1i 6915 . . . . . . 7 ((0 · 𝑁) + 50) = (0 + 50)
79 eqid 2825 . . . . . . . 8 25 = 25
80 2t2e4 11522 . . . . . . . . . 10 (2 · 2) = 4
8180oveq1i 6915 . . . . . . . . 9 ((2 · 2) + 1) = (4 + 1)
8281, 55eqtri 2849 . . . . . . . 8 ((2 · 2) + 1) = 5
83 5t2e10 11923 . . . . . . . 8 (5 · 2) = 10
843, 3, 11, 79, 39, 9, 82, 83decmul1c 11888 . . . . . . 7 (25 · 2) = 50
8577, 78, 843eqtr4i 2859 . . . . . 6 ((0 · 𝑁) + 50) = (25 · 2)
8626, 1, 50, 7, 51, 49, 72, 75, 85modxp1i 16145 . . . . 5 ((2↑153) mod 𝑁) = (50 mod 𝑁)
87 eqid 2825 . . . . . 6 153 = 153
88 eqid 2825 . . . . . . . . 9 15 = 15
8957mulid1i 10361 . . . . . . . . . . 11 (2 · 1) = 2
9089oveq1i 6915 . . . . . . . . . 10 ((2 · 1) + 1) = (2 + 1)
9190, 73eqtri 2849 . . . . . . . . 9 ((2 · 1) + 1) = 3
92 5cn 11441 . . . . . . . . . 10 5 ∈ ℂ
9392, 57, 83mulcomli 10366 . . . . . . . . 9 (2 · 5) = 10
943, 9, 11, 88, 39, 9, 91, 93decmul2c 11889 . . . . . . . 8 (2 · 15) = 30
9594oveq1i 6915 . . . . . . 7 ((2 · 15) + 0) = (30 + 0)
9640nn0cni 11631 . . . . . . . 8 30 ∈ ℂ
9796addid1i 10542 . . . . . . 7 (30 + 0) = 30
9895, 97eqtri 2849 . . . . . 6 ((2 · 15) + 0) = 30
99 3cn 11432 . . . . . . . 8 3 ∈ ℂ
100 3t2e6 11524 . . . . . . . 8 (3 · 2) = 6
10199, 57, 100mulcomli 10366 . . . . . . 7 (2 · 3) = 6
1022dec0h 11844 . . . . . . 7 6 = 06
103101, 102eqtri 2849 . . . . . 6 (2 · 3) = 06
1043, 46, 29, 87, 2, 39, 98, 103decmul2c 11889 . . . . 5 (2 · 153) = 306
10567mulid2i 10362 . . . . . . . 8 (1 · 𝑁) = 𝑁
106105, 17eqtri 2849 . . . . . . 7 (1 · 𝑁) = 1259
107 eqid 2825 . . . . . . 7 1241 = 1241
1083, 30deccl 11836 . . . . . . . 8 24 ∈ ℕ0
109 eqid 2825 . . . . . . . . 9 24 = 24
1103, 30, 55, 109decsuc 11853 . . . . . . . 8 (24 + 1) = 25
111 eqid 2825 . . . . . . . . 9 125 = 125
112 eqid 2825 . . . . . . . . 9 124 = 124
113 eqid 2825 . . . . . . . . . 10 12 = 12
114 1p1e2 11483 . . . . . . . . . 10 (1 + 1) = 2
115 2p2e4 11493 . . . . . . . . . 10 (2 + 2) = 4
1169, 3, 9, 3, 113, 113, 114, 115decadd 11876 . . . . . . . . 9 (12 + 12) = 24
117 5p4e9 11516 . . . . . . . . 9 (5 + 4) = 9
11810, 11, 10, 30, 111, 112, 116, 117decadd 11876 . . . . . . . 8 (125 + 124) = 249
119108, 110, 118decsucc 11863 . . . . . . 7 ((125 + 124) + 1) = 250
120 9p1e10 11823 . . . . . . 7 (9 + 1) = 10
12112, 5, 44, 9, 106, 107, 119, 120decaddc2 11878 . . . . . 6 ((1 · 𝑁) + 1241) = 2500
122 eqid 2825 . . . . . . 7 50 = 50
12392mul02i 10544 . . . . . . . . . 10 (0 · 5) = 0
12411, 11, 39, 122, 70, 123decmul1 11886 . . . . . . . . 9 (50 · 5) = 250
125124oveq1i 6915 . . . . . . . 8 ((50 · 5) + 0) = (250 + 0)
12651, 39deccl 11836 . . . . . . . . . 10 250 ∈ ℕ0
127126nn0cni 11631 . . . . . . . . 9 250 ∈ ℂ
128127addid1i 10542 . . . . . . . 8 (250 + 0) = 250
129125, 128eqtri 2849 . . . . . . 7 ((50 · 5) + 0) = 250
13076mul01i 10545 . . . . . . . 8 (50 · 0) = 0
13139dec0h 11844 . . . . . . . 8 0 = 00
132130, 131eqtri 2849 . . . . . . 7 (50 · 0) = 00
13349, 11, 39, 122, 39, 39, 129, 132decmul2c 11889 . . . . . 6 (50 · 50) = 2500
134121, 133eqtr4i 2852 . . . . 5 ((1 · 𝑁) + 1241) = (50 · 50)
13526, 1, 47, 48, 49, 45, 86, 104, 134mod2xi 16144 . . . 4 ((2↑306) mod 𝑁) = (1241 mod 𝑁)
136 eqid 2825 . . . . 5 306 = 306
137 eqid 2825 . . . . . 6 30 = 30
1389dec0h 11844 . . . . . 6 1 = 01
139 00id 10530 . . . . . . . 8 (0 + 0) = 0
140101, 139oveq12i 6917 . . . . . . 7 ((2 · 3) + (0 + 0)) = (6 + 0)
14161addid1i 10542 . . . . . . 7 (6 + 0) = 6
142140, 141eqtri 2849 . . . . . 6 ((2 · 3) + (0 + 0)) = 6
14357mul01i 10545 . . . . . . . 8 (2 · 0) = 0
144143oveq1i 6915 . . . . . . 7 ((2 · 0) + 1) = (0 + 1)
145 0p1e1 11480 . . . . . . 7 (0 + 1) = 1
146144, 145, 1383eqtri 2853 . . . . . 6 ((2 · 0) + 1) = 01
14729, 39, 39, 9, 137, 138, 3, 9, 39, 142, 146decma2c 11875 . . . . 5 ((2 · 30) + 1) = 61
1483, 40, 2, 136, 3, 9, 147, 63decmul2c 11889 . . . 4 (2 · 306) = 612
149 eqid 2825 . . . . . 6 18 = 18
15010, 30, 55, 112decsuc 11853 . . . . . 6 (124 + 1) = 125
151 8cn 11453 . . . . . . 7 8 ∈ ℂ
152151, 16, 18addcomli 10547 . . . . . 6 (1 + 8) = 9
15344, 9, 9, 13, 107, 149, 150, 152decadd 11876 . . . . 5 (1241 + 18) = 1259
154153, 17eqtr4i 2852 . . . 4 (1241 + 18) = 𝑁
15534nn0cni 11631 . . . . . 6 324 ∈ ℂ
156155addid2i 10543 . . . . 5 (0 + 324) = 324
15768oveq1i 6915 . . . . 5 ((0 · 𝑁) + 324) = (0 + 324)
1589, 13deccl 11836 . . . . . 6 18 ∈ ℕ0
1599, 30deccl 11836 . . . . . 6 14 ∈ ℕ0
160 eqid 2825 . . . . . . 7 14 = 14
16116mulid1i 10361 . . . . . . . . 9 (1 · 1) = 1
162161, 114oveq12i 6917 . . . . . . . 8 ((1 · 1) + (1 + 1)) = (1 + 2)
163 1p2e3 11501 . . . . . . . 8 (1 + 2) = 3
164162, 163eqtri 2849 . . . . . . 7 ((1 · 1) + (1 + 1)) = 3
165151mulid1i 10361 . . . . . . . . 9 (8 · 1) = 8
166165oveq1i 6915 . . . . . . . 8 ((8 · 1) + 4) = (8 + 4)
167 8p4e12 11905 . . . . . . . 8 (8 + 4) = 12
168166, 167eqtri 2849 . . . . . . 7 ((8 · 1) + 4) = 12
1699, 13, 9, 30, 149, 160, 9, 3, 9, 164, 168decmac 11874 . . . . . 6 ((18 · 1) + 14) = 32
170151mulid2i 10362 . . . . . . . . 9 (1 · 8) = 8
171170oveq1i 6915 . . . . . . . 8 ((1 · 8) + 6) = (8 + 6)
172 8p6e14 11907 . . . . . . . 8 (8 + 6) = 14
173171, 172eqtri 2849 . . . . . . 7 ((1 · 8) + 6) = 14
174 8t8e64 11944 . . . . . . 7 (8 · 8) = 64
17513, 9, 13, 149, 30, 2, 173, 174decmul1c 11888 . . . . . 6 (18 · 8) = 144
176158, 9, 13, 149, 30, 159, 169, 175decmul2c 11889 . . . . 5 (18 · 18) = 324
177156, 157, 1763eqtr4i 2859 . . . 4 ((0 · 𝑁) + 324) = (18 · 18)
1781, 41, 7, 43, 34, 45, 135, 148, 154, 177mod2xnegi 16146 . . 3 ((2↑612) mod 𝑁) = (324 mod 𝑁)
179171259lem1 16203 . . 3 ((2↑17) mod 𝑁) = (136 mod 𝑁)
180 eqid 2825 . . . 4 612 = 612
181 eqid 2825 . . . 4 17 = 17
182 eqid 2825 . . . . 5 61 = 61
1832, 9, 114, 182decsuc 11853 . . . 4 (61 + 1) = 62
184 7p2e9 11519 . . . . 5 (7 + 2) = 9
18556, 57, 184addcomli 10547 . . . 4 (2 + 7) = 9
18627, 3, 9, 35, 180, 181, 183, 185decadd 11876 . . 3 (612 + 17) = 629
18729, 9deccl 11836 . . . . 5 31 ∈ ℕ0
188 eqid 2825 . . . . . . 7 31 = 31
189 3p2e5 11509 . . . . . . . . 9 (3 + 2) = 5
19099, 57, 189addcomli 10547 . . . . . . . 8 (2 + 3) = 5
1919, 3, 29, 113, 190decaddi 11882 . . . . . . 7 (12 + 3) = 15
192 5p1e6 11505 . . . . . . 7 (5 + 1) = 6
19310, 11, 29, 9, 111, 188, 191, 192decadd 11876 . . . . . 6 (125 + 31) = 156
194114oveq1i 6915 . . . . . . . . 9 ((1 + 1) + 1) = (2 + 1)
195194, 73eqtri 2849 . . . . . . . 8 ((1 + 1) + 1) = 3
196 7p5e12 11900 . . . . . . . . 9 (7 + 5) = 12
19756, 92, 196addcomli 10547 . . . . . . . 8 (5 + 7) = 12
1989, 11, 9, 35, 88, 181, 195, 3, 197decaddc 11877 . . . . . . 7 (15 + 17) = 32
199 eqid 2825 . . . . . . . 8 34 = 34
200 7p3e10 11898 . . . . . . . . 9 (7 + 3) = 10
20156, 99, 200addcomli 10547 . . . . . . . 8 (3 + 7) = 10
20299mulid1i 10361 . . . . . . . . . 10 (3 · 1) = 3
20316addid1i 10542 . . . . . . . . . 10 (1 + 0) = 1
204202, 203oveq12i 6917 . . . . . . . . 9 ((3 · 1) + (1 + 0)) = (3 + 1)
205 3p1e4 11503 . . . . . . . . 9 (3 + 1) = 4
206204, 205eqtri 2849 . . . . . . . 8 ((3 · 1) + (1 + 0)) = 4
207 4cn 11437 . . . . . . . . . . 11 4 ∈ ℂ
208207mulid1i 10361 . . . . . . . . . 10 (4 · 1) = 4
209208oveq1i 6915 . . . . . . . . 9 ((4 · 1) + 0) = (4 + 0)
210207addid1i 10542 . . . . . . . . 9 (4 + 0) = 4
21130dec0h 11844 . . . . . . . . 9 4 = 04
212209, 210, 2113eqtri 2853 . . . . . . . 8 ((4 · 1) + 0) = 04
21329, 30, 9, 39, 199, 201, 9, 30, 39, 206, 212decmac 11874 . . . . . . 7 ((34 · 1) + (3 + 7)) = 44
2143dec0h 11844 . . . . . . . 8 2 = 02
215100, 145oveq12i 6917 . . . . . . . . 9 ((3 · 2) + (0 + 1)) = (6 + 1)
216 6p1e7 11506 . . . . . . . . 9 (6 + 1) = 7
217215, 216eqtri 2849 . . . . . . . 8 ((3 · 2) + (0 + 1)) = 7
218 4t2e8 11526 . . . . . . . . . 10 (4 · 2) = 8
219218oveq1i 6915 . . . . . . . . 9 ((4 · 2) + 2) = (8 + 2)
220 8p2e10 11903 . . . . . . . . 9 (8 + 2) = 10
221219, 220eqtri 2849 . . . . . . . 8 ((4 · 2) + 2) = 10
22229, 30, 39, 3, 199, 214, 3, 39, 9, 217, 221decmac 11874 . . . . . . 7 ((34 · 2) + 2) = 70
2239, 3, 29, 3, 113, 198, 31, 39, 35, 213, 222decma2c 11875 . . . . . 6 ((34 · 12) + (15 + 17)) = 440
224 5t3e15 11924 . . . . . . . . 9 (5 · 3) = 15
22592, 99, 224mulcomli 10366 . . . . . . . 8 (3 · 5) = 15
226 5p2e7 11514 . . . . . . . 8 (5 + 2) = 7
2279, 11, 3, 225, 226decaddi 11882 . . . . . . 7 ((3 · 5) + 2) = 17
228 5t4e20 11925 . . . . . . . . 9 (5 · 4) = 20
22992, 207, 228mulcomli 10366 . . . . . . . 8 (4 · 5) = 20
23061addid2i 10543 . . . . . . . 8 (0 + 6) = 6
2313, 39, 2, 229, 230decaddi 11882 . . . . . . 7 ((4 · 5) + 6) = 26
23229, 30, 2, 199, 11, 2, 3, 227, 231decrmac 11880 . . . . . 6 ((34 · 5) + 6) = 176
23310, 11, 46, 2, 111, 193, 31, 2, 36, 223, 232decma2c 11875 . . . . 5 ((34 · 125) + (125 + 31)) = 4406
234 9cn 11457 . . . . . . . 8 9 ∈ ℂ
235 9t3e27 11946 . . . . . . . 8 (9 · 3) = 27
236234, 99, 235mulcomli 10366 . . . . . . 7 (3 · 9) = 27
237 7p4e11 11899 . . . . . . 7 (7 + 4) = 11
2383, 35, 30, 236, 73, 9, 237decaddci 11883 . . . . . 6 ((3 · 9) + 4) = 31
239 9t4e36 11947 . . . . . . . 8 (9 · 4) = 36
240234, 207, 239mulcomli 10366 . . . . . . 7 (4 · 9) = 36
241151, 61, 172addcomli 10547 . . . . . . 7 (6 + 8) = 14
24229, 2, 13, 240, 205, 30, 241decaddci 11883 . . . . . 6 ((4 · 9) + 8) = 44
24329, 30, 13, 199, 5, 30, 30, 238, 242decrmac 11880 . . . . 5 ((34 · 9) + 8) = 314
24412, 5, 12, 13, 17, 22, 31, 30, 187, 233, 243decma2c 11875 . . . 4 ((34 · 𝑁) + (𝑁 − 1)) = 44064
245 eqid 2825 . . . . 5 136 = 136
2469, 5deccl 11836 . . . . . 6 19 ∈ ℕ0
247246, 30deccl 11836 . . . . 5 194 ∈ ℕ0
248 eqid 2825 . . . . . 6 13 = 13
249 eqid 2825 . . . . . 6 194 = 194
2505, 35deccl 11836 . . . . . 6 97 ∈ ℕ0
2519, 9deccl 11836 . . . . . . 7 11 ∈ ℕ0
252 eqid 2825 . . . . . . 7 324 = 324
253 eqid 2825 . . . . . . . 8 19 = 19
254 eqid 2825 . . . . . . . 8 97 = 97
255234, 16, 120addcomli 10547 . . . . . . . . 9 (1 + 9) = 10
2569, 39, 145, 255decsuc 11853 . . . . . . . 8 ((1 + 9) + 1) = 11
257 9p7e16 11915 . . . . . . . 8 (9 + 7) = 16
2589, 5, 5, 35, 253, 254, 256, 2, 257decaddc 11877 . . . . . . 7 (19 + 97) = 116
259 eqid 2825 . . . . . . . 8 32 = 32
260 eqid 2825 . . . . . . . . 9 11 = 11
2619, 9, 114, 260decsuc 11853 . . . . . . . 8 (11 + 1) = 12
26289oveq1i 6915 . . . . . . . . 9 ((2 · 1) + 2) = (2 + 2)
263262, 115, 2113eqtri 2853 . . . . . . . 8 ((2 · 1) + 2) = 04
26429, 3, 9, 3, 259, 261, 9, 30, 39, 206, 263decmac 11874 . . . . . . 7 ((32 · 1) + (11 + 1)) = 44
265208oveq1i 6915 . . . . . . . 8 ((4 · 1) + 6) = (4 + 6)
266 6p4e10 11895 . . . . . . . . 9 (6 + 4) = 10
26761, 207, 266addcomli 10547 . . . . . . . 8 (4 + 6) = 10
268265, 267eqtri 2849 . . . . . . 7 ((4 · 1) + 6) = 10
26933, 30, 251, 2, 252, 258, 9, 39, 9, 264, 268decmac 11874 . . . . . 6 ((324 · 1) + (19 + 97)) = 440
270145, 138eqtri 2849 . . . . . . . 8 (0 + 1) = 01
271 3t3e9 11525 . . . . . . . . . 10 (3 · 3) = 9
272271, 139oveq12i 6917 . . . . . . . . 9 ((3 · 3) + (0 + 0)) = (9 + 0)
273234addid1i 10542 . . . . . . . . 9 (9 + 0) = 9
274272, 273eqtri 2849 . . . . . . . 8 ((3 · 3) + (0 + 0)) = 9
275101oveq1i 6915 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
27635dec0h 11844 . . . . . . . . 9 7 = 07
277275, 216, 2763eqtri 2853 . . . . . . . 8 ((2 · 3) + 1) = 07
27829, 3, 39, 9, 259, 270, 29, 35, 39, 274, 277decmac 11874 . . . . . . 7 ((32 · 3) + (0 + 1)) = 97
279 4t3e12 11921 . . . . . . . 8 (4 · 3) = 12
280 4p2e6 11511 . . . . . . . . 9 (4 + 2) = 6
281207, 57, 280addcomli 10547 . . . . . . . 8 (2 + 4) = 6
2829, 3, 30, 279, 281decaddi 11882 . . . . . . 7 ((4 · 3) + 4) = 16
28333, 30, 39, 30, 252, 211, 29, 2, 9, 278, 282decmac 11874 . . . . . 6 ((324 · 3) + 4) = 976
2849, 29, 246, 30, 248, 249, 34, 2, 250, 269, 283decma2c 11875 . . . . 5 ((324 · 13) + 194) = 4406
285 6t3e18 11928 . . . . . . . . 9 (6 · 3) = 18
28661, 99, 285mulcomli 10366 . . . . . . . 8 (3 · 6) = 18
2879, 13, 18, 286decsuc 11853 . . . . . . 7 ((3 · 6) + 1) = 19
2889, 3, 3, 63, 115decaddi 11882 . . . . . . 7 ((2 · 6) + 2) = 14
28929, 3, 3, 259, 2, 30, 9, 287, 288decrmac 11880 . . . . . 6 ((32 · 6) + 2) = 194
290 6t4e24 11929 . . . . . . 7 (6 · 4) = 24
29161, 207, 290mulcomli 10366 . . . . . 6 (4 · 6) = 24
2922, 33, 30, 252, 30, 3, 289, 291decmul1c 11888 . . . . 5 (324 · 6) = 1944
29334, 37, 2, 245, 30, 247, 284, 292decmul2c 11889 . . . 4 (324 · 136) = 44064
294244, 293eqtr4i 2852 . . 3 ((34 · 𝑁) + (𝑁 − 1)) = (324 · 136)
29526, 1, 28, 32, 34, 23, 36, 38, 178, 179, 186, 294modxai 16143 . 2 ((2↑629) mod 𝑁) = ((𝑁 − 1) mod 𝑁)
296 eqid 2825 . . . 4 629 = 629
297 eqid 2825 . . . . 5 62 = 62
298139oveq2i 6916 . . . . . 6 ((2 · 6) + (0 + 0)) = ((2 · 6) + 0)
29963oveq1i 6915 . . . . . 6 ((2 · 6) + 0) = (12 + 0)
30010nn0cni 11631 . . . . . . 7 12 ∈ ℂ
301300addid1i 10542 . . . . . 6 (12 + 0) = 12
302298, 299, 3013eqtri 2853 . . . . 5 ((2 · 6) + (0 + 0)) = 12
30311dec0h 11844 . . . . . 6 5 = 05
30481, 55, 3033eqtri 2853 . . . . 5 ((2 · 2) + 1) = 05
3052, 3, 39, 9, 297, 138, 3, 11, 39, 302, 304decma2c 11875 . . . 4 ((2 · 62) + 1) = 125
306 9t2e18 11945 . . . . 5 (9 · 2) = 18
307234, 57, 306mulcomli 10366 . . . 4 (2 · 9) = 18
3083, 4, 5, 296, 13, 9, 305, 307decmul2c 11889 . . 3 (2 · 629) = 1258
309308, 22eqtr4i 2852 . 2 (2 · 629) = (𝑁 − 1)
310 npcan 10611 . . 3 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
31167, 16, 310mp2an 685 . 2 ((𝑁 − 1) + 1) = 𝑁
31268oveq1i 6915 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
313145, 312, 1613eqtr4i 2859 . 2 ((0 · 𝑁) + 1) = (1 · 1)
3141, 6, 7, 8, 9, 23, 295, 309, 311, 313mod2xnegi 16146 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1658   ∈ wcel 2166  (class class class)co 6905  ℂcc 10250  0cc0 10252  1c1 10253   + caddc 10255   · cmul 10257   − cmin 10585  ℕcn 11350  2c2 11406  3c3 11407  4c4 11408  5c5 11409  6c6 11410  7c7 11411  8c8 11412  9c9 11413  ℕ0cn0 11618  ;cdc 11821   mod cmo 12963  ↑cexp 13154 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pow 5065  ax-pr 5127  ax-un 7209  ax-cnex 10308  ax-resscn 10309  ax-1cn 10310  ax-icn 10311  ax-addcl 10312  ax-addrcl 10313  ax-mulcl 10314  ax-mulrcl 10315  ax-mulcom 10316  ax-addass 10317  ax-mulass 10318  ax-distr 10319  ax-i2m1 10320  ax-1ne0 10321  ax-1rid 10322  ax-rnegex 10323  ax-rrecex 10324  ax-cnre 10325  ax-pre-lttri 10326  ax-pre-lttrn 10327  ax-pre-ltadd 10328  ax-pre-mulgt0 10329  ax-pre-sup 10330 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4145  df-if 4307  df-pw 4380  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4659  df-iun 4742  df-br 4874  df-opab 4936  df-mpt 4953  df-tr 4976  df-id 5250  df-eprel 5255  df-po 5263  df-so 5264  df-fr 5301  df-we 5303  df-xp 5348  df-rel 5349  df-cnv 5350  df-co 5351  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355  df-pred 5920  df-ord 5966  df-on 5967  df-lim 5968  df-suc 5969  df-iota 6086  df-fun 6125  df-fn 6126  df-f 6127  df-f1 6128  df-fo 6129  df-f1o 6130  df-fv 6131  df-riota 6866  df-ov 6908  df-oprab 6909  df-mpt2 6910  df-om 7327  df-2nd 7429  df-wrecs 7672  df-recs 7734  df-rdg 7772  df-er 8009  df-en 8223  df-dom 8224  df-sdom 8225  df-sup 8617  df-inf 8618  df-pnf 10393  df-mnf 10394  df-xr 10395  df-ltxr 10396  df-le 10397  df-sub 10587  df-neg 10588  df-div 11010  df-nn 11351  df-2 11414  df-3 11415  df-4 11416  df-5 11417  df-6 11418  df-7 11419  df-8 11420  df-9 11421  df-n0 11619  df-z 11705  df-dec 11822  df-uz 11969  df-rp 12113  df-fl 12888  df-mod 12964  df-seq 13096  df-exp 13155 This theorem is referenced by:  1259prm  16208
 Copyright terms: Public domain W3C validator