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

Theorem 4001lem2 16465
Description: Lemma for 4001prm 16468. 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 11905 . . . . . 6 4 ∈ ℕ0
3 0nn0 11901 . . . . . 6 0 ∈ ℕ0
42, 3deccl 12102 . . . . 5 40 ∈ ℕ0
54, 3deccl 12102 . . . 4 400 ∈ ℕ0
6 1nn 11638 . . . 4 1 ∈ ℕ
75, 6decnncl 12107 . . 3 4001 ∈ ℕ
81, 7eqeltri 2914 . 2 𝑁 ∈ ℕ
9 2nn 11699 . 2 2 ∈ ℕ
10 9nn0 11910 . . . . 5 9 ∈ ℕ0
112, 10deccl 12102 . . . 4 49 ∈ ℕ0
1211, 3deccl 12102 . . 3 490 ∈ ℕ0
1312nn0zi 11996 . 2 490 ∈ ℤ
14 1nn0 11902 . . . . 5 1 ∈ ℕ0
1514, 2deccl 12102 . . . 4 14 ∈ ℕ0
1615, 3deccl 12102 . . 3 140 ∈ ℕ0
1716, 14deccl 12102 . 2 1401 ∈ ℕ0
18 2nn0 11903 . . . . 5 2 ∈ ℕ0
19 3nn0 11904 . . . . 5 3 ∈ ℕ0
2018, 19deccl 12102 . . . 4 23 ∈ ℕ0
2120, 14deccl 12102 . . 3 231 ∈ ℕ0
2221, 14deccl 12102 . 2 2311 ∈ ℕ0
2318, 3deccl 12102 . . . 4 20 ∈ ℕ0
2423, 3deccl 12102 . . 3 200 ∈ ℕ0
2523, 19deccl 12102 . . . 4 203 ∈ ℕ0
2625nn0zi 11996 . . 3 203 ∈ ℤ
2710, 3deccl 12102 . . . 4 90 ∈ ℕ0
2827, 18deccl 12102 . . 3 902 ∈ ℕ0
2914001lem1 16464 . . 3 ((2↑200) mod 𝑁) = (902 mod 𝑁)
3024nn0cni 11898 . . . 4 200 ∈ ℂ
31 2cn 11701 . . . 4 2 ∈ ℂ
32 eqid 2826 . . . . 5 200 = 200
33 eqid 2826 . . . . . 6 20 = 20
34 2t2e4 11790 . . . . . 6 (2 · 2) = 4
3531mul02i 10818 . . . . . 6 (0 · 2) = 0
3618, 18, 3, 33, 34, 35decmul1 12151 . . . . 5 (20 · 2) = 40
3718, 23, 3, 32, 36, 35decmul1 12151 . . . 4 (200 · 2) = 400
3830, 31, 37mulcomli 10639 . . 3 (2 · 200) = 400
39 eqid 2826 . . . . 5 1401 = 1401
40 6nn0 11907 . . . . . . 7 6 ∈ ℕ0
4114, 40deccl 12102 . . . . . 6 16 ∈ ℕ0
42 eqid 2826 . . . . . 6 400 = 400
43 eqid 2826 . . . . . . 7 140 = 140
44 eqid 2826 . . . . . . . 8 14 = 14
45 4p2e6 11779 . . . . . . . 8 (4 + 2) = 6
4614, 2, 18, 44, 45decaddi 12147 . . . . . . 7 (14 + 2) = 16
47 00id 10804 . . . . . . 7 (0 + 0) = 0
4815, 3, 18, 3, 43, 33, 46, 47decadd 12141 . . . . . 6 (140 + 20) = 160
49 eqid 2826 . . . . . . 7 40 = 40
5041nn0cni 11898 . . . . . . . 8 16 ∈ ℂ
5150addid1i 10816 . . . . . . 7 (16 + 0) = 16
52 eqid 2826 . . . . . . . 8 203 = 203
53 ax-1cn 10584 . . . . . . . . . 10 1 ∈ ℂ
5453addid1i 10816 . . . . . . . . 9 (1 + 0) = 1
5514dec0h 12109 . . . . . . . . 9 1 = 01
5654, 55eqtri 2849 . . . . . . . 8 (1 + 0) = 01
5753addid2i 10817 . . . . . . . . . 10 (0 + 1) = 1
5857, 14eqeltri 2914 . . . . . . . . 9 (0 + 1) ∈ ℕ0
59 4cn 11711 . . . . . . . . . 10 4 ∈ ℂ
60 4t2e8 11794 . . . . . . . . . 10 (4 · 2) = 8
6159, 31, 60mulcomli 10639 . . . . . . . . 9 (2 · 4) = 8
6259mul02i 10818 . . . . . . . . . . 11 (0 · 4) = 0
6362, 57oveq12i 7160 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = (0 + 1)
6463, 57eqtri 2849 . . . . . . . . 9 ((0 · 4) + (0 + 1)) = 1
6518, 3, 58, 33, 2, 61, 64decrmanc 12144 . . . . . . . 8 ((20 · 4) + (0 + 1)) = 81
66 2p1e3 11768 . . . . . . . . 9 (2 + 1) = 3
67 3cn 11707 . . . . . . . . . 10 3 ∈ ℂ
68 4t3e12 12185 . . . . . . . . . 10 (4 · 3) = 12
6959, 67, 68mulcomli 10639 . . . . . . . . 9 (3 · 4) = 12
7014, 18, 66, 69decsuc 12118 . . . . . . . 8 ((3 · 4) + 1) = 13
7123, 19, 3, 14, 52, 56, 2, 19, 14, 65, 70decmac 12139 . . . . . . 7 ((203 · 4) + (1 + 0)) = 813
7225nn0cni 11898 . . . . . . . . . 10 203 ∈ ℂ
7372mul01i 10819 . . . . . . . . 9 (203 · 0) = 0
7473oveq1i 7158 . . . . . . . 8 ((203 · 0) + 6) = (0 + 6)
75 6cn 11717 . . . . . . . . 9 6 ∈ ℂ
7675addid2i 10817 . . . . . . . 8 (0 + 6) = 6
7740dec0h 12109 . . . . . . . 8 6 = 06
7874, 76, 773eqtri 2853 . . . . . . 7 ((203 · 0) + 6) = 06
792, 3, 14, 40, 49, 51, 25, 40, 3, 71, 78decma2c 12140 . . . . . 6 ((203 · 40) + (16 + 0)) = 8136
8073oveq1i 7158 . . . . . . 7 ((203 · 0) + 0) = (0 + 0)
813dec0h 12109 . . . . . . 7 0 = 00
8280, 47, 813eqtri 2853 . . . . . 6 ((203 · 0) + 0) = 00
834, 3, 41, 3, 42, 48, 25, 3, 3, 79, 82decma2c 12140 . . . . 5 ((203 · 400) + (140 + 20)) = 81360
8431mulid1i 10634 . . . . . . 7 (2 · 1) = 2
8553mul02i 10818 . . . . . . 7 (0 · 1) = 0
8614, 18, 3, 33, 84, 85decmul1 12151 . . . . . 6 (20 · 1) = 20
8767mulid1i 10634 . . . . . . . 8 (3 · 1) = 3
8887oveq1i 7158 . . . . . . 7 ((3 · 1) + 1) = (3 + 1)
89 3p1e4 11771 . . . . . . 7 (3 + 1) = 4
9088, 89eqtri 2849 . . . . . 6 ((3 · 1) + 1) = 4
9123, 19, 14, 52, 14, 86, 90decrmanc 12144 . . . . 5 ((203 · 1) + 1) = 204
925, 14, 16, 14, 1, 39, 25, 2, 23, 83, 91decma2c 12140 . . . 4 ((203 · 𝑁) + 1401) = 813604
93 eqid 2826 . . . . 5 902 = 902
94 8nn0 11909 . . . . . . 7 8 ∈ ℕ0
9514, 94deccl 12102 . . . . . 6 18 ∈ ℕ0
9695, 3deccl 12102 . . . . 5 180 ∈ ℕ0
97 eqid 2826 . . . . . 6 90 = 90
98 eqid 2826 . . . . . 6 180 = 180
9995nn0cni 11898 . . . . . . . 8 18 ∈ ℂ
10099addid1i 10816 . . . . . . 7 (18 + 0) = 18
101 1p2e3 11769 . . . . . . . . 9 (1 + 2) = 3
102101, 19eqeltri 2914 . . . . . . . 8 (1 + 2) ∈ ℕ0
103 9t9e81 12216 . . . . . . . 8 (9 · 9) = 81
104 9cn 11726 . . . . . . . . . . 11 9 ∈ ℂ
105104mul02i 10818 . . . . . . . . . 10 (0 · 9) = 0
106105, 101oveq12i 7160 . . . . . . . . 9 ((0 · 9) + (1 + 2)) = (0 + 3)
10767addid2i 10817 . . . . . . . . 9 (0 + 3) = 3
108106, 107eqtri 2849 . . . . . . . 8 ((0 · 9) + (1 + 2)) = 3
10910, 3, 102, 97, 10, 103, 108decrmanc 12144 . . . . . . 7 ((90 · 9) + (1 + 2)) = 813
110 9t2e18 12209 . . . . . . . . 9 (9 · 2) = 18
111104, 31, 110mulcomli 10639 . . . . . . . 8 (2 · 9) = 18
112 1p1e2 11751 . . . . . . . 8 (1 + 1) = 2
113 8p8e16 12173 . . . . . . . 8 (8 + 8) = 16
11414, 94, 94, 111, 112, 40, 113decaddci 12148 . . . . . . 7 ((2 · 9) + 8) = 26
11527, 18, 14, 94, 93, 100, 10, 40, 18, 109, 114decmac 12139 . . . . . 6 ((902 · 9) + (18 + 0)) = 8136
11628nn0cni 11898 . . . . . . . . 9 902 ∈ ℂ
117116mul01i 10819 . . . . . . . 8 (902 · 0) = 0
118117oveq1i 7158 . . . . . . 7 ((902 · 0) + 0) = (0 + 0)
119118, 47, 813eqtri 2853 . . . . . 6 ((902 · 0) + 0) = 00
12010, 3, 95, 3, 97, 98, 28, 3, 3, 115, 119decma2c 12140 . . . . 5 ((902 · 90) + 180) = 81360
12118, 10, 3, 97, 110, 35decmul1 12151 . . . . . 6 (90 · 2) = 180
12218, 27, 18, 93, 121, 34decmul1 12151 . . . . 5 (902 · 2) = 1804
12328, 27, 18, 93, 2, 96, 120, 122decmul2c 12153 . . . 4 (902 · 902) = 813604
12492, 123eqtr4i 2852 . . 3 ((203 · 𝑁) + 1401) = (902 · 902)
1258, 9, 24, 26, 28, 17, 29, 38, 124mod2xi 16395 . 2 ((2↑400) mod 𝑁) = (1401 mod 𝑁)
1265nn0cni 11898 . . 3 400 ∈ ℂ
12718, 2, 3, 49, 60, 35decmul1 12151 . . . 4 (40 · 2) = 80
12818, 4, 3, 42, 127, 35decmul1 12151 . . 3 (400 · 2) = 800
129126, 31, 128mulcomli 10639 . 2 (2 · 400) = 800
130 eqid 2826 . . . 4 2311 = 2311
13118, 94deccl 12102 . . . . 5 28 ∈ ℕ0
132 eqid 2826 . . . . . 6 231 = 231
133 eqid 2826 . . . . . 6 49 = 49
134 7nn0 11908 . . . . . . 7 7 ∈ ℕ0
135 7p1e8 11775 . . . . . . 7 (7 + 1) = 8
136 eqid 2826 . . . . . . . 8 23 = 23
137 4p3e7 11780 . . . . . . . . 9 (4 + 3) = 7
13859, 67, 137addcomli 10821 . . . . . . . 8 (3 + 4) = 7
13918, 19, 2, 136, 138decaddi 12147 . . . . . . 7 (23 + 4) = 27
14018, 134, 135, 139decsuc 12118 . . . . . 6 ((23 + 4) + 1) = 28
141 9p1e10 12089 . . . . . . 7 (9 + 1) = 10
142104, 53, 141addcomli 10821 . . . . . 6 (1 + 9) = 10
14320, 14, 2, 10, 132, 133, 140, 142decaddc2 12143 . . . . 5 (231 + 49) = 280
144131nn0cni 11898 . . . . . . 7 28 ∈ ℂ
145144addid1i 10816 . . . . . 6 (28 + 0) = 28
14631addid1i 10816 . . . . . . . 8 (2 + 0) = 2
147146, 18eqeltri 2914 . . . . . . 7 (2 + 0) ∈ ℕ0
148 eqid 2826 . . . . . . 7 490 = 490
149 4t4e16 12186 . . . . . . . . 9 (4 · 4) = 16
150 6p3e9 11786 . . . . . . . . 9 (6 + 3) = 9
15114, 40, 19, 149, 150decaddi 12147 . . . . . . . 8 ((4 · 4) + 3) = 19
152 9t4e36 12211 . . . . . . . 8 (9 · 4) = 36
1532, 2, 10, 133, 40, 19, 151, 152decmul1c 12152 . . . . . . 7 (49 · 4) = 196
15462, 146oveq12i 7160 . . . . . . . 8 ((0 · 4) + (2 + 0)) = (0 + 2)
15531addid2i 10817 . . . . . . . 8 (0 + 2) = 2
156154, 155eqtri 2849 . . . . . . 7 ((0 · 4) + (2 + 0)) = 2
15711, 3, 147, 148, 2, 153, 156decrmanc 12144 . . . . . 6 ((490 · 4) + (2 + 0)) = 1962
15812nn0cni 11898 . . . . . . . . 9 490 ∈ ℂ
159158mul01i 10819 . . . . . . . 8 (490 · 0) = 0
160159oveq1i 7158 . . . . . . 7 ((490 · 0) + 8) = (0 + 8)
161 8cn 11723 . . . . . . . 8 8 ∈ ℂ
162161addid2i 10817 . . . . . . 7 (0 + 8) = 8
16394dec0h 12109 . . . . . . 7 8 = 08
164160, 162, 1633eqtri 2853 . . . . . 6 ((490 · 0) + 8) = 08
1652, 3, 18, 94, 49, 145, 12, 94, 3, 157, 164decma2c 12140 . . . . 5 ((490 · 40) + (28 + 0)) = 19628
166159oveq1i 7158 . . . . . 6 ((490 · 0) + 0) = (0 + 0)
167166, 47, 813eqtri 2853 . . . . 5 ((490 · 0) + 0) = 00
1684, 3, 131, 3, 42, 143, 12, 3, 3, 165, 167decma2c 12140 . . . 4 ((490 · 400) + (231 + 49)) = 196280
16959mulid1i 10634 . . . . . 6 (4 · 1) = 4
170104mulid1i 10634 . . . . . 6 (9 · 1) = 9
17114, 2, 10, 133, 169, 170decmul1 12151 . . . . 5 (49 · 1) = 49
17285oveq1i 7158 . . . . . 6 ((0 · 1) + 1) = (0 + 1)
173172, 57eqtri 2849 . . . . 5 ((0 · 1) + 1) = 1
17411, 3, 14, 148, 14, 171, 173decrmanc 12144 . . . 4 ((490 · 1) + 1) = 491
1755, 14, 21, 14, 1, 130, 12, 14, 11, 168, 174decma2c 12140 . . 3 ((490 · 𝑁) + 2311) = 1962801
17615nn0cni 11898 . . . . . . 7 14 ∈ ℂ
177176addid1i 10816 . . . . . 6 (14 + 0) = 14
178 5nn0 11906 . . . . . . . 8 5 ∈ ℕ0
179178, 40deccl 12102 . . . . . . 7 56 ∈ ℕ0
180179, 3deccl 12102 . . . . . 6 560 ∈ ℕ0
181 eqid 2826 . . . . . . . 8 560 = 560
182179nn0cni 11898 . . . . . . . . 9 56 ∈ ℂ
183182addid2i 10817 . . . . . . . 8 (0 + 56) = 56
1843, 14, 179, 3, 55, 181, 183, 54decadd 12141 . . . . . . 7 (1 + 560) = 561
185182addid1i 10816 . . . . . . . 8 (56 + 0) = 56
186 5cn 11714 . . . . . . . . . . 11 5 ∈ ℂ
187186addid1i 10816 . . . . . . . . . 10 (5 + 0) = 5
188187, 178eqeltri 2914 . . . . . . . . 9 (5 + 0) ∈ ℕ0
18953mulid1i 10634 . . . . . . . . 9 (1 · 1) = 1
190169, 187oveq12i 7160 . . . . . . . . . 10 ((4 · 1) + (5 + 0)) = (4 + 5)
191 5p4e9 11784 . . . . . . . . . . 11 (5 + 4) = 9
192186, 59, 191addcomli 10821 . . . . . . . . . 10 (4 + 5) = 9
193190, 192eqtri 2849 . . . . . . . . 9 ((4 · 1) + (5 + 0)) = 9
19414, 2, 188, 44, 14, 189, 193decrmanc 12144 . . . . . . . 8 ((14 · 1) + (5 + 0)) = 19
19585oveq1i 7158 . . . . . . . . 9 ((0 · 1) + 6) = (0 + 6)
196195, 76, 773eqtri 2853 . . . . . . . 8 ((0 · 1) + 6) = 06
19715, 3, 178, 40, 43, 185, 14, 40, 3, 194, 196decmac 12139 . . . . . . 7 ((140 · 1) + (56 + 0)) = 196
198189oveq1i 7158 . . . . . . . 8 ((1 · 1) + 1) = (1 + 1)
19918dec0h 12109 . . . . . . . 8 2 = 02
200198, 112, 1993eqtri 2853 . . . . . . 7 ((1 · 1) + 1) = 02
20116, 14, 179, 14, 39, 184, 14, 18, 3, 197, 200decmac 12139 . . . . . 6 ((1401 · 1) + (1 + 560)) = 1962
20259mulid2i 10635 . . . . . . . . . . . 12 (1 · 4) = 4
203202oveq1i 7158 . . . . . . . . . . 11 ((1 · 4) + 1) = (4 + 1)
204 4p1e5 11772 . . . . . . . . . . 11 (4 + 1) = 5
205203, 204eqtri 2849 . . . . . . . . . 10 ((1 · 4) + 1) = 5
2062, 14, 2, 44, 40, 14, 205, 149decmul1c 12152 . . . . . . . . 9 (14 · 4) = 56
20775addid1i 10816 . . . . . . . . 9 (6 + 0) = 6
208178, 40, 3, 206, 207decaddi 12147 . . . . . . . 8 ((14 · 4) + 0) = 56
209 0cn 10622 . . . . . . . . 9 0 ∈ ℂ
21059mul01i 10819 . . . . . . . . . 10 (4 · 0) = 0
211210, 81eqtri 2849 . . . . . . . . 9 (4 · 0) = 00
21259, 209, 211mulcomli 10639 . . . . . . . 8 (0 · 4) = 00
2132, 15, 3, 43, 3, 3, 208, 212decmul1c 12152 . . . . . . 7 (140 · 4) = 560
214202oveq1i 7158 . . . . . . . 8 ((1 · 4) + 4) = (4 + 4)
215 4p4e8 11781 . . . . . . . 8 (4 + 4) = 8
216214, 215eqtri 2849 . . . . . . 7 ((1 · 4) + 4) = 8
21716, 14, 2, 39, 2, 213, 216decrmanc 12144 . . . . . 6 ((1401 · 4) + 4) = 5608
21814, 2, 14, 2, 44, 177, 17, 94, 180, 201, 217decma2c 12140 . . . . 5 ((1401 · 14) + (14 + 0)) = 19628
21917nn0cni 11898 . . . . . . . 8 1401 ∈ ℂ
220219mul01i 10819 . . . . . . 7 (1401 · 0) = 0
221220oveq1i 7158 . . . . . 6 ((1401 · 0) + 0) = (0 + 0)
222221, 47, 813eqtri 2853 . . . . 5 ((1401 · 0) + 0) = 00
22315, 3, 15, 3, 43, 43, 17, 3, 3, 218, 222decma2c 12140 . . . 4 ((1401 · 140) + 140) = 196280
224219mulid1i 10634 . . . 4 (1401 · 1) = 1401
22517, 16, 14, 39, 14, 16, 223, 224decmul2c 12153 . . 3 (1401 · 1401) = 1962801
226175, 225eqtr4i 2852 . 2 ((490 · 𝑁) + 2311) = (1401 · 1401)
2278, 9, 5, 13, 17, 22, 125, 129, 226mod2xi 16395 1 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530  (class class class)co 7148  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  cn 11627  2c2 11681  3c3 11682  4c4 11683  5c5 11684  6c6 11685  7c7 11686  8c8 11687  9c9 11688  0cn0 11886  cdc 12087   mod cmo 13227  cexp 13419
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 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7451  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-nel 3129  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6146  df-ord 6192  df-on 6193  df-lim 6194  df-suc 6195  df-iota 6312  df-fun 6354  df-fn 6355  df-f 6356  df-f1 6357  df-fo 6358  df-f1o 6359  df-fv 6360  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7569  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-sup 8895  df-inf 8896  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11628  df-2 11689  df-3 11690  df-4 11691  df-5 11692  df-6 11693  df-7 11694  df-8 11695  df-9 11696  df-n0 11887  df-z 11971  df-dec 12088  df-uz 12233  df-rp 12380  df-fl 13152  df-mod 13228  df-seq 13360  df-exp 13420
This theorem is referenced by:  4001lem3  16466  4001lem4  16467
  Copyright terms: Public domain W3C validator