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

Theorem 1259lem4 16446
Description: Lemma for 1259prm 16448. 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 11688 . 2 2 ∈ ℕ
2 6nn0 11896 . . . 4 6 ∈ ℕ0
3 2nn0 11892 . . . 4 2 ∈ ℕ0
42, 3deccl 12091 . . 3 62 ∈ ℕ0
5 9nn0 11899 . . 3 9 ∈ ℕ0
64, 5deccl 12091 . 2 629 ∈ ℕ0
7 0z 11970 . 2 0 ∈ ℤ
8 1nn 11626 . 2 1 ∈ ℕ
9 1nn0 11891 . 2 1 ∈ ℕ0
109, 3deccl 12091 . . . . . . 7 12 ∈ ℕ0
11 5nn0 11895 . . . . . . 7 5 ∈ ℕ0
1210, 11deccl 12091 . . . . . 6 125 ∈ ℕ0
13 8nn0 11898 . . . . . 6 8 ∈ ℕ0
1412, 13deccl 12091 . . . . 5 1258 ∈ ℕ0
1514nn0cni 11887 . . . 4 1258 ∈ ℂ
16 ax-1cn 10572 . . . 4 1 ∈ ℂ
17 1259prm.1 . . . . 5 𝑁 = 1259
18 8p1e9 11765 . . . . . 6 (8 + 1) = 9
19 eqid 2821 . . . . . 6 1258 = 1258
2012, 13, 18, 19decsuc 12107 . . . . 5 (1258 + 1) = 1259
2117, 20eqtr4i 2847 . . . 4 𝑁 = (1258 + 1)
2215, 16, 21mvrraddi 10880 . . 3 (𝑁 − 1) = 1258
2322, 14eqeltri 2908 . 2 (𝑁 − 1) ∈ ℕ0
24 9nn 11713 . . . . 5 9 ∈ ℕ
2512, 24decnncl 12096 . . . 4 1259 ∈ ℕ
2617, 25eqeltri 2908 . . 3 𝑁 ∈ ℕ
272, 9deccl 12091 . . . 4 61 ∈ ℕ0
2827, 3deccl 12091 . . 3 612 ∈ ℕ0
29 3nn0 11893 . . . . 5 3 ∈ ℕ0
30 4nn0 11894 . . . . 5 4 ∈ ℕ0
3129, 30deccl 12091 . . . 4 34 ∈ ℕ0
3231nn0zi 11985 . . 3 34 ∈ ℤ
3329, 3deccl 12091 . . . 4 32 ∈ ℕ0
3433, 30deccl 12091 . . 3 324 ∈ ℕ0
35 7nn0 11897 . . . 4 7 ∈ ℕ0
369, 35deccl 12091 . . 3 17 ∈ ℕ0
379, 29deccl 12091 . . . 4 13 ∈ ℕ0
3837, 2deccl 12091 . . 3 136 ∈ ℕ0
39 0nn0 11890 . . . . . 6 0 ∈ ℕ0
4029, 39deccl 12091 . . . . 5 30 ∈ ℕ0
4140, 2deccl 12091 . . . 4 306 ∈ ℕ0
42 8nn 11710 . . . . 5 8 ∈ ℕ
439, 42decnncl 12096 . . . 4 18 ∈ ℕ
4410, 30deccl 12091 . . . . 5 124 ∈ ℕ0
4544, 9deccl 12091 . . . 4 1241 ∈ ℕ0
469, 11deccl 12091 . . . . . 6 15 ∈ ℕ0
4746, 29deccl 12091 . . . . 5 153 ∈ ℕ0
48 1z 11990 . . . . 5 1 ∈ ℤ
4911, 39deccl 12091 . . . . 5 50 ∈ ℕ0
5046, 3deccl 12091 . . . . . 6 152 ∈ ℕ0
513, 11deccl 12091 . . . . . 6 25 ∈ ℕ0
5235, 2deccl 12091 . . . . . . 7 76 ∈ ℕ0
53171259lem3 16445 . . . . . . 7 ((2↑76) mod 𝑁) = (5 mod 𝑁)
54 eqid 2821 . . . . . . . 8 76 = 76
55 4p1e5 11761 . . . . . . . . 9 (4 + 1) = 5
56 7cn 11709 . . . . . . . . . 10 7 ∈ ℂ
57 2cn 11690 . . . . . . . . . 10 2 ∈ ℂ
58 7t2e14 12185 . . . . . . . . . 10 (7 · 2) = 14
5956, 57, 58mulcomli 10627 . . . . . . . . 9 (2 · 7) = 14
609, 30, 55, 59decsuc 12107 . . . . . . . 8 ((2 · 7) + 1) = 15
61 6cn 11706 . . . . . . . . 9 6 ∈ ℂ
62 6t2e12 12180 . . . . . . . . 9 (6 · 2) = 12
6361, 57, 62mulcomli 10627 . . . . . . . 8 (2 · 6) = 12
643, 35, 2, 54, 3, 9, 60, 63decmul2c 12142 . . . . . . 7 (2 · 76) = 152
6551nn0cni 11887 . . . . . . . . 9 25 ∈ ℂ
6665addid2i 10805 . . . . . . . 8 (0 + 25) = 25
6726nncni 11625 . . . . . . . . . 10 𝑁 ∈ ℂ
6867mul02i 10806 . . . . . . . . 9 (0 · 𝑁) = 0
6968oveq1i 7140 . . . . . . . 8 ((0 · 𝑁) + 25) = (0 + 25)
70 5t5e25 12179 . . . . . . . 8 (5 · 5) = 25
7166, 69, 703eqtr4i 2854 . . . . . . 7 ((0 · 𝑁) + 25) = (5 · 5)
7226, 1, 52, 7, 11, 51, 53, 64, 71mod2xi 16382 . . . . . 6 ((2↑152) mod 𝑁) = (25 mod 𝑁)
73 2p1e3 11757 . . . . . . 7 (2 + 1) = 3
74 eqid 2821 . . . . . . 7 152 = 152
7546, 3, 73, 74decsuc 12107 . . . . . 6 (152 + 1) = 153
7649nn0cni 11887 . . . . . . . 8 50 ∈ ℂ
7776addid2i 10805 . . . . . . 7 (0 + 50) = 50
7868oveq1i 7140 . . . . . . 7 ((0 · 𝑁) + 50) = (0 + 50)
79 eqid 2821 . . . . . . . 8 25 = 25
80 2t2e4 11779 . . . . . . . . . 10 (2 · 2) = 4
8180oveq1i 7140 . . . . . . . . 9 ((2 · 2) + 1) = (4 + 1)
8281, 55eqtri 2844 . . . . . . . 8 ((2 · 2) + 1) = 5
83 5t2e10 12176 . . . . . . . 8 (5 · 2) = 10
843, 3, 11, 79, 39, 9, 82, 83decmul1c 12141 . . . . . . 7 (25 · 2) = 50
8577, 78, 843eqtr4i 2854 . . . . . 6 ((0 · 𝑁) + 50) = (25 · 2)
8626, 1, 50, 7, 51, 49, 72, 75, 85modxp1i 16383 . . . . 5 ((2↑153) mod 𝑁) = (50 mod 𝑁)
87 eqid 2821 . . . . . 6 153 = 153
88 eqid 2821 . . . . . . . . 9 15 = 15
8957mulid1i 10622 . . . . . . . . . . 11 (2 · 1) = 2
9089oveq1i 7140 . . . . . . . . . 10 ((2 · 1) + 1) = (2 + 1)
9190, 73eqtri 2844 . . . . . . . . 9 ((2 · 1) + 1) = 3
92 5cn 11703 . . . . . . . . . 10 5 ∈ ℂ
9392, 57, 83mulcomli 10627 . . . . . . . . 9 (2 · 5) = 10
943, 9, 11, 88, 39, 9, 91, 93decmul2c 12142 . . . . . . . 8 (2 · 15) = 30
9594oveq1i 7140 . . . . . . 7 ((2 · 15) + 0) = (30 + 0)
9640nn0cni 11887 . . . . . . . 8 30 ∈ ℂ
9796addid1i 10804 . . . . . . 7 (30 + 0) = 30
9895, 97eqtri 2844 . . . . . 6 ((2 · 15) + 0) = 30
99 3cn 11696 . . . . . . . 8 3 ∈ ℂ
100 3t2e6 11781 . . . . . . . 8 (3 · 2) = 6
10199, 57, 100mulcomli 10627 . . . . . . 7 (2 · 3) = 6
1022dec0h 12098 . . . . . . 7 6 = 06
103101, 102eqtri 2844 . . . . . 6 (2 · 3) = 06
1043, 46, 29, 87, 2, 39, 98, 103decmul2c 12142 . . . . 5 (2 · 153) = 306
10567mulid2i 10623 . . . . . . . 8 (1 · 𝑁) = 𝑁
106105, 17eqtri 2844 . . . . . . 7 (1 · 𝑁) = 1259
107 eqid 2821 . . . . . . 7 1241 = 1241
1083, 30deccl 12091 . . . . . . . 8 24 ∈ ℕ0
109 eqid 2821 . . . . . . . . 9 24 = 24
1103, 30, 55, 109decsuc 12107 . . . . . . . 8 (24 + 1) = 25
111 eqid 2821 . . . . . . . . 9 125 = 125
112 eqid 2821 . . . . . . . . 9 124 = 124
113 eqid 2821 . . . . . . . . . 10 12 = 12
114 1p1e2 11740 . . . . . . . . . 10 (1 + 1) = 2
115 2p2e4 11750 . . . . . . . . . 10 (2 + 2) = 4
1169, 3, 9, 3, 113, 113, 114, 115decadd 12130 . . . . . . . . 9 (12 + 12) = 24
117 5p4e9 11773 . . . . . . . . 9 (5 + 4) = 9
11810, 11, 10, 30, 111, 112, 116, 117decadd 12130 . . . . . . . 8 (125 + 124) = 249
119108, 110, 118decsucc 12117 . . . . . . 7 ((125 + 124) + 1) = 250
120 9p1e10 12078 . . . . . . 7 (9 + 1) = 10
12112, 5, 44, 9, 106, 107, 119, 120decaddc2 12132 . . . . . 6 ((1 · 𝑁) + 1241) = 2500
122 eqid 2821 . . . . . . 7 50 = 50
12392mul02i 10806 . . . . . . . . . 10 (0 · 5) = 0
12411, 11, 39, 122, 70, 123decmul1 12140 . . . . . . . . 9 (50 · 5) = 250
125124oveq1i 7140 . . . . . . . 8 ((50 · 5) + 0) = (250 + 0)
12651, 39deccl 12091 . . . . . . . . . 10 250 ∈ ℕ0
127126nn0cni 11887 . . . . . . . . 9 250 ∈ ℂ
128127addid1i 10804 . . . . . . . 8 (250 + 0) = 250
129125, 128eqtri 2844 . . . . . . 7 ((50 · 5) + 0) = 250
13076mul01i 10807 . . . . . . . 8 (50 · 0) = 0
13139dec0h 12098 . . . . . . . 8 0 = 00
132130, 131eqtri 2844 . . . . . . 7 (50 · 0) = 00
13349, 11, 39, 122, 39, 39, 129, 132decmul2c 12142 . . . . . 6 (50 · 50) = 2500
134121, 133eqtr4i 2847 . . . . 5 ((1 · 𝑁) + 1241) = (50 · 50)
13526, 1, 47, 48, 49, 45, 86, 104, 134mod2xi 16382 . . . 4 ((2↑306) mod 𝑁) = (1241 mod 𝑁)
136 eqid 2821 . . . . 5 306 = 306
137 eqid 2821 . . . . . 6 30 = 30
1389dec0h 12098 . . . . . 6 1 = 01
139 00id 10792 . . . . . . . 8 (0 + 0) = 0
140101, 139oveq12i 7142 . . . . . . 7 ((2 · 3) + (0 + 0)) = (6 + 0)
14161addid1i 10804 . . . . . . 7 (6 + 0) = 6
142140, 141eqtri 2844 . . . . . 6 ((2 · 3) + (0 + 0)) = 6
14357mul01i 10807 . . . . . . . 8 (2 · 0) = 0
144143oveq1i 7140 . . . . . . 7 ((2 · 0) + 1) = (0 + 1)
145 0p1e1 11737 . . . . . . 7 (0 + 1) = 1
146144, 145, 1383eqtri 2848 . . . . . 6 ((2 · 0) + 1) = 01
14729, 39, 39, 9, 137, 138, 3, 9, 39, 142, 146decma2c 12129 . . . . 5 ((2 · 30) + 1) = 61
1483, 40, 2, 136, 3, 9, 147, 63decmul2c 12142 . . . 4 (2 · 306) = 612
149 eqid 2821 . . . . . 6 18 = 18
15010, 30, 55, 112decsuc 12107 . . . . . 6 (124 + 1) = 125
151 8cn 11712 . . . . . . 7 8 ∈ ℂ
152151, 16, 18addcomli 10809 . . . . . 6 (1 + 8) = 9
15344, 9, 9, 13, 107, 149, 150, 152decadd 12130 . . . . 5 (1241 + 18) = 1259
154153, 17eqtr4i 2847 . . . 4 (1241 + 18) = 𝑁
15534nn0cni 11887 . . . . . 6 324 ∈ ℂ
156155addid2i 10805 . . . . 5 (0 + 324) = 324
15768oveq1i 7140 . . . . 5 ((0 · 𝑁) + 324) = (0 + 324)
1589, 13deccl 12091 . . . . . 6 18 ∈ ℕ0
1599, 30deccl 12091 . . . . . 6 14 ∈ ℕ0
160 eqid 2821 . . . . . . 7 14 = 14
16116mulid1i 10622 . . . . . . . . 9 (1 · 1) = 1
162161, 114oveq12i 7142 . . . . . . . 8 ((1 · 1) + (1 + 1)) = (1 + 2)
163 1p2e3 11758 . . . . . . . 8 (1 + 2) = 3
164162, 163eqtri 2844 . . . . . . 7 ((1 · 1) + (1 + 1)) = 3
165151mulid1i 10622 . . . . . . . . 9 (8 · 1) = 8
166165oveq1i 7140 . . . . . . . 8 ((8 · 1) + 4) = (8 + 4)
167 8p4e12 12158 . . . . . . . 8 (8 + 4) = 12
168166, 167eqtri 2844 . . . . . . 7 ((8 · 1) + 4) = 12
1699, 13, 9, 30, 149, 160, 9, 3, 9, 164, 168decmac 12128 . . . . . 6 ((18 · 1) + 14) = 32
170151mulid2i 10623 . . . . . . . . 9 (1 · 8) = 8
171170oveq1i 7140 . . . . . . . 8 ((1 · 8) + 6) = (8 + 6)
172 8p6e14 12160 . . . . . . . 8 (8 + 6) = 14
173171, 172eqtri 2844 . . . . . . 7 ((1 · 8) + 6) = 14
174 8t8e64 12197 . . . . . . 7 (8 · 8) = 64
17513, 9, 13, 149, 30, 2, 173, 174decmul1c 12141 . . . . . 6 (18 · 8) = 144
176158, 9, 13, 149, 30, 159, 169, 175decmul2c 12142 . . . . 5 (18 · 18) = 324
177156, 157, 1763eqtr4i 2854 . . . 4 ((0 · 𝑁) + 324) = (18 · 18)
1781, 41, 7, 43, 34, 45, 135, 148, 154, 177mod2xnegi 16384 . . 3 ((2↑612) mod 𝑁) = (324 mod 𝑁)
179171259lem1 16443 . . 3 ((2↑17) mod 𝑁) = (136 mod 𝑁)
180 eqid 2821 . . . 4 612 = 612
181 eqid 2821 . . . 4 17 = 17
182 eqid 2821 . . . . 5 61 = 61
1832, 9, 114, 182decsuc 12107 . . . 4 (61 + 1) = 62
184 7p2e9 11776 . . . . 5 (7 + 2) = 9
18556, 57, 184addcomli 10809 . . . 4 (2 + 7) = 9
18627, 3, 9, 35, 180, 181, 183, 185decadd 12130 . . 3 (612 + 17) = 629
18729, 9deccl 12091 . . . . 5 31 ∈ ℕ0
188 eqid 2821 . . . . . . 7 31 = 31
189 3p2e5 11766 . . . . . . . . 9 (3 + 2) = 5
19099, 57, 189addcomli 10809 . . . . . . . 8 (2 + 3) = 5
1919, 3, 29, 113, 190decaddi 12136 . . . . . . 7 (12 + 3) = 15
192 5p1e6 11762 . . . . . . 7 (5 + 1) = 6
19310, 11, 29, 9, 111, 188, 191, 192decadd 12130 . . . . . 6 (125 + 31) = 156
194114oveq1i 7140 . . . . . . . . 9 ((1 + 1) + 1) = (2 + 1)
195194, 73eqtri 2844 . . . . . . . 8 ((1 + 1) + 1) = 3
196 7p5e12 12153 . . . . . . . . 9 (7 + 5) = 12
19756, 92, 196addcomli 10809 . . . . . . . 8 (5 + 7) = 12
1989, 11, 9, 35, 88, 181, 195, 3, 197decaddc 12131 . . . . . . 7 (15 + 17) = 32
199 eqid 2821 . . . . . . . 8 34 = 34
200 7p3e10 12151 . . . . . . . . 9 (7 + 3) = 10
20156, 99, 200addcomli 10809 . . . . . . . 8 (3 + 7) = 10
20299mulid1i 10622 . . . . . . . . . 10 (3 · 1) = 3
20316addid1i 10804 . . . . . . . . . 10 (1 + 0) = 1
204202, 203oveq12i 7142 . . . . . . . . 9 ((3 · 1) + (1 + 0)) = (3 + 1)
205 3p1e4 11760 . . . . . . . . 9 (3 + 1) = 4
206204, 205eqtri 2844 . . . . . . . 8 ((3 · 1) + (1 + 0)) = 4
207 4cn 11700 . . . . . . . . . . 11 4 ∈ ℂ
208207mulid1i 10622 . . . . . . . . . 10 (4 · 1) = 4
209208oveq1i 7140 . . . . . . . . 9 ((4 · 1) + 0) = (4 + 0)
210207addid1i 10804 . . . . . . . . 9 (4 + 0) = 4
21130dec0h 12098 . . . . . . . . 9 4 = 04
212209, 210, 2113eqtri 2848 . . . . . . . 8 ((4 · 1) + 0) = 04
21329, 30, 9, 39, 199, 201, 9, 30, 39, 206, 212decmac 12128 . . . . . . 7 ((34 · 1) + (3 + 7)) = 44
2143dec0h 12098 . . . . . . . 8 2 = 02
215100, 145oveq12i 7142 . . . . . . . . 9 ((3 · 2) + (0 + 1)) = (6 + 1)
216 6p1e7 11763 . . . . . . . . 9 (6 + 1) = 7
217215, 216eqtri 2844 . . . . . . . 8 ((3 · 2) + (0 + 1)) = 7
218 4t2e8 11783 . . . . . . . . . 10 (4 · 2) = 8
219218oveq1i 7140 . . . . . . . . 9 ((4 · 2) + 2) = (8 + 2)
220 8p2e10 12156 . . . . . . . . 9 (8 + 2) = 10
221219, 220eqtri 2844 . . . . . . . 8 ((4 · 2) + 2) = 10
22229, 30, 39, 3, 199, 214, 3, 39, 9, 217, 221decmac 12128 . . . . . . 7 ((34 · 2) + 2) = 70
2239, 3, 29, 3, 113, 198, 31, 39, 35, 213, 222decma2c 12129 . . . . . 6 ((34 · 12) + (15 + 17)) = 440
224 5t3e15 12177 . . . . . . . . 9 (5 · 3) = 15
22592, 99, 224mulcomli 10627 . . . . . . . 8 (3 · 5) = 15
226 5p2e7 11771 . . . . . . . 8 (5 + 2) = 7
2279, 11, 3, 225, 226decaddi 12136 . . . . . . 7 ((3 · 5) + 2) = 17
228 5t4e20 12178 . . . . . . . . 9 (5 · 4) = 20
22992, 207, 228mulcomli 10627 . . . . . . . 8 (4 · 5) = 20
23061addid2i 10805 . . . . . . . 8 (0 + 6) = 6
2313, 39, 2, 229, 230decaddi 12136 . . . . . . 7 ((4 · 5) + 6) = 26
23229, 30, 2, 199, 11, 2, 3, 227, 231decrmac 12134 . . . . . 6 ((34 · 5) + 6) = 176
23310, 11, 46, 2, 111, 193, 31, 2, 36, 223, 232decma2c 12129 . . . . 5 ((34 · 125) + (125 + 31)) = 4406
234 9cn 11715 . . . . . . . 8 9 ∈ ℂ
235 9t3e27 12199 . . . . . . . 8 (9 · 3) = 27
236234, 99, 235mulcomli 10627 . . . . . . 7 (3 · 9) = 27
237 7p4e11 12152 . . . . . . 7 (7 + 4) = 11
2383, 35, 30, 236, 73, 9, 237decaddci 12137 . . . . . 6 ((3 · 9) + 4) = 31
239 9t4e36 12200 . . . . . . . 8 (9 · 4) = 36
240234, 207, 239mulcomli 10627 . . . . . . 7 (4 · 9) = 36
241151, 61, 172addcomli 10809 . . . . . . 7 (6 + 8) = 14
24229, 2, 13, 240, 205, 30, 241decaddci 12137 . . . . . 6 ((4 · 9) + 8) = 44
24329, 30, 13, 199, 5, 30, 30, 238, 242decrmac 12134 . . . . 5 ((34 · 9) + 8) = 314
24412, 5, 12, 13, 17, 22, 31, 30, 187, 233, 243decma2c 12129 . . . 4 ((34 · 𝑁) + (𝑁 − 1)) = 44064
245 eqid 2821 . . . . 5 136 = 136
2469, 5deccl 12091 . . . . . 6 19 ∈ ℕ0
247246, 30deccl 12091 . . . . 5 194 ∈ ℕ0
248 eqid 2821 . . . . . 6 13 = 13
249 eqid 2821 . . . . . 6 194 = 194
2505, 35deccl 12091 . . . . . 6 97 ∈ ℕ0
2519, 9deccl 12091 . . . . . . 7 11 ∈ ℕ0
252 eqid 2821 . . . . . . 7 324 = 324
253 eqid 2821 . . . . . . . 8 19 = 19
254 eqid 2821 . . . . . . . 8 97 = 97
255234, 16, 120addcomli 10809 . . . . . . . . 9 (1 + 9) = 10
2569, 39, 145, 255decsuc 12107 . . . . . . . 8 ((1 + 9) + 1) = 11
257 9p7e16 12168 . . . . . . . 8 (9 + 7) = 16
2589, 5, 5, 35, 253, 254, 256, 2, 257decaddc 12131 . . . . . . 7 (19 + 97) = 116
259 eqid 2821 . . . . . . . 8 32 = 32
260 eqid 2821 . . . . . . . . 9 11 = 11
2619, 9, 114, 260decsuc 12107 . . . . . . . 8 (11 + 1) = 12
26289oveq1i 7140 . . . . . . . . 9 ((2 · 1) + 2) = (2 + 2)
263262, 115, 2113eqtri 2848 . . . . . . . 8 ((2 · 1) + 2) = 04
26429, 3, 9, 3, 259, 261, 9, 30, 39, 206, 263decmac 12128 . . . . . . 7 ((32 · 1) + (11 + 1)) = 44
265208oveq1i 7140 . . . . . . . 8 ((4 · 1) + 6) = (4 + 6)
266 6p4e10 12148 . . . . . . . . 9 (6 + 4) = 10
26761, 207, 266addcomli 10809 . . . . . . . 8 (4 + 6) = 10
268265, 267eqtri 2844 . . . . . . 7 ((4 · 1) + 6) = 10
26933, 30, 251, 2, 252, 258, 9, 39, 9, 264, 268decmac 12128 . . . . . 6 ((324 · 1) + (19 + 97)) = 440
270145, 138eqtri 2844 . . . . . . . 8 (0 + 1) = 01
271 3t3e9 11782 . . . . . . . . . 10 (3 · 3) = 9
272271, 139oveq12i 7142 . . . . . . . . 9 ((3 · 3) + (0 + 0)) = (9 + 0)
273234addid1i 10804 . . . . . . . . 9 (9 + 0) = 9
274272, 273eqtri 2844 . . . . . . . 8 ((3 · 3) + (0 + 0)) = 9
275101oveq1i 7140 . . . . . . . . 9 ((2 · 3) + 1) = (6 + 1)
27635dec0h 12098 . . . . . . . . 9 7 = 07
277275, 216, 2763eqtri 2848 . . . . . . . 8 ((2 · 3) + 1) = 07
27829, 3, 39, 9, 259, 270, 29, 35, 39, 274, 277decmac 12128 . . . . . . 7 ((32 · 3) + (0 + 1)) = 97
279 4t3e12 12174 . . . . . . . 8 (4 · 3) = 12
280 4p2e6 11768 . . . . . . . . 9 (4 + 2) = 6
281207, 57, 280addcomli 10809 . . . . . . . 8 (2 + 4) = 6
2829, 3, 30, 279, 281decaddi 12136 . . . . . . 7 ((4 · 3) + 4) = 16
28333, 30, 39, 30, 252, 211, 29, 2, 9, 278, 282decmac 12128 . . . . . 6 ((324 · 3) + 4) = 976
2849, 29, 246, 30, 248, 249, 34, 2, 250, 269, 283decma2c 12129 . . . . 5 ((324 · 13) + 194) = 4406
285 6t3e18 12181 . . . . . . . . 9 (6 · 3) = 18
28661, 99, 285mulcomli 10627 . . . . . . . 8 (3 · 6) = 18
2879, 13, 18, 286decsuc 12107 . . . . . . 7 ((3 · 6) + 1) = 19
2889, 3, 3, 63, 115decaddi 12136 . . . . . . 7 ((2 · 6) + 2) = 14
28929, 3, 3, 259, 2, 30, 9, 287, 288decrmac 12134 . . . . . 6 ((32 · 6) + 2) = 194
290 6t4e24 12182 . . . . . . 7 (6 · 4) = 24
29161, 207, 290mulcomli 10627 . . . . . 6 (4 · 6) = 24
2922, 33, 30, 252, 30, 3, 289, 291decmul1c 12141 . . . . 5 (324 · 6) = 1944
29334, 37, 2, 245, 30, 247, 284, 292decmul2c 12142 . . . 4 (324 · 136) = 44064
294244, 293eqtr4i 2847 . . 3 ((34 · 𝑁) + (𝑁 − 1)) = (324 · 136)
29526, 1, 28, 32, 34, 23, 36, 38, 178, 179, 186, 294modxai 16381 . 2 ((2↑629) mod 𝑁) = ((𝑁 − 1) mod 𝑁)
296 eqid 2821 . . . 4 629 = 629
297 eqid 2821 . . . . 5 62 = 62
298139oveq2i 7141 . . . . . 6 ((2 · 6) + (0 + 0)) = ((2 · 6) + 0)
29963oveq1i 7140 . . . . . 6 ((2 · 6) + 0) = (12 + 0)
30010nn0cni 11887 . . . . . . 7 12 ∈ ℂ
301300addid1i 10804 . . . . . 6 (12 + 0) = 12
302298, 299, 3013eqtri 2848 . . . . 5 ((2 · 6) + (0 + 0)) = 12
30311dec0h 12098 . . . . . 6 5 = 05
30481, 55, 3033eqtri 2848 . . . . 5 ((2 · 2) + 1) = 05
3052, 3, 39, 9, 297, 138, 3, 11, 39, 302, 304decma2c 12129 . . . 4 ((2 · 62) + 1) = 125
306 9t2e18 12198 . . . . 5 (9 · 2) = 18
307234, 57, 306mulcomli 10627 . . . 4 (2 · 9) = 18
3083, 4, 5, 296, 13, 9, 305, 307decmul2c 12142 . . 3 (2 · 629) = 1258
309308, 22eqtr4i 2847 . 2 (2 · 629) = (𝑁 − 1)
310 npcan 10872 . . 3 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 − 1) + 1) = 𝑁)
31167, 16, 310mp2an 691 . 2 ((𝑁 − 1) + 1) = 𝑁
31268oveq1i 7140 . . 3 ((0 · 𝑁) + 1) = (0 + 1)
313145, 312, 1613eqtr4i 2854 . 2 ((0 · 𝑁) + 1) = (1 · 1)
3141, 6, 7, 8, 9, 23, 295, 309, 311, 313mod2xnegi 16384 1 ((2↑(𝑁 − 1)) mod 𝑁) = (1 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  (class class class)co 7130  cc 10512  0cc0 10514  1c1 10515   + caddc 10517   · cmul 10519  cmin 10847  cn 11615  2c2 11670  3c3 11671  4c4 11672  5c5 11673  6c6 11674  7c7 11675  8c8 11676  9c9 11677  0cn0 11875  cdc 12076   mod cmo 13220  cexp 13413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pow 5239  ax-pr 5303  ax-un 7436  ax-cnex 10570  ax-resscn 10571  ax-1cn 10572  ax-icn 10573  ax-addcl 10574  ax-addrcl 10575  ax-mulcl 10576  ax-mulrcl 10577  ax-mulcom 10578  ax-addass 10579  ax-mulass 10580  ax-distr 10581  ax-i2m1 10582  ax-1ne0 10583  ax-1rid 10584  ax-rnegex 10585  ax-rrecex 10586  ax-cnre 10587  ax-pre-lttri 10588  ax-pre-lttrn 10589  ax-pre-ltadd 10590  ax-pre-mulgt0 10591  ax-pre-sup 10592
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ne 3008  df-nel 3112  df-ral 3131  df-rex 3132  df-reu 3133  df-rmo 3134  df-rab 3135  df-v 3473  df-sbc 3750  df-csb 3858  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4267  df-if 4441  df-pw 4514  df-sn 4541  df-pr 4543  df-tp 4545  df-op 4547  df-uni 4812  df-iun 4894  df-br 5040  df-opab 5102  df-mpt 5120  df-tr 5146  df-id 5433  df-eprel 5438  df-po 5447  df-so 5448  df-fr 5487  df-we 5489  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-pred 6121  df-ord 6167  df-on 6168  df-lim 6169  df-suc 6170  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-riota 7088  df-ov 7133  df-oprab 7134  df-mpo 7135  df-om 7556  df-2nd 7665  df-wrecs 7922  df-recs 7983  df-rdg 8021  df-er 8264  df-en 8485  df-dom 8486  df-sdom 8487  df-sup 8882  df-inf 8883  df-pnf 10654  df-mnf 10655  df-xr 10656  df-ltxr 10657  df-le 10658  df-sub 10849  df-neg 10850  df-div 11275  df-nn 11616  df-2 11678  df-3 11679  df-4 11680  df-5 11681  df-6 11682  df-7 11683  df-8 11684  df-9 11685  df-n0 11876  df-z 11960  df-dec 12077  df-uz 12222  df-rp 12368  df-fl 13145  df-mod 13221  df-seq 13353  df-exp 13414
This theorem is referenced by:  1259prm  16448
  Copyright terms: Public domain W3C validator