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

Theorem 4001lem1 17175
Description: Lemma for 4001prm 17179. 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 12543 . . . . . 6 4 ∈ ℕ0
3 0nn0 12539 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12746 . . . . 5 40 ∈ ℕ0
54, 3deccl 12746 . . . 4 400 ∈ ℕ0
6 1nn 12275 . . . 4 1 ∈ ℕ
75, 6decnncl 12751 . . 3 4001 ∈ ℕ
81, 7eqeltri 2835 . 2 𝑁 ∈ ℕ
9 2nn 12337 . 2 2 ∈ ℕ
10 10nn0 12749 . . 3 10 ∈ ℕ0
1110, 3deccl 12746 . 2 100 ∈ ℕ0
12 9nn0 12548 . . . 4 9 ∈ ℕ0
1312, 2deccl 12746 . . 3 94 ∈ ℕ0
1413nn0zi 12640 . 2 94 ∈ ℤ
15 6nn0 12545 . . . 4 6 ∈ ℕ0
16 1nn0 12540 . . . 4 1 ∈ ℕ0
1715, 16deccl 12746 . . 3 61 ∈ ℕ0
1817, 2deccl 12746 . 2 614 ∈ ℕ0
1912, 3deccl 12746 . . 3 90 ∈ ℕ0
20 2nn0 12541 . . 3 2 ∈ ℕ0
2119, 20deccl 12746 . 2 902 ∈ ℕ0
22 5nn0 12544 . . . 4 5 ∈ ℕ0
2322, 3deccl 12746 . . 3 50 ∈ ℕ0
24 8nn0 12547 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 12746 . . . . 5 28 ∈ ℕ0
2625, 15deccl 12746 . . . 4 286 ∈ ℕ0
2726nn0zi 12640 . . 3 286 ∈ ℤ
28 7nn0 12546 . . . . 5 7 ∈ ℕ0
2910, 28deccl 12746 . . . 4 107 ∈ ℕ0
3029, 3deccl 12746 . . 3 1070 ∈ ℕ0
3120, 22deccl 12746 . . . 4 25 ∈ ℕ0
3210, 2deccl 12746 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 12746 . . . . 5 1046 ∈ ℕ0
3433nn0zi 12640 . . . 4 1046 ∈ ℤ
3520, 3deccl 12746 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 12746 . . . . 5 204 ∈ ℕ0
3736, 15deccl 12746 . . . 4 2046 ∈ ℕ0
3820, 2deccl 12746 . . . . 5 24 ∈ ℕ0
39 0z 12622 . . . . 5 0 ∈ ℤ
4010, 20deccl 12746 . . . . . 6 102 ∈ ℕ0
41 3nn0 12542 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 12746 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 12746 . . . . . 6 12 ∈ ℕ0
44 2z 12647 . . . . . 6 2 ∈ ℤ
4512, 22deccl 12746 . . . . . 6 95 ∈ ℕ0
46 1z 12645 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 12746 . . . . . . 7 64 ∈ ℕ0
48 2exp6 17121 . . . . . . . 8 (2↑6) = 64
4948oveq1i 7441 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 12355 . . . . . . . 8 6 ∈ ℂ
51 2cn 12339 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 12835 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 11268 . . . . . . 7 (2 · 6) = 12
54 eqid 2735 . . . . . . . . 9 95 = 95
55 eqid 2735 . . . . . . . . . 10 400 = 400
56 9cn 12364 . . . . . . . . . . . 12 9 ∈ ℂ
5756addridi 11446 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 12753 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2763 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2735 . . . . . . . . . . 11 40 = 40
61 00id 11434 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 12753 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2763 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 12349 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mullidi 11264 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 7443 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addridi 11446 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2763 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 11211 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 11449 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 7441 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2767 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 12784 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 7441 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addlidi 11447 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2767 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 12784 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulridi 11263 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 7441 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 12352 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 12411 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 11451 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 12753 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2767 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 12784 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2735 . . . . . . . . 9 64 = 64
87 eqid 2735 . . . . . . . . . 10 25 = 25
88 2p2e4 12399 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 7442 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 12839 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 12409 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 12803 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 12793 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2763 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 12837 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 11268 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 12422 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 11451 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 12791 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 12783 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 12410 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 12762 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 12830 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 12796 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 12797 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2766 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 17103 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2735 . . . . . . 7 12 = 12
10951mulridi 11263 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 7441 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addridi 11446 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2763 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 12428 . . . . . . . 8 (2 · 2) = 4
1142dec0h 12753 . . . . . . . 8 4 = 04
115113, 114eqtri 2763 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 12797 . . . . . 6 (2 · 12) = 24
117 eqid 2735 . . . . . . . 8 1023 = 1023
11840nn0cni 12536 . . . . . . . . . 10 102 ∈ ℂ
119118addridi 11446 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 12774 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 12432 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 11268 . . . . . . . . . . . 12 (2 · 4) = 8
12369addridi 11446 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 7443 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 12414 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2763 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 11449 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 7441 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2767 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 12784 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 7441 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addlidi 11447 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 12753 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2767 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 12784 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 7441 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 12345 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 12415 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 11451 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 12753 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2767 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 12784 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 12746 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2735 . . . . . . . . 9 47 = 47
14598oveq2i 7442 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 12860 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 12733 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 11451 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 12793 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2763 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 12856 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 11268 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 12358 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 12808 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 11451 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 12792 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 12783 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 12420 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 12791 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 12834 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 12796 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 12797 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2766 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 17103 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2735 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 12762 . . . . 5 (24 + 1) = 25
16737nn0cni 12536 . . . . . . 7 2046 ∈ ℂ
168167addlidi 11447 . . . . . 6 (0 + 2046) = 2046
1698nncni 12274 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 11448 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 7441 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2735 . . . . . . . 8 102 = 102
17320dec0u 12752 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 173, 113decmul1 12795 . . . . . . 7 (102 · 2) = 204
175 3t2e6 12430 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 174, 175decmul1 12795 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2773 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 17104 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 7441 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2763 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 12831 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 11268 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 12797 . . . 4 (2 · 25) = 50
184 eqid 2735 . . . . . 6 1070 = 1070
18520, 16deccl 12746 . . . . . . 7 21 ∈ ℕ0
186 eqid 2735 . . . . . . . 8 107 = 107
187 eqid 2735 . . . . . . . 8 104 = 104
188 0p1e1 12386 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 12826 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 12762 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 12807 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 12786 . . . . . . 7 (107 + 104) = 211
193185nn0cni 12536 . . . . . . . . 9 21 ∈ ℂ
194193addridi 11446 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2835 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2735 . . . . . . . . 9 1046 = 1046
197 dfdec10 12734 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2744 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 12423 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 12791 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 12789 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 7443 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 12417 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 12791 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2763 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 12789 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 12536 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 11449 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 7441 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 12753 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2767 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 12784 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 12784 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulridi 11263 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 7441 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addridi 11446 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2763 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 12784 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2735 . . . . . 6 2046 = 2046
22043, 20deccl 12746 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 12746 . . . . . 6 1227 ∈ ℕ0
222 eqid 2735 . . . . . . 7 204 = 204
223 eqid 2735 . . . . . . 7 1227 = 1227
22424, 16deccl 12746 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 12746 . . . . . . 7 819 ∈ ℕ0
226 eqid 2735 . . . . . . . 8 20 = 20
227 eqid 2735 . . . . . . . . 9 122 = 122
228 eqid 2735 . . . . . . . . 9 819 = 819
229 eqid 2735 . . . . . . . . . . 11 81 = 81
230 8cn 12361 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 11451 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 12406 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 12785 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 12762 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 12818 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 11451 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 12786 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 12536 . . . . . . . . . 10 94 ∈ ℂ
239238addridi 11446 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2835 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 11448 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 7443 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2763 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 12788 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 7441 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addridi 11446 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 12753 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2767 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 12783 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 11451 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 12791 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 12783 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 11449 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 7441 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2767 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 12784 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 12753 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2835 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 11448 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 7443 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2763 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 12788 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 12424 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 12791 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 12783 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 11451 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 12792 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 12789 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 12784 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 11448 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 7441 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2763 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 12788 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 12418 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 12791 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 12789 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 12796 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 12797 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2766 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 17103 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 12536 . . . 4 50 ∈ ℂ
282 eqid 2735 . . . . 5 50 = 50
28320, 22, 3, 282, 181, 241decmul1 12795 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 11268 . . 3 (2 · 50) = 100
285 eqid 2735 . . . . 5 614 = 614
28620, 12deccl 12746 . . . . 5 29 ∈ ℕ0
287 eqid 2735 . . . . . . 7 61 = 61
288 eqid 2735 . . . . . . 7 29 = 29
289199oveq1i 7441 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2763 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 12787 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2835 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2735 . . . . . . . 8 286 = 286
294 eqid 2735 . . . . . . . . 9 28 = 28
295122oveq1i 7441 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 12812 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2763 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 12848 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 12791 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 12789 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 7443 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 12536 . . . . . . . . . 10 24 ∈ ℂ
303302addridi 11446 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2763 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 12789 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 12536 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 11449 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 7441 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2767 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 12784 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 7441 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2767 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 12784 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulridi 11263 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 109, 314decmul1 12795 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 12762 . . . . . 6 ((28 · 1) + 1) = 29
31750mulridi 11263 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 7441 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2763 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 12789 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 12784 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 12746 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 12746 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 12746 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 12746 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 12746 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 12746 . . . . . . 7 749 ∈ ℕ0
328 eqid 2735 . . . . . . . 8 10 = 10
329 eqid 2735 . . . . . . . 8 749 = 749
330326nn0cni 12536 . . . . . . . . . 10 74 ∈ ℂ
331330addridi 11446 . . . . . . . . 9 (74 + 0) = 74
332153addridi 11446 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2835 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 12536 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulridi 11263 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 12762 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulridi 11263 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 7443 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 12810 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2763 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 12789 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 11448 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 7441 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addlidi 11447 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2767 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 12783 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 12536 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 11449 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 7441 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2767 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 12784 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 12734 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2744 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 12845 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 12796 . . . . . . . 8 (107 · 7) = 749
356153mul02i 11448 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 355, 356decmul1 12795 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 12797 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 12791 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2763 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 12797 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2766 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 17103 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 12536 . . 3 100 ∈ ℂ
365 eqid 2735 . . . 4 100 = 100
36620, 10, 3, 365, 173, 241decmul1 12795 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 11268 . 2 (2 · 100) = 200
368 eqid 2735 . . . 4 902 = 902
369 eqid 2735 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 12791 . . . . 5 (90 + 9) = 99
371 eqid 2735 . . . . . . 7 94 = 94
372 6p1e7 12412 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 12855 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 12762 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 7443 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 12746 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 12536 . . . . . . . . 9 16 ∈ ℂ
378377addridi 11446 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2763 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 12789 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 11449 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 7441 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2767 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 12784 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 12784 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulridi 11263 . . . . 5 (9 · 1) = 9
38764mulridi 11263 . . . . . . 7 (4 · 1) = 4
388387oveq1i 7441 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2763 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 12788 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 12784 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 12746 . . . 4 245 ∈ ℕ0
393 eqid 2735 . . . . 5 245 = 245
39450, 51, 199addcomli 11451 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 12785 . . . . . 6 (24 + 61) = 85
396 8p2e10 12811 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 12762 . . . . . . 7 ((6 · 6) + 1) = 37
39850mullidi 11264 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 7441 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addridi 11446 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2763 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 12782 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 12783 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 317, 78decmul1 12795 . . . . . 6 (61 · 1) = 61
405387oveq1i 7441 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2763 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 12788 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 12784 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 7441 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2763 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 12788 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 12796 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 12797 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2766 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 17103 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  (class class class)co 7431  0cc0 11153  1c1 11154   + caddc 11156   · cmul 11158  cn 12264  2c2 12319  3c3 12320  4c4 12321  5c5 12322  6c6 12323  7c7 12324  8c8 12325  9c9 12326  0cn0 12524  cdc 12731   mod cmo 13906  cexp 14099
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-sup 9480  df-inf 9481  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-rp 13033  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100
This theorem is referenced by:  4001lem2  17176  4001lem3  17177
  Copyright terms: Public domain W3C validator