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

Theorem 4001lem2 17120
Description: Lemma for 4001prm 17123. Calculate a power mod. In decimal, we calculate 2↑400 = (2↑200)↑2≡902↑2 = 203𝑁 + 1401 and 2↑800 = (2↑400)↑2≡1401↑2 = 490𝑁 + 2311 ≡2311. (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
4001lem2 ((2↑800) mod 𝑁) = (2311 mod 𝑁)

Proof of Theorem 4001lem2
StepHypRef Expression
1 4001prm.1 . . 3 𝑁 = 4001
2 4nn0 12531 . . . . . 6 4 ∈ ℕ0
3 0nn0 12527 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12732 . . . . 5 40 ∈ ℕ0
54, 3deccl 12732 . . . 4 400 ∈ ℕ0
6 1nn 12263 . . . 4 1 ∈ ℕ
75, 6decnncl 12737 . . 3 4001 ∈ ℕ
81, 7eqeltri 2825 . 2 𝑁 ∈ ℕ
9 2nn 12325 . 2 2 ∈ ℕ
10 9nn0 12536 . . . . 5 9 ∈ ℕ0
112, 10deccl 12732 . . . 4 49 ∈ ℕ0
1211, 3deccl 12732 . . 3 490 ∈ ℕ0
1312nn0zi 12627 . 2 490 ∈ ℤ
14 1nn0 12528 . . . . 5 1 ∈ ℕ0
1514, 2deccl 12732 . . . 4 14 ∈ ℕ0
1615, 3deccl 12732 . . 3 140 ∈ ℕ0
1716, 14deccl 12732 . 2 1401 ∈ ℕ0
18 2nn0 12529 . . . . 5 2 ∈ ℕ0
19 3nn0 12530 . . . . 5 3 ∈ ℕ0
2018, 19deccl 12732 . . . 4 23 ∈ ℕ0
2120, 14deccl 12732 . . 3 231 ∈ ℕ0
2221, 14deccl 12732 . 2 2311 ∈ ℕ0
2318, 3deccl 12732 . . . 4 20 ∈ ℕ0
2423, 3deccl 12732 . . 3 200 ∈ ℕ0
2523, 19deccl 12732 . . . 4 203 ∈ ℕ0
2625nn0zi 12627 . . 3 203 ∈ ℤ
2710, 3deccl 12732 . . . 4 90 ∈ ℕ0
2827, 18deccl 12732 . . 3 902 ∈ ℕ0
2914001lem1 17119 . . 3 ((2↑200) mod 𝑁) = (902 mod 𝑁)
3024nn0cni 12524 . . . 4 200 ∈ ℂ
31 2cn 12327 . . . 4 2 ∈ ℂ
32 eqid 2728 . . . . 5 200 = 200
33 eqid 2728 . . . . . 6 20 = 20
34 2t2e4 12416 . . . . . 6 (2 · 2) = 4
3531mul02i 11443 . . . . . 6 (0 · 2) = 0
3618, 18, 3, 33, 34, 35decmul1 12781 . . . . 5 (20 · 2) = 40
3718, 23, 3, 32, 36, 35decmul1 12781 . . . 4 (200 · 2) = 400
3830, 31, 37mulcomli 11263 . . 3 (2 · 200) = 400
39 eqid 2728 . . . . 5 1401 = 1401
40 6nn0 12533 . . . . . . 7 6 ∈ ℕ0
4114, 40deccl 12732 . . . . . 6 16 ∈ ℕ0
42 eqid 2728 . . . . . 6 400 = 400
43 eqid 2728 . . . . . . 7 140 = 140
44 eqid 2728 . . . . . . . 8 14 = 14
45 4p2e6 12405 . . . . . . . 8 (4 + 2) = 6
4614, 2, 18, 44, 45decaddi 12777 . . . . . . 7 (14 + 2) = 16
47 00id 11429 . . . . . . 7 (0 + 0) = 0
4815, 3, 18, 3, 43, 33, 46, 47decadd 12771 . . . . . 6 (140 + 20) = 160
49 eqid 2728 . . . . . . 7 40 = 40
5041nn0cni 12524 . . . . . . . 8 16 ∈ ℂ
5150addridi 11441 . . . . . . 7 (16 + 0) = 16
52 eqid 2728 . . . . . . . 8 203 = 203
53 ax-1cn 11206 . . . . . . . . . 10 1 ∈ ℂ
5453addridi 11441 . . . . . . . . 9 (1 + 0) = 1
5514dec0h 12739 . . . . . . . . 9 1 = 01
5654, 55eqtri 2756 . . . . . . . 8 (1 + 0) = 01
5753addlidi 11442 . . . . . . . . . 10 (0 + 1) = 1
5857, 14eqeltri 2825 . . . . . . . . 9 (0 + 1) ∈ ℕ0
59 4cn 12337 . . . . . . . . . 10 4 ∈ ℂ
60 4t2e8 12420 . . . . . . . . . 10 (4 · 2) = 8
6159, 31, 60mulcomli 11263 . . . . . . . . 9 (2 · 4) = 8
6259mul02i 11443 . . . . . . . . . . 11 (0 · 4) = 0
6362, 57oveq12i 7438 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = (0 + 1)
6463, 57eqtri 2756 . . . . . . . . 9 ((0 · 4) + (0 + 1)) = 1
6518, 3, 58, 33, 2, 61, 64decrmanc 12774 . . . . . . . 8 ((20 · 4) + (0 + 1)) = 81
66 2p1e3 12394 . . . . . . . . 9 (2 + 1) = 3
67 3cn 12333 . . . . . . . . . 10 3 ∈ ℂ
68 4t3e12 12815 . . . . . . . . . 10 (4 · 3) = 12
6959, 67, 68mulcomli 11263 . . . . . . . . 9 (3 · 4) = 12
7014, 18, 66, 69decsuc 12748 . . . . . . . 8 ((3 · 4) + 1) = 13
7123, 19, 3, 14, 52, 56, 2, 19, 14, 65, 70decmac 12769 . . . . . . 7 ((203 · 4) + (1 + 0)) = 813
7225nn0cni 12524 . . . . . . . . . 10 203 ∈ ℂ
7372mul01i 11444 . . . . . . . . 9 (203 · 0) = 0
7473oveq1i 7436 . . . . . . . 8 ((203 · 0) + 6) = (0 + 6)
75 6cn 12343 . . . . . . . . 9 6 ∈ ℂ
7675addlidi 11442 . . . . . . . 8 (0 + 6) = 6
7740dec0h 12739 . . . . . . . 8 6 = 06
7874, 76, 773eqtri 2760 . . . . . . 7 ((203 · 0) + 6) = 06
792, 3, 14, 40, 49, 51, 25, 40, 3, 71, 78decma2c 12770 . . . . . 6 ((203 · 40) + (16 + 0)) = 8136
8073oveq1i 7436 . . . . . . 7 ((203 · 0) + 0) = (0 + 0)
813dec0h 12739 . . . . . . 7 0 = 00
8280, 47, 813eqtri 2760 . . . . . 6 ((203 · 0) + 0) = 00
834, 3, 41, 3, 42, 48, 25, 3, 3, 79, 82decma2c 12770 . . . . 5 ((203 · 400) + (140 + 20)) = 81360
8431mulridi 11258 . . . . . . 7 (2 · 1) = 2
8553mul02i 11443 . . . . . . 7 (0 · 1) = 0
8614, 18, 3, 33, 84, 85decmul1 12781 . . . . . 6 (20 · 1) = 20
8767mulridi 11258 . . . . . . . 8 (3 · 1) = 3
8887oveq1i 7436 . . . . . . 7 ((3 · 1) + 1) = (3 + 1)
89 3p1e4 12397 . . . . . . 7 (3 + 1) = 4
9088, 89eqtri 2756 . . . . . 6 ((3 · 1) + 1) = 4
9123, 19, 14, 52, 14, 86, 90decrmanc 12774 . . . . 5 ((203 · 1) + 1) = 204
925, 14, 16, 14, 1, 39, 25, 2, 23, 83, 91decma2c 12770 . . . 4 ((203 · 𝑁) + 1401) = 813604
93 eqid 2728 . . . . 5 902 = 902
94 8nn0 12535 . . . . . . 7 8 ∈ ℕ0
9514, 94deccl 12732 . . . . . 6 18 ∈ ℕ0
9695, 3deccl 12732 . . . . 5 180 ∈ ℕ0
97 eqid 2728 . . . . . 6 90 = 90
98 eqid 2728 . . . . . 6 180 = 180
9995nn0cni 12524 . . . . . . . 8 18 ∈ ℂ
10099addridi 11441 . . . . . . 7 (18 + 0) = 18
101 1p2e3 12395 . . . . . . . . 9 (1 + 2) = 3
102101, 19eqeltri 2825 . . . . . . . 8 (1 + 2) ∈ ℕ0
103 9t9e81 12846 . . . . . . . 8 (9 · 9) = 81
104 9cn 12352 . . . . . . . . . . 11 9 ∈ ℂ
105104mul02i 11443 . . . . . . . . . 10 (0 · 9) = 0
106105, 101oveq12i 7438 . . . . . . . . 9 ((0 · 9) + (1 + 2)) = (0 + 3)
10767addlidi 11442 . . . . . . . . 9 (0 + 3) = 3
108106, 107eqtri 2756 . . . . . . . 8 ((0 · 9) + (1 + 2)) = 3
10910, 3, 102, 97, 10, 103, 108decrmanc 12774 . . . . . . 7 ((90 · 9) + (1 + 2)) = 813
110 9t2e18 12839 . . . . . . . . 9 (9 · 2) = 18
111104, 31, 110mulcomli 11263 . . . . . . . 8 (2 · 9) = 18
112 1p1e2 12377 . . . . . . . 8 (1 + 1) = 2
113 8p8e16 12803 . . . . . . . 8 (8 + 8) = 16
11414, 94, 94, 111, 112, 40, 113decaddci 12778 . . . . . . 7 ((2 · 9) + 8) = 26
11527, 18, 14, 94, 93, 100, 10, 40, 18, 109, 114decmac 12769 . . . . . 6 ((902 · 9) + (18 + 0)) = 8136
11628nn0cni 12524 . . . . . . . . 9 902 ∈ ℂ
117116mul01i 11444 . . . . . . . 8 (902 · 0) = 0
118117oveq1i 7436 . . . . . . 7 ((902 · 0) + 0) = (0 + 0)
119118, 47, 813eqtri 2760 . . . . . 6 ((902 · 0) + 0) = 00
12010, 3, 95, 3, 97, 98, 28, 3, 3, 115, 119decma2c 12770 . . . . 5 ((902 · 90) + 180) = 81360
12118, 10, 3, 97, 110, 35decmul1 12781 . . . . . 6 (90 · 2) = 180
12218, 27, 18, 93, 121, 34decmul1 12781 . . . . 5 (902 · 2) = 1804
12328, 27, 18, 93, 2, 96, 120, 122decmul2c 12783 . . . 4 (902 · 902) = 813604
12492, 123eqtr4i 2759 . . 3 ((203 · 𝑁) + 1401) = (902 · 902)
1258, 9, 24, 26, 28, 17, 29, 38, 124mod2xi 17047 . 2 ((2↑400) mod 𝑁) = (1401 mod 𝑁)
1265nn0cni 12524 . . 3 400 ∈ ℂ
12718, 2, 3, 49, 60, 35decmul1 12781 . . . 4 (40 · 2) = 80
12818, 4, 3, 42, 127, 35decmul1 12781 . . 3 (400 · 2) = 800
129126, 31, 128mulcomli 11263 . 2 (2 · 400) = 800
130 eqid 2728 . . . 4 2311 = 2311
13118, 94deccl 12732 . . . . 5 28 ∈ ℕ0
132 eqid 2728 . . . . . 6 231 = 231
133 eqid 2728 . . . . . 6 49 = 49
134 7nn0 12534 . . . . . . 7 7 ∈ ℕ0
135 7p1e8 12401 . . . . . . 7 (7 + 1) = 8
136 eqid 2728 . . . . . . . 8 23 = 23
137 4p3e7 12406 . . . . . . . . 9 (4 + 3) = 7
13859, 67, 137addcomli 11446 . . . . . . . 8 (3 + 4) = 7
13918, 19, 2, 136, 138decaddi 12777 . . . . . . 7 (23 + 4) = 27
14018, 134, 135, 139decsuc 12748 . . . . . 6 ((23 + 4) + 1) = 28
141 9p1e10 12719 . . . . . . 7 (9 + 1) = 10
142104, 53, 141addcomli 11446 . . . . . 6 (1 + 9) = 10
14320, 14, 2, 10, 132, 133, 140, 142decaddc2 12773 . . . . 5 (231 + 49) = 280
144131nn0cni 12524 . . . . . . 7 28 ∈ ℂ
145144addridi 11441 . . . . . 6 (28 + 0) = 28
14631addridi 11441 . . . . . . . 8 (2 + 0) = 2
147146, 18eqeltri 2825 . . . . . . 7 (2 + 0) ∈ ℕ0
148 eqid 2728 . . . . . . 7 490 = 490
149 4t4e16 12816 . . . . . . . . 9 (4 · 4) = 16
150 6p3e9 12412 . . . . . . . . 9 (6 + 3) = 9
15114, 40, 19, 149, 150decaddi 12777 . . . . . . . 8 ((4 · 4) + 3) = 19
152 9t4e36 12841 . . . . . . . 8 (9 · 4) = 36
1532, 2, 10, 133, 40, 19, 151, 152decmul1c 12782 . . . . . . 7 (49 · 4) = 196
15462, 146oveq12i 7438 . . . . . . . 8 ((0 · 4) + (2 + 0)) = (0 + 2)
15531addlidi 11442 . . . . . . . 8 (0 + 2) = 2
156154, 155eqtri 2756 . . . . . . 7 ((0 · 4) + (2 + 0)) = 2
15711, 3, 147, 148, 2, 153, 156decrmanc 12774 . . . . . 6 ((490 · 4) + (2 + 0)) = 1962
15812nn0cni 12524 . . . . . . . . 9 490 ∈ ℂ
159158mul01i 11444 . . . . . . . 8 (490 · 0) = 0
160159oveq1i 7436 . . . . . . 7 ((490 · 0) + 8) = (0 + 8)
161 8cn 12349 . . . . . . . 8 8 ∈ ℂ
162161addlidi 11442 . . . . . . 7 (0 + 8) = 8
16394dec0h 12739 . . . . . . 7 8 = 08
164160, 162, 1633eqtri 2760 . . . . . 6 ((490 · 0) + 8) = 08
1652, 3, 18, 94, 49, 145, 12, 94, 3, 157, 164decma2c 12770 . . . . 5 ((490 · 40) + (28 + 0)) = 19628
166159oveq1i 7436 . . . . . 6 ((490 · 0) + 0) = (0 + 0)
167166, 47, 813eqtri 2760 . . . . 5 ((490 · 0) + 0) = 00
1684, 3, 131, 3, 42, 143, 12, 3, 3, 165, 167decma2c 12770 . . . 4 ((490 · 400) + (231 + 49)) = 196280
16959mulridi 11258 . . . . . 6 (4 · 1) = 4
170104mulridi 11258 . . . . . 6 (9 · 1) = 9
17114, 2, 10, 133, 169, 170decmul1 12781 . . . . 5 (49 · 1) = 49
17285oveq1i 7436 . . . . . 6 ((0 · 1) + 1) = (0 + 1)
173172, 57eqtri 2756 . . . . 5 ((0 · 1) + 1) = 1
17411, 3, 14, 148, 14, 171, 173decrmanc 12774 . . . 4 ((490 · 1) + 1) = 491
1755, 14, 21, 14, 1, 130, 12, 14, 11, 168, 174decma2c 12770 . . 3 ((490 · 𝑁) + 2311) = 1962801
17615nn0cni 12524 . . . . . . 7 14 ∈ ℂ
177176addridi 11441 . . . . . 6 (14 + 0) = 14
178 5nn0 12532 . . . . . . . 8 5 ∈ ℕ0
179178, 40deccl 12732 . . . . . . 7 56 ∈ ℕ0
180179, 3deccl 12732 . . . . . 6 560 ∈ ℕ0
181 eqid 2728 . . . . . . . 8 560 = 560
182179nn0cni 12524 . . . . . . . . 9 56 ∈ ℂ
183182addlidi 11442 . . . . . . . 8 (0 + 56) = 56
1843, 14, 179, 3, 55, 181, 183, 54decadd 12771 . . . . . . 7 (1 + 560) = 561
185182addridi 11441 . . . . . . . 8 (56 + 0) = 56
186 5cn 12340 . . . . . . . . . . 11 5 ∈ ℂ
187186addridi 11441 . . . . . . . . . 10 (5 + 0) = 5
188187, 178eqeltri 2825 . . . . . . . . 9 (5 + 0) ∈ ℕ0
18953mulridi 11258 . . . . . . . . 9 (1 · 1) = 1
190169, 187oveq12i 7438 . . . . . . . . . 10 ((4 · 1) + (5 + 0)) = (4 + 5)
191 5p4e9 12410 . . . . . . . . . . 11 (5 + 4) = 9
192186, 59, 191addcomli 11446 . . . . . . . . . 10 (4 + 5) = 9
193190, 192eqtri 2756 . . . . . . . . 9 ((4 · 1) + (5 + 0)) = 9
19414, 2, 188, 44, 14, 189, 193decrmanc 12774 . . . . . . . 8 ((14 · 1) + (5 + 0)) = 19
19585oveq1i 7436 . . . . . . . . 9 ((0 · 1) + 6) = (0 + 6)
196195, 76, 773eqtri 2760 . . . . . . . 8 ((0 · 1) + 6) = 06
19715, 3, 178, 40, 43, 185, 14, 40, 3, 194, 196decmac 12769 . . . . . . 7 ((140 · 1) + (56 + 0)) = 196
198189oveq1i 7436 . . . . . . . 8 ((1 · 1) + 1) = (1 + 1)
19918dec0h 12739 . . . . . . . 8 2 = 02
200198, 112, 1993eqtri 2760 . . . . . . 7 ((1 · 1) + 1) = 02
20116, 14, 179, 14, 39, 184, 14, 18, 3, 197, 200decmac 12769 . . . . . 6 ((1401 · 1) + (1 + 560)) = 1962
20259mullidi 11259 . . . . . . . . . . . 12 (1 · 4) = 4
203202oveq1i 7436 . . . . . . . . . . 11 ((1 · 4) + 1) = (4 + 1)
204 4p1e5 12398 . . . . . . . . . . 11 (4 + 1) = 5
205203, 204eqtri 2756 . . . . . . . . . 10 ((1 · 4) + 1) = 5
2062, 14, 2, 44, 40, 14, 205, 149decmul1c 12782 . . . . . . . . 9 (14 · 4) = 56
20775addridi 11441 . . . . . . . . 9 (6 + 0) = 6
208178, 40, 3, 206, 207decaddi 12777 . . . . . . . 8 ((14 · 4) + 0) = 56
209 0cn 11246 . . . . . . . . 9 0 ∈ ℂ
21059mul01i 11444 . . . . . . . . . 10 (4 · 0) = 0
211210, 81eqtri 2756 . . . . . . . . 9 (4 · 0) = 00
21259, 209, 211mulcomli 11263 . . . . . . . 8 (0 · 4) = 00
2132, 15, 3, 43, 3, 3, 208, 212decmul1c 12782 . . . . . . 7 (140 · 4) = 560
214202oveq1i 7436 . . . . . . . 8 ((1 · 4) + 4) = (4 + 4)
215 4p4e8 12407 . . . . . . . 8 (4 + 4) = 8
216214, 215eqtri 2756 . . . . . . 7 ((1 · 4) + 4) = 8
21716, 14, 2, 39, 2, 213, 216decrmanc 12774 . . . . . 6 ((1401 · 4) + 4) = 5608
21814, 2, 14, 2, 44, 177, 17, 94, 180, 201, 217decma2c 12770 . . . . 5 ((1401 · 14) + (14 + 0)) = 19628
21917nn0cni 12524 . . . . . . . 8 1401 ∈ ℂ
220219mul01i 11444 . . . . . . 7 (1401 · 0) = 0
221220oveq1i 7436 . . . . . 6 ((1401 · 0) + 0) = (0 + 0)
222221, 47, 813eqtri 2760 . . . . 5 ((1401 · 0) + 0) = 00
22315, 3, 15, 3, 43, 43, 17, 3, 3, 218, 222decma2c 12770 . . . 4 ((1401 · 140) + 140) = 196280
224219mulridi 11258 . . . 4 (1401 · 1) = 1401
22517, 16, 14, 39, 14, 16, 223, 224decmul2c 12783 . . 3 (1401 · 1401) = 1962801
226175, 225eqtr4i 2759 . 2 ((490 · 𝑁) + 2311) = (1401 · 1401)
2278, 9, 5, 13, 17, 22, 125, 129, 226mod2xi 17047 1 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  (class class class)co 7426  0cc0 11148  1c1 11149   + caddc 11151   · cmul 11153  cn 12252  2c2 12307  3c3 12308  4c4 12309  5c5 12310  6c6 12311  7c7 12312  8c8 12313  9c9 12314  0cn0 12512  cdc 12717   mod cmo 13876  cexp 14068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pow 5369  ax-pr 5433  ax-un 7748  ax-cnex 11204  ax-resscn 11205  ax-1cn 11206  ax-icn 11207  ax-addcl 11208  ax-addrcl 11209  ax-mulcl 11210  ax-mulrcl 11211  ax-mulcom 11212  ax-addass 11213  ax-mulass 11214  ax-distr 11215  ax-i2m1 11216  ax-1ne0 11217  ax-1rid 11218  ax-rnegex 11219  ax-rrecex 11220  ax-cnre 11221  ax-pre-lttri 11222  ax-pre-lttrn 11223  ax-pre-ltadd 11224  ax-pre-mulgt0 11225  ax-pre-sup 11226
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4327  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6310  df-ord 6377  df-on 6378  df-lim 6379  df-suc 6380  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7382  df-ov 7429  df-oprab 7430  df-mpo 7431  df-om 7879  df-2nd 8002  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-er 8733  df-en 8973  df-dom 8974  df-sdom 8975  df-sup 9475  df-inf 9476  df-pnf 11290  df-mnf 11291  df-xr 11292  df-ltxr 11293  df-le 11294  df-sub 11486  df-neg 11487  df-div 11912  df-nn 12253  df-2 12315  df-3 12316  df-4 12317  df-5 12318  df-6 12319  df-7 12320  df-8 12321  df-9 12322  df-n0 12513  df-z 12599  df-dec 12718  df-uz 12863  df-rp 13017  df-fl 13799  df-mod 13877  df-seq 14009  df-exp 14069
This theorem is referenced by:  4001lem3  17121  4001lem4  17122
  Copyright terms: Public domain W3C validator