Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > dchrhash | Structured version Visualization version GIF version | ||
| Description: There are exactly ϕ(𝑁) Dirichlet characters modulo 𝑁. Part of Theorem 6.5.1 of [Shapiro] p. 230. (Contributed by Mario Carneiro, 28-Apr-2016.) |
| Ref | Expression |
|---|---|
| sumdchr.g | ⊢ 𝐺 = (DChr‘𝑁) |
| sumdchr.d | ⊢ 𝐷 = (Base‘𝐺) |
| Ref | Expression |
|---|---|
| dchrhash | ⊢ (𝑁 ∈ ℕ → (♯‘𝐷) = (ϕ‘𝑁)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqid 2760 | . . . . . 6 ⊢ (ℤ/nℤ‘𝑁) = (ℤ/nℤ‘𝑁) | |
| 2 | eqid 2760 | . . . . . 6 ⊢ (Base‘(ℤ/nℤ‘𝑁)) = (Base‘(ℤ/nℤ‘𝑁)) | |
| 3 | 1, 2 | znfi 21865 | . . . . 5 ⊢ (𝑁 ∈ ℕ → (Base‘(ℤ/nℤ‘𝑁)) ∈ Fin) |
| 4 | sumdchr.g | . . . . . 6 ⊢ 𝐺 = (DChr‘𝑁) | |
| 5 | sumdchr.d | . . . . . 6 ⊢ 𝐷 = (Base‘𝐺) | |
| 6 | 4, 5 | dchrfi 27582 | . . . . 5 ⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |
| 7 | simprr 785 | . . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ (𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ 𝑥 ∈ 𝐷)) → 𝑥 ∈ 𝐷) | |
| 8 | 4, 1, 5, 2, 7 | dchrf 27569 | . . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ 𝑥 ∈ 𝐷)) → 𝑥:(Base‘(ℤ/nℤ‘𝑁))⟶ℂ) |
| 9 | simprl 783 | . . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ (𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ 𝑥 ∈ 𝐷)) → 𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))) | |
| 10 | 8, 9 | ffvelcdmd 7085 | . . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ (𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ 𝑥 ∈ 𝐷)) → (𝑥‘𝑎) ∈ ℂ) |
| 11 | 3, 6, 10 | fsumcom 15941 | . . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))Σ𝑥 ∈ 𝐷 (𝑥‘𝑎) = Σ𝑥 ∈ 𝐷 Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))(𝑥‘𝑎)) |
| 12 | eqid 2760 | . . . . . . 7 ⊢ (1r‘(ℤ/nℤ‘𝑁)) = (1r‘(ℤ/nℤ‘𝑁)) | |
| 13 | simpl 488 | . . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))) → 𝑁 ∈ ℕ) | |
| 14 | simpr 490 | . . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))) → 𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))) | |
| 15 | 4, 5, 1, 12, 2, 13, 14 | sumdchr2 27597 | . . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))) → Σ𝑥 ∈ 𝐷 (𝑥‘𝑎) = if(𝑎 = (1r‘(ℤ/nℤ‘𝑁)), (♯‘𝐷), 0)) |
| 16 | velsn 4599 | . . . . . . 7 ⊢ (𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))} ↔ 𝑎 = (1r‘(ℤ/nℤ‘𝑁))) | |
| 17 | ifbi 4504 | . . . . . . 7 ⊢ ((𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))} ↔ 𝑎 = (1r‘(ℤ/nℤ‘𝑁))) → if(𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))}, (♯‘𝐷), 0) = if(𝑎 = (1r‘(ℤ/nℤ‘𝑁)), (♯‘𝐷), 0)) | |
| 18 | 16, 17 | mp1i 14 | . . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))) → if(𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))}, (♯‘𝐷), 0) = if(𝑎 = (1r‘(ℤ/nℤ‘𝑁)), (♯‘𝐷), 0)) |
| 19 | 15, 18 | eqtr4d 2798 | . . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))) → Σ𝑥 ∈ 𝐷 (𝑥‘𝑎) = if(𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))}, (♯‘𝐷), 0)) |
| 20 | 19 | sumeq2dv 15869 | . . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))Σ𝑥 ∈ 𝐷 (𝑥‘𝑎) = Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))if(𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))}, (♯‘𝐷), 0)) |
| 21 | eqid 2760 | . . . . . . 7 ⊢ (0g‘𝐺) = (0g‘𝐺) | |
| 22 | simpr 490 | . . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐷) | |
| 23 | 4, 1, 5, 21, 22, 2 | dchrsum 27596 | . . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐷) → Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))(𝑥‘𝑎) = if(𝑥 = (0g‘𝐺), (ϕ‘𝑁), 0)) |
| 24 | velsn 4599 | . . . . . . 7 ⊢ (𝑥 ∈ {(0g‘𝐺)} ↔ 𝑥 = (0g‘𝐺)) | |
| 25 | ifbi 4504 | . . . . . . 7 ⊢ ((𝑥 ∈ {(0g‘𝐺)} ↔ 𝑥 = (0g‘𝐺)) → if(𝑥 ∈ {(0g‘𝐺)}, (ϕ‘𝑁), 0) = if(𝑥 = (0g‘𝐺), (ϕ‘𝑁), 0)) | |
| 26 | 24, 25 | mp1i 14 | . . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐷) → if(𝑥 ∈ {(0g‘𝐺)}, (ϕ‘𝑁), 0) = if(𝑥 = (0g‘𝐺), (ϕ‘𝑁), 0)) |
| 27 | 23, 26 | eqtr4d 2798 | . . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑥 ∈ 𝐷) → Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))(𝑥‘𝑎) = if(𝑥 ∈ {(0g‘𝐺)}, (ϕ‘𝑁), 0)) |
| 28 | 27 | sumeq2dv 15869 | . . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑥 ∈ 𝐷 Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))(𝑥‘𝑎) = Σ𝑥 ∈ 𝐷 if(𝑥 ∈ {(0g‘𝐺)}, (ϕ‘𝑁), 0)) |
| 29 | 11, 20, 28 | 3eqtr3d 2803 | . . 3 ⊢ (𝑁 ∈ ℕ → Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))if(𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))}, (♯‘𝐷), 0) = Σ𝑥 ∈ 𝐷 if(𝑥 ∈ {(0g‘𝐺)}, (ϕ‘𝑁), 0)) |
| 30 | nnnn0 12613 | . . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0) | |
| 31 | 1 | zncrng 21850 | . . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (ℤ/nℤ‘𝑁) ∈ CRing) |
| 32 | crngring 20472 | . . . . . 6 ⊢ ((ℤ/nℤ‘𝑁) ∈ CRing → (ℤ/nℤ‘𝑁) ∈ Ring) | |
| 33 | 2, 12 | ringidcl 20494 | . . . . . 6 ⊢ ((ℤ/nℤ‘𝑁) ∈ Ring → (1r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁))) |
| 34 | 30, 31, 32, 33 | 4syl 20 | . . . . 5 ⊢ (𝑁 ∈ ℕ → (1r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁))) |
| 35 | 34 | snssd 4746 | . . . 4 ⊢ (𝑁 ∈ ℕ → {(1r‘(ℤ/nℤ‘𝑁))} ⊆ (Base‘(ℤ/nℤ‘𝑁))) |
| 36 | hashcl 14500 | . . . . . 6 ⊢ (𝐷 ∈ Fin → (♯‘𝐷) ∈ ℕ0) | |
| 37 | nn0cn 12616 | . . . . . 6 ⊢ ((♯‘𝐷) ∈ ℕ0 → (♯‘𝐷) ∈ ℂ) | |
| 38 | 6, 36, 37 | 3syl 19 | . . . . 5 ⊢ (𝑁 ∈ ℕ → (♯‘𝐷) ∈ ℂ) |
| 39 | 38 | ralrimivw 3158 | . . . 4 ⊢ (𝑁 ∈ ℕ → ∀𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))} (♯‘𝐷) ∈ ℂ) |
| 40 | 3 | olcd 888 | . . . 4 ⊢ (𝑁 ∈ ℕ → ((Base‘(ℤ/nℤ‘𝑁)) ⊆ (ℤ≥‘0) ∨ (Base‘(ℤ/nℤ‘𝑁)) ∈ Fin)) |
| 41 | sumss2 15892 | . . . 4 ⊢ ((({(1r‘(ℤ/nℤ‘𝑁))} ⊆ (Base‘(ℤ/nℤ‘𝑁)) ∧ ∀𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))} (♯‘𝐷) ∈ ℂ) ∧ ((Base‘(ℤ/nℤ‘𝑁)) ⊆ (ℤ≥‘0) ∨ (Base‘(ℤ/nℤ‘𝑁)) ∈ Fin)) → Σ𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))} (♯‘𝐷) = Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))if(𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))}, (♯‘𝐷), 0)) | |
| 42 | 35, 39, 40, 41 | syl21anc 851 | . . 3 ⊢ (𝑁 ∈ ℕ → Σ𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))} (♯‘𝐷) = Σ𝑎 ∈ (Base‘(ℤ/nℤ‘𝑁))if(𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))}, (♯‘𝐷), 0)) |
| 43 | 4 | dchrabl 27581 | . . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
| 44 | ablgrp 19999 | . . . . . 6 ⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) | |
| 45 | 5, 21 | grpidcl 19176 | . . . . . 6 ⊢ (𝐺 ∈ Grp → (0g‘𝐺) ∈ 𝐷) |
| 46 | 43, 44, 45 | 3syl 19 | . . . . 5 ⊢ (𝑁 ∈ ℕ → (0g‘𝐺) ∈ 𝐷) |
| 47 | 46 | snssd 4746 | . . . 4 ⊢ (𝑁 ∈ ℕ → {(0g‘𝐺)} ⊆ 𝐷) |
| 48 | phicl 16946 | . . . . . 6 ⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ ℕ) | |
| 49 | 48 | nncnd 12351 | . . . . 5 ⊢ (𝑁 ∈ ℕ → (ϕ‘𝑁) ∈ ℂ) |
| 50 | 49 | ralrimivw 3158 | . . . 4 ⊢ (𝑁 ∈ ℕ → ∀𝑥 ∈ {(0g‘𝐺)} (ϕ‘𝑁) ∈ ℂ) |
| 51 | 6 | olcd 888 | . . . 4 ⊢ (𝑁 ∈ ℕ → (𝐷 ⊆ (ℤ≥‘0) ∨ 𝐷 ∈ Fin)) |
| 52 | sumss2 15892 | . . . 4 ⊢ ((({(0g‘𝐺)} ⊆ 𝐷 ∧ ∀𝑥 ∈ {(0g‘𝐺)} (ϕ‘𝑁) ∈ ℂ) ∧ (𝐷 ⊆ (ℤ≥‘0) ∨ 𝐷 ∈ Fin)) → Σ𝑥 ∈ {(0g‘𝐺)} (ϕ‘𝑁) = Σ𝑥 ∈ 𝐷 if(𝑥 ∈ {(0g‘𝐺)}, (ϕ‘𝑁), 0)) | |
| 53 | 47, 50, 51, 52 | syl21anc 851 | . . 3 ⊢ (𝑁 ∈ ℕ → Σ𝑥 ∈ {(0g‘𝐺)} (ϕ‘𝑁) = Σ𝑥 ∈ 𝐷 if(𝑥 ∈ {(0g‘𝐺)}, (ϕ‘𝑁), 0)) |
| 54 | 29, 42, 53 | 3eqtr4d 2805 | . 2 ⊢ (𝑁 ∈ ℕ → Σ𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))} (♯‘𝐷) = Σ𝑥 ∈ {(0g‘𝐺)} (ϕ‘𝑁)) |
| 55 | eqidd 2761 | . . . 4 ⊢ (𝑎 = (1r‘(ℤ/nℤ‘𝑁)) → (♯‘𝐷) = (♯‘𝐷)) | |
| 56 | 55 | sumsn 15912 | . . 3 ⊢ (((1r‘(ℤ/nℤ‘𝑁)) ∈ (Base‘(ℤ/nℤ‘𝑁)) ∧ (♯‘𝐷) ∈ ℂ) → Σ𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))} (♯‘𝐷) = (♯‘𝐷)) |
| 57 | 34, 38, 56 | syl2anc 596 | . 2 ⊢ (𝑁 ∈ ℕ → Σ𝑎 ∈ {(1r‘(ℤ/nℤ‘𝑁))} (♯‘𝐷) = (♯‘𝐷)) |
| 58 | eqidd 2761 | . . . 4 ⊢ (𝑥 = (0g‘𝐺) → (ϕ‘𝑁) = (ϕ‘𝑁)) | |
| 59 | 58 | sumsn 15912 | . . 3 ⊢ (((0g‘𝐺) ∈ 𝐷 ∧ (ϕ‘𝑁) ∈ ℂ) → Σ𝑥 ∈ {(0g‘𝐺)} (ϕ‘𝑁) = (ϕ‘𝑁)) |
| 60 | 46, 49, 59 | syl2anc 596 | . 2 ⊢ (𝑁 ∈ ℕ → Σ𝑥 ∈ {(0g‘𝐺)} (ϕ‘𝑁) = (ϕ‘𝑁)) |
| 61 | 54, 57, 60 | 3eqtr3d 2803 | 1 ⊢ (𝑁 ∈ ℕ → (♯‘𝐷) = (ϕ‘𝑁)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1569 ∈ wcel 2144 ∀wral 3076 ⊆ wss 3895 ifcif 4481 {csn 4583 ‘cfv 6538 Fincfn 8973 ℂcc 11198 0cc0 11200 ℕcn 12335 ℕ0cn0 12606 ℤ≥cuz 12965 ♯chash 14474 Σcsu 15853 ϕcphi 16941 Basecbs 17387 0gc0g 17610 Grpcgrp 19144 Abelcabl 19995 1rcur 20407 Ringcrg 20459 CRingccrg 20460 ℤ/nℤczn 21808 DChrcdchr 27559 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-inf2 9642 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278 ax-addf 11279 ax-mulf 11280 |
| This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-tp 4588 df-op 4590 df-uni 4867 df-int 4907 df-iun 4952 df-iin 4953 df-disj 5070 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-isom 6547 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-of 7693 df-rpss 7739 df-om 7878 df-1st 8001 df-2nd 8002 df-supp 8178 df-tpos 8243 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-1o 8476 df-2o 8477 df-oadd 8480 df-omul 8481 df-er 8717 df-ec 8719 df-qs 8723 df-map 8849 df-pm 8850 df-ixp 8926 df-en 8974 df-dom 8975 df-sdom 8976 df-fin 8977 df-fsupp 9354 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9504 df-dju 9982 df-card 10020 df-acn 10023 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-5 12408 df-6 12409 df-7 12410 df-8 12411 df-9 12412 df-n0 12607 df-xnn0 12680 df-z 12694 df-dec 12815 df-uz 12966 df-q 13076 df-rp 13121 df-xneg 13241 df-xadd 13242 df-xmul 13243 df-ioo 13480 df-ioc 13481 df-ico 13482 df-icc 13483 df-fz 13640 df-fzo 13789 df-fl 13932 df-mod 14010 df-seq 14145 df-exp 14205 df-fac 14418 df-bc 14447 df-hash 14475 df-word 14659 df-concat 14716 df-s1 14743 df-shft 15220 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-limsup 15638 df-clim 15655 df-rlim 15656 df-sum 15854 df-ef 16233 df-sin 16235 df-cos 16236 df-pi 16238 df-dvds 16423 df-gcd 16665 df-prm 16847 df-phi 16943 df-pc 17015 df-struct 17325 df-sets 17342 df-slot 17360 df-ndx 17372 df-base 17388 df-ress 17409 df-plusg 17441 df-mulr 17442 df-starv 17443 df-sca 17444 df-vsca 17445 df-ip 17446 df-tset 17447 df-ple 17448 df-ds 17450 df-unif 17451 df-hom 17452 df-cco 17453 df-rest 17593 df-topn 17594 df-0g 17612 df-gsum 17613 df-topgen 17614 df-pt 17615 df-prds 17618 df-xrs 17674 df-qtop 17679 df-imas 17680 df-qus 17681 df-xps 17682 df-mre 17756 df-mrc 17757 df-acs 17759 df-mgm 18816 df-sgrp 18908 df-mnd 18924 df-mhm 18978 df-submnd 18979 df-grp 19147 df-minusg 19148 df-sbg 19149 df-mulg 19278 df-subg 19333 df-nsg 19334 df-eqg 19335 df-ghm 19428 df-gim 19473 df-ga 19504 df-cntz 19531 df-oppg 19560 df-od 19742 df-gex 19743 df-pgp 19744 df-lsm 19850 df-pj1 19851 df-cmn 19996 df-abl 19997 df-cyg 20092 df-dprd 20211 df-dpj 20212 df-mgp 20361 df-rng 20375 df-ur 20408 df-ring 20461 df-cring 20462 df-oppr 20567 df-dvdsr 20587 df-unit 20588 df-invr 20618 df-rhm 20702 df-subrng 20798 df-subrg 20822 df-lmod 21137 df-lss 21207 df-lsp 21247 df-sra 21448 df-rgmod 21449 df-lidl 21486 df-rsp 21487 df-2idl 21543 df-psmet 21670 df-xmet 21671 df-met 21672 df-bl 21673 df-mopn 21674 df-fbas 21675 df-fg 21676 df-cnfld 21679 df-zring 21753 df-zrh 21809 df-zn 21812 df-top 23212 df-topon 23229 df-topsp 23251 df-bases 23264 df-cld 23337 df-ntr 23338 df-cls 23339 df-nei 23416 df-lp 23454 df-perf 23455 df-cn 23545 df-cnp 23546 df-haus 23633 df-tx 23881 df-hmeo 24074 df-fil 24165 df-fm 24257 df-flim 24258 df-flf 24259 df-xms 24639 df-ms 24640 df-tms 24641 df-cncf 25199 df-0p 25991 df-limc 26186 df-dv 26187 df-ply 26506 df-idp 26507 df-coe 26508 df-dgr 26509 df-quot 26612 df-log 26884 df-cxp 26885 df-dchr 27560 |
| This theorem is used by: sumdchr 27599 |
| Copyright terms: Public domain | W3C validator |