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

Theorem 4001lem1 17075
Description: Lemma for 4001prm 17079. 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 12489 . . . . . 6 4 ∈ ℕ0
3 0nn0 12485 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12690 . . . . 5 40 ∈ ℕ0
54, 3deccl 12690 . . . 4 400 ∈ ℕ0
6 1nn 12221 . . . 4 1 ∈ ℕ
75, 6decnncl 12695 . . 3 4001 ∈ ℕ
81, 7eqeltri 2821 . 2 𝑁 ∈ ℕ
9 2nn 12283 . 2 2 ∈ ℕ
10 10nn0 12693 . . 3 10 ∈ ℕ0
1110, 3deccl 12690 . 2 100 ∈ ℕ0
12 9nn0 12494 . . . 4 9 ∈ ℕ0
1312, 2deccl 12690 . . 3 94 ∈ ℕ0
1413nn0zi 12585 . 2 94 ∈ ℤ
15 6nn0 12491 . . . 4 6 ∈ ℕ0
16 1nn0 12486 . . . 4 1 ∈ ℕ0
1715, 16deccl 12690 . . 3 61 ∈ ℕ0
1817, 2deccl 12690 . 2 614 ∈ ℕ0
1912, 3deccl 12690 . . 3 90 ∈ ℕ0
20 2nn0 12487 . . 3 2 ∈ ℕ0
2119, 20deccl 12690 . 2 902 ∈ ℕ0
22 5nn0 12490 . . . 4 5 ∈ ℕ0
2322, 3deccl 12690 . . 3 50 ∈ ℕ0
24 8nn0 12493 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 12690 . . . . 5 28 ∈ ℕ0
2625, 15deccl 12690 . . . 4 286 ∈ ℕ0
2726nn0zi 12585 . . 3 286 ∈ ℤ
28 7nn0 12492 . . . . 5 7 ∈ ℕ0
2910, 28deccl 12690 . . . 4 107 ∈ ℕ0
3029, 3deccl 12690 . . 3 1070 ∈ ℕ0
3120, 22deccl 12690 . . . 4 25 ∈ ℕ0
3210, 2deccl 12690 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 12690 . . . . 5 1046 ∈ ℕ0
3433nn0zi 12585 . . . 4 1046 ∈ ℤ
3520, 3deccl 12690 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 12690 . . . . 5 204 ∈ ℕ0
3736, 15deccl 12690 . . . 4 2046 ∈ ℕ0
3820, 2deccl 12690 . . . . 5 24 ∈ ℕ0
39 0z 12567 . . . . 5 0 ∈ ℤ
4010, 20deccl 12690 . . . . . 6 102 ∈ ℕ0
41 3nn0 12488 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 12690 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 12690 . . . . . 6 12 ∈ ℕ0
44 2z 12592 . . . . . 6 2 ∈ ℤ
4512, 22deccl 12690 . . . . . 6 95 ∈ ℕ0
46 1z 12590 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 12690 . . . . . . 7 64 ∈ ℕ0
48 2exp6 17021 . . . . . . . 8 (2↑6) = 64
4948oveq1i 7412 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 12301 . . . . . . . 8 6 ∈ ℂ
51 2cn 12285 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 12779 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 11221 . . . . . . 7 (2 · 6) = 12
54 eqid 2724 . . . . . . . . 9 95 = 95
55 eqid 2724 . . . . . . . . . 10 400 = 400
56 9cn 12310 . . . . . . . . . . . 12 9 ∈ ℂ
5756addridi 11399 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 12697 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2752 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2724 . . . . . . . . . . 11 40 = 40
61 00id 11387 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 12697 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2752 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 12295 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mullidi 11217 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 7414 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addridi 11399 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2752 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 11165 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 11402 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 7412 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2756 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 12728 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 7412 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addlidi 11400 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2756 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 12728 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulridi 11216 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 7412 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 12298 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 12357 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 11404 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 12697 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2756 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 12728 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2724 . . . . . . . . 9 64 = 64
87 eqid 2724 . . . . . . . . . 10 25 = 25
88 2p2e4 12345 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 7413 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 12783 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 12355 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 12747 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 12737 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2752 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 12781 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 11221 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 12368 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 11404 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 12735 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 12727 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 12356 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 12706 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 12774 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 12740 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 12741 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2755 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 17003 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2724 . . . . . . 7 12 = 12
10951mulridi 11216 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 7412 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addridi 11399 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2752 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 12374 . . . . . . . 8 (2 · 2) = 4
1142dec0h 12697 . . . . . . . 8 4 = 04
115113, 114eqtri 2752 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 12741 . . . . . 6 (2 · 12) = 24
117 eqid 2724 . . . . . . . 8 1023 = 1023
11840nn0cni 12482 . . . . . . . . . 10 102 ∈ ℂ
119118addridi 11399 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 12718 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 12378 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 11221 . . . . . . . . . . . 12 (2 · 4) = 8
12369addridi 11399 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 7414 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 12360 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2752 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 11402 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 7412 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2756 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 12728 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 7412 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addlidi 11400 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 12697 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2756 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 12728 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 7412 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 12291 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 12361 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 11404 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 12697 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2756 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 12728 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 12690 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2724 . . . . . . . . 9 47 = 47
14598oveq2i 7413 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 12804 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 12677 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 11404 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 12737 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2752 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 12800 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 11221 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 12304 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 12752 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 11404 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 12736 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 12727 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 12366 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 12735 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 12778 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 12740 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 12741 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2755 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 17003 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2724 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 12706 . . . . 5 (24 + 1) = 25
16737nn0cni 12482 . . . . . . 7 2046 ∈ ℂ
168167addlidi 11400 . . . . . 6 (0 + 2046) = 2046
1698nncni 12220 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 11401 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 7412 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2724 . . . . . . . 8 102 = 102
17320dec0u 12696 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 173, 113decmul1 12739 . . . . . . 7 (102 · 2) = 204
175 3t2e6 12376 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 174, 175decmul1 12739 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2762 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 17004 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 7412 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2752 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 12775 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 11221 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 12741 . . . 4 (2 · 25) = 50
184 eqid 2724 . . . . . 6 1070 = 1070
18520, 16deccl 12690 . . . . . . 7 21 ∈ ℕ0
186 eqid 2724 . . . . . . . 8 107 = 107
187 eqid 2724 . . . . . . . 8 104 = 104
188 0p1e1 12332 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 12770 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 12706 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 12751 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 12730 . . . . . . 7 (107 + 104) = 211
193185nn0cni 12482 . . . . . . . . 9 21 ∈ ℂ
194193addridi 11399 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2821 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2724 . . . . . . . . 9 1046 = 1046
197 dfdec10 12678 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2733 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 12369 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 12735 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 12733 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 7414 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 12363 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 12735 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2752 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 12733 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 12482 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 11402 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 7412 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 12697 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2756 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 12728 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 12728 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulridi 11216 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 7412 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addridi 11399 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2752 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 12728 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2724 . . . . . 6 2046 = 2046
22043, 20deccl 12690 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 12690 . . . . . 6 1227 ∈ ℕ0
222 eqid 2724 . . . . . . 7 204 = 204
223 eqid 2724 . . . . . . 7 1227 = 1227
22424, 16deccl 12690 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 12690 . . . . . . 7 819 ∈ ℕ0
226 eqid 2724 . . . . . . . 8 20 = 20
227 eqid 2724 . . . . . . . . 9 122 = 122
228 eqid 2724 . . . . . . . . 9 819 = 819
229 eqid 2724 . . . . . . . . . . 11 81 = 81
230 8cn 12307 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 11404 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 12352 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 12729 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 12706 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 12762 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 11404 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 12730 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 12482 . . . . . . . . . 10 94 ∈ ℂ
239238addridi 11399 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2821 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 11401 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 7414 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2752 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 12732 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 7412 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addridi 11399 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 12697 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2756 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 12727 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 11404 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 12735 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 12727 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 11402 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 7412 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2756 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 12728 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 12697 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2821 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 11401 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 7414 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2752 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 12732 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 12370 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 12735 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 12727 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 11404 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 12736 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 12733 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 12728 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 11401 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 7412 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2752 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 12732 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 12364 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 12735 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 12733 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 12740 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 12741 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2755 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 17003 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 12482 . . . 4 50 ∈ ℂ
282 eqid 2724 . . . . 5 50 = 50
28320, 22, 3, 282, 181, 241decmul1 12739 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 11221 . . 3 (2 · 50) = 100
285 eqid 2724 . . . . 5 614 = 614
28620, 12deccl 12690 . . . . 5 29 ∈ ℕ0
287 eqid 2724 . . . . . . 7 61 = 61
288 eqid 2724 . . . . . . 7 29 = 29
289199oveq1i 7412 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2752 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 12731 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2821 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2724 . . . . . . . 8 286 = 286
294 eqid 2724 . . . . . . . . 9 28 = 28
295122oveq1i 7412 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 12756 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2752 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 12792 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 12735 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 12733 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 7414 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 12482 . . . . . . . . . 10 24 ∈ ℂ
303302addridi 11399 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2752 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 12733 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 12482 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 11402 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 7412 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2756 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 12728 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 7412 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2756 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 12728 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulridi 11216 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 109, 314decmul1 12739 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 12706 . . . . . 6 ((28 · 1) + 1) = 29
31750mulridi 11216 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 7412 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2752 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 12733 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 12728 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 12690 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 12690 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 12690 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 12690 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 12690 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 12690 . . . . . . 7 749 ∈ ℕ0
328 eqid 2724 . . . . . . . 8 10 = 10
329 eqid 2724 . . . . . . . 8 749 = 749
330326nn0cni 12482 . . . . . . . . . 10 74 ∈ ℂ
331330addridi 11399 . . . . . . . . 9 (74 + 0) = 74
332153addridi 11399 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2821 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 12482 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulridi 11216 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 12706 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulridi 11216 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 7414 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 12754 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2752 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 12733 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 11401 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 7412 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addlidi 11400 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2756 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 12727 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 12482 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 11402 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 7412 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2756 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 12728 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 12678 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2733 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 12789 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 12740 . . . . . . . 8 (107 · 7) = 749
356153mul02i 11401 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 355, 356decmul1 12739 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 12741 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 12735 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2752 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 12741 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2755 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 17003 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 12482 . . 3 100 ∈ ℂ
365 eqid 2724 . . . 4 100 = 100
36620, 10, 3, 365, 173, 241decmul1 12739 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 11221 . 2 (2 · 100) = 200
368 eqid 2724 . . . 4 902 = 902
369 eqid 2724 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 12735 . . . . 5 (90 + 9) = 99
371 eqid 2724 . . . . . . 7 94 = 94
372 6p1e7 12358 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 12799 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 12706 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 7414 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 12690 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 12482 . . . . . . . . 9 16 ∈ ℂ
378377addridi 11399 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2752 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 12733 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 11402 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 7412 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2756 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 12728 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 12728 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulridi 11216 . . . . 5 (9 · 1) = 9
38764mulridi 11216 . . . . . . 7 (4 · 1) = 4
388387oveq1i 7412 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2752 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 12732 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 12728 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 12690 . . . 4 245 ∈ ℕ0
393 eqid 2724 . . . . 5 245 = 245
39450, 51, 199addcomli 11404 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 12729 . . . . . 6 (24 + 61) = 85
396 8p2e10 12755 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 12706 . . . . . . 7 ((6 · 6) + 1) = 37
39850mullidi 11217 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 7412 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addridi 11399 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2752 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 12726 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 12727 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 317, 78decmul1 12739 . . . . . 6 (61 · 1) = 61
405387oveq1i 7412 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2752 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 12732 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 12728 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 7412 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2752 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 12732 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 12740 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 12741 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2755 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 17003 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  (class class class)co 7402  0cc0 11107  1c1 11108   + caddc 11110   · cmul 11112  cn 12210  2c2 12265  3c3 12266  4c4 12267  5c5 12268  6c6 12269  7c7 12270  8c8 12271  9c9 12272  0cn0 12470  cdc 12675   mod cmo 13832  cexp 14025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-om 7850  df-2nd 7970  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-sup 9434  df-inf 9435  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-div 11870  df-nn 12211  df-2 12273  df-3 12274  df-4 12275  df-5 12276  df-6 12277  df-7 12278  df-8 12279  df-9 12280  df-n0 12471  df-z 12557  df-dec 12676  df-uz 12821  df-rp 12973  df-fl 13755  df-mod 13833  df-seq 13965  df-exp 14026
This theorem is referenced by:  4001lem2  17076  4001lem3  17077
  Copyright terms: Public domain W3C validator