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

Theorem 4001lem1 16050
Description: Lemma for 4001prm 16054. Calculate a power mod. In decimal, we calculate 2↑12 = 4096 = 𝑁 + 95, 2↑24 = (2↑12)↑2≡95↑2 = 2𝑁 + 1023, 2↑25 = 2↑24 · 2≡1023 · 2 = 2046, 2↑50 = (2↑25)↑2≡2046↑2 = 1046𝑁 + 1070, 2↑100 = (2↑50)↑2≡1070↑2 = 286𝑁 + 614 and 2↑200 = (2↑100)↑2≡614↑2 = 94𝑁 + 902 ≡902. (Contributed by Mario Carneiro, 3-Mar-2014.) (Revised by Mario Carneiro, 20-Apr-2015.) (Proof shortened by AV, 16-Sep-2021.)
Hypothesis
Ref Expression
4001prm.1 𝑁 = 4001
Assertion
Ref Expression
4001lem1 ((2↑200) mod 𝑁) = (902 mod 𝑁)

Proof of Theorem 4001lem1
StepHypRef Expression
1 4001prm.1 . . 3 𝑁 = 4001
2 4nn0 11503 . . . . . 6 4 ∈ ℕ0
3 0nn0 11499 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11704 . . . . 5 40 ∈ ℕ0
54, 3deccl 11704 . . . 4 400 ∈ ℕ0
6 1nn 11223 . . . 4 1 ∈ ℕ
75, 6decnncl 11710 . . 3 4001 ∈ ℕ
81, 7eqeltri 2835 . 2 𝑁 ∈ ℕ
9 2nn 11377 . 2 2 ∈ ℕ
10 10nn0 11708 . . 3 10 ∈ ℕ0
1110, 3deccl 11704 . 2 100 ∈ ℕ0
12 9nn0 11508 . . . 4 9 ∈ ℕ0
1312, 2deccl 11704 . . 3 94 ∈ ℕ0
1413nn0zi 11594 . 2 94 ∈ ℤ
15 6nn0 11505 . . . 4 6 ∈ ℕ0
16 1nn0 11500 . . . 4 1 ∈ ℕ0
1715, 16deccl 11704 . . 3 61 ∈ ℕ0
1817, 2deccl 11704 . 2 614 ∈ ℕ0
1912, 3deccl 11704 . . 3 90 ∈ ℕ0
20 2nn0 11501 . . 3 2 ∈ ℕ0
2119, 20deccl 11704 . 2 902 ∈ ℕ0
22 5nn0 11504 . . . 4 5 ∈ ℕ0
2322, 3deccl 11704 . . 3 50 ∈ ℕ0
24 8nn0 11507 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 11704 . . . . 5 28 ∈ ℕ0
2625, 15deccl 11704 . . . 4 286 ∈ ℕ0
2726nn0zi 11594 . . 3 286 ∈ ℤ
28 7nn0 11506 . . . . 5 7 ∈ ℕ0
2910, 28deccl 11704 . . . 4 107 ∈ ℕ0
3029, 3deccl 11704 . . 3 1070 ∈ ℕ0
3120, 22deccl 11704 . . . 4 25 ∈ ℕ0
3210, 2deccl 11704 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 11704 . . . . 5 1046 ∈ ℕ0
3433nn0zi 11594 . . . 4 1046 ∈ ℤ
3520, 3deccl 11704 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 11704 . . . . 5 204 ∈ ℕ0
3736, 15deccl 11704 . . . 4 2046 ∈ ℕ0
3820, 2deccl 11704 . . . . 5 24 ∈ ℕ0
39 0z 11580 . . . . 5 0 ∈ ℤ
4010, 20deccl 11704 . . . . . 6 102 ∈ ℕ0
41 3nn0 11502 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 11704 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 11704 . . . . . 6 12 ∈ ℕ0
44 2z 11601 . . . . . 6 2 ∈ ℤ
4512, 22deccl 11704 . . . . . 6 95 ∈ ℕ0
46 1z 11599 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 11704 . . . . . . 7 64 ∈ ℕ0
48 2exp6 15997 . . . . . . . 8 (2↑6) = 64
4948oveq1i 6823 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 11294 . . . . . . . 8 6 ∈ ℂ
51 2cn 11283 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 11833 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 10239 . . . . . . 7 (2 · 6) = 12
54 eqid 2760 . . . . . . . . 9 95 = 95
55 eqid 2760 . . . . . . . . . 10 400 = 400
56 9cn 11300 . . . . . . . . . . . 12 9 ∈ ℂ
5756addid1i 10415 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 11714 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2782 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2760 . . . . . . . . . . 11 40 = 40
61 00id 10403 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 11714 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2782 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 11290 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mulid2i 10235 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 6825 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addid1i 10415 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2782 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 10186 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 10418 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 6823 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2786 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 11760 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 6823 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addid2i 10416 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2786 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 11760 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulid1i 10234 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 6823 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 11292 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 11347 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 10420 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 11714 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2786 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 11760 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2760 . . . . . . . . 9 64 = 64
87 eqid 2760 . . . . . . . . . 10 25 = 25
88 2p2e4 11336 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 6824 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 11838 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 11345 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 11790 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 11773 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2782 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 11835 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 10239 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 11359 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 10420 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 11771 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 11758 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 11346 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 11727 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 11825 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 11779 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 11781 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2785 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 15975 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2760 . . . . . . 7 12 = 12
10951mulid1i 10234 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 6823 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addid1i 10415 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2782 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 11369 . . . . . . . 8 (2 · 2) = 4
1142dec0h 11714 . . . . . . . 8 4 = 04
115113, 114eqtri 2782 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 11781 . . . . . 6 (2 · 12) = 24
117 eqid 2760 . . . . . . . 8 1023 = 1023
11840nn0cni 11496 . . . . . . . . . 10 102 ∈ ℂ
119118addid1i 10415 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 11745 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 11373 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 10239 . . . . . . . . . . . 12 (2 · 4) = 8
12369addid1i 10415 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 6825 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 11350 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2782 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 10418 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 6823 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2786 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 11760 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 6823 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addid2i 10416 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 11714 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2786 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 11760 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 6823 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 11287 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 11352 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 10420 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 11714 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2786 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 11760 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 11704 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2760 . . . . . . . . 9 47 = 47
14598oveq2i 6824 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 11862 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 11688 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 10420 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 11773 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2782 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 11858 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 10239 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 11296 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 11799 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 10420 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 11772 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 11758 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 11357 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 11771 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 11831 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 11779 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 11781 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2785 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 15975 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2760 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 11727 . . . . 5 (24 + 1) = 25
16737nn0cni 11496 . . . . . . 7 2046 ∈ ℂ
168167addid2i 10416 . . . . . 6 (0 + 2046) = 2046
1698nncni 11222 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 10417 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 6823 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2760 . . . . . . . 8 102 = 102
17320dec0u 11712 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 2, 173, 113decmul1 11777 . . . . . . 7 (102 · 2) = 204
175 3t2e6 11371 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 15, 174, 175decmul1 11777 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2792 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 15976 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 6823 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2782 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 11826 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 10239 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 11781 . . . 4 (2 · 25) = 50
184 eqid 2760 . . . . . 6 1070 = 1070
18520, 16deccl 11704 . . . . . . 7 21 ∈ ℕ0
186 eqid 2760 . . . . . . . 8 107 = 107
187 eqid 2760 . . . . . . . 8 104 = 104
188 0p1e1 11324 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 11820 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 11727 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 11797 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 11764 . . . . . . 7 (107 + 104) = 211
193185nn0cni 11496 . . . . . . . . 9 21 ∈ ℂ
194193addid1i 10415 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2835 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2760 . . . . . . . . 9 1046 = 1046
197 dfdec10 11689 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2769 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 11361 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 11771 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 11769 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 6825 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 11354 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 11771 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2782 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 11769 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 11496 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 10418 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 6823 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 11714 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2786 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 11760 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 11760 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulid1i 10234 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 6823 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addid1i 10415 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2782 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 11760 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2760 . . . . . 6 2046 = 2046
22043, 20deccl 11704 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 11704 . . . . . 6 1227 ∈ ℕ0
222 eqid 2760 . . . . . . 7 204 = 204
223 eqid 2760 . . . . . . 7 1227 = 1227
22424, 16deccl 11704 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 11704 . . . . . . 7 819 ∈ ℕ0
226 eqid 2760 . . . . . . . 8 20 = 20
227 eqid 2760 . . . . . . . . 9 122 = 122
228 eqid 2760 . . . . . . . . 9 819 = 819
229 eqid 2760 . . . . . . . . . . 11 81 = 81
230 8cn 11298 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 10420 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 11343 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 11762 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 11727 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 11811 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 10420 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 11764 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 11496 . . . . . . . . . 10 94 ∈ ℂ
239238addid1i 10415 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2835 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 10417 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 6825 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2782 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 11768 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 6823 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addid1i 10415 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 11714 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2786 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 11758 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 10420 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 11771 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 11758 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 10418 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 6823 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2786 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 11760 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 11714 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2835 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 10417 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 6825 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2782 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 11768 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 11362 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 11771 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 11758 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 10420 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 11772 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 11769 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 11760 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 10417 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 6823 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2782 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 11768 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 11355 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 11771 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 11769 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 11779 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 11781 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2785 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 15975 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 11496 . . . 4 50 ∈ ℂ
282 eqid 2760 . . . . 5 50 = 50
28320, 22, 3, 282, 3, 181, 241decmul1 11777 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 10239 . . 3 (2 · 50) = 100
285 eqid 2760 . . . . 5 614 = 614
28620, 12deccl 11704 . . . . 5 29 ∈ ℕ0
287 eqid 2760 . . . . . . 7 61 = 61
288 eqid 2760 . . . . . . 7 29 = 29
289199oveq1i 6823 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2782 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 11767 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2835 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2760 . . . . . . . 8 286 = 286
294 eqid 2760 . . . . . . . . 9 28 = 28
295122oveq1i 6823 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 11804 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2782 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 11848 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 11771 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 11769 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 6825 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 11496 . . . . . . . . . 10 24 ∈ ℂ
303302addid1i 10415 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2782 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 11769 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 11496 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 10418 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 6823 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2786 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 11760 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 6823 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2786 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 11760 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulid1i 10234 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 24, 109, 314decmul1 11777 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 11727 . . . . . 6 ((28 · 1) + 1) = 29
31750mulid1i 10234 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 6823 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2782 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 11769 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 11760 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 11704 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 11704 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 11704 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 11704 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 11704 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 11704 . . . . . . 7 749 ∈ ℕ0
328 eqid 2760 . . . . . . . 8 10 = 10
329 eqid 2760 . . . . . . . 8 749 = 749
330326nn0cni 11496 . . . . . . . . . 10 74 ∈ ℂ
331330addid1i 10415 . . . . . . . . 9 (74 + 0) = 74
332153addid1i 10415 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2835 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 11496 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulid1i 10234 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 11727 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulid1i 10234 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 6825 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 11801 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2782 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 11769 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 10417 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 6823 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addid2i 10416 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2786 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 11758 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 11496 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 10418 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 6823 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2786 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 11760 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 11689 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2769 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 11845 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 11779 . . . . . . . 8 (107 · 7) = 749
356153mul02i 10417 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 3, 355, 356decmul1 11777 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 11781 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 11771 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2782 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 11781 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2785 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 15975 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 11496 . . 3 100 ∈ ℂ
365 eqid 2760 . . . 4 100 = 100
36620, 10, 3, 365, 3, 173, 241decmul1 11777 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 10239 . 2 (2 · 100) = 200
368 eqid 2760 . . . 4 902 = 902
369 eqid 2760 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 11771 . . . . 5 (90 + 9) = 99
371 eqid 2760 . . . . . . 7 94 = 94
372 6p1e7 11348 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 11857 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 11727 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 6825 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 11704 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 11496 . . . . . . . . 9 16 ∈ ℂ
378377addid1i 10415 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2782 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 11769 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 10418 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 6823 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2786 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 11760 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 11760 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulid1i 10234 . . . . 5 (9 · 1) = 9
38764mulid1i 10234 . . . . . . 7 (4 · 1) = 4
388387oveq1i 6823 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2782 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 11768 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 11760 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 11704 . . . 4 245 ∈ ℕ0
393 eqid 2760 . . . . 5 245 = 245
39450, 51, 199addcomli 10420 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 11762 . . . . . 6 (24 + 61) = 85
396 8p2e10 11802 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 11727 . . . . . . 7 ((6 · 6) + 1) = 37
39850mulid2i 10235 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 6823 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addid1i 10415 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2782 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 11756 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 11758 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 16, 317, 78decmul1 11777 . . . . . 6 (61 · 1) = 61
405387oveq1i 6823 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2782 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 11768 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 11760 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 6823 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2782 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 11768 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 11779 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 11781 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2785 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 15975 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  (class class class)co 6813  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133  cn 11212  2c2 11262  3c3 11263  4c4 11264  5c5 11265  6c6 11266  7c7 11267  8c8 11268  9c9 11269  0cn0 11484  cdc 11685   mod cmo 12862  cexp 13054
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-sup 8513  df-inf 8514  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-rp 12026  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055
This theorem is referenced by:  4001lem2  16051  4001lem3  16052
  Copyright terms: Public domain W3C validator