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

Theorem 4001lem2 17082
Description: Lemma for 4001prm 17085. 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 12498 . . . . . 6 4 ∈ ℕ0
3 0nn0 12494 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12699 . . . . 5 40 ∈ ℕ0
54, 3deccl 12699 . . . 4 400 ∈ ℕ0
6 1nn 12230 . . . 4 1 ∈ ℕ
75, 6decnncl 12704 . . 3 4001 ∈ ℕ
81, 7eqeltri 2828 . 2 𝑁 ∈ ℕ
9 2nn 12292 . 2 2 ∈ ℕ
10 9nn0 12503 . . . . 5 9 ∈ ℕ0
112, 10deccl 12699 . . . 4 49 ∈ ℕ0
1211, 3deccl 12699 . . 3 490 ∈ ℕ0
1312nn0zi 12594 . 2 490 ∈ ℤ
14 1nn0 12495 . . . . 5 1 ∈ ℕ0
1514, 2deccl 12699 . . . 4 14 ∈ ℕ0
1615, 3deccl 12699 . . 3 140 ∈ ℕ0
1716, 14deccl 12699 . 2 1401 ∈ ℕ0
18 2nn0 12496 . . . . 5 2 ∈ ℕ0
19 3nn0 12497 . . . . 5 3 ∈ ℕ0
2018, 19deccl 12699 . . . 4 23 ∈ ℕ0
2120, 14deccl 12699 . . 3 231 ∈ ℕ0
2221, 14deccl 12699 . 2 2311 ∈ ℕ0
2318, 3deccl 12699 . . . 4 20 ∈ ℕ0
2423, 3deccl 12699 . . 3 200 ∈ ℕ0
2523, 19deccl 12699 . . . 4 203 ∈ ℕ0
2625nn0zi 12594 . . 3 203 ∈ ℤ
2710, 3deccl 12699 . . . 4 90 ∈ ℕ0
2827, 18deccl 12699 . . 3 902 ∈ ℕ0
2914001lem1 17081 . . 3 ((2↑200) mod 𝑁) = (902 mod 𝑁)
3024nn0cni 12491 . . . 4 200 ∈ ℂ
31 2cn 12294 . . . 4 2 ∈ ℂ
32 eqid 2731 . . . . 5 200 = 200
33 eqid 2731 . . . . . 6 20 = 20
34 2t2e4 12383 . . . . . 6 (2 · 2) = 4
3531mul02i 11410 . . . . . 6 (0 · 2) = 0
3618, 18, 3, 33, 34, 35decmul1 12748 . . . . 5 (20 · 2) = 40
3718, 23, 3, 32, 36, 35decmul1 12748 . . . 4 (200 · 2) = 400
3830, 31, 37mulcomli 11230 . . 3 (2 · 200) = 400
39 eqid 2731 . . . . 5 1401 = 1401
40 6nn0 12500 . . . . . . 7 6 ∈ ℕ0
4114, 40deccl 12699 . . . . . 6 16 ∈ ℕ0
42 eqid 2731 . . . . . 6 400 = 400
43 eqid 2731 . . . . . . 7 140 = 140
44 eqid 2731 . . . . . . . 8 14 = 14
45 4p2e6 12372 . . . . . . . 8 (4 + 2) = 6
4614, 2, 18, 44, 45decaddi 12744 . . . . . . 7 (14 + 2) = 16
47 00id 11396 . . . . . . 7 (0 + 0) = 0
4815, 3, 18, 3, 43, 33, 46, 47decadd 12738 . . . . . 6 (140 + 20) = 160
49 eqid 2731 . . . . . . 7 40 = 40
5041nn0cni 12491 . . . . . . . 8 16 ∈ ℂ
5150addridi 11408 . . . . . . 7 (16 + 0) = 16
52 eqid 2731 . . . . . . . 8 203 = 203
53 ax-1cn 11174 . . . . . . . . . 10 1 ∈ ℂ
5453addridi 11408 . . . . . . . . 9 (1 + 0) = 1
5514dec0h 12706 . . . . . . . . 9 1 = 01
5654, 55eqtri 2759 . . . . . . . 8 (1 + 0) = 01
5753addlidi 11409 . . . . . . . . . 10 (0 + 1) = 1
5857, 14eqeltri 2828 . . . . . . . . 9 (0 + 1) ∈ ℕ0
59 4cn 12304 . . . . . . . . . 10 4 ∈ ℂ
60 4t2e8 12387 . . . . . . . . . 10 (4 · 2) = 8
6159, 31, 60mulcomli 11230 . . . . . . . . 9 (2 · 4) = 8
6259mul02i 11410 . . . . . . . . . . 11 (0 · 4) = 0
6362, 57oveq12i 7424 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = (0 + 1)
6463, 57eqtri 2759 . . . . . . . . 9 ((0 · 4) + (0 + 1)) = 1
6518, 3, 58, 33, 2, 61, 64decrmanc 12741 . . . . . . . 8 ((20 · 4) + (0 + 1)) = 81
66 2p1e3 12361 . . . . . . . . 9 (2 + 1) = 3
67 3cn 12300 . . . . . . . . . 10 3 ∈ ℂ
68 4t3e12 12782 . . . . . . . . . 10 (4 · 3) = 12
6959, 67, 68mulcomli 11230 . . . . . . . . 9 (3 · 4) = 12
7014, 18, 66, 69decsuc 12715 . . . . . . . 8 ((3 · 4) + 1) = 13
7123, 19, 3, 14, 52, 56, 2, 19, 14, 65, 70decmac 12736 . . . . . . 7 ((203 · 4) + (1 + 0)) = 813
7225nn0cni 12491 . . . . . . . . . 10 203 ∈ ℂ
7372mul01i 11411 . . . . . . . . 9 (203 · 0) = 0
7473oveq1i 7422 . . . . . . . 8 ((203 · 0) + 6) = (0 + 6)
75 6cn 12310 . . . . . . . . 9 6 ∈ ℂ
7675addlidi 11409 . . . . . . . 8 (0 + 6) = 6
7740dec0h 12706 . . . . . . . 8 6 = 06
7874, 76, 773eqtri 2763 . . . . . . 7 ((203 · 0) + 6) = 06
792, 3, 14, 40, 49, 51, 25, 40, 3, 71, 78decma2c 12737 . . . . . 6 ((203 · 40) + (16 + 0)) = 8136
8073oveq1i 7422 . . . . . . 7 ((203 · 0) + 0) = (0 + 0)
813dec0h 12706 . . . . . . 7 0 = 00
8280, 47, 813eqtri 2763 . . . . . 6 ((203 · 0) + 0) = 00
834, 3, 41, 3, 42, 48, 25, 3, 3, 79, 82decma2c 12737 . . . . 5 ((203 · 400) + (140 + 20)) = 81360
8431mulridi 11225 . . . . . . 7 (2 · 1) = 2
8553mul02i 11410 . . . . . . 7 (0 · 1) = 0
8614, 18, 3, 33, 84, 85decmul1 12748 . . . . . 6 (20 · 1) = 20
8767mulridi 11225 . . . . . . . 8 (3 · 1) = 3
8887oveq1i 7422 . . . . . . 7 ((3 · 1) + 1) = (3 + 1)
89 3p1e4 12364 . . . . . . 7 (3 + 1) = 4
9088, 89eqtri 2759 . . . . . 6 ((3 · 1) + 1) = 4
9123, 19, 14, 52, 14, 86, 90decrmanc 12741 . . . . 5 ((203 · 1) + 1) = 204
925, 14, 16, 14, 1, 39, 25, 2, 23, 83, 91decma2c 12737 . . . 4 ((203 · 𝑁) + 1401) = 813604
93 eqid 2731 . . . . 5 902 = 902
94 8nn0 12502 . . . . . . 7 8 ∈ ℕ0
9514, 94deccl 12699 . . . . . 6 18 ∈ ℕ0
9695, 3deccl 12699 . . . . 5 180 ∈ ℕ0
97 eqid 2731 . . . . . 6 90 = 90
98 eqid 2731 . . . . . 6 180 = 180
9995nn0cni 12491 . . . . . . . 8 18 ∈ ℂ
10099addridi 11408 . . . . . . 7 (18 + 0) = 18
101 1p2e3 12362 . . . . . . . . 9 (1 + 2) = 3
102101, 19eqeltri 2828 . . . . . . . 8 (1 + 2) ∈ ℕ0
103 9t9e81 12813 . . . . . . . 8 (9 · 9) = 81
104 9cn 12319 . . . . . . . . . . 11 9 ∈ ℂ
105104mul02i 11410 . . . . . . . . . 10 (0 · 9) = 0
106105, 101oveq12i 7424 . . . . . . . . 9 ((0 · 9) + (1 + 2)) = (0 + 3)
10767addlidi 11409 . . . . . . . . 9 (0 + 3) = 3
108106, 107eqtri 2759 . . . . . . . 8 ((0 · 9) + (1 + 2)) = 3
10910, 3, 102, 97, 10, 103, 108decrmanc 12741 . . . . . . 7 ((90 · 9) + (1 + 2)) = 813
110 9t2e18 12806 . . . . . . . . 9 (9 · 2) = 18
111104, 31, 110mulcomli 11230 . . . . . . . 8 (2 · 9) = 18
112 1p1e2 12344 . . . . . . . 8 (1 + 1) = 2
113 8p8e16 12770 . . . . . . . 8 (8 + 8) = 16
11414, 94, 94, 111, 112, 40, 113decaddci 12745 . . . . . . 7 ((2 · 9) + 8) = 26
11527, 18, 14, 94, 93, 100, 10, 40, 18, 109, 114decmac 12736 . . . . . 6 ((902 · 9) + (18 + 0)) = 8136
11628nn0cni 12491 . . . . . . . . 9 902 ∈ ℂ
117116mul01i 11411 . . . . . . . 8 (902 · 0) = 0
118117oveq1i 7422 . . . . . . 7 ((902 · 0) + 0) = (0 + 0)
119118, 47, 813eqtri 2763 . . . . . 6 ((902 · 0) + 0) = 00
12010, 3, 95, 3, 97, 98, 28, 3, 3, 115, 119decma2c 12737 . . . . 5 ((902 · 90) + 180) = 81360
12118, 10, 3, 97, 110, 35decmul1 12748 . . . . . 6 (90 · 2) = 180
12218, 27, 18, 93, 121, 34decmul1 12748 . . . . 5 (902 · 2) = 1804
12328, 27, 18, 93, 2, 96, 120, 122decmul2c 12750 . . . 4 (902 · 902) = 813604
12492, 123eqtr4i 2762 . . 3 ((203 · 𝑁) + 1401) = (902 · 902)
1258, 9, 24, 26, 28, 17, 29, 38, 124mod2xi 17009 . 2 ((2↑400) mod 𝑁) = (1401 mod 𝑁)
1265nn0cni 12491 . . 3 400 ∈ ℂ
12718, 2, 3, 49, 60, 35decmul1 12748 . . . 4 (40 · 2) = 80
12818, 4, 3, 42, 127, 35decmul1 12748 . . 3 (400 · 2) = 800
129126, 31, 128mulcomli 11230 . 2 (2 · 400) = 800
130 eqid 2731 . . . 4 2311 = 2311
13118, 94deccl 12699 . . . . 5 28 ∈ ℕ0
132 eqid 2731 . . . . . 6 231 = 231
133 eqid 2731 . . . . . 6 49 = 49
134 7nn0 12501 . . . . . . 7 7 ∈ ℕ0
135 7p1e8 12368 . . . . . . 7 (7 + 1) = 8
136 eqid 2731 . . . . . . . 8 23 = 23
137 4p3e7 12373 . . . . . . . . 9 (4 + 3) = 7
13859, 67, 137addcomli 11413 . . . . . . . 8 (3 + 4) = 7
13918, 19, 2, 136, 138decaddi 12744 . . . . . . 7 (23 + 4) = 27
14018, 134, 135, 139decsuc 12715 . . . . . 6 ((23 + 4) + 1) = 28
141 9p1e10 12686 . . . . . . 7 (9 + 1) = 10
142104, 53, 141addcomli 11413 . . . . . 6 (1 + 9) = 10
14320, 14, 2, 10, 132, 133, 140, 142decaddc2 12740 . . . . 5 (231 + 49) = 280
144131nn0cni 12491 . . . . . . 7 28 ∈ ℂ
145144addridi 11408 . . . . . 6 (28 + 0) = 28
14631addridi 11408 . . . . . . . 8 (2 + 0) = 2
147146, 18eqeltri 2828 . . . . . . 7 (2 + 0) ∈ ℕ0
148 eqid 2731 . . . . . . 7 490 = 490
149 4t4e16 12783 . . . . . . . . 9 (4 · 4) = 16
150 6p3e9 12379 . . . . . . . . 9 (6 + 3) = 9
15114, 40, 19, 149, 150decaddi 12744 . . . . . . . 8 ((4 · 4) + 3) = 19
152 9t4e36 12808 . . . . . . . 8 (9 · 4) = 36
1532, 2, 10, 133, 40, 19, 151, 152decmul1c 12749 . . . . . . 7 (49 · 4) = 196
15462, 146oveq12i 7424 . . . . . . . 8 ((0 · 4) + (2 + 0)) = (0 + 2)
15531addlidi 11409 . . . . . . . 8 (0 + 2) = 2
156154, 155eqtri 2759 . . . . . . 7 ((0 · 4) + (2 + 0)) = 2
15711, 3, 147, 148, 2, 153, 156decrmanc 12741 . . . . . 6 ((490 · 4) + (2 + 0)) = 1962
15812nn0cni 12491 . . . . . . . . 9 490 ∈ ℂ
159158mul01i 11411 . . . . . . . 8 (490 · 0) = 0
160159oveq1i 7422 . . . . . . 7 ((490 · 0) + 8) = (0 + 8)
161 8cn 12316 . . . . . . . 8 8 ∈ ℂ
162161addlidi 11409 . . . . . . 7 (0 + 8) = 8
16394dec0h 12706 . . . . . . 7 8 = 08
164160, 162, 1633eqtri 2763 . . . . . 6 ((490 · 0) + 8) = 08
1652, 3, 18, 94, 49, 145, 12, 94, 3, 157, 164decma2c 12737 . . . . 5 ((490 · 40) + (28 + 0)) = 19628
166159oveq1i 7422 . . . . . 6 ((490 · 0) + 0) = (0 + 0)
167166, 47, 813eqtri 2763 . . . . 5 ((490 · 0) + 0) = 00
1684, 3, 131, 3, 42, 143, 12, 3, 3, 165, 167decma2c 12737 . . . 4 ((490 · 400) + (231 + 49)) = 196280
16959mulridi 11225 . . . . . 6 (4 · 1) = 4
170104mulridi 11225 . . . . . 6 (9 · 1) = 9
17114, 2, 10, 133, 169, 170decmul1 12748 . . . . 5 (49 · 1) = 49
17285oveq1i 7422 . . . . . 6 ((0 · 1) + 1) = (0 + 1)
173172, 57eqtri 2759 . . . . 5 ((0 · 1) + 1) = 1
17411, 3, 14, 148, 14, 171, 173decrmanc 12741 . . . 4 ((490 · 1) + 1) = 491
1755, 14, 21, 14, 1, 130, 12, 14, 11, 168, 174decma2c 12737 . . 3 ((490 · 𝑁) + 2311) = 1962801
17615nn0cni 12491 . . . . . . 7 14 ∈ ℂ
177176addridi 11408 . . . . . 6 (14 + 0) = 14
178 5nn0 12499 . . . . . . . 8 5 ∈ ℕ0
179178, 40deccl 12699 . . . . . . 7 56 ∈ ℕ0
180179, 3deccl 12699 . . . . . 6 560 ∈ ℕ0
181 eqid 2731 . . . . . . . 8 560 = 560
182179nn0cni 12491 . . . . . . . . 9 56 ∈ ℂ
183182addlidi 11409 . . . . . . . 8 (0 + 56) = 56
1843, 14, 179, 3, 55, 181, 183, 54decadd 12738 . . . . . . 7 (1 + 560) = 561
185182addridi 11408 . . . . . . . 8 (56 + 0) = 56
186 5cn 12307 . . . . . . . . . . 11 5 ∈ ℂ
187186addridi 11408 . . . . . . . . . 10 (5 + 0) = 5
188187, 178eqeltri 2828 . . . . . . . . 9 (5 + 0) ∈ ℕ0
18953mulridi 11225 . . . . . . . . 9 (1 · 1) = 1
190169, 187oveq12i 7424 . . . . . . . . . 10 ((4 · 1) + (5 + 0)) = (4 + 5)
191 5p4e9 12377 . . . . . . . . . . 11 (5 + 4) = 9
192186, 59, 191addcomli 11413 . . . . . . . . . 10 (4 + 5) = 9
193190, 192eqtri 2759 . . . . . . . . 9 ((4 · 1) + (5 + 0)) = 9
19414, 2, 188, 44, 14, 189, 193decrmanc 12741 . . . . . . . 8 ((14 · 1) + (5 + 0)) = 19
19585oveq1i 7422 . . . . . . . . 9 ((0 · 1) + 6) = (0 + 6)
196195, 76, 773eqtri 2763 . . . . . . . 8 ((0 · 1) + 6) = 06
19715, 3, 178, 40, 43, 185, 14, 40, 3, 194, 196decmac 12736 . . . . . . 7 ((140 · 1) + (56 + 0)) = 196
198189oveq1i 7422 . . . . . . . 8 ((1 · 1) + 1) = (1 + 1)
19918dec0h 12706 . . . . . . . 8 2 = 02
200198, 112, 1993eqtri 2763 . . . . . . 7 ((1 · 1) + 1) = 02
20116, 14, 179, 14, 39, 184, 14, 18, 3, 197, 200decmac 12736 . . . . . 6 ((1401 · 1) + (1 + 560)) = 1962
20259mullidi 11226 . . . . . . . . . . . 12 (1 · 4) = 4
203202oveq1i 7422 . . . . . . . . . . 11 ((1 · 4) + 1) = (4 + 1)
204 4p1e5 12365 . . . . . . . . . . 11 (4 + 1) = 5
205203, 204eqtri 2759 . . . . . . . . . 10 ((1 · 4) + 1) = 5
2062, 14, 2, 44, 40, 14, 205, 149decmul1c 12749 . . . . . . . . 9 (14 · 4) = 56
20775addridi 11408 . . . . . . . . 9 (6 + 0) = 6
208178, 40, 3, 206, 207decaddi 12744 . . . . . . . 8 ((14 · 4) + 0) = 56
209 0cn 11213 . . . . . . . . 9 0 ∈ ℂ
21059mul01i 11411 . . . . . . . . . 10 (4 · 0) = 0
211210, 81eqtri 2759 . . . . . . . . 9 (4 · 0) = 00
21259, 209, 211mulcomli 11230 . . . . . . . 8 (0 · 4) = 00
2132, 15, 3, 43, 3, 3, 208, 212decmul1c 12749 . . . . . . 7 (140 · 4) = 560
214202oveq1i 7422 . . . . . . . 8 ((1 · 4) + 4) = (4 + 4)
215 4p4e8 12374 . . . . . . . 8 (4 + 4) = 8
216214, 215eqtri 2759 . . . . . . 7 ((1 · 4) + 4) = 8
21716, 14, 2, 39, 2, 213, 216decrmanc 12741 . . . . . 6 ((1401 · 4) + 4) = 5608
21814, 2, 14, 2, 44, 177, 17, 94, 180, 201, 217decma2c 12737 . . . . 5 ((1401 · 14) + (14 + 0)) = 19628
21917nn0cni 12491 . . . . . . . 8 1401 ∈ ℂ
220219mul01i 11411 . . . . . . 7 (1401 · 0) = 0
221220oveq1i 7422 . . . . . 6 ((1401 · 0) + 0) = (0 + 0)
222221, 47, 813eqtri 2763 . . . . 5 ((1401 · 0) + 0) = 00
22315, 3, 15, 3, 43, 43, 17, 3, 3, 218, 222decma2c 12737 . . . 4 ((1401 · 140) + 140) = 196280
224219mulridi 11225 . . . 4 (1401 · 1) = 1401
22517, 16, 14, 39, 14, 16, 223, 224decmul2c 12750 . . 3 (1401 · 1401) = 1962801
226175, 225eqtr4i 2762 . 2 ((490 · 𝑁) + 2311) = (1401 · 1401)
2278, 9, 5, 13, 17, 22, 125, 129, 226mod2xi 17009 1 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  (class class class)co 7412  0cc0 11116  1c1 11117   + caddc 11119   · cmul 11121  cn 12219  2c2 12274  3c3 12275  4c4 12276  5c5 12277  6c6 12278  7c7 12279  8c8 12280  9c9 12281  0cn0 12479  cdc 12684   mod cmo 13841  cexp 14034
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729  ax-cnex 11172  ax-resscn 11173  ax-1cn 11174  ax-icn 11175  ax-addcl 11176  ax-addrcl 11177  ax-mulcl 11178  ax-mulrcl 11179  ax-mulcom 11180  ax-addass 11181  ax-mulass 11182  ax-distr 11183  ax-i2m1 11184  ax-1ne0 11185  ax-1rid 11186  ax-rnegex 11187  ax-rrecex 11188  ax-cnre 11189  ax-pre-lttri 11190  ax-pre-lttrn 11191  ax-pre-ltadd 11192  ax-pre-mulgt0 11193  ax-pre-sup 11194
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7860  df-2nd 7980  df-frecs 8272  df-wrecs 8303  df-recs 8377  df-rdg 8416  df-er 8709  df-en 8946  df-dom 8947  df-sdom 8948  df-sup 9443  df-inf 9444  df-pnf 11257  df-mnf 11258  df-xr 11259  df-ltxr 11260  df-le 11261  df-sub 11453  df-neg 11454  df-div 11879  df-nn 12220  df-2 12282  df-3 12283  df-4 12284  df-5 12285  df-6 12286  df-7 12287  df-8 12288  df-9 12289  df-n0 12480  df-z 12566  df-dec 12685  df-uz 12830  df-rp 12982  df-fl 13764  df-mod 13842  df-seq 13974  df-exp 14035
This theorem is referenced by:  4001lem3  17083  4001lem4  17084
  Copyright terms: Public domain W3C validator