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

Theorem 4001lem1 16079
Description: Lemma for 4001prm 16083. 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 11598 . . . . . 6 4 ∈ ℕ0
3 0nn0 11594 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11794 . . . . 5 40 ∈ ℕ0
54, 3deccl 11794 . . . 4 400 ∈ ℕ0
6 1nn 11328 . . . 4 1 ∈ ℕ
75, 6decnncl 11799 . . 3 4001 ∈ ℕ
81, 7eqeltri 2892 . 2 𝑁 ∈ ℕ
9 2nn 11386 . 2 2 ∈ ℕ
10 10nn0 11797 . . 3 10 ∈ ℕ0
1110, 3deccl 11794 . 2 100 ∈ ℕ0
12 9nn0 11603 . . . 4 9 ∈ ℕ0
1312, 2deccl 11794 . . 3 94 ∈ ℕ0
1413nn0zi 11688 . 2 94 ∈ ℤ
15 6nn0 11600 . . . 4 6 ∈ ℕ0
16 1nn0 11595 . . . 4 1 ∈ ℕ0
1715, 16deccl 11794 . . 3 61 ∈ ℕ0
1817, 2deccl 11794 . 2 614 ∈ ℕ0
1912, 3deccl 11794 . . 3 90 ∈ ℕ0
20 2nn0 11596 . . 3 2 ∈ ℕ0
2119, 20deccl 11794 . 2 902 ∈ ℕ0
22 5nn0 11599 . . . 4 5 ∈ ℕ0
2322, 3deccl 11794 . . 3 50 ∈ ℕ0
24 8nn0 11602 . . . . . 6 8 ∈ ℕ0
2520, 24deccl 11794 . . . . 5 28 ∈ ℕ0
2625, 15deccl 11794 . . . 4 286 ∈ ℕ0
2726nn0zi 11688 . . 3 286 ∈ ℤ
28 7nn0 11601 . . . . 5 7 ∈ ℕ0
2910, 28deccl 11794 . . . 4 107 ∈ ℕ0
3029, 3deccl 11794 . . 3 1070 ∈ ℕ0
3120, 22deccl 11794 . . . 4 25 ∈ ℕ0
3210, 2deccl 11794 . . . . . 6 104 ∈ ℕ0
3332, 15deccl 11794 . . . . 5 1046 ∈ ℕ0
3433nn0zi 11688 . . . 4 1046 ∈ ℤ
3520, 3deccl 11794 . . . . . 6 20 ∈ ℕ0
3635, 2deccl 11794 . . . . 5 204 ∈ ℕ0
3736, 15deccl 11794 . . . 4 2046 ∈ ℕ0
3820, 2deccl 11794 . . . . 5 24 ∈ ℕ0
39 0z 11674 . . . . 5 0 ∈ ℤ
4010, 20deccl 11794 . . . . . 6 102 ∈ ℕ0
41 3nn0 11597 . . . . . 6 3 ∈ ℕ0
4240, 41deccl 11794 . . . . 5 1023 ∈ ℕ0
4316, 20deccl 11794 . . . . . 6 12 ∈ ℕ0
44 2z 11695 . . . . . 6 2 ∈ ℤ
4512, 22deccl 11794 . . . . . 6 95 ∈ ℕ0
46 1z 11693 . . . . . . 7 1 ∈ ℤ
4715, 2deccl 11794 . . . . . . 7 64 ∈ ℕ0
48 2exp6 16027 . . . . . . . 8 (2↑6) = 64
4948oveq1i 6894 . . . . . . 7 ((2↑6) mod 𝑁) = (64 mod 𝑁)
50 6cn 11407 . . . . . . . 8 6 ∈ ℂ
51 2cn 11388 . . . . . . . 8 2 ∈ ℂ
52 6t2e12 11883 . . . . . . . 8 (6 · 2) = 12
5350, 51, 52mulcomli 10344 . . . . . . 7 (2 · 6) = 12
54 eqid 2817 . . . . . . . . 9 95 = 95
55 eqid 2817 . . . . . . . . . 10 400 = 400
56 9cn 11419 . . . . . . . . . . . 12 9 ∈ ℂ
5756addid1i 10518 . . . . . . . . . . 11 (9 + 0) = 9
5812dec0h 11801 . . . . . . . . . . 11 9 = 09
5957, 58eqtri 2839 . . . . . . . . . 10 (9 + 0) = 09
60 eqid 2817 . . . . . . . . . . 11 40 = 40
61 00id 10506 . . . . . . . . . . . 12 (0 + 0) = 0
623dec0h 11801 . . . . . . . . . . . 12 0 = 00
6361, 62eqtri 2839 . . . . . . . . . . 11 (0 + 0) = 00
64 4cn 11399 . . . . . . . . . . . . . 14 4 ∈ ℂ
6564mulid2i 10340 . . . . . . . . . . . . 13 (1 · 4) = 4
6665, 61oveq12i 6896 . . . . . . . . . . . 12 ((1 · 4) + (0 + 0)) = (4 + 0)
6764addid1i 10518 . . . . . . . . . . . 12 (4 + 0) = 4
6866, 67eqtri 2839 . . . . . . . . . . 11 ((1 · 4) + (0 + 0)) = 4
69 ax-1cn 10289 . . . . . . . . . . . . . 14 1 ∈ ℂ
7069mul01i 10521 . . . . . . . . . . . . 13 (1 · 0) = 0
7170oveq1i 6894 . . . . . . . . . . . 12 ((1 · 0) + 0) = (0 + 0)
7271, 61, 623eqtri 2843 . . . . . . . . . . 11 ((1 · 0) + 0) = 00
732, 3, 3, 3, 60, 63, 16, 3, 3, 68, 72decma2c 11832 . . . . . . . . . 10 ((1 · 40) + (0 + 0)) = 40
7470oveq1i 6894 . . . . . . . . . . 11 ((1 · 0) + 9) = (0 + 9)
7556addid2i 10519 . . . . . . . . . . 11 (0 + 9) = 9
7674, 75, 583eqtri 2843 . . . . . . . . . 10 ((1 · 0) + 9) = 09
774, 3, 3, 12, 55, 59, 16, 12, 3, 73, 76decma2c 11832 . . . . . . . . 9 ((1 · 400) + (9 + 0)) = 409
7869mulid1i 10339 . . . . . . . . . . 11 (1 · 1) = 1
7978oveq1i 6894 . . . . . . . . . 10 ((1 · 1) + 5) = (1 + 5)
80 5cn 11403 . . . . . . . . . . 11 5 ∈ ℂ
81 5p1e6 11466 . . . . . . . . . . 11 (5 + 1) = 6
8280, 69, 81addcomli 10523 . . . . . . . . . 10 (1 + 5) = 6
8315dec0h 11801 . . . . . . . . . 10 6 = 06
8479, 82, 833eqtri 2843 . . . . . . . . 9 ((1 · 1) + 5) = 06
855, 16, 12, 22, 1, 54, 16, 15, 3, 77, 84decma2c 11832 . . . . . . . 8 ((1 · 𝑁) + 95) = 4096
86 eqid 2817 . . . . . . . . 9 64 = 64
87 eqid 2817 . . . . . . . . . 10 25 = 25
88 2p2e4 11455 . . . . . . . . . . . 12 (2 + 2) = 4
8988oveq2i 6895 . . . . . . . . . . 11 ((6 · 6) + (2 + 2)) = ((6 · 6) + 4)
90 6t6e36 11887 . . . . . . . . . . . 12 (6 · 6) = 36
91 3p1e4 11464 . . . . . . . . . . . 12 (3 + 1) = 4
92 6p4e10 11851 . . . . . . . . . . . 12 (6 + 4) = 10
9341, 15, 2, 90, 91, 92decaddci2 11841 . . . . . . . . . . 11 ((6 · 6) + 4) = 40
9489, 93eqtri 2839 . . . . . . . . . 10 ((6 · 6) + (2 + 2)) = 40
95 6t4e24 11885 . . . . . . . . . . . 12 (6 · 4) = 24
9650, 64, 95mulcomli 10344 . . . . . . . . . . 11 (4 · 6) = 24
97 5p4e9 11477 . . . . . . . . . . . 12 (5 + 4) = 9
9880, 64, 97addcomli 10523 . . . . . . . . . . 11 (4 + 5) = 9
9920, 2, 22, 96, 98decaddi 11839 . . . . . . . . . 10 ((4 · 6) + 5) = 29
10015, 2, 20, 22, 86, 87, 15, 12, 20, 94, 99decmac 11831 . . . . . . . . 9 ((64 · 6) + 25) = 409
101 4p1e5 11465 . . . . . . . . . . 11 (4 + 1) = 5
10220, 2, 101, 95decsuc 11810 . . . . . . . . . 10 ((6 · 4) + 1) = 25
103 4t4e16 11878 . . . . . . . . . 10 (4 · 4) = 16
1042, 15, 2, 86, 15, 16, 102, 103decmul1c 11844 . . . . . . . . 9 (64 · 4) = 256
10547, 15, 2, 86, 15, 31, 100, 104decmul2c 11845 . . . . . . . 8 (64 · 64) = 4096
10685, 105eqtr4i 2842 . . . . . . 7 ((1 · 𝑁) + 95) = (64 · 64)
1078, 9, 15, 46, 47, 45, 49, 53, 106mod2xi 16010 . . . . . 6 ((2↑12) mod 𝑁) = (95 mod 𝑁)
108 eqid 2817 . . . . . . 7 12 = 12
10951mulid1i 10339 . . . . . . . . 9 (2 · 1) = 2
110109oveq1i 6894 . . . . . . . 8 ((2 · 1) + 0) = (2 + 0)
11151addid1i 10518 . . . . . . . 8 (2 + 0) = 2
112110, 111eqtri 2839 . . . . . . 7 ((2 · 1) + 0) = 2
113 2t2e4 11483 . . . . . . . 8 (2 · 2) = 4
1142dec0h 11801 . . . . . . . 8 4 = 04
115113, 114eqtri 2839 . . . . . . 7 (2 · 2) = 04
11620, 16, 20, 108, 2, 3, 112, 115decmul2c 11845 . . . . . 6 (2 · 12) = 24
117 eqid 2817 . . . . . . . 8 1023 = 1023
11840nn0cni 11591 . . . . . . . . . 10 102 ∈ ℂ
119118addid1i 10518 . . . . . . . . 9 (102 + 0) = 102
120 dec10p 11822 . . . . . . . . . 10 (10 + 0) = 10
121 4t2e8 11487 . . . . . . . . . . . . 13 (4 · 2) = 8
12264, 51, 121mulcomli 10344 . . . . . . . . . . . 12 (2 · 4) = 8
12369addid1i 10518 . . . . . . . . . . . 12 (1 + 0) = 1
124122, 123oveq12i 6896 . . . . . . . . . . 11 ((2 · 4) + (1 + 0)) = (8 + 1)
125 8p1e9 11469 . . . . . . . . . . 11 (8 + 1) = 9
126124, 125eqtri 2839 . . . . . . . . . 10 ((2 · 4) + (1 + 0)) = 9
12751mul01i 10521 . . . . . . . . . . . 12 (2 · 0) = 0
128127oveq1i 6894 . . . . . . . . . . 11 ((2 · 0) + 0) = (0 + 0)
129128, 61, 623eqtri 2843 . . . . . . . . . 10 ((2 · 0) + 0) = 00
1302, 3, 16, 3, 60, 120, 20, 3, 3, 126, 129decma2c 11832 . . . . . . . . 9 ((2 · 40) + (10 + 0)) = 90
131127oveq1i 6894 . . . . . . . . . 10 ((2 · 0) + 2) = (0 + 2)
13251addid2i 10519 . . . . . . . . . 10 (0 + 2) = 2
13320dec0h 11801 . . . . . . . . . 10 2 = 02
134131, 132, 1333eqtri 2843 . . . . . . . . 9 ((2 · 0) + 2) = 02
1354, 3, 10, 20, 55, 119, 20, 20, 3, 130, 134decma2c 11832 . . . . . . . 8 ((2 · 400) + (102 + 0)) = 902
136109oveq1i 6894 . . . . . . . . 9 ((2 · 1) + 3) = (2 + 3)
137 3cn 11394 . . . . . . . . . 10 3 ∈ ℂ
138 3p2e5 11470 . . . . . . . . . 10 (3 + 2) = 5
139137, 51, 138addcomli 10523 . . . . . . . . 9 (2 + 3) = 5
14022dec0h 11801 . . . . . . . . 9 5 = 05
141136, 139, 1403eqtri 2843 . . . . . . . 8 ((2 · 1) + 3) = 05
1425, 16, 40, 41, 1, 117, 20, 22, 3, 135, 141decma2c 11832 . . . . . . 7 ((2 · 𝑁) + 1023) = 9025
1432, 28deccl 11794 . . . . . . . 8 47 ∈ ℕ0
144 eqid 2817 . . . . . . . . 9 47 = 47
14598oveq2i 6895 . . . . . . . . . 10 ((9 · 9) + (4 + 5)) = ((9 · 9) + 9)
146 9t9e81 11908 . . . . . . . . . . 11 (9 · 9) = 81
147 9p1e10 11781 . . . . . . . . . . . 12 (9 + 1) = 10
14856, 69, 147addcomli 10523 . . . . . . . . . . 11 (1 + 9) = 10
14924, 16, 12, 146, 125, 148decaddci2 11841 . . . . . . . . . 10 ((9 · 9) + 9) = 90
150145, 149eqtri 2839 . . . . . . . . 9 ((9 · 9) + (4 + 5)) = 90
151 9t5e45 11904 . . . . . . . . . . 11 (9 · 5) = 45
15256, 80, 151mulcomli 10344 . . . . . . . . . 10 (5 · 9) = 45
153 7cn 11411 . . . . . . . . . . 11 7 ∈ ℂ
154 7p5e12 11856 . . . . . . . . . . 11 (7 + 5) = 12
155153, 80, 154addcomli 10523 . . . . . . . . . 10 (5 + 7) = 12
1562, 22, 28, 152, 101, 20, 155decaddci 11840 . . . . . . . . 9 ((5 · 9) + 7) = 52
15712, 22, 2, 28, 54, 144, 12, 20, 22, 150, 156decmac 11831 . . . . . . . 8 ((95 · 9) + 47) = 902
158 5p2e7 11475 . . . . . . . . . 10 (5 + 2) = 7
1592, 22, 20, 151, 158decaddi 11839 . . . . . . . . 9 ((9 · 5) + 2) = 47
160 5t5e25 11882 . . . . . . . . 9 (5 · 5) = 25
16122, 12, 22, 54, 22, 20, 159, 160decmul1c 11844 . . . . . . . 8 (95 · 5) = 475
16245, 12, 22, 54, 22, 143, 157, 161decmul2c 11845 . . . . . . 7 (95 · 95) = 9025
163142, 162eqtr4i 2842 . . . . . 6 ((2 · 𝑁) + 1023) = (95 · 95)
1648, 9, 43, 44, 45, 42, 107, 116, 163mod2xi 16010 . . . . 5 ((2↑24) mod 𝑁) = (1023 mod 𝑁)
165 eqid 2817 . . . . . 6 24 = 24
16620, 2, 101, 165decsuc 11810 . . . . 5 (24 + 1) = 25
16737nn0cni 11591 . . . . . . 7 2046 ∈ ℂ
168167addid2i 10519 . . . . . 6 (0 + 2046) = 2046
1698nncni 11326 . . . . . . . 8 𝑁 ∈ ℂ
170169mul02i 10520 . . . . . . 7 (0 · 𝑁) = 0
171170oveq1i 6894 . . . . . 6 ((0 · 𝑁) + 2046) = (0 + 2046)
172 eqid 2817 . . . . . . . 8 102 = 102
17320dec0u 11800 . . . . . . . 8 (10 · 2) = 20
17420, 10, 20, 172, 2, 173, 113decmul1 11843 . . . . . . 7 (102 · 2) = 204
175 3t2e6 11485 . . . . . . 7 (3 · 2) = 6
17620, 40, 41, 117, 15, 174, 175decmul1 11843 . . . . . 6 (1023 · 2) = 2046
177168, 171, 1763eqtr4i 2849 . . . . 5 ((0 · 𝑁) + 2046) = (1023 · 2)
1788, 9, 38, 39, 42, 37, 164, 166, 177modxp1i 16011 . . . 4 ((2↑25) mod 𝑁) = (2046 mod 𝑁)
179113oveq1i 6894 . . . . . 6 ((2 · 2) + 1) = (4 + 1)
180179, 101eqtri 2839 . . . . 5 ((2 · 2) + 1) = 5
181 5t2e10 11879 . . . . . 6 (5 · 2) = 10
18280, 51, 181mulcomli 10344 . . . . 5 (2 · 5) = 10
18320, 20, 22, 87, 3, 16, 180, 182decmul2c 11845 . . . 4 (2 · 25) = 50
184 eqid 2817 . . . . . 6 1070 = 1070
18520, 16deccl 11794 . . . . . . 7 21 ∈ ℕ0
186 eqid 2817 . . . . . . . 8 107 = 107
187 eqid 2817 . . . . . . . 8 104 = 104
188 0p1e1 11442 . . . . . . . . 9 (0 + 1) = 1
189 10p10e20 11874 . . . . . . . . 9 (10 + 10) = 20
19020, 3, 188, 189decsuc 11810 . . . . . . . 8 ((10 + 10) + 1) = 21
191 7p4e11 11855 . . . . . . . 8 (7 + 4) = 11
19210, 28, 10, 2, 186, 187, 190, 16, 191decaddc 11834 . . . . . . 7 (107 + 104) = 211
193185nn0cni 11591 . . . . . . . . 9 21 ∈ ℂ
194193addid1i 10518 . . . . . . . 8 (21 + 0) = 21
195111, 20eqeltri 2892 . . . . . . . . 9 (2 + 0) ∈ ℕ0
196 eqid 2817 . . . . . . . . 9 1046 = 1046
197 dfdec10 11782 . . . . . . . . . . 11 41 = ((10 · 4) + 1)
198197eqcomi 2826 . . . . . . . . . 10 ((10 · 4) + 1) = 41
199 6p2e8 11478 . . . . . . . . . . 11 (6 + 2) = 8
20016, 15, 20, 103, 199decaddi 11839 . . . . . . . . . 10 ((4 · 4) + 2) = 18
20110, 2, 20, 187, 2, 24, 16, 198, 200decrmac 11837 . . . . . . . . 9 ((104 · 4) + 2) = 418
20295, 111oveq12i 6896 . . . . . . . . . 10 ((6 · 4) + (2 + 0)) = (24 + 2)
203 4p2e6 11472 . . . . . . . . . . 11 (4 + 2) = 6
20420, 2, 20, 165, 203decaddi 11839 . . . . . . . . . 10 (24 + 2) = 26
205202, 204eqtri 2839 . . . . . . . . 9 ((6 · 4) + (2 + 0)) = 26
20632, 15, 195, 196, 2, 15, 20, 201, 205decrmac 11837 . . . . . . . 8 ((1046 · 4) + (2 + 0)) = 4186
20733nn0cni 11591 . . . . . . . . . . 11 1046 ∈ ℂ
208207mul01i 10521 . . . . . . . . . 10 (1046 · 0) = 0
209208oveq1i 6894 . . . . . . . . 9 ((1046 · 0) + 1) = (0 + 1)
21016dec0h 11801 . . . . . . . . 9 1 = 01
211209, 188, 2103eqtri 2843 . . . . . . . 8 ((1046 · 0) + 1) = 01
2122, 3, 20, 16, 60, 194, 33, 16, 3, 206, 211decma2c 11832 . . . . . . 7 ((1046 · 40) + (21 + 0)) = 41861
2134, 3, 185, 16, 55, 192, 33, 16, 3, 212, 211decma2c 11832 . . . . . 6 ((1046 · 400) + (107 + 104)) = 418611
214207mulid1i 10339 . . . . . . . 8 (1046 · 1) = 1046
215214oveq1i 6894 . . . . . . 7 ((1046 · 1) + 0) = (1046 + 0)
216207addid1i 10518 . . . . . . 7 (1046 + 0) = 1046
217215, 216eqtri 2839 . . . . . 6 ((1046 · 1) + 0) = 1046
2185, 16, 29, 3, 1, 184, 33, 15, 32, 213, 217decma2c 11832 . . . . 5 ((1046 · 𝑁) + 1070) = 4186116
219 eqid 2817 . . . . . 6 2046 = 2046
22043, 20deccl 11794 . . . . . . 7 122 ∈ ℕ0
221220, 28deccl 11794 . . . . . 6 1227 ∈ ℕ0
222 eqid 2817 . . . . . . 7 204 = 204
223 eqid 2817 . . . . . . 7 1227 = 1227
22424, 16deccl 11794 . . . . . . . 8 81 ∈ ℕ0
225224, 12deccl 11794 . . . . . . 7 819 ∈ ℕ0
226 eqid 2817 . . . . . . . 8 20 = 20
227 eqid 2817 . . . . . . . . 9 122 = 122
228 eqid 2817 . . . . . . . . 9 819 = 819
229 eqid 2817 . . . . . . . . . . 11 81 = 81
230 8cn 11415 . . . . . . . . . . . 12 8 ∈ ℂ
231230, 69, 125addcomli 10523 . . . . . . . . . . 11 (1 + 8) = 9
232 2p1e3 11462 . . . . . . . . . . 11 (2 + 1) = 3
23316, 20, 24, 16, 108, 229, 231, 232decadd 11833 . . . . . . . . . 10 (12 + 81) = 93
23412, 41, 91, 233decsuc 11810 . . . . . . . . 9 ((12 + 81) + 1) = 94
235 9p2e11 11866 . . . . . . . . . 10 (9 + 2) = 11
23656, 51, 235addcomli 10523 . . . . . . . . 9 (2 + 9) = 11
23743, 20, 224, 12, 227, 228, 234, 16, 236decaddc 11834 . . . . . . . 8 (122 + 819) = 941
23813nn0cni 11591 . . . . . . . . . 10 94 ∈ ℂ
239238addid1i 10518 . . . . . . . . 9 (94 + 0) = 94
240123, 16eqeltri 2892 . . . . . . . . . . 11 (1 + 0) ∈ ℕ0
24151mul02i 10520 . . . . . . . . . . . . 13 (0 · 2) = 0
242241, 123oveq12i 6896 . . . . . . . . . . . 12 ((0 · 2) + (1 + 0)) = (0 + 1)
243242, 188eqtri 2839 . . . . . . . . . . 11 ((0 · 2) + (1 + 0)) = 1
24420, 3, 240, 226, 20, 113, 243decrmanc 11836 . . . . . . . . . 10 ((20 · 2) + (1 + 0)) = 41
245121oveq1i 6894 . . . . . . . . . . 11 ((4 · 2) + 0) = (8 + 0)
246230addid1i 10518 . . . . . . . . . . 11 (8 + 0) = 8
24724dec0h 11801 . . . . . . . . . . 11 8 = 08
248245, 246, 2473eqtri 2843 . . . . . . . . . 10 ((4 · 2) + 0) = 08
24935, 2, 16, 3, 222, 147, 20, 24, 3, 244, 248decmac 11831 . . . . . . . . 9 ((204 · 2) + (9 + 1)) = 418
25064, 51, 203addcomli 10523 . . . . . . . . . 10 (2 + 4) = 6
25116, 20, 2, 52, 250decaddi 11839 . . . . . . . . 9 ((6 · 2) + 4) = 16
25236, 15, 12, 2, 219, 239, 20, 15, 16, 249, 251decmac 11831 . . . . . . . 8 ((2046 · 2) + (94 + 0)) = 4186
253167mul01i 10521 . . . . . . . . . 10 (2046 · 0) = 0
254253oveq1i 6894 . . . . . . . . 9 ((2046 · 0) + 1) = (0 + 1)
255254, 188, 2103eqtri 2843 . . . . . . . 8 ((2046 · 0) + 1) = 01
25620, 3, 13, 16, 226, 237, 37, 16, 3, 252, 255decma2c 11832 . . . . . . 7 ((2046 · 20) + (122 + 819)) = 41861
25741dec0h 11801 . . . . . . . . 9 3 = 03
258188, 16eqeltri 2892 . . . . . . . . . 10 (0 + 1) ∈ ℕ0
25964mul02i 10520 . . . . . . . . . . . 12 (0 · 4) = 0
260259, 188oveq12i 6896 . . . . . . . . . . 11 ((0 · 4) + (0 + 1)) = (0 + 1)
261260, 188eqtri 2839 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = 1
26220, 3, 258, 226, 2, 122, 261decrmanc 11836 . . . . . . . . 9 ((20 · 4) + (0 + 1)) = 81
263 6p3e9 11479 . . . . . . . . . 10 (6 + 3) = 9
26416, 15, 41, 103, 263decaddi 11839 . . . . . . . . 9 ((4 · 4) + 3) = 19
26535, 2, 3, 41, 222, 257, 2, 12, 16, 262, 264decmac 11831 . . . . . . . 8 ((204 · 4) + 3) = 819
266153, 64, 191addcomli 10523 . . . . . . . . 9 (4 + 7) = 11
26720, 2, 28, 95, 232, 16, 266decaddci 11840 . . . . . . . 8 ((6 · 4) + 7) = 31
26836, 15, 28, 219, 2, 16, 41, 265, 267decrmac 11837 . . . . . . 7 ((2046 · 4) + 7) = 8191
26935, 2, 220, 28, 222, 223, 37, 16, 225, 256, 268decma2c 11832 . . . . . 6 ((2046 · 204) + 1227) = 418611
27050mul02i 10520 . . . . . . . . . . 11 (0 · 6) = 0
271270oveq1i 6894 . . . . . . . . . 10 ((0 · 6) + 2) = (0 + 2)
272271, 132eqtri 2839 . . . . . . . . 9 ((0 · 6) + 2) = 2
27320, 3, 20, 226, 15, 53, 272decrmanc 11836 . . . . . . . 8 ((20 · 6) + 2) = 122
274 4p3e7 11473 . . . . . . . . 9 (4 + 3) = 7
27520, 2, 41, 96, 274decaddi 11839 . . . . . . . 8 ((4 · 6) + 3) = 27
27635, 2, 41, 222, 15, 28, 20, 273, 275decrmac 11837 . . . . . . 7 ((204 · 6) + 3) = 1227
27715, 36, 15, 219, 15, 41, 276, 90decmul1c 11844 . . . . . 6 (2046 · 6) = 12276
27837, 36, 15, 219, 15, 221, 269, 277decmul2c 11845 . . . . 5 (2046 · 2046) = 4186116
279218, 278eqtr4i 2842 . . . 4 ((1046 · 𝑁) + 1070) = (2046 · 2046)
2808, 9, 31, 34, 37, 30, 178, 183, 279mod2xi 16010 . . 3 ((2↑50) mod 𝑁) = (1070 mod 𝑁)
28123nn0cni 11591 . . . 4 50 ∈ ℂ
282 eqid 2817 . . . . 5 50 = 50
28320, 22, 3, 282, 3, 181, 241decmul1 11843 . . . 4 (50 · 2) = 100
284281, 51, 283mulcomli 10344 . . 3 (2 · 50) = 100
285 eqid 2817 . . . . 5 614 = 614
28620, 12deccl 11794 . . . . 5 29 ∈ ℕ0
287 eqid 2817 . . . . . . 7 61 = 61
288 eqid 2817 . . . . . . 7 29 = 29
289199oveq1i 6894 . . . . . . . 8 ((6 + 2) + 1) = (8 + 1)
290289, 125eqtri 2839 . . . . . . 7 ((6 + 2) + 1) = 9
29115, 16, 20, 12, 287, 288, 290, 148decaddc2 11835 . . . . . 6 (61 + 29) = 90
29261, 3eqeltri 2892 . . . . . . . 8 (0 + 0) ∈ ℕ0
293 eqid 2817 . . . . . . . 8 286 = 286
294 eqid 2817 . . . . . . . . 9 28 = 28
295122oveq1i 6894 . . . . . . . . . 10 ((2 · 4) + 3) = (8 + 3)
296 8p3e11 11860 . . . . . . . . . 10 (8 + 3) = 11
297295, 296eqtri 2839 . . . . . . . . 9 ((2 · 4) + 3) = 11
298 8t4e32 11896 . . . . . . . . . 10 (8 · 4) = 32
29941, 20, 20, 298, 88decaddi 11839 . . . . . . . . 9 ((8 · 4) + 2) = 34
30020, 24, 20, 294, 2, 2, 41, 297, 299decrmac 11837 . . . . . . . 8 ((28 · 4) + 2) = 114
30195, 61oveq12i 6896 . . . . . . . . 9 ((6 · 4) + (0 + 0)) = (24 + 0)
30238nn0cni 11591 . . . . . . . . . 10 24 ∈ ℂ
303302addid1i 10518 . . . . . . . . 9 (24 + 0) = 24
304301, 303eqtri 2839 . . . . . . . 8 ((6 · 4) + (0 + 0)) = 24
30525, 15, 292, 293, 2, 2, 20, 300, 304decrmac 11837 . . . . . . 7 ((286 · 4) + (0 + 0)) = 1144
30626nn0cni 11591 . . . . . . . . . 10 286 ∈ ℂ
307306mul01i 10521 . . . . . . . . 9 (286 · 0) = 0
308307oveq1i 6894 . . . . . . . 8 ((286 · 0) + 9) = (0 + 9)
309308, 75, 583eqtri 2843 . . . . . . 7 ((286 · 0) + 9) = 09
3102, 3, 3, 12, 60, 59, 26, 12, 3, 305, 309decma2c 11832 . . . . . 6 ((286 · 40) + (9 + 0)) = 11449
311307oveq1i 6894 . . . . . . 7 ((286 · 0) + 0) = (0 + 0)
312311, 61, 623eqtri 2843 . . . . . 6 ((286 · 0) + 0) = 00
3134, 3, 12, 3, 55, 291, 26, 3, 3, 310, 312decma2c 11832 . . . . 5 ((286 · 400) + (61 + 29)) = 114490
314230mulid1i 10339 . . . . . . . 8 (8 · 1) = 8
31516, 20, 24, 294, 24, 109, 314decmul1 11843 . . . . . . 7 (28 · 1) = 28
31620, 24, 125, 315decsuc 11810 . . . . . 6 ((28 · 1) + 1) = 29
31750mulid1i 10339 . . . . . . . 8 (6 · 1) = 6
318317oveq1i 6894 . . . . . . 7 ((6 · 1) + 4) = (6 + 4)
319318, 92eqtri 2839 . . . . . 6 ((6 · 1) + 4) = 10
32025, 15, 2, 293, 16, 3, 16, 316, 319decrmac 11837 . . . . 5 ((286 · 1) + 4) = 290
3215, 16, 17, 2, 1, 285, 26, 3, 286, 313, 320decma2c 11832 . . . 4 ((286 · 𝑁) + 614) = 1144900
32216, 16deccl 11794 . . . . . . . . 9 11 ∈ ℕ0
323322, 2deccl 11794 . . . . . . . 8 114 ∈ ℕ0
324323, 2deccl 11794 . . . . . . 7 1144 ∈ ℕ0
325324, 12deccl 11794 . . . . . 6 11449 ∈ ℕ0
32628, 2deccl 11794 . . . . . . . 8 74 ∈ ℕ0
327326, 12deccl 11794 . . . . . . 7 749 ∈ ℕ0
328 eqid 2817 . . . . . . . 8 10 = 10
329 eqid 2817 . . . . . . . 8 749 = 749
330326nn0cni 11591 . . . . . . . . . 10 74 ∈ ℂ
331330addid1i 10518 . . . . . . . . 9 (74 + 0) = 74
332153addid1i 10518 . . . . . . . . . . 11 (7 + 0) = 7
333332, 28eqeltri 2892 . . . . . . . . . 10 (7 + 0) ∈ ℕ0
33410nn0cni 11591 . . . . . . . . . . . 12 10 ∈ ℂ
335334mulid1i 10339 . . . . . . . . . . 11 (10 · 1) = 10
33616, 3, 188, 335decsuc 11810 . . . . . . . . . 10 ((10 · 1) + 1) = 11
337153mulid1i 10339 . . . . . . . . . . . 12 (7 · 1) = 7
338337, 332oveq12i 6896 . . . . . . . . . . 11 ((7 · 1) + (7 + 0)) = (7 + 7)
339 7p7e14 11858 . . . . . . . . . . 11 (7 + 7) = 14
340338, 339eqtri 2839 . . . . . . . . . 10 ((7 · 1) + (7 + 0)) = 14
34110, 28, 333, 186, 16, 2, 16, 336, 340decrmac 11837 . . . . . . . . 9 ((107 · 1) + (7 + 0)) = 114
34269mul02i 10520 . . . . . . . . . . 11 (0 · 1) = 0
343342oveq1i 6894 . . . . . . . . . 10 ((0 · 1) + 4) = (0 + 4)
34464addid2i 10519 . . . . . . . . . 10 (0 + 4) = 4
345343, 344, 1143eqtri 2843 . . . . . . . . 9 ((0 · 1) + 4) = 04
34629, 3, 28, 2, 184, 331, 16, 2, 3, 341, 345decmac 11831 . . . . . . . 8 ((1070 · 1) + (74 + 0)) = 1144
34730nn0cni 11591 . . . . . . . . . . 11 1070 ∈ ℂ
348347mul01i 10521 . . . . . . . . . 10 (1070 · 0) = 0
349348oveq1i 6894 . . . . . . . . 9 ((1070 · 0) + 9) = (0 + 9)
350349, 75, 583eqtri 2843 . . . . . . . 8 ((1070 · 0) + 9) = 09
35116, 3, 326, 12, 328, 329, 30, 12, 3, 346, 350decma2c 11832 . . . . . . 7 ((1070 · 10) + 749) = 11449
352 dfdec10 11782 . . . . . . . . . 10 74 = ((10 · 7) + 4)
353352eqcomi 2826 . . . . . . . . 9 ((10 · 7) + 4) = 74
354 7t7e49 11893 . . . . . . . . 9 (7 · 7) = 49
35528, 10, 28, 186, 12, 2, 353, 354decmul1c 11844 . . . . . . . 8 (107 · 7) = 749
356153mul02i 10520 . . . . . . . 8 (0 · 7) = 0
35728, 29, 3, 184, 3, 355, 356decmul1 11843 . . . . . . 7 (1070 · 7) = 7490
35830, 10, 28, 186, 3, 327, 351, 357decmul2c 11845 . . . . . 6 (1070 · 107) = 114490
359325, 3, 3, 358, 61decaddi 11839 . . . . 5 ((1070 · 107) + 0) = 114490
360348, 62eqtri 2839 . . . . 5 (1070 · 0) = 00
36130, 29, 3, 184, 3, 3, 359, 360decmul2c 11845 . . . 4 (1070 · 1070) = 1144900
362321, 361eqtr4i 2842 . . 3 ((286 · 𝑁) + 614) = (1070 · 1070)
3638, 9, 23, 27, 30, 18, 280, 284, 362mod2xi 16010 . 2 ((2↑100) mod 𝑁) = (614 mod 𝑁)
36411nn0cni 11591 . . 3 100 ∈ ℂ
365 eqid 2817 . . . 4 100 = 100
36620, 10, 3, 365, 3, 173, 241decmul1 11843 . . 3 (100 · 2) = 200
367364, 51, 366mulcomli 10344 . 2 (2 · 100) = 200
368 eqid 2817 . . . 4 902 = 902
369 eqid 2817 . . . . . 6 90 = 90
37012, 3, 12, 369, 75decaddi 11839 . . . . 5 (90 + 9) = 99
371 eqid 2817 . . . . . . 7 94 = 94
372 6p1e7 11467 . . . . . . . 8 (6 + 1) = 7
373 9t4e36 11903 . . . . . . . 8 (9 · 4) = 36
37441, 15, 372, 373decsuc 11810 . . . . . . 7 ((9 · 4) + 1) = 37
375103, 61oveq12i 6896 . . . . . . . 8 ((4 · 4) + (0 + 0)) = (16 + 0)
37616, 15deccl 11794 . . . . . . . . . 10 16 ∈ ℕ0
377376nn0cni 11591 . . . . . . . . 9 16 ∈ ℂ
378377addid1i 10518 . . . . . . . 8 (16 + 0) = 16
379375, 378eqtri 2839 . . . . . . 7 ((4 · 4) + (0 + 0)) = 16
38012, 2, 292, 371, 2, 15, 16, 374, 379decrmac 11837 . . . . . 6 ((94 · 4) + (0 + 0)) = 376
381238mul01i 10521 . . . . . . . 8 (94 · 0) = 0
382381oveq1i 6894 . . . . . . 7 ((94 · 0) + 9) = (0 + 9)
383382, 75, 583eqtri 2843 . . . . . 6 ((94 · 0) + 9) = 09
3842, 3, 3, 12, 60, 59, 13, 12, 3, 380, 383decma2c 11832 . . . . 5 ((94 · 40) + (9 + 0)) = 3769
3854, 3, 12, 12, 55, 370, 13, 12, 3, 384, 383decma2c 11832 . . . 4 ((94 · 400) + (90 + 9)) = 37699
38656mulid1i 10339 . . . . 5 (9 · 1) = 9
38764mulid1i 10339 . . . . . . 7 (4 · 1) = 4
388387oveq1i 6894 . . . . . 6 ((4 · 1) + 2) = (4 + 2)
389388, 203eqtri 2839 . . . . 5 ((4 · 1) + 2) = 6
39012, 2, 20, 371, 16, 386, 389decrmanc 11836 . . . 4 ((94 · 1) + 2) = 96
3915, 16, 19, 20, 1, 368, 13, 15, 12, 385, 390decma2c 11832 . . 3 ((94 · 𝑁) + 902) = 376996
39238, 22deccl 11794 . . . 4 245 ∈ ℕ0
393 eqid 2817 . . . . 5 245 = 245
39450, 51, 199addcomli 10523 . . . . . . 7 (2 + 6) = 8
39520, 2, 15, 16, 165, 287, 394, 101decadd 11833 . . . . . 6 (24 + 61) = 85
396 8p2e10 11859 . . . . . . 7 (8 + 2) = 10
39741, 15, 372, 90decsuc 11810 . . . . . . 7 ((6 · 6) + 1) = 37
39850mulid2i 10340 . . . . . . . . 9 (1 · 6) = 6
399398oveq1i 6894 . . . . . . . 8 ((1 · 6) + 0) = (6 + 0)
40050addid1i 10518 . . . . . . . 8 (6 + 0) = 6
401399, 400eqtri 2839 . . . . . . 7 ((1 · 6) + 0) = 6
40215, 16, 16, 3, 287, 396, 15, 397, 401decma 11830 . . . . . 6 ((61 · 6) + (8 + 2)) = 376
40317, 2, 24, 22, 285, 395, 15, 12, 20, 402, 99decmac 11831 . . . . 5 ((614 · 6) + (24 + 61)) = 3769
40416, 15, 16, 287, 16, 317, 78decmul1 11843 . . . . . 6 (61 · 1) = 61
405387oveq1i 6894 . . . . . . 7 ((4 · 1) + 5) = (4 + 5)
406405, 98eqtri 2839 . . . . . 6 ((4 · 1) + 5) = 9
40717, 2, 22, 285, 16, 404, 406decrmanc 11836 . . . . 5 ((614 · 1) + 5) = 619
40815, 16, 38, 22, 287, 393, 18, 12, 17, 403, 407decma2c 11832 . . . 4 ((614 · 61) + 245) = 37699
40965oveq1i 6894 . . . . . . 7 ((1 · 4) + 1) = (4 + 1)
410409, 101eqtri 2839 . . . . . 6 ((1 · 4) + 1) = 5
41115, 16, 16, 287, 2, 95, 410decrmanc 11836 . . . . 5 ((61 · 4) + 1) = 245
4122, 17, 2, 285, 15, 16, 411, 103decmul1c 11844 . . . 4 (614 · 4) = 2456
41318, 17, 2, 285, 15, 392, 408, 412decmul2c 11845 . . 3 (614 · 614) = 376996
414391, 413eqtr4i 2842 . 2 ((94 · 𝑁) + 902) = (614 · 614)
4158, 9, 11, 14, 18, 21, 363, 367, 414mod2xi 16010 1 ((2↑200) mod 𝑁) = (902 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  (class class class)co 6884  0cc0 10231  1c1 10232   + caddc 10234   · cmul 10236  cn 11315  2c2 11368  3c3 11369  4c4 11370  5c5 11371  6c6 11372  7c7 11373  8c8 11374  9c9 11375  0cn0 11579  cdc 11779   mod cmo 12912  cexp 13103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-cnex 10287  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308  ax-pre-sup 10309
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-om 7306  df-2nd 7409  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-er 7989  df-en 8203  df-dom 8204  df-sdom 8205  df-sup 8597  df-inf 8598  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-div 10980  df-nn 11316  df-2 11376  df-3 11377  df-4 11378  df-5 11379  df-6 11380  df-7 11381  df-8 11382  df-9 11383  df-n0 11580  df-z 11664  df-dec 11780  df-uz 11925  df-rp 12067  df-fl 12837  df-mod 12913  df-seq 13045  df-exp 13104
This theorem is referenced by:  4001lem2  16080  4001lem3  16081
  Copyright terms: Public domain W3C validator