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

Theorem 4001lem1 17178
Description: Lemma for 4001prm 17182. 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 12545 . . . . . 6 4 ∈ ℕ0
3 0nn0 12541 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12748 . . . . 5 40 ∈ ℕ0
54, 3deccl 12748 . . . 4 400 ∈ ℕ0
6 1nn 12277 . . . 4 1 ∈ ℕ
75, 6decnncl 12753 . . 3 4001 ∈ ℕ
81, 7eqeltri 2837 . 2 𝑁 ∈ ℕ
9 2nn 12339 . 2 2 ∈ ℕ
10 10nn0 12751 . . 3 10 ∈ ℕ0
1110, 3deccl 12748 . 2 100 ∈ ℕ0
12 9nn0 12550 . . . 4 9 ∈ ℕ0
1312, 2deccl 12748 . . 3 94 ∈ ℕ0
1413nn0zi 12642 . 2 94 ∈ ℤ
15 6nn0 12547 . . . 4 6 ∈ ℕ0
16 1nn0 12542 . . . 4 1 ∈ ℕ0
1715, 16deccl 12748 . . 3 61 ∈ ℕ0
1817, 2deccl 12748 . 2 614 ∈ ℕ0
1912, 3deccl 12748 . . 3 90 ∈ ℕ0
20 2nn0 12543 . . 3 2 ∈ ℕ0
2119, 20deccl 12748 . 2 902 ∈ ℕ0
22 5nn0 12546 . . . 4 5 ∈ ℕ0
2322, 3deccl 12748 . . 3 50 ∈ ℕ0
24 8nn0 12549 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 12748 . . . . 5 28 ∈ ℕ0
2625, 15deccl 12748 . . . 4 286 ∈ ℕ0
2726nn0zi 12642 . . 3 286 ∈ ℤ
28 7nn0 12548 . . . . 5 7 ∈ ℕ0
2910, 28deccl 12748 . . . 4 107 ∈ ℕ0
3029, 3deccl 12748 . . 3 1070 ∈ ℕ0
3120, 22deccl 12748 . . . 4 25 ∈ ℕ0
3210, 2deccl 12748 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 12748 . . . . 5 1046 ∈ ℕ0
3433nn0zi 12642 . . . 4 1046 ∈ ℤ
3520, 3deccl 12748 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 12748 . . . . 5 204 ∈ ℕ0
3736, 15deccl 12748 . . . 4 2046 ∈ ℕ0
3820, 2deccl 12748 . . . . 5 24 ∈ ℕ0
39 0z 12624 . . . . 5 0 ∈ ℤ
4010, 20deccl 12748 . . . . . 6 102 ∈ ℕ0
41 3nn0 12544 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 12748 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 12748 . . . . . 6 12 ∈ ℕ0
44 2z 12649 . . . . . 6 2 ∈ ℤ
4512, 22deccl 12748 . . . . . 6 95 ∈ ℕ0
46 1z 12647 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 12748 . . . . . . 7 64 ∈ ℕ0
48 2exp6 17124 . . . . . . . 8 (2↑6) = 64
4948oveq1i 7441 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 12357 . . . . . . . 8 6 ∈ ℂ
51 2cn 12341 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 12837 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 11270 . . . . . . 7 (2 · 6) = 12
54 eqid 2737 . . . . . . . . 9 95 = 95
55 eqid 2737 . . . . . . . . . 10 400 = 400
56 9cn 12366 . . . . . . . . . . . 12 9 ∈ ℂ
5756addridi 11448 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 12755 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2765 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2737 . . . . . . . . . . 11 40 = 40
61 00id 11436 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 12755 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2765 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 12351 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mullidi 11266 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 7443 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addridi 11448 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2765 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 11213 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 11451 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 7441 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2769 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 12786 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 7441 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addlidi 11449 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2769 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 12786 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulridi 11265 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 7441 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 12354 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 12413 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 11453 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 12755 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2769 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 12786 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2737 . . . . . . . . 9 64 = 64
87 eqid 2737 . . . . . . . . . 10 25 = 25
88 2p2e4 12401 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 7442 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 12841 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 12411 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 12805 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 12795 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2765 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 12839 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 11270 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 12424 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 11453 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 12793 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 12785 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 12412 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 12764 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 12832 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 12798 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 12799 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2768 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 17107 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2737 . . . . . . 7 12 = 12
10951mulridi 11265 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 7441 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addridi 11448 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2765 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 12430 . . . . . . . 8 (2 · 2) = 4
1142dec0h 12755 . . . . . . . 8 4 = 04
115113, 114eqtri 2765 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 12799 . . . . . 6 (2 · 12) = 24
117 eqid 2737 . . . . . . . 8 1023 = 1023
11840nn0cni 12538 . . . . . . . . . 10 102 ∈ ℂ
119118addridi 11448 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 12776 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 12434 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 11270 . . . . . . . . . . . 12 (2 · 4) = 8
12369addridi 11448 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 7443 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 12416 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2765 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 11451 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 7441 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2769 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 12786 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 7441 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addlidi 11449 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 12755 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2769 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 12786 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 7441 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 12347 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 12417 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 11453 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 12755 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2769 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 12786 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 12748 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2737 . . . . . . . . 9 47 = 47
14598oveq2i 7442 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 12862 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 12735 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 11453 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 12795 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2765 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 12858 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 11270 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 12360 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 12810 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 11453 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 12794 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 12785 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 12422 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 12793 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 12836 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 12798 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 12799 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2768 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 17107 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2737 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 12764 . . . . 5 (24 + 1) = 25
16737nn0cni 12538 . . . . . . 7 2046 ∈ ℂ
168167addlidi 11449 . . . . . 6 (0 + 2046) = 2046
1698nncni 12276 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 11450 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 7441 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2737 . . . . . . . 8 102 = 102
17320dec0u 12754 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 173, 113decmul1 12797 . . . . . . 7 (102 · 2) = 204
175 3t2e6 12432 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 174, 175decmul1 12797 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2775 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 17108 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 7441 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2765 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 12833 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 11270 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 12799 . . . 4 (2 · 25) = 50
184 eqid 2737 . . . . . 6 1070 = 1070
18520, 16deccl 12748 . . . . . . 7 21 ∈ ℕ0
186 eqid 2737 . . . . . . . 8 107 = 107
187 eqid 2737 . . . . . . . 8 104 = 104
188 0p1e1 12388 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 12828 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 12764 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 12809 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 12788 . . . . . . 7 (107 + 104) = 211
193185nn0cni 12538 . . . . . . . . 9 21 ∈ ℂ
194193addridi 11448 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2837 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2737 . . . . . . . . 9 1046 = 1046
197 dfdec10 12736 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2746 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 12425 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 12793 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 12791 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 7443 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 12419 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 12793 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2765 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 12791 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 12538 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 11451 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 7441 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 12755 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2769 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 12786 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 12786 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulridi 11265 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 7441 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addridi 11448 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2765 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 12786 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2737 . . . . . 6 2046 = 2046
22043, 20deccl 12748 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 12748 . . . . . 6 1227 ∈ ℕ0
222 eqid 2737 . . . . . . 7 204 = 204
223 eqid 2737 . . . . . . 7 1227 = 1227
22424, 16deccl 12748 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 12748 . . . . . . 7 819 ∈ ℕ0
226 eqid 2737 . . . . . . . 8 20 = 20
227 eqid 2737 . . . . . . . . 9 122 = 122
228 eqid 2737 . . . . . . . . 9 819 = 819
229 eqid 2737 . . . . . . . . . . 11 81 = 81
230 8cn 12363 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 11453 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 12408 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 12787 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 12764 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 12820 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 11453 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 12788 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 12538 . . . . . . . . . 10 94 ∈ ℂ
239238addridi 11448 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2837 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 11450 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 7443 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2765 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 12790 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 7441 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addridi 11448 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 12755 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2769 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 12785 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 11453 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 12793 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 12785 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 11451 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 7441 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2769 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 12786 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 12755 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2837 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 11450 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 7443 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2765 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 12790 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 12426 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 12793 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 12785 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 11453 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 12794 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 12791 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 12786 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 11450 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 7441 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2765 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 12790 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 12420 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 12793 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 12791 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 12798 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 12799 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2768 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 17107 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 12538 . . . 4 50 ∈ ℂ
282 eqid 2737 . . . . 5 50 = 50
28320, 22, 3, 282, 181, 241decmul1 12797 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 11270 . . 3 (2 · 50) = 100
285 eqid 2737 . . . . 5 614 = 614
28620, 12deccl 12748 . . . . 5 29 ∈ ℕ0
287 eqid 2737 . . . . . . 7 61 = 61
288 eqid 2737 . . . . . . 7 29 = 29
289199oveq1i 7441 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2765 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 12789 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2837 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2737 . . . . . . . 8 286 = 286
294 eqid 2737 . . . . . . . . 9 28 = 28
295122oveq1i 7441 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 12814 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2765 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 12850 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 12793 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 12791 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 7443 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 12538 . . . . . . . . . 10 24 ∈ ℂ
303302addridi 11448 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2765 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 12791 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 12538 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 11451 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 7441 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2769 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 12786 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 7441 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2769 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 12786 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulridi 11265 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 109, 314decmul1 12797 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 12764 . . . . . 6 ((28 · 1) + 1) = 29
31750mulridi 11265 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 7441 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2765 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 12791 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 12786 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 12748 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 12748 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 12748 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 12748 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 12748 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 12748 . . . . . . 7 749 ∈ ℕ0
328 eqid 2737 . . . . . . . 8 10 = 10
329 eqid 2737 . . . . . . . 8 749 = 749
330326nn0cni 12538 . . . . . . . . . 10 74 ∈ ℂ
331330addridi 11448 . . . . . . . . 9 (74 + 0) = 74
332153addridi 11448 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2837 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 12538 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulridi 11265 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 12764 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulridi 11265 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 7443 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 12812 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2765 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 12791 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 11450 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 7441 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addlidi 11449 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2769 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 12785 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 12538 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 11451 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 7441 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2769 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 12786 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 12736 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2746 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 12847 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 12798 . . . . . . . 8 (107 · 7) = 749
356153mul02i 11450 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 355, 356decmul1 12797 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 12799 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 12793 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2765 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 12799 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2768 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 17107 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 12538 . . 3 100 ∈ ℂ
365 eqid 2737 . . . 4 100 = 100
36620, 10, 3, 365, 173, 241decmul1 12797 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 11270 . 2 (2 · 100) = 200
368 eqid 2737 . . . 4 902 = 902
369 eqid 2737 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 12793 . . . . 5 (90 + 9) = 99
371 eqid 2737 . . . . . . 7 94 = 94
372 6p1e7 12414 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 12857 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 12764 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 7443 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 12748 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 12538 . . . . . . . . 9 16 ∈ ℂ
378377addridi 11448 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2765 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 12791 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 11451 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 7441 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2769 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 12786 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 12786 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulridi 11265 . . . . 5 (9 · 1) = 9
38764mulridi 11265 . . . . . . 7 (4 · 1) = 4
388387oveq1i 7441 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2765 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 12790 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 12786 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 12748 . . . 4 245 ∈ ℕ0
393 eqid 2737 . . . . 5 245 = 245
39450, 51, 199addcomli 11453 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 12787 . . . . . 6 (24 + 61) = 85
396 8p2e10 12813 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 12764 . . . . . . 7 ((6 · 6) + 1) = 37
39850mullidi 11266 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 7441 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addridi 11448 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2765 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 12784 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 12785 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 317, 78decmul1 12797 . . . . . 6 (61 · 1) = 61
405387oveq1i 7441 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2765 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 12790 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 12786 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 7441 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2765 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 12790 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 12798 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 12799 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2768 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 17107 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  (class class class)co 7431  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  cn 12266  2c2 12321  3c3 12322  4c4 12323  5c5 12324  6c6 12325  7c7 12326  8c8 12327  9c9 12328  0cn0 12526  cdc 12733   mod cmo 13909  cexp 14102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-sup 9482  df-inf 9483  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103
This theorem is referenced by:  4001lem2  17179  4001lem3  17180
  Copyright terms: Public domain W3C validator