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

Theorem 4001lem1 15772
Description: Lemma for 4001prm 15776. 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 11255 . . . . . 6 4 ∈ ℕ0
3 0nn0 11251 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11456 . . . . 5 40 ∈ ℕ0
54, 3deccl 11456 . . . 4 400 ∈ ℕ0
6 1nn 10975 . . . 4 1 ∈ ℕ
75, 6decnncl 11462 . . 3 4001 ∈ ℕ
81, 7eqeltri 2694 . 2 𝑁 ∈ ℕ
9 2nn 11129 . 2 2 ∈ ℕ
10 10nn0 11460 . . 3 10 ∈ ℕ0
1110, 3deccl 11456 . 2 100 ∈ ℕ0
12 9nn0 11260 . . . 4 9 ∈ ℕ0
1312, 2deccl 11456 . . 3 94 ∈ ℕ0
1413nn0zi 11346 . 2 94 ∈ ℤ
15 6nn0 11257 . . . 4 6 ∈ ℕ0
16 1nn0 11252 . . . 4 1 ∈ ℕ0
1715, 16deccl 11456 . . 3 61 ∈ ℕ0
1817, 2deccl 11456 . 2 614 ∈ ℕ0
1912, 3deccl 11456 . . 3 90 ∈ ℕ0
20 2nn0 11253 . . 3 2 ∈ ℕ0
2119, 20deccl 11456 . 2 902 ∈ ℕ0
22 5nn0 11256 . . . 4 5 ∈ ℕ0
2322, 3deccl 11456 . . 3 50 ∈ ℕ0
24 8nn0 11259 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 11456 . . . . 5 28 ∈ ℕ0
2625, 15deccl 11456 . . . 4 286 ∈ ℕ0
2726nn0zi 11346 . . 3 286 ∈ ℤ
28 7nn0 11258 . . . . 5 7 ∈ ℕ0
2910, 28deccl 11456 . . . 4 107 ∈ ℕ0
3029, 3deccl 11456 . . 3 1070 ∈ ℕ0
3120, 22deccl 11456 . . . 4 25 ∈ ℕ0
3210, 2deccl 11456 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 11456 . . . . 5 1046 ∈ ℕ0
3433nn0zi 11346 . . . 4 1046 ∈ ℤ
3520, 3deccl 11456 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 11456 . . . . 5 204 ∈ ℕ0
3736, 15deccl 11456 . . . 4 2046 ∈ ℕ0
3820, 2deccl 11456 . . . . 5 24 ∈ ℕ0
39 0z 11332 . . . . 5 0 ∈ ℤ
4010, 20deccl 11456 . . . . . 6 102 ∈ ℕ0
41 3nn0 11254 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 11456 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 11456 . . . . . 6 12 ∈ ℕ0
44 2z 11353 . . . . . 6 2 ∈ ℤ
4512, 22deccl 11456 . . . . . 6 95 ∈ ℕ0
46 1z 11351 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 11456 . . . . . . 7 64 ∈ ℕ0
48 2exp6 15719 . . . . . . . 8 (2↑6) = 64
4948oveq1i 6614 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 11046 . . . . . . . 8 6 ∈ ℂ
51 2cn 11035 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 11585 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 9991 . . . . . . 7 (2 · 6) = 12
54 eqid 2621 . . . . . . . . 9 95 = 95
55 eqid 2621 . . . . . . . . . 10 400 = 400
56 9cn 11052 . . . . . . . . . . . 12 9 ∈ ℂ
5756addid1i 10167 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 11466 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2643 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2621 . . . . . . . . . . 11 40 = 40
61 00id 10155 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 11466 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2643 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 11042 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mulid2i 9987 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 6616 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addid1i 10167 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2643 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 9938 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 10170 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 6614 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2647 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 11512 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 6614 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addid2i 10168 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2647 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 11512 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulid1i 9986 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 6614 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 11044 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 11099 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 10172 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 11466 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2647 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 11512 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2621 . . . . . . . . 9 64 = 64
87 eqid 2621 . . . . . . . . . 10 25 = 25
88 2p2e4 11088 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 6615 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 11590 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 11097 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 11542 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 11525 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2643 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 11587 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 9991 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 11111 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 10172 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 11523 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 11510 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 11098 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 11479 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 11577 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 11531 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 11533 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2646 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 15697 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2621 . . . . . . 7 12 = 12
10951mulid1i 9986 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 6614 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addid1i 10167 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2643 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 11121 . . . . . . . 8 (2 · 2) = 4
1142dec0h 11466 . . . . . . . 8 4 = 04
115113, 114eqtri 2643 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 11533 . . . . . 6 (2 · 12) = 24
117 eqid 2621 . . . . . . . 8 1023 = 1023
11840nn0cni 11248 . . . . . . . . . 10 102 ∈ ℂ
119118addid1i 10167 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 11497 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 11125 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 9991 . . . . . . . . . . . 12 (2 · 4) = 8
12369addid1i 10167 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 6616 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 11102 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2643 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 10170 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 6614 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2647 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 11512 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 6614 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addid2i 10168 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 11466 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2647 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 11512 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 6614 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 11039 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 11104 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 10172 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 11466 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2647 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 11512 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 11456 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2621 . . . . . . . . 9 47 = 47
14598oveq2i 6615 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 11614 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 11440 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 10172 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 11525 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2643 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 11610 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 9991 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 11048 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 11551 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 10172 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 11524 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 11510 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 11109 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 11523 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 11583 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 11531 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 11533 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2646 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 15697 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2621 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 11479 . . . . 5 (24 + 1) = 25
16737nn0cni 11248 . . . . . . 7 2046 ∈ ℂ
168167addid2i 10168 . . . . . 6 (0 + 2046) = 2046
1698nncni 10974 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 10169 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 6614 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2621 . . . . . . . 8 102 = 102
17320dec0u 11464 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 2, 173, 113decmul1 11529 . . . . . . 7 (102 · 2) = 204
175 3t2e6 11123 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 15, 174, 175decmul1 11529 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2653 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 15698 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 6614 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2643 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 11578 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 9991 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 11533 . . . 4 (2 · 25) = 50
184 eqid 2621 . . . . . 6 1070 = 1070
18520, 16deccl 11456 . . . . . . 7 21 ∈ ℕ0
186 eqid 2621 . . . . . . . 8 107 = 107
187 eqid 2621 . . . . . . . 8 104 = 104
188 0p1e1 11076 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 11572 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 11479 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 11549 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 11516 . . . . . . 7 (107 + 104) = 211
193185nn0cni 11248 . . . . . . . . 9 21 ∈ ℂ
194193addid1i 10167 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2694 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2621 . . . . . . . . 9 1046 = 1046
197 dfdec10 11441 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2630 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 11113 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 11523 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 11521 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 6616 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 11106 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 11523 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2643 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 11521 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 11248 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 10170 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 6614 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 11466 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2647 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 11512 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 11512 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulid1i 9986 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 6614 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addid1i 10167 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2643 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 11512 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2621 . . . . . 6 2046 = 2046
22043, 20deccl 11456 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 11456 . . . . . 6 1227 ∈ ℕ0
222 eqid 2621 . . . . . . 7 204 = 204
223 eqid 2621 . . . . . . 7 1227 = 1227
22424, 16deccl 11456 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 11456 . . . . . . 7 819 ∈ ℕ0
226 eqid 2621 . . . . . . . 8 20 = 20
227 eqid 2621 . . . . . . . . 9 122 = 122
228 eqid 2621 . . . . . . . . 9 819 = 819
229 eqid 2621 . . . . . . . . . . 11 81 = 81
230 8cn 11050 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 10172 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 11095 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 11514 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 11479 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 11563 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 10172 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 11516 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 11248 . . . . . . . . . 10 94 ∈ ℂ
239238addid1i 10167 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2694 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 10169 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 6616 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2643 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 11520 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 6614 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addid1i 10167 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 11466 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2647 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 11510 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 10172 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 11523 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 11510 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 10170 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 6614 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2647 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 11512 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 11466 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2694 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 10169 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 6616 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2643 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 11520 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 11114 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 11523 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 11510 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 10172 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 11524 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 11521 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 11512 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 10169 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 6614 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2643 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 11520 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 11107 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 11523 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 11521 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 11531 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 11533 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2646 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 15697 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 11248 . . . 4 50 ∈ ℂ
282 eqid 2621 . . . . 5 50 = 50
28320, 22, 3, 282, 3, 181, 241decmul1 11529 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 9991 . . 3 (2 · 50) = 100
285 eqid 2621 . . . . 5 614 = 614
28620, 12deccl 11456 . . . . 5 29 ∈ ℕ0
287 eqid 2621 . . . . . . 7 61 = 61
288 eqid 2621 . . . . . . 7 29 = 29
289199oveq1i 6614 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2643 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 11519 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2694 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2621 . . . . . . . 8 286 = 286
294 eqid 2621 . . . . . . . . 9 28 = 28
295122oveq1i 6614 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 11556 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2643 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 11600 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 11523 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 11521 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 6616 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 11248 . . . . . . . . . 10 24 ∈ ℂ
303302addid1i 10167 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2643 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 11521 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 11248 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 10170 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 6614 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2647 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 11512 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 6614 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2647 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 11512 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulid1i 9986 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 24, 109, 314decmul1 11529 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 11479 . . . . . 6 ((28 · 1) + 1) = 29
31750mulid1i 9986 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 6614 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2643 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 11521 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 11512 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 11456 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 11456 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 11456 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 11456 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 11456 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 11456 . . . . . . 7 749 ∈ ℕ0
328 eqid 2621 . . . . . . . 8 10 = 10
329 eqid 2621 . . . . . . . 8 749 = 749
330326nn0cni 11248 . . . . . . . . . 10 74 ∈ ℂ
331330addid1i 10167 . . . . . . . . 9 (74 + 0) = 74
332153addid1i 10167 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2694 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 11248 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulid1i 9986 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 11479 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulid1i 9986 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 6616 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 11553 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2643 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 11521 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 10169 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 6614 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addid2i 10168 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2647 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 11510 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 11248 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 10170 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 6614 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2647 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 11512 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 11441 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2630 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 11597 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 11531 . . . . . . . 8 (107 · 7) = 749
356153mul02i 10169 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 3, 355, 356decmul1 11529 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 11533 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 11523 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2643 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 11533 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2646 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 15697 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 11248 . . 3 100 ∈ ℂ
365 eqid 2621 . . . 4 100 = 100
36620, 10, 3, 365, 3, 173, 241decmul1 11529 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 9991 . 2 (2 · 100) = 200
368 eqid 2621 . . . 4 902 = 902
369 eqid 2621 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 11523 . . . . 5 (90 + 9) = 99
371 eqid 2621 . . . . . . 7 94 = 94
372 6p1e7 11100 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 11609 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 11479 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 6616 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 11456 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 11248 . . . . . . . . 9 16 ∈ ℂ
378377addid1i 10167 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2643 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 11521 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 10170 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 6614 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2647 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 11512 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 11512 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulid1i 9986 . . . . 5 (9 · 1) = 9
38764mulid1i 9986 . . . . . . 7 (4 · 1) = 4
388387oveq1i 6614 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2643 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 11520 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 11512 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 11456 . . . 4 245 ∈ ℕ0
393 eqid 2621 . . . . 5 245 = 245
39450, 51, 199addcomli 10172 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 11514 . . . . . 6 (24 + 61) = 85
396 8p2e10 11554 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 11479 . . . . . . 7 ((6 · 6) + 1) = 37
39850mulid2i 9987 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 6614 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addid1i 10167 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2643 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 11508 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 11510 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 16, 317, 78decmul1 11529 . . . . . 6 (61 · 1) = 61
405387oveq1i 6614 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2643 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 11520 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 11512 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 6614 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2643 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 11520 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 11531 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 11533 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2646 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 15697 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6604  0cc0 9880  1c1 9881   + caddc 9883   · cmul 9885  cn 10964  2c2 11014  3c3 11015  4c4 11016  5c5 11017  6c6 11018  7c7 11019  8c8 11020  9c9 11021  0cn0 11236  cdc 11437   mod cmo 12608  cexp 12800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957  ax-pre-sup 9958
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-sup 8292  df-inf 8293  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-div 10629  df-nn 10965  df-2 11023  df-3 11024  df-4 11025  df-5 11026  df-6 11027  df-7 11028  df-8 11029  df-9 11030  df-n0 11237  df-z 11322  df-dec 11438  df-uz 11632  df-rp 11777  df-fl 12533  df-mod 12609  df-seq 12742  df-exp 12801
This theorem is referenced by:  4001lem2  15773  4001lem3  15774
  Copyright terms: Public domain W3C validator