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