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

Theorem 4001lem2 16080
Description: Lemma for 4001prm 16083. 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 11598 . . . . . 6 4 ∈ ℕ0
3 0nn0 11594 . . . . . 6 0 ∈ ℕ0
42, 3deccl 11794 . . . . 5 40 ∈ ℕ0
54, 3deccl 11794 . . . 4 400 ∈ ℕ0
6 1nn 11328 . . . 4 1 ∈ ℕ
75, 6decnncl 11799 . . 3 4001 ∈ ℕ
81, 7eqeltri 2892 . 2 𝑁 ∈ ℕ
9 2nn 11386 . 2 2 ∈ ℕ
10 9nn0 11603 . . . . 5 9 ∈ ℕ0
112, 10deccl 11794 . . . 4 49 ∈ ℕ0
1211, 3deccl 11794 . . 3 490 ∈ ℕ0
1312nn0zi 11688 . 2 490 ∈ ℤ
14 1nn0 11595 . . . . 5 1 ∈ ℕ0
1514, 2deccl 11794 . . . 4 14 ∈ ℕ0
1615, 3deccl 11794 . . 3 140 ∈ ℕ0
1716, 14deccl 11794 . 2 1401 ∈ ℕ0
18 2nn0 11596 . . . . 5 2 ∈ ℕ0
19 3nn0 11597 . . . . 5 3 ∈ ℕ0
2018, 19deccl 11794 . . . 4 23 ∈ ℕ0
2120, 14deccl 11794 . . 3 231 ∈ ℕ0
2221, 14deccl 11794 . 2 2311 ∈ ℕ0
2318, 3deccl 11794 . . . 4 20 ∈ ℕ0
2423, 3deccl 11794 . . 3 200 ∈ ℕ0
2523, 19deccl 11794 . . . 4 203 ∈ ℕ0
2625nn0zi 11688 . . 3 203 ∈ ℤ
2710, 3deccl 11794 . . . 4 90 ∈ ℕ0
2827, 18deccl 11794 . . 3 902 ∈ ℕ0
2914001lem1 16079 . . 3 ((2↑200) mod 𝑁) = (902 mod 𝑁)
3024nn0cni 11591 . . . 4 200 ∈ ℂ
31 2cn 11388 . . . 4 2 ∈ ℂ
32 eqid 2817 . . . . 5 200 = 200
33 eqid 2817 . . . . . 6 20 = 20
34 2t2e4 11483 . . . . . 6 (2 · 2) = 4
3531mul02i 10520 . . . . . 6 (0 · 2) = 0
3618, 18, 3, 33, 3, 34, 35decmul1 11843 . . . . 5 (20 · 2) = 40
3718, 23, 3, 32, 3, 36, 35decmul1 11843 . . . 4 (200 · 2) = 400
3830, 31, 37mulcomli 10344 . . 3 (2 · 200) = 400
39 eqid 2817 . . . . 5 1401 = 1401
40 6nn0 11600 . . . . . . 7 6 ∈ ℕ0
4114, 40deccl 11794 . . . . . 6 16 ∈ ℕ0
42 eqid 2817 . . . . . 6 400 = 400
43 eqid 2817 . . . . . . 7 140 = 140
44 eqid 2817 . . . . . . . 8 14 = 14
45 4p2e6 11472 . . . . . . . 8 (4 + 2) = 6
4614, 2, 18, 44, 45decaddi 11839 . . . . . . 7 (14 + 2) = 16
47 00id 10506 . . . . . . 7 (0 + 0) = 0
4815, 3, 18, 3, 43, 33, 46, 47decadd 11833 . . . . . 6 (140 + 20) = 160
49 eqid 2817 . . . . . . 7 40 = 40
5041nn0cni 11591 . . . . . . . 8 16 ∈ ℂ
5150addid1i 10518 . . . . . . 7 (16 + 0) = 16
52 eqid 2817 . . . . . . . 8 203 = 203
53 ax-1cn 10289 . . . . . . . . . 10 1 ∈ ℂ
5453addid1i 10518 . . . . . . . . 9 (1 + 0) = 1
5514dec0h 11801 . . . . . . . . 9 1 = 01
5654, 55eqtri 2839 . . . . . . . 8 (1 + 0) = 01
5753addid2i 10519 . . . . . . . . . 10 (0 + 1) = 1
5857, 14eqeltri 2892 . . . . . . . . 9 (0 + 1) ∈ ℕ0
59 4cn 11399 . . . . . . . . . 10 4 ∈ ℂ
60 4t2e8 11487 . . . . . . . . . 10 (4 · 2) = 8
6159, 31, 60mulcomli 10344 . . . . . . . . 9 (2 · 4) = 8
6259mul02i 10520 . . . . . . . . . . 11 (0 · 4) = 0
6362, 57oveq12i 6896 . . . . . . . . . 10 ((0 · 4) + (0 + 1)) = (0 + 1)
6463, 57eqtri 2839 . . . . . . . . 9 ((0 · 4) + (0 + 1)) = 1
6518, 3, 58, 33, 2, 61, 64decrmanc 11836 . . . . . . . 8 ((20 · 4) + (0 + 1)) = 81
66 2p1e3 11462 . . . . . . . . 9 (2 + 1) = 3
67 3cn 11394 . . . . . . . . . 10 3 ∈ ℂ
68 4t3e12 11877 . . . . . . . . . 10 (4 · 3) = 12
6959, 67, 68mulcomli 10344 . . . . . . . . 9 (3 · 4) = 12
7014, 18, 66, 69decsuc 11810 . . . . . . . 8 ((3 · 4) + 1) = 13
7123, 19, 3, 14, 52, 56, 2, 19, 14, 65, 70decmac 11831 . . . . . . 7 ((203 · 4) + (1 + 0)) = 813
7225nn0cni 11591 . . . . . . . . . 10 203 ∈ ℂ
7372mul01i 10521 . . . . . . . . 9 (203 · 0) = 0
7473oveq1i 6894 . . . . . . . 8 ((203 · 0) + 6) = (0 + 6)
75 6cn 11407 . . . . . . . . 9 6 ∈ ℂ
7675addid2i 10519 . . . . . . . 8 (0 + 6) = 6
7740dec0h 11801 . . . . . . . 8 6 = 06
7874, 76, 773eqtri 2843 . . . . . . 7 ((203 · 0) + 6) = 06
792, 3, 14, 40, 49, 51, 25, 40, 3, 71, 78decma2c 11832 . . . . . 6 ((203 · 40) + (16 + 0)) = 8136
8073oveq1i 6894 . . . . . . 7 ((203 · 0) + 0) = (0 + 0)
813dec0h 11801 . . . . . . 7 0 = 00
8280, 47, 813eqtri 2843 . . . . . 6 ((203 · 0) + 0) = 00
834, 3, 41, 3, 42, 48, 25, 3, 3, 79, 82decma2c 11832 . . . . 5 ((203 · 400) + (140 + 20)) = 81360
8431mulid1i 10339 . . . . . . 7 (2 · 1) = 2
8553mul02i 10520 . . . . . . 7 (0 · 1) = 0
8614, 18, 3, 33, 3, 84, 85decmul1 11843 . . . . . 6 (20 · 1) = 20
8767mulid1i 10339 . . . . . . . 8 (3 · 1) = 3
8887oveq1i 6894 . . . . . . 7 ((3 · 1) + 1) = (3 + 1)
89 3p1e4 11464 . . . . . . 7 (3 + 1) = 4
9088, 89eqtri 2839 . . . . . 6 ((3 · 1) + 1) = 4
9123, 19, 14, 52, 14, 86, 90decrmanc 11836 . . . . 5 ((203 · 1) + 1) = 204
925, 14, 16, 14, 1, 39, 25, 2, 23, 83, 91decma2c 11832 . . . 4 ((203 · 𝑁) + 1401) = 813604
93 eqid 2817 . . . . 5 902 = 902
94 8nn0 11602 . . . . . . 7 8 ∈ ℕ0
9514, 94deccl 11794 . . . . . 6 18 ∈ ℕ0
9695, 3deccl 11794 . . . . 5 180 ∈ ℕ0
97 eqid 2817 . . . . . 6 90 = 90
98 eqid 2817 . . . . . 6 180 = 180
9995nn0cni 11591 . . . . . . . 8 18 ∈ ℂ
10099addid1i 10518 . . . . . . 7 (18 + 0) = 18
101 1p2e3 11463 . . . . . . . . 9 (1 + 2) = 3
102101, 19eqeltri 2892 . . . . . . . 8 (1 + 2) ∈ ℕ0
103 9t9e81 11908 . . . . . . . 8 (9 · 9) = 81
104 9cn 11419 . . . . . . . . . . 11 9 ∈ ℂ
105104mul02i 10520 . . . . . . . . . 10 (0 · 9) = 0
106105, 101oveq12i 6896 . . . . . . . . 9 ((0 · 9) + (1 + 2)) = (0 + 3)
10767addid2i 10519 . . . . . . . . 9 (0 + 3) = 3
108106, 107eqtri 2839 . . . . . . . 8 ((0 · 9) + (1 + 2)) = 3
10910, 3, 102, 97, 10, 103, 108decrmanc 11836 . . . . . . 7 ((90 · 9) + (1 + 2)) = 813
110 9t2e18 11901 . . . . . . . . 9 (9 · 2) = 18
111104, 31, 110mulcomli 10344 . . . . . . . 8 (2 · 9) = 18
112 1p1e2 11445 . . . . . . . 8 (1 + 1) = 2
113 8p8e16 11865 . . . . . . . 8 (8 + 8) = 16
11414, 94, 94, 111, 112, 40, 113decaddci 11840 . . . . . . 7 ((2 · 9) + 8) = 26
11527, 18, 14, 94, 93, 100, 10, 40, 18, 109, 114decmac 11831 . . . . . 6 ((902 · 9) + (18 + 0)) = 8136
11628nn0cni 11591 . . . . . . . . 9 902 ∈ ℂ
117116mul01i 10521 . . . . . . . 8 (902 · 0) = 0
118117oveq1i 6894 . . . . . . 7 ((902 · 0) + 0) = (0 + 0)
119118, 47, 813eqtri 2843 . . . . . 6 ((902 · 0) + 0) = 00
12010, 3, 95, 3, 97, 98, 28, 3, 3, 115, 119decma2c 11832 . . . . 5 ((902 · 90) + 180) = 81360
12118, 10, 3, 97, 3, 110, 35decmul1 11843 . . . . . 6 (90 · 2) = 180
12218, 27, 18, 93, 2, 121, 34decmul1 11843 . . . . 5 (902 · 2) = 1804
12328, 27, 18, 93, 2, 96, 120, 122decmul2c 11845 . . . 4 (902 · 902) = 813604
12492, 123eqtr4i 2842 . . 3 ((203 · 𝑁) + 1401) = (902 · 902)
1258, 9, 24, 26, 28, 17, 29, 38, 124mod2xi 16010 . 2 ((2↑400) mod 𝑁) = (1401 mod 𝑁)
1265nn0cni 11591 . . 3 400 ∈ ℂ
12718, 2, 3, 49, 3, 60, 35decmul1 11843 . . . 4 (40 · 2) = 80
12818, 4, 3, 42, 3, 127, 35decmul1 11843 . . 3 (400 · 2) = 800
129126, 31, 128mulcomli 10344 . 2 (2 · 400) = 800
130 eqid 2817 . . . 4 2311 = 2311
13118, 94deccl 11794 . . . . 5 28 ∈ ℕ0
132 eqid 2817 . . . . . 6 231 = 231
133 eqid 2817 . . . . . 6 49 = 49
134 7nn0 11601 . . . . . . 7 7 ∈ ℕ0
135 7p1e8 11468 . . . . . . 7 (7 + 1) = 8
136 eqid 2817 . . . . . . . 8 23 = 23
137 4p3e7 11473 . . . . . . . . 9 (4 + 3) = 7
13859, 67, 137addcomli 10523 . . . . . . . 8 (3 + 4) = 7
13918, 19, 2, 136, 138decaddi 11839 . . . . . . 7 (23 + 4) = 27
14018, 134, 135, 139decsuc 11810 . . . . . 6 ((23 + 4) + 1) = 28
141 9p1e10 11781 . . . . . . 7 (9 + 1) = 10
142104, 53, 141addcomli 10523 . . . . . 6 (1 + 9) = 10
14320, 14, 2, 10, 132, 133, 140, 142decaddc2 11835 . . . . 5 (231 + 49) = 280
144131nn0cni 11591 . . . . . . 7 28 ∈ ℂ
145144addid1i 10518 . . . . . 6 (28 + 0) = 28
14631addid1i 10518 . . . . . . . 8 (2 + 0) = 2
147146, 18eqeltri 2892 . . . . . . 7 (2 + 0) ∈ ℕ0
148 eqid 2817 . . . . . . 7 490 = 490
149 4t4e16 11878 . . . . . . . . 9 (4 · 4) = 16
150 6p3e9 11479 . . . . . . . . 9 (6 + 3) = 9
15114, 40, 19, 149, 150decaddi 11839 . . . . . . . 8 ((4 · 4) + 3) = 19
152 9t4e36 11903 . . . . . . . 8 (9 · 4) = 36
1532, 2, 10, 133, 40, 19, 151, 152decmul1c 11844 . . . . . . 7 (49 · 4) = 196
15462, 146oveq12i 6896 . . . . . . . 8 ((0 · 4) + (2 + 0)) = (0 + 2)
15531addid2i 10519 . . . . . . . 8 (0 + 2) = 2
156154, 155eqtri 2839 . . . . . . 7 ((0 · 4) + (2 + 0)) = 2
15711, 3, 147, 148, 2, 153, 156decrmanc 11836 . . . . . 6 ((490 · 4) + (2 + 0)) = 1962
15812nn0cni 11591 . . . . . . . . 9 490 ∈ ℂ
159158mul01i 10521 . . . . . . . 8 (490 · 0) = 0
160159oveq1i 6894 . . . . . . 7 ((490 · 0) + 8) = (0 + 8)
161 8cn 11415 . . . . . . . 8 8 ∈ ℂ
162161addid2i 10519 . . . . . . 7 (0 + 8) = 8
16394dec0h 11801 . . . . . . 7 8 = 08
164160, 162, 1633eqtri 2843 . . . . . 6 ((490 · 0) + 8) = 08
1652, 3, 18, 94, 49, 145, 12, 94, 3, 157, 164decma2c 11832 . . . . 5 ((490 · 40) + (28 + 0)) = 19628
166159oveq1i 6894 . . . . . 6 ((490 · 0) + 0) = (0 + 0)
167166, 47, 813eqtri 2843 . . . . 5 ((490 · 0) + 0) = 00
1684, 3, 131, 3, 42, 143, 12, 3, 3, 165, 167decma2c 11832 . . . 4 ((490 · 400) + (231 + 49)) = 196280
16959mulid1i 10339 . . . . . 6 (4 · 1) = 4
170104mulid1i 10339 . . . . . 6 (9 · 1) = 9
17114, 2, 10, 133, 10, 169, 170decmul1 11843 . . . . 5 (49 · 1) = 49
17285oveq1i 6894 . . . . . 6 ((0 · 1) + 1) = (0 + 1)
173172, 57eqtri 2839 . . . . 5 ((0 · 1) + 1) = 1
17411, 3, 14, 148, 14, 171, 173decrmanc 11836 . . . 4 ((490 · 1) + 1) = 491
1755, 14, 21, 14, 1, 130, 12, 14, 11, 168, 174decma2c 11832 . . 3 ((490 · 𝑁) + 2311) = 1962801
17615nn0cni 11591 . . . . . . 7 14 ∈ ℂ
177176addid1i 10518 . . . . . 6 (14 + 0) = 14
178 5nn0 11599 . . . . . . . 8 5 ∈ ℕ0
179178, 40deccl 11794 . . . . . . 7 56 ∈ ℕ0
180179, 3deccl 11794 . . . . . 6 560 ∈ ℕ0
181 eqid 2817 . . . . . . . 8 560 = 560
182179nn0cni 11591 . . . . . . . . 9 56 ∈ ℂ
183182addid2i 10519 . . . . . . . 8 (0 + 56) = 56
1843, 14, 179, 3, 55, 181, 183, 54decadd 11833 . . . . . . 7 (1 + 560) = 561
185182addid1i 10518 . . . . . . . 8 (56 + 0) = 56
186 5cn 11403 . . . . . . . . . . 11 5 ∈ ℂ
187186addid1i 10518 . . . . . . . . . 10 (5 + 0) = 5
188187, 178eqeltri 2892 . . . . . . . . 9 (5 + 0) ∈ ℕ0
18953mulid1i 10339 . . . . . . . . 9 (1 · 1) = 1
190169, 187oveq12i 6896 . . . . . . . . . 10 ((4 · 1) + (5 + 0)) = (4 + 5)
191 5p4e9 11477 . . . . . . . . . . 11 (5 + 4) = 9
192186, 59, 191addcomli 10523 . . . . . . . . . 10 (4 + 5) = 9
193190, 192eqtri 2839 . . . . . . . . 9 ((4 · 1) + (5 + 0)) = 9
19414, 2, 188, 44, 14, 189, 193decrmanc 11836 . . . . . . . 8 ((14 · 1) + (5 + 0)) = 19
19585oveq1i 6894 . . . . . . . . 9 ((0 · 1) + 6) = (0 + 6)
196195, 76, 773eqtri 2843 . . . . . . . 8 ((0 · 1) + 6) = 06
19715, 3, 178, 40, 43, 185, 14, 40, 3, 194, 196decmac 11831 . . . . . . 7 ((140 · 1) + (56 + 0)) = 196
198189oveq1i 6894 . . . . . . . 8 ((1 · 1) + 1) = (1 + 1)
19918dec0h 11801 . . . . . . . 8 2 = 02
200198, 112, 1993eqtri 2843 . . . . . . 7 ((1 · 1) + 1) = 02
20116, 14, 179, 14, 39, 184, 14, 18, 3, 197, 200decmac 11831 . . . . . 6 ((1401 · 1) + (1 + 560)) = 1962
20259mulid2i 10340 . . . . . . . . . . . 12 (1 · 4) = 4
203202oveq1i 6894 . . . . . . . . . . 11 ((1 · 4) + 1) = (4 + 1)
204 4p1e5 11465 . . . . . . . . . . 11 (4 + 1) = 5
205203, 204eqtri 2839 . . . . . . . . . 10 ((1 · 4) + 1) = 5
2062, 14, 2, 44, 40, 14, 205, 149decmul1c 11844 . . . . . . . . 9 (14 · 4) = 56
20775addid1i 10518 . . . . . . . . 9 (6 + 0) = 6
208178, 40, 3, 206, 207decaddi 11839 . . . . . . . 8 ((14 · 4) + 0) = 56
209 0cn 10327 . . . . . . . . 9 0 ∈ ℂ
21059mul01i 10521 . . . . . . . . . 10 (4 · 0) = 0
211210, 81eqtri 2839 . . . . . . . . 9 (4 · 0) = 00
21259, 209, 211mulcomli 10344 . . . . . . . 8 (0 · 4) = 00
2132, 15, 3, 43, 3, 3, 208, 212decmul1c 11844 . . . . . . 7 (140 · 4) = 560
214202oveq1i 6894 . . . . . . . 8 ((1 · 4) + 4) = (4 + 4)
215 4p4e8 11474 . . . . . . . 8 (4 + 4) = 8
216214, 215eqtri 2839 . . . . . . 7 ((1 · 4) + 4) = 8
21716, 14, 2, 39, 2, 213, 216decrmanc 11836 . . . . . 6 ((1401 · 4) + 4) = 5608
21814, 2, 14, 2, 44, 177, 17, 94, 180, 201, 217decma2c 11832 . . . . 5 ((1401 · 14) + (14 + 0)) = 19628
21917nn0cni 11591 . . . . . . . 8 1401 ∈ ℂ
220219mul01i 10521 . . . . . . 7 (1401 · 0) = 0
221220oveq1i 6894 . . . . . 6 ((1401 · 0) + 0) = (0 + 0)
222221, 47, 813eqtri 2843 . . . . 5 ((1401 · 0) + 0) = 00
22315, 3, 15, 3, 43, 43, 17, 3, 3, 218, 222decma2c 11832 . . . 4 ((1401 · 140) + 140) = 196280
224219mulid1i 10339 . . . 4 (1401 · 1) = 1401
22517, 16, 14, 39, 14, 16, 223, 224decmul2c 11845 . . 3 (1401 · 1401) = 1962801
226175, 225eqtr4i 2842 . 2 ((490 · 𝑁) + 2311) = (1401 · 1401)
2278, 9, 5, 13, 17, 22, 125, 129, 226mod2xi 16010 1 ((2↑800) mod 𝑁) = (2311 mod 𝑁)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  (class class class)co 6884  0cc0 10231  1c1 10232   + caddc 10234   · cmul 10236  cn 11315  2c2 11368  3c3 11369  4c4 11370  5c5 11371  6c6 11372  7c7 11373  8c8 11374  9c9 11375  0cn0 11579  cdc 11779   mod cmo 12912  cexp 13103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-cnex 10287  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308  ax-pre-sup 10309
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-om 7306  df-2nd 7409  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-er 7989  df-en 8203  df-dom 8204  df-sdom 8205  df-sup 8597  df-inf 8598  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-div 10980  df-nn 11316  df-2 11376  df-3 11377  df-4 11378  df-5 11379  df-6 11380  df-7 11381  df-8 11382  df-9 11383  df-n0 11580  df-z 11664  df-dec 11780  df-uz 11925  df-rp 12067  df-fl 12837  df-mod 12913  df-seq 13045  df-exp 13104
This theorem is referenced by:  4001lem3  16081  4001lem4  16082
  Copyright terms: Public domain W3C validator