MPE Home 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