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

Theorem 4001lem1 15686
 Description: Lemma for 4001prm 15690. 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 11188 . . . . . 6 4 ∈ ℕ0
3 0nn0 11184 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11388 . . . . 5 40 ∈ ℕ0
54, 3deccl 11388 . . . 4 400 ∈ ℕ0
6 1nn 10908 . . . 4 1 ∈ ℕ
75, 6decnncl 11394 . . 3 4001 ∈ ℕ
81, 7eqeltri 2684 . 2 𝑁 ∈ ℕ
9 2nn 11062 . 2 2 ∈ ℕ
10 10nn0 11392 . . 3 10 ∈ ℕ0
1110, 3deccl 11388 . 2 100 ∈ ℕ0
12 9nn0 11193 . . . 4 9 ∈ ℕ0
1312, 2deccl 11388 . . 3 94 ∈ ℕ0
1413nn0zi 11279 . 2 94 ∈ ℤ
15 6nn0 11190 . . . 4 6 ∈ ℕ0
16 1nn0 11185 . . . 4 1 ∈ ℕ0
1715, 16deccl 11388 . . 3 61 ∈ ℕ0
1817, 2deccl 11388 . 2 614 ∈ ℕ0
1912, 3deccl 11388 . . 3 90 ∈ ℕ0
20 2nn0 11186 . . 3 2 ∈ ℕ0
2119, 20deccl 11388 . 2 902 ∈ ℕ0
22 5nn0 11189 . . . 4 5 ∈ ℕ0
2322, 3deccl 11388 . . 3 50 ∈ ℕ0
24 8nn0 11192 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 11388 . . . . 5 28 ∈ ℕ0
2625, 15deccl 11388 . . . 4 286 ∈ ℕ0
2726nn0zi 11279 . . 3 286 ∈ ℤ
28 7nn0 11191 . . . . 5 7 ∈ ℕ0
2910, 28deccl 11388 . . . 4 107 ∈ ℕ0
3029, 3deccl 11388 . . 3 1070 ∈ ℕ0
3120, 22deccl 11388 . . . 4 25 ∈ ℕ0
3210, 2deccl 11388 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 11388 . . . . 5 1046 ∈ ℕ0
3433nn0zi 11279 . . . 4 1046 ∈ ℤ
3520, 3deccl 11388 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 11388 . . . . 5 204 ∈ ℕ0
3736, 15deccl 11388 . . . 4 2046 ∈ ℕ0
3820, 2deccl 11388 . . . . 5 24 ∈ ℕ0
39 0z 11265 . . . . 5 0 ∈ ℤ
4010, 20deccl 11388 . . . . . 6 102 ∈ ℕ0
41 3nn0 11187 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 11388 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 11388 . . . . . 6 12 ∈ ℕ0
44 2z 11286 . . . . . 6 2 ∈ ℤ
4512, 22deccl 11388 . . . . . 6 95 ∈ ℕ0
46 1z 11284 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 11388 . . . . . . 7 64 ∈ ℕ0
48 2exp6 15633 . . . . . . . 8 (2↑6) = 64
4948oveq1i 6559 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 10979 . . . . . . . 8 6 ∈ ℂ
51 2cn 10968 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 11517 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 9926 . . . . . . 7 (2 · 6) = 12
54 eqid 2610 . . . . . . . . 9 95 = 95
55 eqid 2610 . . . . . . . . . 10 400 = 400
56 9cn 10985 . . . . . . . . . . . 12 9 ∈ ℂ
5756addid1i 10102 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 11398 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2632 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2610 . . . . . . . . . . 11 40 = 40
61 00id 10090 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 11398 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2632 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 10975 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mulid2i 9922 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 6561 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addid1i 10102 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2632 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 9873 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 10105 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 6559 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2636 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 11444 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 6559 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addid2i 10103 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2636 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 11444 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulid1i 9921 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 6559 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 10977 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 11032 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 10107 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 11398 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2636 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 11444 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2610 . . . . . . . . 9 64 = 64
87 eqid 2610 . . . . . . . . . 10 25 = 25
88 2p2e4 11021 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 6560 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 11522 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 11030 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 11474 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 11457 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2632 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 11519 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 9926 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 11044 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 10107 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 11455 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 11442 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 11031 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 11411 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 11509 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 11463 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 11465 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2635 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 15611 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2610 . . . . . . 7 12 = 12
10951mulid1i 9921 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 6559 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addid1i 10102 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2632 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 11054 . . . . . . . 8 (2 · 2) = 4
1142dec0h 11398 . . . . . . . 8 4 = 04
115113, 114eqtri 2632 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 11465 . . . . . 6 (2 · 12) = 24
117 eqid 2610 . . . . . . . 8 1023 = 1023
11840nn0cni 11181 . . . . . . . . . 10 102 ∈ ℂ
119118addid1i 10102 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 11429 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 11058 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 9926 . . . . . . . . . . . 12 (2 · 4) = 8
12369addid1i 10102 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 6561 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 11035 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2632 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 10105 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 6559 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2636 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 11444 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 6559 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addid2i 10103 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 11398 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2636 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 11444 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 6559 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 10972 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 11037 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 10107 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 11398 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2636 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 11444 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 11388 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2610 . . . . . . . . 9 47 = 47
14598oveq2i 6560 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 11546 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 11372 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 10107 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 11457 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2632 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 11542 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 9926 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 10981 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 11483 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 10107 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 11456 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 11442 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 11042 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 11455 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 11515 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 11463 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 11465 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2635 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 15611 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2610 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 11411 . . . . 5 (24 + 1) = 25
16737nn0cni 11181 . . . . . . 7 2046 ∈ ℂ
168167addid2i 10103 . . . . . 6 (0 + 2046) = 2046
1698nncni 10907 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 10104 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 6559 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2610 . . . . . . . 8 102 = 102
17320dec0u 11396 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 2, 173, 113decmul1 11461 . . . . . . 7 (102 · 2) = 204
175 3t2e6 11056 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 15, 174, 175decmul1 11461 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2642 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 15612 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 6559 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2632 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 11510 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 9926 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 11465 . . . 4 (2 · 25) = 50
184 eqid 2610 . . . . . 6 1070 = 1070
18520, 16deccl 11388 . . . . . . 7 21 ∈ ℕ0
186 eqid 2610 . . . . . . . 8 107 = 107
187 eqid 2610 . . . . . . . 8 104 = 104
188 0p1e1 11009 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 11504 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 11411 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 11481 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 11448 . . . . . . 7 (107 + 104) = 211
193185nn0cni 11181 . . . . . . . . 9 21 ∈ ℂ
194193addid1i 10102 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2684 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2610 . . . . . . . . 9 1046 = 1046
197 dfdec10 11373 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2619 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 11046 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 11455 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 11453 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 6561 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 11039 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 11455 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2632 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 11453 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 11181 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 10105 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 6559 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 11398 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2636 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 11444 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 11444 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulid1i 9921 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 6559 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addid1i 10102 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2632 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 11444 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2610 . . . . . 6 2046 = 2046
22043, 20deccl 11388 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 11388 . . . . . 6 1227 ∈ ℕ0
222 eqid 2610 . . . . . . 7 204 = 204
223 eqid 2610 . . . . . . 7 1227 = 1227
22424, 16deccl 11388 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 11388 . . . . . . 7 819 ∈ ℕ0
226 eqid 2610 . . . . . . . 8 20 = 20
227 eqid 2610 . . . . . . . . 9 122 = 122
228 eqid 2610 . . . . . . . . 9 819 = 819
229 eqid 2610 . . . . . . . . . . 11 81 = 81
230 8cn 10983 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 10107 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 11028 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 11446 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 11411 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 11495 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 10107 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 11448 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 11181 . . . . . . . . . 10 94 ∈ ℂ
239238addid1i 10102 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2684 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 10104 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 6561 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2632 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 11452 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 6559 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addid1i 10102 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 11398 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2636 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 11442 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 10107 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 11455 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 11442 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 10105 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 6559 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2636 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 11444 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 11398 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2684 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 10104 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 6561 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2632 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 11452 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 11047 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 11455 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 11442 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 10107 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 11456 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 11453 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 11444 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 10104 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 6559 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2632 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 11452 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 11040 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 11455 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 11453 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 11463 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 11465 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2635 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 15611 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 11181 . . . 4 50 ∈ ℂ
282 eqid 2610 . . . . 5 50 = 50
28320, 22, 3, 282, 3, 181, 241decmul1 11461 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 9926 . . 3 (2 · 50) = 100
285 eqid 2610 . . . . 5 614 = 614
28620, 12deccl 11388 . . . . 5 29 ∈ ℕ0
287 eqid 2610 . . . . . . 7 61 = 61
288 eqid 2610 . . . . . . 7 29 = 29
289199oveq1i 6559 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2632 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 11451 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2684 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2610 . . . . . . . 8 286 = 286
294 eqid 2610 . . . . . . . . 9 28 = 28
295122oveq1i 6559 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 11488 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2632 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 11532 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 11455 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 11453 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 6561 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 11181 . . . . . . . . . 10 24 ∈ ℂ
303302addid1i 10102 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2632 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 11453 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 11181 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 10105 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 6559 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2636 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 11444 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 6559 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2636 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 11444 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulid1i 9921 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 24, 109, 314decmul1 11461 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 11411 . . . . . 6 ((28 · 1) + 1) = 29
31750mulid1i 9921 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 6559 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2632 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 11453 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 11444 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 11388 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 11388 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 11388 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 11388 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 11388 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 11388 . . . . . . 7 749 ∈ ℕ0
328 eqid 2610 . . . . . . . 8 10 = 10
329 eqid 2610 . . . . . . . 8 749 = 749
330326nn0cni 11181 . . . . . . . . . 10 74 ∈ ℂ
331330addid1i 10102 . . . . . . . . 9 (74 + 0) = 74
332153addid1i 10102 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2684 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 11181 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulid1i 9921 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 11411 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulid1i 9921 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 6561 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 11485 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2632 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 11453 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 10104 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 6559 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addid2i 10103 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2636 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 11442 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 11181 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 10105 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 6559 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2636 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 11444 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 11373 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2619 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 11529 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 11463 . . . . . . . 8 (107 · 7) = 749
356153mul02i 10104 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 3, 355, 356decmul1 11461 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 11465 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 11455 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2632 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 11465 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2635 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 15611 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 11181 . . 3 100 ∈ ℂ
365 eqid 2610 . . . 4 100 = 100
36620, 10, 3, 365, 3, 173, 241decmul1 11461 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 9926 . 2 (2 · 100) = 200
368 eqid 2610 . . . 4 902 = 902
369 eqid 2610 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 11455 . . . . 5 (90 + 9) = 99
371 eqid 2610 . . . . . . 7 94 = 94
372 6p1e7 11033 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 11541 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 11411 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 6561 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 11388 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 11181 . . . . . . . . 9 16 ∈ ℂ
378377addid1i 10102 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2632 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 11453 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 10105 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 6559 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2636 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 11444 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 11444 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulid1i 9921 . . . . 5 (9 · 1) = 9
38764mulid1i 9921 . . . . . . 7 (4 · 1) = 4
388387oveq1i 6559 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2632 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 11452 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 11444 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 11388 . . . 4 245 ∈ ℕ0
393 eqid 2610 . . . . 5 245 = 245
39450, 51, 199addcomli 10107 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 11446 . . . . . 6 (24 + 61) = 85
396 8p2e10 11486 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 11411 . . . . . . 7 ((6 · 6) + 1) = 37
39850mulid2i 9922 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 6559 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addid1i 10102 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2632 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 11440 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 11442 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 16, 317, 78decmul1 11461 . . . . . 6 (61 · 1) = 61
405387oveq1i 6559 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2632 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 11452 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 11444 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 6559 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2632 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 11452 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 11463 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 11465 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2635 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 15611 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475  (class class class)co 6549  0cc0 9815  1c1 9816   + caddc 9818   · cmul 9820  ℕcn 10897  2c2 10947  3c3 10948  4c4 10949  5c5 10950  6c6 10951  7c7 10952  8c8 10953  9c9 10954  ℕ0cn0 11169  ;cdc 11369   mod cmo 12530  ↑cexp 12722 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-2 10956  df-3 10957  df-4 10958  df-5 10959  df-6 10960  df-7 10961  df-8 10962  df-9 10963  df-n0 11170  df-z 11255  df-dec 11370  df-uz 11564  df-rp 11709  df-fl 12455  df-mod 12531  df-seq 12664  df-exp 12723 This theorem is referenced by:  4001lem2  15687  4001lem3  15688
 Copyright terms: Public domain W3C validator