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

Theorem 4001lem2 17084
Description: Lemma for 4001prm 17087. 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 12495 . . . . . 6 4 ∈ ℕ0
3 0nn0 12491 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12696 . . . . 5 40 ∈ ℕ0
54, 3deccl 12696 . . . 4 400 ∈ ℕ0
6 1nn 12227 . . . 4 1 ∈ ℕ
75, 6decnncl 12701 . . 3 4001 ∈ ℕ
81, 7eqeltri 2823 . 2 𝑁 ∈ ℕ
9 2nn 12289 . 2 2 ∈ ℕ
10 9nn0 12500 . . . . 5 9 ∈ ℕ0
112, 10deccl 12696 . . . 4 49 ∈ ℕ0
1211, 3deccl 12696 . . 3 490 ∈ ℕ0
1312nn0zi 12591 . 2 490 ∈ ℤ
14 1nn0 12492 . . . . 5 1 ∈ ℕ0
1514, 2deccl 12696 . . . 4 14 ∈ ℕ0
1615, 3deccl 12696 . . 3 140 ∈ ℕ0
1716, 14deccl 12696 . 2 1401 ∈ ℕ0
18 2nn0 12493 . . . . 5 2 ∈ ℕ0
19 3nn0 12494 . . . . 5 3 ∈ ℕ0
2018, 19deccl 12696 . . . 4 23 ∈ ℕ0
2120, 14deccl 12696 . . 3 231 ∈ ℕ0
2221, 14deccl 12696 . 2 2311 ∈ ℕ0
2318, 3deccl 12696 . . . 4 20 ∈ ℕ0
2423, 3deccl 12696 . . 3 200 ∈ ℕ0
2523, 19deccl 12696 . . . 4 203 ∈ ℕ0
2625nn0zi 12591 . . 3 203 ∈ ℤ
2710, 3deccl 12696 . . . 4 90 ∈ ℕ0
2827, 18deccl 12696 . . 3 902 ∈ ℕ0
2914001lem1 17083 . . 3 ((2↑200) mod 𝑁) = (902 mod 𝑁)
3024nn0cni 12488 . . . 4 200 ∈ ℂ
31 2cn 12291 . . . 4 2 ∈ ℂ
32 eqid 2726 . . . . 5 200 = 200
33 eqid 2726 . . . . . 6 20 = 20
34 2t2e4 12380 . . . . . 6 (2 · 2) = 4
3531mul02i 11407 . . . . . 6 (0 · 2) = 0
3618, 18, 3, 33, 34, 35decmul1 12745 . . . . 5 (20 · 2) = 40
3718, 23, 3, 32, 36, 35decmul1 12745 . . . 4 (200 · 2) = 400
3830, 31, 37mulcomli 11227 . . 3 (2 · 200) = 400
39 eqid 2726 . . . . 5 1401 = 1401
40 6nn0 12497 . . . . . . 7 6 ∈ ℕ0
4114, 40deccl 12696 . . . . . 6 16 ∈ ℕ0
42 eqid 2726 . . . . . 6 400 = 400
43 eqid 2726 . . . . . . 7 140 = 140
44 eqid 2726 . . . . . . . 8 14 = 14
45 4p2e6 12369 . . . . . . . 8 (4 + 2) = 6
4614, 2, 18, 44, 45decaddi 12741 . . . . . . 7 (14 + 2) = 16
47 00id 11393 . . . . . . 7 (0 + 0) = 0
4815, 3, 18, 3, 43, 33, 46, 47decadd 12735 . . . . . 6 (140 + 20) = 160
49 eqid 2726 . . . . . . 7 40 = 40
5041nn0cni 12488 . . . . . . . 8 16 ∈ ℂ
5150addridi 11405 . . . . . . 7 (16 + 0) = 16
52 eqid 2726 . . . . . . . 8 203 = 203
53 ax-1cn 11170 . . . . . . . . . 10 1 ∈ ℂ
5453addridi 11405 . . . . . . . . 9 (1 + 0) = 1
5514dec0h 12703 . . . . . . . . 9 1 = 01
5654, 55eqtri 2754 . . . . . . . 8 (1 + 0) = 01
5753addlidi 11406 . . . . . . . . . 10 (0 + 1) = 1
5857, 14eqeltri 2823 . . . . . . . . 9 (0 + 1) ∈ ℕ0
59 4cn 12301 . . . . . . . . . 10 4 ∈ ℂ
60 4t2e8 12384 . . . . . . . . . 10 (4 · 2) = 8
6159, 31, 60mulcomli 11227 . . . . . . . . 9 (2 · 4) = 8
6259mul02i 11407 . . . . . . . . . . 11 (0 · 4) = 0
6362, 57oveq12i 7417 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = (0 + 1)
6463, 57eqtri 2754 . . . . . . . . 9 ((0 · 4) + (0 + 1)) = 1
6518, 3, 58, 33, 2, 61, 64decrmanc 12738 . . . . . . . 8 ((20 · 4) + (0 + 1)) = 81
66 2p1e3 12358 . . . . . . . . 9 (2 + 1) = 3
67 3cn 12297 . . . . . . . . . 10 3 ∈ ℂ
68 4t3e12 12779 . . . . . . . . . 10 (4 · 3) = 12
6959, 67, 68mulcomli 11227 . . . . . . . . 9 (3 · 4) = 12
7014, 18, 66, 69decsuc 12712 . . . . . . . 8 ((3 · 4) + 1) = 13
7123, 19, 3, 14, 52, 56, 2, 19, 14, 65, 70decmac 12733 . . . . . . 7 ((203 · 4) + (1 + 0)) = 813
7225nn0cni 12488 . . . . . . . . . 10 203 ∈ ℂ
7372mul01i 11408 . . . . . . . . 9 (203 · 0) = 0
7473oveq1i 7415 . . . . . . . 8 ((203 · 0) + 6) = (0 + 6)
75 6cn 12307 . . . . . . . . 9 6 ∈ ℂ
7675addlidi 11406 . . . . . . . 8 (0 + 6) = 6
7740dec0h 12703 . . . . . . . 8 6 = 06
7874, 76, 773eqtri 2758 . . . . . . 7 ((203 · 0) + 6) = 06
792, 3, 14, 40, 49, 51, 25, 40, 3, 71, 78decma2c 12734 . . . . . 6 ((203 · 40) + (16 + 0)) = 8136
8073oveq1i 7415 . . . . . . 7 ((203 · 0) + 0) = (0 + 0)
813dec0h 12703 . . . . . . 7 0 = 00
8280, 47, 813eqtri 2758 . . . . . 6 ((203 · 0) + 0) = 00
834, 3, 41, 3, 42, 48, 25, 3, 3, 79, 82decma2c 12734 . . . . 5 ((203 · 400) + (140 + 20)) = 81360
8431mulridi 11222 . . . . . . 7 (2 · 1) = 2
8553mul02i 11407 . . . . . . 7 (0 · 1) = 0
8614, 18, 3, 33, 84, 85decmul1 12745 . . . . . 6 (20 · 1) = 20
8767mulridi 11222 . . . . . . . 8 (3 · 1) = 3
8887oveq1i 7415 . . . . . . 7 ((3 · 1) + 1) = (3 + 1)
89 3p1e4 12361 . . . . . . 7 (3 + 1) = 4
9088, 89eqtri 2754 . . . . . 6 ((3 · 1) + 1) = 4
9123, 19, 14, 52, 14, 86, 90decrmanc 12738 . . . . 5 ((203 · 1) + 1) = 204
925, 14, 16, 14, 1, 39, 25, 2, 23, 83, 91decma2c 12734 . . . 4 ((203 · 𝑁) + 1401) = 813604
93 eqid 2726 . . . . 5 902 = 902
94 8nn0 12499 . . . . . . 7 8 ∈ ℕ0
9514, 94deccl 12696 . . . . . 6 18 ∈ ℕ0
9695, 3deccl 12696 . . . . 5 180 ∈ ℕ0
97 eqid 2726 . . . . . 6 90 = 90
98 eqid 2726 . . . . . 6 180 = 180
9995nn0cni 12488 . . . . . . . 8 18 ∈ ℂ
10099addridi 11405 . . . . . . 7 (18 + 0) = 18
101 1p2e3 12359 . . . . . . . . 9 (1 + 2) = 3
102101, 19eqeltri 2823 . . . . . . . 8 (1 + 2) ∈ ℕ0
103 9t9e81 12810 . . . . . . . 8 (9 · 9) = 81
104 9cn 12316 . . . . . . . . . . 11 9 ∈ ℂ
105104mul02i 11407 . . . . . . . . . 10 (0 · 9) = 0
106105, 101oveq12i 7417 . . . . . . . . 9 ((0 · 9) + (1 + 2)) = (0 + 3)
10767addlidi 11406 . . . . . . . . 9 (0 + 3) = 3
108106, 107eqtri 2754 . . . . . . . 8 ((0 · 9) + (1 + 2)) = 3
10910, 3, 102, 97, 10, 103, 108decrmanc 12738 . . . . . . 7 ((90 · 9) + (1 + 2)) = 813
110 9t2e18 12803 . . . . . . . . 9 (9 · 2) = 18
111104, 31, 110mulcomli 11227 . . . . . . . 8 (2 · 9) = 18
112 1p1e2 12341 . . . . . . . 8 (1 + 1) = 2
113 8p8e16 12767 . . . . . . . 8 (8 + 8) = 16
11414, 94, 94, 111, 112, 40, 113decaddci 12742 . . . . . . 7 ((2 · 9) + 8) = 26
11527, 18, 14, 94, 93, 100, 10, 40, 18, 109, 114decmac 12733 . . . . . 6 ((902 · 9) + (18 + 0)) = 8136
11628nn0cni 12488 . . . . . . . . 9 902 ∈ ℂ
117116mul01i 11408 . . . . . . . 8 (902 · 0) = 0
118117oveq1i 7415 . . . . . . 7 ((902 · 0) + 0) = (0 + 0)
119118, 47, 813eqtri 2758 . . . . . 6 ((902 · 0) + 0) = 00
12010, 3, 95, 3, 97, 98, 28, 3, 3, 115, 119decma2c 12734 . . . . 5 ((902 · 90) + 180) = 81360
12118, 10, 3, 97, 110, 35decmul1 12745 . . . . . 6 (90 · 2) = 180
12218, 27, 18, 93, 121, 34decmul1 12745 . . . . 5 (902 · 2) = 1804
12328, 27, 18, 93, 2, 96, 120, 122decmul2c 12747 . . . 4 (902 · 902) = 813604
12492, 123eqtr4i 2757 . . 3 ((203 · 𝑁) + 1401) = (902 · 902)
1258, 9, 24, 26, 28, 17, 29, 38, 124mod2xi 17011 . 2 ((2↑400) mod 𝑁) = (1401 mod 𝑁)
1265nn0cni 12488 . . 3 400 ∈ ℂ
12718, 2, 3, 49, 60, 35decmul1 12745 . . . 4 (40 · 2) = 80
12818, 4, 3, 42, 127, 35decmul1 12745 . . 3 (400 · 2) = 800
129126, 31, 128mulcomli 11227 . 2 (2 · 400) = 800
130 eqid 2726 . . . 4 2311 = 2311
13118, 94deccl 12696 . . . . 5 28 ∈ ℕ0
132 eqid 2726 . . . . . 6 231 = 231
133 eqid 2726 . . . . . 6 49 = 49
134 7nn0 12498 . . . . . . 7 7 ∈ ℕ0
135 7p1e8 12365 . . . . . . 7 (7 + 1) = 8
136 eqid 2726 . . . . . . . 8 23 = 23
137 4p3e7 12370 . . . . . . . . 9 (4 + 3) = 7
13859, 67, 137addcomli 11410 . . . . . . . 8 (3 + 4) = 7
13918, 19, 2, 136, 138decaddi 12741 . . . . . . 7 (23 + 4) = 27
14018, 134, 135, 139decsuc 12712 . . . . . 6 ((23 + 4) + 1) = 28
141 9p1e10 12683 . . . . . . 7 (9 + 1) = 10
142104, 53, 141addcomli 11410 . . . . . 6 (1 + 9) = 10
14320, 14, 2, 10, 132, 133, 140, 142decaddc2 12737 . . . . 5 (231 + 49) = 280
144131nn0cni 12488 . . . . . . 7 28 ∈ ℂ
145144addridi 11405 . . . . . 6 (28 + 0) = 28
14631addridi 11405 . . . . . . . 8 (2 + 0) = 2
147146, 18eqeltri 2823 . . . . . . 7 (2 + 0) ∈ ℕ0
148 eqid 2726 . . . . . . 7 490 = 490
149 4t4e16 12780 . . . . . . . . 9 (4 · 4) = 16
150 6p3e9 12376 . . . . . . . . 9 (6 + 3) = 9
15114, 40, 19, 149, 150decaddi 12741 . . . . . . . 8 ((4 · 4) + 3) = 19
152 9t4e36 12805 . . . . . . . 8 (9 · 4) = 36
1532, 2, 10, 133, 40, 19, 151, 152decmul1c 12746 . . . . . . 7 (49 · 4) = 196
15462, 146oveq12i 7417 . . . . . . . 8 ((0 · 4) + (2 + 0)) = (0 + 2)
15531addlidi 11406 . . . . . . . 8 (0 + 2) = 2
156154, 155eqtri 2754 . . . . . . 7 ((0 · 4) + (2 + 0)) = 2
15711, 3, 147, 148, 2, 153, 156decrmanc 12738 . . . . . 6 ((490 · 4) + (2 + 0)) = 1962
15812nn0cni 12488 . . . . . . . . 9 490 ∈ ℂ
159158mul01i 11408 . . . . . . . 8 (490 · 0) = 0
160159oveq1i 7415 . . . . . . 7 ((490 · 0) + 8) = (0 + 8)
161 8cn 12313 . . . . . . . 8 8 ∈ ℂ
162161addlidi 11406 . . . . . . 7 (0 + 8) = 8
16394dec0h 12703 . . . . . . 7 8 = 08
164160, 162, 1633eqtri 2758 . . . . . 6 ((490 · 0) + 8) = 08
1652, 3, 18, 94, 49, 145, 12, 94, 3, 157, 164decma2c 12734 . . . . 5 ((490 · 40) + (28 + 0)) = 19628
166159oveq1i 7415 . . . . . 6 ((490 · 0) + 0) = (0 + 0)
167166, 47, 813eqtri 2758 . . . . 5 ((490 · 0) + 0) = 00
1684, 3, 131, 3, 42, 143, 12, 3, 3, 165, 167decma2c 12734 . . . 4 ((490 · 400) + (231 + 49)) = 196280
16959mulridi 11222 . . . . . 6 (4 · 1) = 4
170104mulridi 11222 . . . . . 6 (9 · 1) = 9
17114, 2, 10, 133, 169, 170decmul1 12745 . . . . 5 (49 · 1) = 49
17285oveq1i 7415 . . . . . 6 ((0 · 1) + 1) = (0 + 1)
173172, 57eqtri 2754 . . . . 5 ((0 · 1) + 1) = 1
17411, 3, 14, 148, 14, 171, 173decrmanc 12738 . . . 4 ((490 · 1) + 1) = 491
1755, 14, 21, 14, 1, 130, 12, 14, 11, 168, 174decma2c 12734 . . 3 ((490 · 𝑁) + 2311) = 1962801
17615nn0cni 12488 . . . . . . 7 14 ∈ ℂ
177176addridi 11405 . . . . . 6 (14 + 0) = 14
178 5nn0 12496 . . . . . . . 8 5 ∈ ℕ0
179178, 40deccl 12696 . . . . . . 7 56 ∈ ℕ0
180179, 3deccl 12696 . . . . . 6 560 ∈ ℕ0
181 eqid 2726 . . . . . . . 8 560 = 560
182179nn0cni 12488 . . . . . . . . 9 56 ∈ ℂ
183182addlidi 11406 . . . . . . . 8 (0 + 56) = 56
1843, 14, 179, 3, 55, 181, 183, 54decadd 12735 . . . . . . 7 (1 + 560) = 561
185182addridi 11405 . . . . . . . 8 (56 + 0) = 56
186 5cn 12304 . . . . . . . . . . 11 5 ∈ ℂ
187186addridi 11405 . . . . . . . . . 10 (5 + 0) = 5
188187, 178eqeltri 2823 . . . . . . . . 9 (5 + 0) ∈ ℕ0
18953mulridi 11222 . . . . . . . . 9 (1 · 1) = 1
190169, 187oveq12i 7417 . . . . . . . . . 10 ((4 · 1) + (5 + 0)) = (4 + 5)
191 5p4e9 12374 . . . . . . . . . . 11 (5 + 4) = 9
192186, 59, 191addcomli 11410 . . . . . . . . . 10 (4 + 5) = 9
193190, 192eqtri 2754 . . . . . . . . 9 ((4 · 1) + (5 + 0)) = 9
19414, 2, 188, 44, 14, 189, 193decrmanc 12738 . . . . . . . 8 ((14 · 1) + (5 + 0)) = 19
19585oveq1i 7415 . . . . . . . . 9 ((0 · 1) + 6) = (0 + 6)
196195, 76, 773eqtri 2758 . . . . . . . 8 ((0 · 1) + 6) = 06
19715, 3, 178, 40, 43, 185, 14, 40, 3, 194, 196decmac 12733 . . . . . . 7 ((140 · 1) + (56 + 0)) = 196
198189oveq1i 7415 . . . . . . . 8 ((1 · 1) + 1) = (1 + 1)
19918dec0h 12703 . . . . . . . 8 2 = 02
200198, 112, 1993eqtri 2758 . . . . . . 7 ((1 · 1) + 1) = 02
20116, 14, 179, 14, 39, 184, 14, 18, 3, 197, 200decmac 12733 . . . . . 6 ((1401 · 1) + (1 + 560)) = 1962
20259mullidi 11223 . . . . . . . . . . . 12 (1 · 4) = 4
203202oveq1i 7415 . . . . . . . . . . 11 ((1 · 4) + 1) = (4 + 1)
204 4p1e5 12362 . . . . . . . . . . 11 (4 + 1) = 5
205203, 204eqtri 2754 . . . . . . . . . 10 ((1 · 4) + 1) = 5
2062, 14, 2, 44, 40, 14, 205, 149decmul1c 12746 . . . . . . . . 9 (14 · 4) = 56
20775addridi 11405 . . . . . . . . 9 (6 + 0) = 6
208178, 40, 3, 206, 207decaddi 12741 . . . . . . . 8 ((14 · 4) + 0) = 56
209 0cn 11210 . . . . . . . . 9 0 ∈ ℂ
21059mul01i 11408 . . . . . . . . . 10 (4 · 0) = 0
211210, 81eqtri 2754 . . . . . . . . 9 (4 · 0) = 00
21259, 209, 211mulcomli 11227 . . . . . . . 8 (0 · 4) = 00
2132, 15, 3, 43, 3, 3, 208, 212decmul1c 12746 . . . . . . 7 (140 · 4) = 560
214202oveq1i 7415 . . . . . . . 8 ((1 · 4) + 4) = (4 + 4)
215 4p4e8 12371 . . . . . . . 8 (4 + 4) = 8
216214, 215eqtri 2754 . . . . . . 7 ((1 · 4) + 4) = 8
21716, 14, 2, 39, 2, 213, 216decrmanc 12738 . . . . . 6 ((1401 · 4) + 4) = 5608
21814, 2, 14, 2, 44, 177, 17, 94, 180, 201, 217decma2c 12734 . . . . 5 ((1401 · 14) + (14 + 0)) = 19628
21917nn0cni 12488 . . . . . . . 8 1401 ∈ ℂ
220219mul01i 11408 . . . . . . 7 (1401 · 0) = 0
221220oveq1i 7415 . . . . . 6 ((1401 · 0) + 0) = (0 + 0)
222221, 47, 813eqtri 2758 . . . . 5 ((1401 · 0) + 0) = 00
22315, 3, 15, 3, 43, 43, 17, 3, 3, 218, 222decma2c 12734 . . . 4 ((1401 · 140) + 140) = 196280
224219mulridi 11222 . . . 4 (1401 · 1) = 1401
22517, 16, 14, 39, 14, 16, 223, 224decmul2c 12747 . . 3 (1401 · 1401) = 1962801
226175, 225eqtr4i 2757 . 2 ((490 · 𝑁) + 2311) = (1401 · 1401)
2278, 9, 5, 13, 17, 22, 125, 129, 226mod2xi 17011 1 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1533  (class class class)co 7405  0cc0 11112  1c1 11113   + caddc 11115   · cmul 11117  cn 12216  2c2 12271  3c3 12272  4c4 12273  5c5 12274  6c6 12275  7c7 12276  8c8 12277  9c9 12278  0cn0 12476  cdc 12681   mod cmo 13840  cexp 14032
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 2163  ax-ext 2697  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7722  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4903  df-iun 4992  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6294  df-ord 6361  df-on 6362  df-lim 6363  df-suc 6364  df-iota 6489  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7853  df-2nd 7975  df-frecs 8267  df-wrecs 8298  df-recs 8372  df-rdg 8411  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-sup 9439  df-inf 9440  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-rp 12981  df-fl 13763  df-mod 13841  df-seq 13973  df-exp 14033
This theorem is referenced by:  4001lem3  17085  4001lem4  17086
  Copyright terms: Public domain W3C validator