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

Theorem 4001lem2 17179
Description: Lemma for 4001prm 17182. 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 12545 . . . . . 6 4 ∈ ℕ0
3 0nn0 12541 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12748 . . . . 5 40 ∈ ℕ0
54, 3deccl 12748 . . . 4 400 ∈ ℕ0
6 1nn 12277 . . . 4 1 ∈ ℕ
75, 6decnncl 12753 . . 3 4001 ∈ ℕ
81, 7eqeltri 2837 . 2 𝑁 ∈ ℕ
9 2nn 12339 . 2 2 ∈ ℕ
10 9nn0 12550 . . . . 5 9 ∈ ℕ0
112, 10deccl 12748 . . . 4 49 ∈ ℕ0
1211, 3deccl 12748 . . 3 490 ∈ ℕ0
1312nn0zi 12642 . 2 490 ∈ ℤ
14 1nn0 12542 . . . . 5 1 ∈ ℕ0
1514, 2deccl 12748 . . . 4 14 ∈ ℕ0
1615, 3deccl 12748 . . 3 140 ∈ ℕ0
1716, 14deccl 12748 . 2 1401 ∈ ℕ0
18 2nn0 12543 . . . . 5 2 ∈ ℕ0
19 3nn0 12544 . . . . 5 3 ∈ ℕ0
2018, 19deccl 12748 . . . 4 23 ∈ ℕ0
2120, 14deccl 12748 . . 3 231 ∈ ℕ0
2221, 14deccl 12748 . 2 2311 ∈ ℕ0
2318, 3deccl 12748 . . . 4 20 ∈ ℕ0
2423, 3deccl 12748 . . 3 200 ∈ ℕ0
2523, 19deccl 12748 . . . 4 203 ∈ ℕ0
2625nn0zi 12642 . . 3 203 ∈ ℤ
2710, 3deccl 12748 . . . 4 90 ∈ ℕ0
2827, 18deccl 12748 . . 3 902 ∈ ℕ0
2914001lem1 17178 . . 3 ((2↑200) mod 𝑁) = (902 mod 𝑁)
3024nn0cni 12538 . . . 4 200 ∈ ℂ
31 2cn 12341 . . . 4 2 ∈ ℂ
32 eqid 2737 . . . . 5 200 = 200
33 eqid 2737 . . . . . 6 20 = 20
34 2t2e4 12430 . . . . . 6 (2 · 2) = 4
3531mul02i 11450 . . . . . 6 (0 · 2) = 0
3618, 18, 3, 33, 34, 35decmul1 12797 . . . . 5 (20 · 2) = 40
3718, 23, 3, 32, 36, 35decmul1 12797 . . . 4 (200 · 2) = 400
3830, 31, 37mulcomli 11270 . . 3 (2 · 200) = 400
39 eqid 2737 . . . . 5 1401 = 1401
40 6nn0 12547 . . . . . . 7 6 ∈ ℕ0
4114, 40deccl 12748 . . . . . 6 16 ∈ ℕ0
42 eqid 2737 . . . . . 6 400 = 400
43 eqid 2737 . . . . . . 7 140 = 140
44 eqid 2737 . . . . . . . 8 14 = 14
45 4p2e6 12419 . . . . . . . 8 (4 + 2) = 6
4614, 2, 18, 44, 45decaddi 12793 . . . . . . 7 (14 + 2) = 16
47 00id 11436 . . . . . . 7 (0 + 0) = 0
4815, 3, 18, 3, 43, 33, 46, 47decadd 12787 . . . . . 6 (140 + 20) = 160
49 eqid 2737 . . . . . . 7 40 = 40
5041nn0cni 12538 . . . . . . . 8 16 ∈ ℂ
5150addridi 11448 . . . . . . 7 (16 + 0) = 16
52 eqid 2737 . . . . . . . 8 203 = 203
53 ax-1cn 11213 . . . . . . . . . 10 1 ∈ ℂ
5453addridi 11448 . . . . . . . . 9 (1 + 0) = 1
5514dec0h 12755 . . . . . . . . 9 1 = 01
5654, 55eqtri 2765 . . . . . . . 8 (1 + 0) = 01
5753addlidi 11449 . . . . . . . . . 10 (0 + 1) = 1
5857, 14eqeltri 2837 . . . . . . . . 9 (0 + 1) ∈ ℕ0
59 4cn 12351 . . . . . . . . . 10 4 ∈ ℂ
60 4t2e8 12434 . . . . . . . . . 10 (4 · 2) = 8
6159, 31, 60mulcomli 11270 . . . . . . . . 9 (2 · 4) = 8
6259mul02i 11450 . . . . . . . . . . 11 (0 · 4) = 0
6362, 57oveq12i 7443 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = (0 + 1)
6463, 57eqtri 2765 . . . . . . . . 9 ((0 · 4) + (0 + 1)) = 1
6518, 3, 58, 33, 2, 61, 64decrmanc 12790 . . . . . . . 8 ((20 · 4) + (0 + 1)) = 81
66 2p1e3 12408 . . . . . . . . 9 (2 + 1) = 3
67 3cn 12347 . . . . . . . . . 10 3 ∈ ℂ
68 4t3e12 12831 . . . . . . . . . 10 (4 · 3) = 12
6959, 67, 68mulcomli 11270 . . . . . . . . 9 (3 · 4) = 12
7014, 18, 66, 69decsuc 12764 . . . . . . . 8 ((3 · 4) + 1) = 13
7123, 19, 3, 14, 52, 56, 2, 19, 14, 65, 70decmac 12785 . . . . . . 7 ((203 · 4) + (1 + 0)) = 813
7225nn0cni 12538 . . . . . . . . . 10 203 ∈ ℂ
7372mul01i 11451 . . . . . . . . 9 (203 · 0) = 0
7473oveq1i 7441 . . . . . . . 8 ((203 · 0) + 6) = (0 + 6)
75 6cn 12357 . . . . . . . . 9 6 ∈ ℂ
7675addlidi 11449 . . . . . . . 8 (0 + 6) = 6
7740dec0h 12755 . . . . . . . 8 6 = 06
7874, 76, 773eqtri 2769 . . . . . . 7 ((203 · 0) + 6) = 06
792, 3, 14, 40, 49, 51, 25, 40, 3, 71, 78decma2c 12786 . . . . . 6 ((203 · 40) + (16 + 0)) = 8136
8073oveq1i 7441 . . . . . . 7 ((203 · 0) + 0) = (0 + 0)
813dec0h 12755 . . . . . . 7 0 = 00
8280, 47, 813eqtri 2769 . . . . . 6 ((203 · 0) + 0) = 00
834, 3, 41, 3, 42, 48, 25, 3, 3, 79, 82decma2c 12786 . . . . 5 ((203 · 400) + (140 + 20)) = 81360
8431mulridi 11265 . . . . . . 7 (2 · 1) = 2
8553mul02i 11450 . . . . . . 7 (0 · 1) = 0
8614, 18, 3, 33, 84, 85decmul1 12797 . . . . . 6 (20 · 1) = 20
8767mulridi 11265 . . . . . . . 8 (3 · 1) = 3
8887oveq1i 7441 . . . . . . 7 ((3 · 1) + 1) = (3 + 1)
89 3p1e4 12411 . . . . . . 7 (3 + 1) = 4
9088, 89eqtri 2765 . . . . . 6 ((3 · 1) + 1) = 4
9123, 19, 14, 52, 14, 86, 90decrmanc 12790 . . . . 5 ((203 · 1) + 1) = 204
925, 14, 16, 14, 1, 39, 25, 2, 23, 83, 91decma2c 12786 . . . 4 ((203 · 𝑁) + 1401) = 813604
93 eqid 2737 . . . . 5 902 = 902
94 8nn0 12549 . . . . . . 7 8 ∈ ℕ0
9514, 94deccl 12748 . . . . . 6 18 ∈ ℕ0
9695, 3deccl 12748 . . . . 5 180 ∈ ℕ0
97 eqid 2737 . . . . . 6 90 = 90
98 eqid 2737 . . . . . 6 180 = 180
9995nn0cni 12538 . . . . . . . 8 18 ∈ ℂ
10099addridi 11448 . . . . . . 7 (18 + 0) = 18
101 1p2e3 12409 . . . . . . . . 9 (1 + 2) = 3
102101, 19eqeltri 2837 . . . . . . . 8 (1 + 2) ∈ ℕ0
103 9t9e81 12862 . . . . . . . 8 (9 · 9) = 81
104 9cn 12366 . . . . . . . . . . 11 9 ∈ ℂ
105104mul02i 11450 . . . . . . . . . 10 (0 · 9) = 0
106105, 101oveq12i 7443 . . . . . . . . 9 ((0 · 9) + (1 + 2)) = (0 + 3)
10767addlidi 11449 . . . . . . . . 9 (0 + 3) = 3
108106, 107eqtri 2765 . . . . . . . 8 ((0 · 9) + (1 + 2)) = 3
10910, 3, 102, 97, 10, 103, 108decrmanc 12790 . . . . . . 7 ((90 · 9) + (1 + 2)) = 813
110 9t2e18 12855 . . . . . . . . 9 (9 · 2) = 18
111104, 31, 110mulcomli 11270 . . . . . . . 8 (2 · 9) = 18
112 1p1e2 12391 . . . . . . . 8 (1 + 1) = 2
113 8p8e16 12819 . . . . . . . 8 (8 + 8) = 16
11414, 94, 94, 111, 112, 40, 113decaddci 12794 . . . . . . 7 ((2 · 9) + 8) = 26
11527, 18, 14, 94, 93, 100, 10, 40, 18, 109, 114decmac 12785 . . . . . 6 ((902 · 9) + (18 + 0)) = 8136
11628nn0cni 12538 . . . . . . . . 9 902 ∈ ℂ
117116mul01i 11451 . . . . . . . 8 (902 · 0) = 0
118117oveq1i 7441 . . . . . . 7 ((902 · 0) + 0) = (0 + 0)
119118, 47, 813eqtri 2769 . . . . . 6 ((902 · 0) + 0) = 00
12010, 3, 95, 3, 97, 98, 28, 3, 3, 115, 119decma2c 12786 . . . . 5 ((902 · 90) + 180) = 81360
12118, 10, 3, 97, 110, 35decmul1 12797 . . . . . 6 (90 · 2) = 180
12218, 27, 18, 93, 121, 34decmul1 12797 . . . . 5 (902 · 2) = 1804
12328, 27, 18, 93, 2, 96, 120, 122decmul2c 12799 . . . 4 (902 · 902) = 813604
12492, 123eqtr4i 2768 . . 3 ((203 · 𝑁) + 1401) = (902 · 902)
1258, 9, 24, 26, 28, 17, 29, 38, 124mod2xi 17107 . 2 ((2↑400) mod 𝑁) = (1401 mod 𝑁)
1265nn0cni 12538 . . 3 400 ∈ ℂ
12718, 2, 3, 49, 60, 35decmul1 12797 . . . 4 (40 · 2) = 80
12818, 4, 3, 42, 127, 35decmul1 12797 . . 3 (400 · 2) = 800
129126, 31, 128mulcomli 11270 . 2 (2 · 400) = 800
130 eqid 2737 . . . 4 2311 = 2311
13118, 94deccl 12748 . . . . 5 28 ∈ ℕ0
132 eqid 2737 . . . . . 6 231 = 231
133 eqid 2737 . . . . . 6 49 = 49
134 7nn0 12548 . . . . . . 7 7 ∈ ℕ0
135 7p1e8 12415 . . . . . . 7 (7 + 1) = 8
136 eqid 2737 . . . . . . . 8 23 = 23
137 4p3e7 12420 . . . . . . . . 9 (4 + 3) = 7
13859, 67, 137addcomli 11453 . . . . . . . 8 (3 + 4) = 7
13918, 19, 2, 136, 138decaddi 12793 . . . . . . 7 (23 + 4) = 27
14018, 134, 135, 139decsuc 12764 . . . . . 6 ((23 + 4) + 1) = 28
141 9p1e10 12735 . . . . . . 7 (9 + 1) = 10
142104, 53, 141addcomli 11453 . . . . . 6 (1 + 9) = 10
14320, 14, 2, 10, 132, 133, 140, 142decaddc2 12789 . . . . 5 (231 + 49) = 280
144131nn0cni 12538 . . . . . . 7 28 ∈ ℂ
145144addridi 11448 . . . . . 6 (28 + 0) = 28
14631addridi 11448 . . . . . . . 8 (2 + 0) = 2
147146, 18eqeltri 2837 . . . . . . 7 (2 + 0) ∈ ℕ0
148 eqid 2737 . . . . . . 7 490 = 490
149 4t4e16 12832 . . . . . . . . 9 (4 · 4) = 16
150 6p3e9 12426 . . . . . . . . 9 (6 + 3) = 9
15114, 40, 19, 149, 150decaddi 12793 . . . . . . . 8 ((4 · 4) + 3) = 19
152 9t4e36 12857 . . . . . . . 8 (9 · 4) = 36
1532, 2, 10, 133, 40, 19, 151, 152decmul1c 12798 . . . . . . 7 (49 · 4) = 196
15462, 146oveq12i 7443 . . . . . . . 8 ((0 · 4) + (2 + 0)) = (0 + 2)
15531addlidi 11449 . . . . . . . 8 (0 + 2) = 2
156154, 155eqtri 2765 . . . . . . 7 ((0 · 4) + (2 + 0)) = 2
15711, 3, 147, 148, 2, 153, 156decrmanc 12790 . . . . . 6 ((490 · 4) + (2 + 0)) = 1962
15812nn0cni 12538 . . . . . . . . 9 490 ∈ ℂ
159158mul01i 11451 . . . . . . . 8 (490 · 0) = 0
160159oveq1i 7441 . . . . . . 7 ((490 · 0) + 8) = (0 + 8)
161 8cn 12363 . . . . . . . 8 8 ∈ ℂ
162161addlidi 11449 . . . . . . 7 (0 + 8) = 8
16394dec0h 12755 . . . . . . 7 8 = 08
164160, 162, 1633eqtri 2769 . . . . . 6 ((490 · 0) + 8) = 08
1652, 3, 18, 94, 49, 145, 12, 94, 3, 157, 164decma2c 12786 . . . . 5 ((490 · 40) + (28 + 0)) = 19628
166159oveq1i 7441 . . . . . 6 ((490 · 0) + 0) = (0 + 0)
167166, 47, 813eqtri 2769 . . . . 5 ((490 · 0) + 0) = 00
1684, 3, 131, 3, 42, 143, 12, 3, 3, 165, 167decma2c 12786 . . . 4 ((490 · 400) + (231 + 49)) = 196280
16959mulridi 11265 . . . . . 6 (4 · 1) = 4
170104mulridi 11265 . . . . . 6 (9 · 1) = 9
17114, 2, 10, 133, 169, 170decmul1 12797 . . . . 5 (49 · 1) = 49
17285oveq1i 7441 . . . . . 6 ((0 · 1) + 1) = (0 + 1)
173172, 57eqtri 2765 . . . . 5 ((0 · 1) + 1) = 1
17411, 3, 14, 148, 14, 171, 173decrmanc 12790 . . . 4 ((490 · 1) + 1) = 491
1755, 14, 21, 14, 1, 130, 12, 14, 11, 168, 174decma2c 12786 . . 3 ((490 · 𝑁) + 2311) = 1962801
17615nn0cni 12538 . . . . . . 7 14 ∈ ℂ
177176addridi 11448 . . . . . 6 (14 + 0) = 14
178 5nn0 12546 . . . . . . . 8 5 ∈ ℕ0
179178, 40deccl 12748 . . . . . . 7 56 ∈ ℕ0
180179, 3deccl 12748 . . . . . 6 560 ∈ ℕ0
181 eqid 2737 . . . . . . . 8 560 = 560
182179nn0cni 12538 . . . . . . . . 9 56 ∈ ℂ
183182addlidi 11449 . . . . . . . 8 (0 + 56) = 56
1843, 14, 179, 3, 55, 181, 183, 54decadd 12787 . . . . . . 7 (1 + 560) = 561
185182addridi 11448 . . . . . . . 8 (56 + 0) = 56
186 5cn 12354 . . . . . . . . . . 11 5 ∈ ℂ
187186addridi 11448 . . . . . . . . . 10 (5 + 0) = 5
188187, 178eqeltri 2837 . . . . . . . . 9 (5 + 0) ∈ ℕ0
18953mulridi 11265 . . . . . . . . 9 (1 · 1) = 1
190169, 187oveq12i 7443 . . . . . . . . . 10 ((4 · 1) + (5 + 0)) = (4 + 5)
191 5p4e9 12424 . . . . . . . . . . 11 (5 + 4) = 9
192186, 59, 191addcomli 11453 . . . . . . . . . 10 (4 + 5) = 9
193190, 192eqtri 2765 . . . . . . . . 9 ((4 · 1) + (5 + 0)) = 9
19414, 2, 188, 44, 14, 189, 193decrmanc 12790 . . . . . . . 8 ((14 · 1) + (5 + 0)) = 19
19585oveq1i 7441 . . . . . . . . 9 ((0 · 1) + 6) = (0 + 6)
196195, 76, 773eqtri 2769 . . . . . . . 8 ((0 · 1) + 6) = 06
19715, 3, 178, 40, 43, 185, 14, 40, 3, 194, 196decmac 12785 . . . . . . 7 ((140 · 1) + (56 + 0)) = 196
198189oveq1i 7441 . . . . . . . 8 ((1 · 1) + 1) = (1 + 1)
19918dec0h 12755 . . . . . . . 8 2 = 02
200198, 112, 1993eqtri 2769 . . . . . . 7 ((1 · 1) + 1) = 02
20116, 14, 179, 14, 39, 184, 14, 18, 3, 197, 200decmac 12785 . . . . . 6 ((1401 · 1) + (1 + 560)) = 1962
20259mullidi 11266 . . . . . . . . . . . 12 (1 · 4) = 4
203202oveq1i 7441 . . . . . . . . . . 11 ((1 · 4) + 1) = (4 + 1)
204 4p1e5 12412 . . . . . . . . . . 11 (4 + 1) = 5
205203, 204eqtri 2765 . . . . . . . . . 10 ((1 · 4) + 1) = 5
2062, 14, 2, 44, 40, 14, 205, 149decmul1c 12798 . . . . . . . . 9 (14 · 4) = 56
20775addridi 11448 . . . . . . . . 9 (6 + 0) = 6
208178, 40, 3, 206, 207decaddi 12793 . . . . . . . 8 ((14 · 4) + 0) = 56
209 0cn 11253 . . . . . . . . 9 0 ∈ ℂ
21059mul01i 11451 . . . . . . . . . 10 (4 · 0) = 0
211210, 81eqtri 2765 . . . . . . . . 9 (4 · 0) = 00
21259, 209, 211mulcomli 11270 . . . . . . . 8 (0 · 4) = 00
2132, 15, 3, 43, 3, 3, 208, 212decmul1c 12798 . . . . . . 7 (140 · 4) = 560
214202oveq1i 7441 . . . . . . . 8 ((1 · 4) + 4) = (4 + 4)
215 4p4e8 12421 . . . . . . . 8 (4 + 4) = 8
216214, 215eqtri 2765 . . . . . . 7 ((1 · 4) + 4) = 8
21716, 14, 2, 39, 2, 213, 216decrmanc 12790 . . . . . 6 ((1401 · 4) + 4) = 5608
21814, 2, 14, 2, 44, 177, 17, 94, 180, 201, 217decma2c 12786 . . . . 5 ((1401 · 14) + (14 + 0)) = 19628
21917nn0cni 12538 . . . . . . . 8 1401 ∈ ℂ
220219mul01i 11451 . . . . . . 7 (1401 · 0) = 0
221220oveq1i 7441 . . . . . 6 ((1401 · 0) + 0) = (0 + 0)
222221, 47, 813eqtri 2769 . . . . 5 ((1401 · 0) + 0) = 00
22315, 3, 15, 3, 43, 43, 17, 3, 3, 218, 222decma2c 12786 . . . 4 ((1401 · 140) + 140) = 196280
224219mulridi 11265 . . . 4 (1401 · 1) = 1401
22517, 16, 14, 39, 14, 16, 223, 224decmul2c 12799 . . 3 (1401 · 1401) = 1962801
226175, 225eqtr4i 2768 . 2 ((490 · 𝑁) + 2311) = (1401 · 1401)
2278, 9, 5, 13, 17, 22, 125, 129, 226mod2xi 17107 1 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  (class class class)co 7431  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  cn 12266  2c2 12321  3c3 12322  4c4 12323  5c5 12324  6c6 12325  7c7 12326  8c8 12327  9c9 12328  0cn0 12526  cdc 12733   mod cmo 13909  cexp 14102
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-sup 9482  df-inf 9483  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-rp 13035  df-fl 13832  df-mod 13910  df-seq 14043  df-exp 14103
This theorem is referenced by:  4001lem3  17180  4001lem4  17181
  Copyright terms: Public domain W3C validator