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

Theorem 4001lem1 16046
Description: Lemma for 4001prm 16050. 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 11499 . . . . . 6 4 ∈ ℕ0
3 0nn0 11495 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11700 . . . . 5 40 ∈ ℕ0
54, 3deccl 11700 . . . 4 400 ∈ ℕ0
6 1nn 11219 . . . 4 1 ∈ ℕ
75, 6decnncl 11706 . . 3 4001 ∈ ℕ
81, 7eqeltri 2831 . 2 𝑁 ∈ ℕ
9 2nn 11373 . 2 2 ∈ ℕ
10 10nn0 11704 . . 3 10 ∈ ℕ0
1110, 3deccl 11700 . 2 100 ∈ ℕ0
12 9nn0 11504 . . . 4 9 ∈ ℕ0
1312, 2deccl 11700 . . 3 94 ∈ ℕ0
1413nn0zi 11590 . 2 94 ∈ ℤ
15 6nn0 11501 . . . 4 6 ∈ ℕ0
16 1nn0 11496 . . . 4 1 ∈ ℕ0
1715, 16deccl 11700 . . 3 61 ∈ ℕ0
1817, 2deccl 11700 . 2 614 ∈ ℕ0
1912, 3deccl 11700 . . 3 90 ∈ ℕ0
20 2nn0 11497 . . 3 2 ∈ ℕ0
2119, 20deccl 11700 . 2 902 ∈ ℕ0
22 5nn0 11500 . . . 4 5 ∈ ℕ0
2322, 3deccl 11700 . . 3 50 ∈ ℕ0
24 8nn0 11503 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 11700 . . . . 5 28 ∈ ℕ0
2625, 15deccl 11700 . . . 4 286 ∈ ℕ0
2726nn0zi 11590 . . 3 286 ∈ ℤ
28 7nn0 11502 . . . . 5 7 ∈ ℕ0
2910, 28deccl 11700 . . . 4 107 ∈ ℕ0
3029, 3deccl 11700 . . 3 1070 ∈ ℕ0
3120, 22deccl 11700 . . . 4 25 ∈ ℕ0
3210, 2deccl 11700 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 11700 . . . . 5 1046 ∈ ℕ0
3433nn0zi 11590 . . . 4 1046 ∈ ℤ
3520, 3deccl 11700 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 11700 . . . . 5 204 ∈ ℕ0
3736, 15deccl 11700 . . . 4 2046 ∈ ℕ0
3820, 2deccl 11700 . . . . 5 24 ∈ ℕ0
39 0z 11576 . . . . 5 0 ∈ ℤ
4010, 20deccl 11700 . . . . . 6 102 ∈ ℕ0
41 3nn0 11498 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 11700 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 11700 . . . . . 6 12 ∈ ℕ0
44 2z 11597 . . . . . 6 2 ∈ ℤ
4512, 22deccl 11700 . . . . . 6 95 ∈ ℕ0
46 1z 11595 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 11700 . . . . . . 7 64 ∈ ℕ0
48 2exp6 15993 . . . . . . . 8 (2↑6) = 64
4948oveq1i 6819 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 11290 . . . . . . . 8 6 ∈ ℂ
51 2cn 11279 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 11829 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 10235 . . . . . . 7 (2 · 6) = 12
54 eqid 2756 . . . . . . . . 9 95 = 95
55 eqid 2756 . . . . . . . . . 10 400 = 400
56 9cn 11296 . . . . . . . . . . . 12 9 ∈ ℂ
5756addid1i 10411 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 11710 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2778 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2756 . . . . . . . . . . 11 40 = 40
61 00id 10399 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 11710 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2778 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 11286 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mulid2i 10231 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 6821 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addid1i 10411 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2778 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 10182 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 10414 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 6819 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2782 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 11756 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 6819 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addid2i 10412 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2782 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 11756 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulid1i 10230 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 6819 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 11288 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 11343 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 10416 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 11710 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2782 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 11756 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2756 . . . . . . . . 9 64 = 64
87 eqid 2756 . . . . . . . . . 10 25 = 25
88 2p2e4 11332 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 6820 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 11834 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 11341 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 11786 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 11769 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2778 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 11831 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 10235 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 11355 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 10416 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 11767 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 11754 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 11342 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 11723 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 11821 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 11775 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 11777 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2781 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 15971 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2756 . . . . . . 7 12 = 12
10951mulid1i 10230 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 6819 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addid1i 10411 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2778 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 11365 . . . . . . . 8 (2 · 2) = 4
1142dec0h 11710 . . . . . . . 8 4 = 04
115113, 114eqtri 2778 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 11777 . . . . . 6 (2 · 12) = 24
117 eqid 2756 . . . . . . . 8 1023 = 1023
11840nn0cni 11492 . . . . . . . . . 10 102 ∈ ℂ
119118addid1i 10411 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 11741 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 11369 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 10235 . . . . . . . . . . . 12 (2 · 4) = 8
12369addid1i 10411 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 6821 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 11346 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2778 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 10414 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 6819 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2782 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 11756 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 6819 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addid2i 10412 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 11710 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2782 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 11756 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 6819 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 11283 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 11348 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 10416 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 11710 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2782 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 11756 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 11700 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2756 . . . . . . . . 9 47 = 47
14598oveq2i 6820 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 11858 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 11684 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 10416 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 11769 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2778 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 11854 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 10235 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 11292 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 11795 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 10416 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 11768 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 11754 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 11353 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 11767 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 11827 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 11775 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 11777 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2781 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 15971 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2756 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 11723 . . . . 5 (24 + 1) = 25
16737nn0cni 11492 . . . . . . 7 2046 ∈ ℂ
168167addid2i 10412 . . . . . 6 (0 + 2046) = 2046
1698nncni 11218 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 10413 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 6819 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2756 . . . . . . . 8 102 = 102
17320dec0u 11708 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 2, 173, 113decmul1 11773 . . . . . . 7 (102 · 2) = 204
175 3t2e6 11367 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 15, 174, 175decmul1 11773 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2788 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 15972 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 6819 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2778 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 11822 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 10235 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 11777 . . . 4 (2 · 25) = 50
184 eqid 2756 . . . . . 6 1070 = 1070
18520, 16deccl 11700 . . . . . . 7 21 ∈ ℕ0
186 eqid 2756 . . . . . . . 8 107 = 107
187 eqid 2756 . . . . . . . 8 104 = 104
188 0p1e1 11320 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 11816 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 11723 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 11793 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 11760 . . . . . . 7 (107 + 104) = 211
193185nn0cni 11492 . . . . . . . . 9 21 ∈ ℂ
194193addid1i 10411 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2831 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2756 . . . . . . . . 9 1046 = 1046
197 dfdec10 11685 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2765 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 11357 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 11767 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 11765 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 6821 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 11350 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 11767 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2778 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 11765 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 11492 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 10414 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 6819 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 11710 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2782 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 11756 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 11756 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulid1i 10230 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 6819 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addid1i 10411 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2778 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 11756 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2756 . . . . . 6 2046 = 2046
22043, 20deccl 11700 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 11700 . . . . . 6 1227 ∈ ℕ0
222 eqid 2756 . . . . . . 7 204 = 204
223 eqid 2756 . . . . . . 7 1227 = 1227
22424, 16deccl 11700 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 11700 . . . . . . 7 819 ∈ ℕ0
226 eqid 2756 . . . . . . . 8 20 = 20
227 eqid 2756 . . . . . . . . 9 122 = 122
228 eqid 2756 . . . . . . . . 9 819 = 819
229 eqid 2756 . . . . . . . . . . 11 81 = 81
230 8cn 11294 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 10416 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 11339 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 11758 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 11723 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 11807 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 10416 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 11760 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 11492 . . . . . . . . . 10 94 ∈ ℂ
239238addid1i 10411 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2831 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 10413 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 6821 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2778 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 11764 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 6819 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addid1i 10411 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 11710 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2782 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 11754 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 10416 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 11767 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 11754 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 10414 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 6819 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2782 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 11756 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 11710 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2831 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 10413 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 6821 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2778 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 11764 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 11358 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 11767 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 11754 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 10416 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 11768 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 11765 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 11756 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 10413 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 6819 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2778 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 11764 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 11351 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 11767 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 11765 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 11775 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 11777 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2781 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 15971 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 11492 . . . 4 50 ∈ ℂ
282 eqid 2756 . . . . 5 50 = 50
28320, 22, 3, 282, 3, 181, 241decmul1 11773 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 10235 . . 3 (2 · 50) = 100
285 eqid 2756 . . . . 5 614 = 614
28620, 12deccl 11700 . . . . 5 29 ∈ ℕ0
287 eqid 2756 . . . . . . 7 61 = 61
288 eqid 2756 . . . . . . 7 29 = 29
289199oveq1i 6819 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2778 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 11763 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2831 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2756 . . . . . . . 8 286 = 286
294 eqid 2756 . . . . . . . . 9 28 = 28
295122oveq1i 6819 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 11800 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2778 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 11844 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 11767 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 11765 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 6821 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 11492 . . . . . . . . . 10 24 ∈ ℂ
303302addid1i 10411 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2778 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 11765 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 11492 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 10414 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 6819 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2782 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 11756 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 6819 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2782 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 11756 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulid1i 10230 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 24, 109, 314decmul1 11773 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 11723 . . . . . 6 ((28 · 1) + 1) = 29
31750mulid1i 10230 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 6819 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2778 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 11765 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 11756 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 11700 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 11700 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 11700 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 11700 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 11700 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 11700 . . . . . . 7 749 ∈ ℕ0
328 eqid 2756 . . . . . . . 8 10 = 10
329 eqid 2756 . . . . . . . 8 749 = 749
330326nn0cni 11492 . . . . . . . . . 10 74 ∈ ℂ
331330addid1i 10411 . . . . . . . . 9 (74 + 0) = 74
332153addid1i 10411 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2831 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 11492 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulid1i 10230 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 11723 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulid1i 10230 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 6821 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 11797 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2778 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 11765 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 10413 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 6819 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addid2i 10412 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2782 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 11754 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 11492 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 10414 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 6819 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2782 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 11756 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 11685 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2765 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 11841 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 11775 . . . . . . . 8 (107 · 7) = 749
356153mul02i 10413 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 3, 355, 356decmul1 11773 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 11777 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 11767 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2778 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 11777 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2781 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 15971 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 11492 . . 3 100 ∈ ℂ
365 eqid 2756 . . . 4 100 = 100
36620, 10, 3, 365, 3, 173, 241decmul1 11773 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 10235 . 2 (2 · 100) = 200
368 eqid 2756 . . . 4 902 = 902
369 eqid 2756 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 11767 . . . . 5 (90 + 9) = 99
371 eqid 2756 . . . . . . 7 94 = 94
372 6p1e7 11344 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 11853 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 11723 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 6821 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 11700 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 11492 . . . . . . . . 9 16 ∈ ℂ
378377addid1i 10411 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2778 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 11765 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 10414 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 6819 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2782 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 11756 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 11756 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulid1i 10230 . . . . 5 (9 · 1) = 9
38764mulid1i 10230 . . . . . . 7 (4 · 1) = 4
388387oveq1i 6819 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2778 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 11764 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 11756 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 11700 . . . 4 245 ∈ ℕ0
393 eqid 2756 . . . . 5 245 = 245
39450, 51, 199addcomli 10416 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 11758 . . . . . 6 (24 + 61) = 85
396 8p2e10 11798 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 11723 . . . . . . 7 ((6 · 6) + 1) = 37
39850mulid2i 10231 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 6819 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addid1i 10411 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2778 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 11752 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 11754 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 16, 317, 78decmul1 11773 . . . . . 6 (61 · 1) = 61
405387oveq1i 6819 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2778 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 11764 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 11756 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 6819 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2778 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 11764 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 11775 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 11777 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2781 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 15971 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1628  (class class class)co 6809  0cc0 10124  1c1 10125   + caddc 10127   · cmul 10129  cn 11208  2c2 11258  3c3 11259  4c4 11260  5c5 11261  6c6 11262  7c7 11263  8c8 11264  9c9 11265  0cn0 11480  cdc 11681   mod cmo 12858  cexp 13050
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1867  ax-4 1882  ax-5 1984  ax-6 2050  ax-7 2086  ax-8 2137  ax-9 2144  ax-10 2164  ax-11 2179  ax-12 2192  ax-13 2387  ax-ext 2736  ax-sep 4929  ax-nul 4937  ax-pow 4988  ax-pr 5051  ax-un 7110  ax-cnex 10180  ax-resscn 10181  ax-1cn 10182  ax-icn 10183  ax-addcl 10184  ax-addrcl 10185  ax-mulcl 10186  ax-mulrcl 10187  ax-mulcom 10188  ax-addass 10189  ax-mulass 10190  ax-distr 10191  ax-i2m1 10192  ax-1ne0 10193  ax-1rid 10194  ax-rnegex 10195  ax-rrecex 10196  ax-cnre 10197  ax-pre-lttri 10198  ax-pre-lttrn 10199  ax-pre-ltadd 10200  ax-pre-mulgt0 10201  ax-pre-sup 10202
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1631  df-ex 1850  df-nf 1855  df-sb 2043  df-eu 2607  df-mo 2608  df-clab 2743  df-cleq 2749  df-clel 2752  df-nfc 2887  df-ne 2929  df-nel 3032  df-ral 3051  df-rex 3052  df-reu 3053  df-rmo 3054  df-rab 3055  df-v 3338  df-sbc 3573  df-csb 3671  df-dif 3714  df-un 3716  df-in 3718  df-ss 3725  df-pss 3727  df-nul 4055  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4585  df-iun 4670  df-br 4801  df-opab 4861  df-mpt 4878  df-tr 4901  df-id 5170  df-eprel 5175  df-po 5183  df-so 5184  df-fr 5221  df-we 5223  df-xp 5268  df-rel 5269  df-cnv 5270  df-co 5271  df-dm 5272  df-rn 5273  df-res 5274  df-ima 5275  df-pred 5837  df-ord 5883  df-on 5884  df-lim 5885  df-suc 5886  df-iota 6008  df-fun 6047  df-fn 6048  df-f 6049  df-f1 6050  df-fo 6051  df-f1o 6052  df-fv 6053  df-riota 6770  df-ov 6812  df-oprab 6813  df-mpt2 6814  df-om 7227  df-2nd 7330  df-wrecs 7572  df-recs 7633  df-rdg 7671  df-er 7907  df-en 8118  df-dom 8119  df-sdom 8120  df-sup 8509  df-inf 8510  df-pnf 10264  df-mnf 10265  df-xr 10266  df-ltxr 10267  df-le 10268  df-sub 10456  df-neg 10457  df-div 10873  df-nn 11209  df-2 11267  df-3 11268  df-4 11269  df-5 11270  df-6 11271  df-7 11272  df-8 11273  df-9 11274  df-n0 11481  df-z 11566  df-dec 11682  df-uz 11876  df-rp 12022  df-fl 12783  df-mod 12859  df-seq 12992  df-exp 13051
This theorem is referenced by:  4001lem2  16047  4001lem3  16048
  Copyright terms: Public domain W3C validator