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

Theorem 4001lem1 16462
Description: Lemma for 4001prm 16466. 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 11904 . . . . . 6 4 ∈ ℕ0
3 0nn0 11900 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12101 . . . . 5 40 ∈ ℕ0
54, 3deccl 12101 . . . 4 400 ∈ ℕ0
6 1nn 11637 . . . 4 1 ∈ ℕ
75, 6decnncl 12106 . . 3 4001 ∈ ℕ
81, 7eqeltri 2906 . 2 𝑁 ∈ ℕ
9 2nn 11698 . 2 2 ∈ ℕ
10 10nn0 12104 . . 3 10 ∈ ℕ0
1110, 3deccl 12101 . 2 100 ∈ ℕ0
12 9nn0 11909 . . . 4 9 ∈ ℕ0
1312, 2deccl 12101 . . 3 94 ∈ ℕ0
1413nn0zi 11995 . 2 94 ∈ ℤ
15 6nn0 11906 . . . 4 6 ∈ ℕ0
16 1nn0 11901 . . . 4 1 ∈ ℕ0
1715, 16deccl 12101 . . 3 61 ∈ ℕ0
1817, 2deccl 12101 . 2 614 ∈ ℕ0
1912, 3deccl 12101 . . 3 90 ∈ ℕ0
20 2nn0 11902 . . 3 2 ∈ ℕ0
2119, 20deccl 12101 . 2 902 ∈ ℕ0
22 5nn0 11905 . . . 4 5 ∈ ℕ0
2322, 3deccl 12101 . . 3 50 ∈ ℕ0
24 8nn0 11908 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 12101 . . . . 5 28 ∈ ℕ0
2625, 15deccl 12101 . . . 4 286 ∈ ℕ0
2726nn0zi 11995 . . 3 286 ∈ ℤ
28 7nn0 11907 . . . . 5 7 ∈ ℕ0
2910, 28deccl 12101 . . . 4 107 ∈ ℕ0
3029, 3deccl 12101 . . 3 1070 ∈ ℕ0
3120, 22deccl 12101 . . . 4 25 ∈ ℕ0
3210, 2deccl 12101 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 12101 . . . . 5 1046 ∈ ℕ0
3433nn0zi 11995 . . . 4 1046 ∈ ℤ
3520, 3deccl 12101 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 12101 . . . . 5 204 ∈ ℕ0
3736, 15deccl 12101 . . . 4 2046 ∈ ℕ0
3820, 2deccl 12101 . . . . 5 24 ∈ ℕ0
39 0z 11980 . . . . 5 0 ∈ ℤ
4010, 20deccl 12101 . . . . . 6 102 ∈ ℕ0
41 3nn0 11903 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 12101 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 12101 . . . . . 6 12 ∈ ℕ0
44 2z 12002 . . . . . 6 2 ∈ ℤ
4512, 22deccl 12101 . . . . . 6 95 ∈ ℕ0
46 1z 12000 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 12101 . . . . . . 7 64 ∈ ℕ0
48 2exp6 16410 . . . . . . . 8 (2↑6) = 64
4948oveq1i 7155 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 11716 . . . . . . . 8 6 ∈ ℂ
51 2cn 11700 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 12190 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 10638 . . . . . . 7 (2 · 6) = 12
54 eqid 2818 . . . . . . . . 9 95 = 95
55 eqid 2818 . . . . . . . . . 10 400 = 400
56 9cn 11725 . . . . . . . . . . . 12 9 ∈ ℂ
5756addid1i 10815 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 12108 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2841 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2818 . . . . . . . . . . 11 40 = 40
61 00id 10803 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 12108 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2841 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 11710 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mulid2i 10634 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 7157 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addid1i 10815 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2841 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 10583 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 10818 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 7155 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2845 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 12139 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 7155 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addid2i 10816 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2845 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 12139 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulid1i 10633 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 7155 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 11713 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 11772 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 10820 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 12108 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2845 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 12139 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2818 . . . . . . . . 9 64 = 64
87 eqid 2818 . . . . . . . . . 10 25 = 25
88 2p2e4 11760 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 7156 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 12194 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 11770 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 12158 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 12148 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2841 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 12192 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 10638 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 11783 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 10820 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 12146 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 12138 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 11771 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 12117 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 12185 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 12151 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 12152 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2844 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 16393 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2818 . . . . . . 7 12 = 12
10951mulid1i 10633 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 7155 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addid1i 10815 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2841 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 11789 . . . . . . . 8 (2 · 2) = 4
1142dec0h 12108 . . . . . . . 8 4 = 04
115113, 114eqtri 2841 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 12152 . . . . . 6 (2 · 12) = 24
117 eqid 2818 . . . . . . . 8 1023 = 1023
11840nn0cni 11897 . . . . . . . . . 10 102 ∈ ℂ
119118addid1i 10815 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 12129 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 11793 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 10638 . . . . . . . . . . . 12 (2 · 4) = 8
12369addid1i 10815 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 7157 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 11775 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2841 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 10818 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 7155 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2845 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 12139 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 7155 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addid2i 10816 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 12108 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2845 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 12139 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 7155 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 11706 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 11776 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 10820 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 12108 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2845 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 12139 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 12101 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2818 . . . . . . . . 9 47 = 47
14598oveq2i 7156 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 12215 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 12088 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 10820 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 12148 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2841 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 12211 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 10638 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 11719 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 12163 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 10820 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 12147 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 12138 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 11781 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 12146 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 12189 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 12151 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 12152 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2844 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 16393 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2818 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 12117 . . . . 5 (24 + 1) = 25
16737nn0cni 11897 . . . . . . 7 2046 ∈ ℂ
168167addid2i 10816 . . . . . 6 (0 + 2046) = 2046
1698nncni 11636 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 10817 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 7155 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2818 . . . . . . . 8 102 = 102
17320dec0u 12107 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 173, 113decmul1 12150 . . . . . . 7 (102 · 2) = 204
175 3t2e6 11791 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 174, 175decmul1 12150 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2851 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 16394 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 7155 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2841 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 12186 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 10638 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 12152 . . . 4 (2 · 25) = 50
184 eqid 2818 . . . . . 6 1070 = 1070
18520, 16deccl 12101 . . . . . . 7 21 ∈ ℕ0
186 eqid 2818 . . . . . . . 8 107 = 107
187 eqid 2818 . . . . . . . 8 104 = 104
188 0p1e1 11747 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 12181 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 12117 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 12162 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 12141 . . . . . . 7 (107 + 104) = 211
193185nn0cni 11897 . . . . . . . . 9 21 ∈ ℂ
194193addid1i 10815 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2906 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2818 . . . . . . . . 9 1046 = 1046
197 dfdec10 12089 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2827 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 11784 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 12146 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 12144 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 7157 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 11778 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 12146 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2841 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 12144 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 11897 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 10818 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 7155 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 12108 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2845 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 12139 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 12139 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulid1i 10633 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 7155 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addid1i 10815 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2841 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 12139 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2818 . . . . . 6 2046 = 2046
22043, 20deccl 12101 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 12101 . . . . . 6 1227 ∈ ℕ0
222 eqid 2818 . . . . . . 7 204 = 204
223 eqid 2818 . . . . . . 7 1227 = 1227
22424, 16deccl 12101 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 12101 . . . . . . 7 819 ∈ ℕ0
226 eqid 2818 . . . . . . . 8 20 = 20
227 eqid 2818 . . . . . . . . 9 122 = 122
228 eqid 2818 . . . . . . . . 9 819 = 819
229 eqid 2818 . . . . . . . . . . 11 81 = 81
230 8cn 11722 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 10820 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 11767 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 12140 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 12117 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 12173 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 10820 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 12141 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 11897 . . . . . . . . . 10 94 ∈ ℂ
239238addid1i 10815 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2906 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 10817 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 7157 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2841 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 12143 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 7155 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addid1i 10815 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 12108 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2845 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 12138 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 10820 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 12146 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 12138 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 10818 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 7155 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2845 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 12139 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 12108 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2906 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 10817 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 7157 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2841 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 12143 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 11785 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 12146 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 12138 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 10820 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 12147 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 12144 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 12139 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 10817 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 7155 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2841 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 12143 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 11779 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 12146 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 12144 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 12151 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 12152 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2844 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 16393 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 11897 . . . 4 50 ∈ ℂ
282 eqid 2818 . . . . 5 50 = 50
28320, 22, 3, 282, 181, 241decmul1 12150 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 10638 . . 3 (2 · 50) = 100
285 eqid 2818 . . . . 5 614 = 614
28620, 12deccl 12101 . . . . 5 29 ∈ ℕ0
287 eqid 2818 . . . . . . 7 61 = 61
288 eqid 2818 . . . . . . 7 29 = 29
289199oveq1i 7155 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2841 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 12142 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2906 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2818 . . . . . . . 8 286 = 286
294 eqid 2818 . . . . . . . . 9 28 = 28
295122oveq1i 7155 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 12167 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2841 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 12203 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 12146 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 12144 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 7157 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 11897 . . . . . . . . . 10 24 ∈ ℂ
303302addid1i 10815 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2841 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 12144 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 11897 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 10818 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 7155 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2845 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 12139 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 7155 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2845 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 12139 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulid1i 10633 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 109, 314decmul1 12150 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 12117 . . . . . 6 ((28 · 1) + 1) = 29
31750mulid1i 10633 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 7155 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2841 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 12144 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 12139 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 12101 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 12101 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 12101 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 12101 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 12101 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 12101 . . . . . . 7 749 ∈ ℕ0
328 eqid 2818 . . . . . . . 8 10 = 10
329 eqid 2818 . . . . . . . 8 749 = 749
330326nn0cni 11897 . . . . . . . . . 10 74 ∈ ℂ
331330addid1i 10815 . . . . . . . . 9 (74 + 0) = 74
332153addid1i 10815 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2906 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 11897 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulid1i 10633 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 12117 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulid1i 10633 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 7157 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 12165 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2841 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 12144 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 10817 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 7155 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addid2i 10816 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2845 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 12138 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 11897 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 10818 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 7155 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2845 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 12139 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 12089 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2827 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 12200 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 12151 . . . . . . . 8 (107 · 7) = 749
356153mul02i 10817 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 355, 356decmul1 12150 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 12152 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 12146 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2841 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 12152 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2844 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 16393 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 11897 . . 3 100 ∈ ℂ
365 eqid 2818 . . . 4 100 = 100
36620, 10, 3, 365, 173, 241decmul1 12150 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 10638 . 2 (2 · 100) = 200
368 eqid 2818 . . . 4 902 = 902
369 eqid 2818 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 12146 . . . . 5 (90 + 9) = 99
371 eqid 2818 . . . . . . 7 94 = 94
372 6p1e7 11773 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 12210 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 12117 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 7157 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 12101 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 11897 . . . . . . . . 9 16 ∈ ℂ
378377addid1i 10815 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2841 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 12144 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 10818 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 7155 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2845 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 12139 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 12139 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulid1i 10633 . . . . 5 (9 · 1) = 9
38764mulid1i 10633 . . . . . . 7 (4 · 1) = 4
388387oveq1i 7155 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2841 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 12143 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 12139 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 12101 . . . 4 245 ∈ ℕ0
393 eqid 2818 . . . . 5 245 = 245
39450, 51, 199addcomli 10820 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 12140 . . . . . 6 (24 + 61) = 85
396 8p2e10 12166 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 12117 . . . . . . 7 ((6 · 6) + 1) = 37
39850mulid2i 10634 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 7155 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addid1i 10815 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2841 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 12137 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 12138 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 317, 78decmul1 12150 . . . . . 6 (61 · 1) = 61
405387oveq1i 7155 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2841 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 12143 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 12139 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 7155 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2841 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 12143 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 12151 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 12152 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2844 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 16393 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  (class class class)co 7145  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530  cn 11626  2c2 11680  3c3 11681  4c4 11682  5c5 11683  6c6 11684  7c7 11685  8c8 11686  9c9 11687  0cn0 11885  cdc 12086   mod cmo 13225  cexp 13417
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7570  df-2nd 7679  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-er 8278  df-en 8498  df-dom 8499  df-sdom 8500  df-sup 8894  df-inf 8895  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-rp 12378  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418
This theorem is referenced by:  4001lem2  16463  4001lem3  16464
  Copyright terms: Public domain W3C validator