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

Theorem 4001lem1 16466
Description: Lemma for 4001prm 16470. 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 11908 . . . . . 6 4 ∈ ℕ0
3 0nn0 11904 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12105 . . . . 5 40 ∈ ℕ0
54, 3deccl 12105 . . . 4 400 ∈ ℕ0
6 1nn 11641 . . . 4 1 ∈ ℕ
75, 6decnncl 12110 . . 3 4001 ∈ ℕ
81, 7eqeltri 2907 . 2 𝑁 ∈ ℕ
9 2nn 11702 . 2 2 ∈ ℕ
10 10nn0 12108 . . 3 10 ∈ ℕ0
1110, 3deccl 12105 . 2 100 ∈ ℕ0
12 9nn0 11913 . . . 4 9 ∈ ℕ0
1312, 2deccl 12105 . . 3 94 ∈ ℕ0
1413nn0zi 11999 . 2 94 ∈ ℤ
15 6nn0 11910 . . . 4 6 ∈ ℕ0
16 1nn0 11905 . . . 4 1 ∈ ℕ0
1715, 16deccl 12105 . . 3 61 ∈ ℕ0
1817, 2deccl 12105 . 2 614 ∈ ℕ0
1912, 3deccl 12105 . . 3 90 ∈ ℕ0
20 2nn0 11906 . . 3 2 ∈ ℕ0
2119, 20deccl 12105 . 2 902 ∈ ℕ0
22 5nn0 11909 . . . 4 5 ∈ ℕ0
2322, 3deccl 12105 . . 3 50 ∈ ℕ0
24 8nn0 11912 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 12105 . . . . 5 28 ∈ ℕ0
2625, 15deccl 12105 . . . 4 286 ∈ ℕ0
2726nn0zi 11999 . . 3 286 ∈ ℤ
28 7nn0 11911 . . . . 5 7 ∈ ℕ0
2910, 28deccl 12105 . . . 4 107 ∈ ℕ0
3029, 3deccl 12105 . . 3 1070 ∈ ℕ0
3120, 22deccl 12105 . . . 4 25 ∈ ℕ0
3210, 2deccl 12105 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 12105 . . . . 5 1046 ∈ ℕ0
3433nn0zi 11999 . . . 4 1046 ∈ ℤ
3520, 3deccl 12105 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 12105 . . . . 5 204 ∈ ℕ0
3736, 15deccl 12105 . . . 4 2046 ∈ ℕ0
3820, 2deccl 12105 . . . . 5 24 ∈ ℕ0
39 0z 11984 . . . . 5 0 ∈ ℤ
4010, 20deccl 12105 . . . . . 6 102 ∈ ℕ0
41 3nn0 11907 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 12105 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 12105 . . . . . 6 12 ∈ ℕ0
44 2z 12006 . . . . . 6 2 ∈ ℤ
4512, 22deccl 12105 . . . . . 6 95 ∈ ℕ0
46 1z 12004 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 12105 . . . . . . 7 64 ∈ ℕ0
48 2exp6 16414 . . . . . . . 8 (2↑6) = 64
4948oveq1i 7158 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 11720 . . . . . . . 8 6 ∈ ℂ
51 2cn 11704 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 12194 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 10642 . . . . . . 7 (2 · 6) = 12
54 eqid 2819 . . . . . . . . 9 95 = 95
55 eqid 2819 . . . . . . . . . 10 400 = 400
56 9cn 11729 . . . . . . . . . . . 12 9 ∈ ℂ
5756addid1i 10819 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 12112 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2842 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2819 . . . . . . . . . . 11 40 = 40
61 00id 10807 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 12112 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2842 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 11714 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mulid2i 10638 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 7160 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addid1i 10819 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2842 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 10587 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 10822 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 7158 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2846 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 12143 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 7158 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addid2i 10820 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2846 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 12143 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulid1i 10637 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 7158 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 11717 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 11776 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 10824 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 12112 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2846 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 12143 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2819 . . . . . . . . 9 64 = 64
87 eqid 2819 . . . . . . . . . 10 25 = 25
88 2p2e4 11764 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 7159 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 12198 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 11774 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 12162 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 12152 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2842 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 12196 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 10642 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 11787 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 10824 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 12150 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 12142 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 11775 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 12121 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 12189 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 12155 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 12156 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2845 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 16397 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2819 . . . . . . 7 12 = 12
10951mulid1i 10637 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 7158 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addid1i 10819 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2842 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 11793 . . . . . . . 8 (2 · 2) = 4
1142dec0h 12112 . . . . . . . 8 4 = 04
115113, 114eqtri 2842 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 12156 . . . . . 6 (2 · 12) = 24
117 eqid 2819 . . . . . . . 8 1023 = 1023
11840nn0cni 11901 . . . . . . . . . 10 102 ∈ ℂ
119118addid1i 10819 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 12133 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 11797 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 10642 . . . . . . . . . . . 12 (2 · 4) = 8
12369addid1i 10819 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 7160 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 11779 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2842 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 10822 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 7158 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2846 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 12143 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 7158 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addid2i 10820 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 12112 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2846 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 12143 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 7158 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 11710 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 11780 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 10824 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 12112 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2846 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 12143 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 12105 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2819 . . . . . . . . 9 47 = 47
14598oveq2i 7159 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 12219 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 12092 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 10824 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 12152 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2842 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 12215 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 10642 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 11723 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 12167 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 10824 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 12151 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 12142 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 11785 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 12150 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 12193 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 12155 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 12156 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2845 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 16397 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2819 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 12121 . . . . 5 (24 + 1) = 25
16737nn0cni 11901 . . . . . . 7 2046 ∈ ℂ
168167addid2i 10820 . . . . . 6 (0 + 2046) = 2046
1698nncni 11640 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 10821 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 7158 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2819 . . . . . . . 8 102 = 102
17320dec0u 12111 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 173, 113decmul1 12154 . . . . . . 7 (102 · 2) = 204
175 3t2e6 11795 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 174, 175decmul1 12154 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2852 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 16398 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 7158 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2842 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 12190 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 10642 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 12156 . . . 4 (2 · 25) = 50
184 eqid 2819 . . . . . 6 1070 = 1070
18520, 16deccl 12105 . . . . . . 7 21 ∈ ℕ0
186 eqid 2819 . . . . . . . 8 107 = 107
187 eqid 2819 . . . . . . . 8 104 = 104
188 0p1e1 11751 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 12185 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 12121 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 12166 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 12145 . . . . . . 7 (107 + 104) = 211
193185nn0cni 11901 . . . . . . . . 9 21 ∈ ℂ
194193addid1i 10819 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2907 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2819 . . . . . . . . 9 1046 = 1046
197 dfdec10 12093 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2828 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 11788 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 12150 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 12148 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 7160 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 11782 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 12150 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2842 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 12148 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 11901 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 10822 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 7158 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 12112 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2846 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 12143 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 12143 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulid1i 10637 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 7158 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addid1i 10819 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2842 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 12143 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2819 . . . . . 6 2046 = 2046
22043, 20deccl 12105 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 12105 . . . . . 6 1227 ∈ ℕ0
222 eqid 2819 . . . . . . 7 204 = 204
223 eqid 2819 . . . . . . 7 1227 = 1227
22424, 16deccl 12105 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 12105 . . . . . . 7 819 ∈ ℕ0
226 eqid 2819 . . . . . . . 8 20 = 20
227 eqid 2819 . . . . . . . . 9 122 = 122
228 eqid 2819 . . . . . . . . 9 819 = 819
229 eqid 2819 . . . . . . . . . . 11 81 = 81
230 8cn 11726 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 10824 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 11771 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 12144 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 12121 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 12177 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 10824 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 12145 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 11901 . . . . . . . . . 10 94 ∈ ℂ
239238addid1i 10819 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2907 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 10821 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 7160 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2842 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 12147 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 7158 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addid1i 10819 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 12112 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2846 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 12142 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 10824 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 12150 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 12142 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 10822 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 7158 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2846 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 12143 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 12112 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2907 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 10821 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 7160 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2842 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 12147 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 11789 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 12150 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 12142 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 10824 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 12151 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 12148 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 12143 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 10821 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 7158 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2842 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 12147 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 11783 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 12150 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 12148 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 12155 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 12156 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2845 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 16397 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 11901 . . . 4 50 ∈ ℂ
282 eqid 2819 . . . . 5 50 = 50
28320, 22, 3, 282, 181, 241decmul1 12154 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 10642 . . 3 (2 · 50) = 100
285 eqid 2819 . . . . 5 614 = 614
28620, 12deccl 12105 . . . . 5 29 ∈ ℕ0
287 eqid 2819 . . . . . . 7 61 = 61
288 eqid 2819 . . . . . . 7 29 = 29
289199oveq1i 7158 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2842 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 12146 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2907 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2819 . . . . . . . 8 286 = 286
294 eqid 2819 . . . . . . . . 9 28 = 28
295122oveq1i 7158 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 12171 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2842 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 12207 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 12150 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 12148 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 7160 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 11901 . . . . . . . . . 10 24 ∈ ℂ
303302addid1i 10819 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2842 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 12148 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 11901 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 10822 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 7158 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2846 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 12143 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 7158 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2846 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 12143 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulid1i 10637 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 109, 314decmul1 12154 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 12121 . . . . . 6 ((28 · 1) + 1) = 29
31750mulid1i 10637 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 7158 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2842 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 12148 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 12143 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 12105 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 12105 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 12105 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 12105 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 12105 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 12105 . . . . . . 7 749 ∈ ℕ0
328 eqid 2819 . . . . . . . 8 10 = 10
329 eqid 2819 . . . . . . . 8 749 = 749
330326nn0cni 11901 . . . . . . . . . 10 74 ∈ ℂ
331330addid1i 10819 . . . . . . . . 9 (74 + 0) = 74
332153addid1i 10819 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2907 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 11901 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulid1i 10637 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 12121 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulid1i 10637 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 7160 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 12169 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2842 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 12148 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 10821 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 7158 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addid2i 10820 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2846 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 12142 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 11901 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 10822 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 7158 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2846 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 12143 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 12093 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2828 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 12204 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 12155 . . . . . . . 8 (107 · 7) = 749
356153mul02i 10821 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 355, 356decmul1 12154 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 12156 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 12150 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2842 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 12156 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2845 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 16397 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 11901 . . 3 100 ∈ ℂ
365 eqid 2819 . . . 4 100 = 100
36620, 10, 3, 365, 173, 241decmul1 12154 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 10642 . 2 (2 · 100) = 200
368 eqid 2819 . . . 4 902 = 902
369 eqid 2819 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 12150 . . . . 5 (90 + 9) = 99
371 eqid 2819 . . . . . . 7 94 = 94
372 6p1e7 11777 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 12214 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 12121 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 7160 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 12105 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 11901 . . . . . . . . 9 16 ∈ ℂ
378377addid1i 10819 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2842 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 12148 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 10822 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 7158 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2846 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 12143 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 12143 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulid1i 10637 . . . . 5 (9 · 1) = 9
38764mulid1i 10637 . . . . . . 7 (4 · 1) = 4
388387oveq1i 7158 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2842 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 12147 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 12143 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 12105 . . . 4 245 ∈ ℕ0
393 eqid 2819 . . . . 5 245 = 245
39450, 51, 199addcomli 10824 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 12144 . . . . . 6 (24 + 61) = 85
396 8p2e10 12170 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 12121 . . . . . . 7 ((6 · 6) + 1) = 37
39850mulid2i 10638 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 7158 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addid1i 10819 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2842 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 12141 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 12142 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 317, 78decmul1 12154 . . . . . 6 (61 · 1) = 61
405387oveq1i 7158 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2842 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 12147 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 12143 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 7158 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2842 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 12147 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 12155 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 12156 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2845 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 16397 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1531  (class class class)co 7148  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  cn 11630  2c2 11684  3c3 11685  4c4 11686  5c5 11687  6c6 11688  7c7 11689  8c8 11690  9c9 11691  0cn0 11889  cdc 12090   mod cmo 13229  cexp 13421
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1083  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  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 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-er 8281  df-en 8502  df-dom 8503  df-sdom 8504  df-sup 8898  df-inf 8899  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-rp 12382  df-fl 13154  df-mod 13230  df-seq 13362  df-exp 13422
This theorem is referenced by:  4001lem2  16467  4001lem3  16468
  Copyright terms: Public domain W3C validator