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

Theorem pserdv 25694
Description: The derivative of a power series on its region of convergence. (Contributed by Mario Carneiro, 31-Mar-2015.)
Hypotheses
Ref Expression
pserf.g 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
pserf.f 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
pserf.a (𝜑𝐴:ℕ0⟶ℂ)
pserf.r 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
psercn.s 𝑆 = (abs “ (0[,)𝑅))
psercn.m 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))
pserdv.b 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))
Assertion
Ref Expression
pserdv (𝜑 → (ℂ D 𝐹) = (𝑦𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
Distinct variable groups:   𝑗,𝑎,𝑘,𝑛,𝑟,𝑥,𝑦,𝐴   𝑗,𝑀,𝑘,𝑦   𝐵,𝑗,𝑘,𝑥,𝑦   𝑗,𝐺,𝑘,𝑟,𝑦   𝑆,𝑎,𝑗,𝑘,𝑦   𝐹,𝑎   𝜑,𝑎,𝑗,𝑘,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑛,𝑟)   𝐵(𝑛,𝑟,𝑎)   𝑅(𝑥,𝑦,𝑗,𝑘,𝑛,𝑟,𝑎)   𝑆(𝑥,𝑛,𝑟)   𝐹(𝑥,𝑦,𝑗,𝑘,𝑛,𝑟)   𝐺(𝑥,𝑛,𝑎)   𝑀(𝑥,𝑛,𝑟,𝑎)

Proof of Theorem pserdv
StepHypRef Expression
1 dvfcn 25178 . . . . 5 (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
2 ssidd 3955 . . . . . . . 8 (𝜑 → ℂ ⊆ ℂ)
3 pserf.g . . . . . . . . . 10 𝐺 = (𝑥 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑥𝑛))))
4 pserf.f . . . . . . . . . 10 𝐹 = (𝑦𝑆 ↦ Σ𝑗 ∈ ℕ0 ((𝐺𝑦)‘𝑗))
5 pserf.a . . . . . . . . . 10 (𝜑𝐴:ℕ0⟶ℂ)
6 pserf.r . . . . . . . . . 10 𝑅 = sup({𝑟 ∈ ℝ ∣ seq0( + , (𝐺𝑟)) ∈ dom ⇝ }, ℝ*, < )
7 psercn.s . . . . . . . . . 10 𝑆 = (abs “ (0[,)𝑅))
8 psercn.m . . . . . . . . . 10 𝑀 = if(𝑅 ∈ ℝ, (((abs‘𝑎) + 𝑅) / 2), ((abs‘𝑎) + 1))
93, 4, 5, 6, 7, 8psercn 25691 . . . . . . . . 9 (𝜑𝐹 ∈ (𝑆cn→ℂ))
10 cncff 24162 . . . . . . . . 9 (𝐹 ∈ (𝑆cn→ℂ) → 𝐹:𝑆⟶ℂ)
119, 10syl 17 . . . . . . . 8 (𝜑𝐹:𝑆⟶ℂ)
12 cnvimass 6019 . . . . . . . . . . 11 (abs “ (0[,)𝑅)) ⊆ dom abs
13 absf 15148 . . . . . . . . . . . 12 abs:ℂ⟶ℝ
1413fdmi 6663 . . . . . . . . . . 11 dom abs = ℂ
1512, 14sseqtri 3968 . . . . . . . . . 10 (abs “ (0[,)𝑅)) ⊆ ℂ
167, 15eqsstri 3966 . . . . . . . . 9 𝑆 ⊆ ℂ
1716a1i 11 . . . . . . . 8 (𝜑𝑆 ⊆ ℂ)
182, 11, 17dvbss 25171 . . . . . . 7 (𝜑 → dom (ℂ D 𝐹) ⊆ 𝑆)
19 ssidd 3955 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → ℂ ⊆ ℂ)
2011adantr 481 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝐹:𝑆⟶ℂ)
2116a1i 11 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝑆 ⊆ ℂ)
22 pserdv.b . . . . . . . . . . . 12 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))
23 cnxmet 24042 . . . . . . . . . . . . 13 (abs ∘ − ) ∈ (∞Met‘ℂ)
24 0cnd 11069 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 0 ∈ ℂ)
2517sselda 3932 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎𝑆) → 𝑎 ∈ ℂ)
2625abscld 15247 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → (abs‘𝑎) ∈ ℝ)
273, 4, 5, 6, 7, 8psercnlem1 25690 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀𝑀 < 𝑅))
2827simp1d 1141 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ+)
2928rpred 12873 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ)
3026, 29readdcld 11105 . . . . . . . . . . . . . . . 16 ((𝜑𝑎𝑆) → ((abs‘𝑎) + 𝑀) ∈ ℝ)
31 0red 11079 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → 0 ∈ ℝ)
3225absge0d 15255 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → 0 ≤ (abs‘𝑎))
3326, 28ltaddrpd 12906 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → (abs‘𝑎) < ((abs‘𝑎) + 𝑀))
3431, 26, 30, 32, 33lelttrd 11234 . . . . . . . . . . . . . . . 16 ((𝜑𝑎𝑆) → 0 < ((abs‘𝑎) + 𝑀))
3530, 34elrpd 12870 . . . . . . . . . . . . . . 15 ((𝜑𝑎𝑆) → ((abs‘𝑎) + 𝑀) ∈ ℝ+)
3635rphalfcld 12885 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+)
3736rpxrd 12874 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*)
38 blssm 23677 . . . . . . . . . . . . 13 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
3923, 24, 37, 38mp3an2i 1465 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
4022, 39eqsstrid 3980 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝐵 ⊆ ℂ)
41 eqid 2736 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4241cnfldtopon 24052 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
4342toponrestid 22176 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
4441, 43dvres 25181 . . . . . . . . . . 11 (((ℂ ⊆ ℂ ∧ 𝐹:𝑆⟶ℂ) ∧ (𝑆 ⊆ ℂ ∧ 𝐵 ⊆ ℂ)) → (ℂ D (𝐹𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)))
4519, 20, 21, 40, 44syl22anc 836 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)))
46 resss 5948 . . . . . . . . . 10 ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)) ⊆ (ℂ D 𝐹)
4745, 46eqsstrdi 3986 . . . . . . . . 9 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) ⊆ (ℂ D 𝐹))
48 dmss 5844 . . . . . . . . 9 ((ℂ D (𝐹𝐵)) ⊆ (ℂ D 𝐹) → dom (ℂ D (𝐹𝐵)) ⊆ dom (ℂ D 𝐹))
4947, 48syl 17 . . . . . . . 8 ((𝜑𝑎𝑆) → dom (ℂ D (𝐹𝐵)) ⊆ dom (ℂ D 𝐹))
503, 4, 5, 6, 7, 8pserdvlem1 25692 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧ (abs‘𝑎) < (((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅))
513, 4, 5, 6, 7, 50psercnlem2 25689 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∧ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ∧ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆))
5251simp1d 1141 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝑎 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)))
5352, 22eleqtrrdi 2848 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑎𝐵)
543, 4, 5, 6, 7, 8, 22pserdvlem2 25693 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
5554dmeqd 5847 . . . . . . . . . 10 ((𝜑𝑎𝑆) → dom (ℂ D (𝐹𝐵)) = dom (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
56 dmmptg 6180 . . . . . . . . . . 11 (∀𝑦𝐵 Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) ∈ V → dom (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) = 𝐵)
57 sumex 15498 . . . . . . . . . . . 12 Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) ∈ V
5857a1i 11 . . . . . . . . . . 11 (𝑦𝐵 → Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) ∈ V)
5956, 58mprg 3067 . . . . . . . . . 10 dom (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) = 𝐵
6055, 59eqtrdi 2792 . . . . . . . . 9 ((𝜑𝑎𝑆) → dom (ℂ D (𝐹𝐵)) = 𝐵)
6153, 60eleqtrrd 2840 . . . . . . . 8 ((𝜑𝑎𝑆) → 𝑎 ∈ dom (ℂ D (𝐹𝐵)))
6249, 61sseldd 3933 . . . . . . 7 ((𝜑𝑎𝑆) → 𝑎 ∈ dom (ℂ D 𝐹))
6318, 62eqelssd 3953 . . . . . 6 (𝜑 → dom (ℂ D 𝐹) = 𝑆)
6463feq2d 6637 . . . . 5 (𝜑 → ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ↔ (ℂ D 𝐹):𝑆⟶ℂ))
651, 64mpbii 232 . . . 4 (𝜑 → (ℂ D 𝐹):𝑆⟶ℂ)
6665feqmptd 6893 . . 3 (𝜑 → (ℂ D 𝐹) = (𝑎𝑆 ↦ ((ℂ D 𝐹)‘𝑎)))
67 ffun 6654 . . . . . . 7 ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ → Fun (ℂ D 𝐹))
681, 67mp1i 13 . . . . . 6 ((𝜑𝑎𝑆) → Fun (ℂ D 𝐹))
69 funssfv 6846 . . . . . 6 ((Fun (ℂ D 𝐹) ∧ (ℂ D (𝐹𝐵)) ⊆ (ℂ D 𝐹) ∧ 𝑎 ∈ dom (ℂ D (𝐹𝐵))) → ((ℂ D 𝐹)‘𝑎) = ((ℂ D (𝐹𝐵))‘𝑎))
7068, 47, 61, 69syl3anc 1370 . . . . 5 ((𝜑𝑎𝑆) → ((ℂ D 𝐹)‘𝑎) = ((ℂ D (𝐹𝐵))‘𝑎))
7154fveq1d 6827 . . . . 5 ((𝜑𝑎𝑆) → ((ℂ D (𝐹𝐵))‘𝑎) = ((𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))‘𝑎))
72 oveq1 7344 . . . . . . . . 9 (𝑦 = 𝑎 → (𝑦𝑘) = (𝑎𝑘))
7372oveq2d 7353 . . . . . . . 8 (𝑦 = 𝑎 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
7473sumeq2sdv 15515 . . . . . . 7 (𝑦 = 𝑎 → Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
75 eqid 2736 . . . . . . 7 (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
76 sumex 15498 . . . . . . 7 Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)) ∈ V
7774, 75, 76fvmpt 6931 . . . . . 6 (𝑎𝐵 → ((𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))‘𝑎) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
7853, 77syl 17 . . . . 5 ((𝜑𝑎𝑆) → ((𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))‘𝑎) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
7970, 71, 783eqtrd 2780 . . . 4 ((𝜑𝑎𝑆) → ((ℂ D 𝐹)‘𝑎) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
8079mpteq2dva 5192 . . 3 (𝜑 → (𝑎𝑆 ↦ ((ℂ D 𝐹)‘𝑎)) = (𝑎𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘))))
8166, 80eqtrd 2776 . 2 (𝜑 → (ℂ D 𝐹) = (𝑎𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘))))
82 oveq1 7344 . . . . 5 (𝑎 = 𝑦 → (𝑎𝑘) = (𝑦𝑘))
8382oveq2d 7353 . . . 4 (𝑎 = 𝑦 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
8483sumeq2sdv 15515 . . 3 (𝑎 = 𝑦 → Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
8584cbvmptv 5205 . 2 (𝑎𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘))) = (𝑦𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
8681, 85eqtrdi 2792 1 (𝜑 → (ℂ D 𝐹) = (𝑦𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  {crab 3403  Vcvv 3441  wss 3898  ifcif 4473   class class class wbr 5092  cmpt 5175  ccnv 5619  dom cdm 5620  cres 5622  cima 5623  ccom 5624  Fun wfun 6473  wf 6475  cfv 6479  (class class class)co 7337  supcsup 9297  cc 10970  cr 10971  0cc0 10972  1c1 10973   + caddc 10975   · cmul 10977  *cxr 11109   < clt 11110  cmin 11306   / cdiv 11733  2c2 12129  0cn0 12334  +crp 12831  [,)cico 13182  [,]cicc 13183  seqcseq 13822  cexp 13883  abscabs 15044  cli 15292  Σcsu 15496  TopOpenctopn 17229  ∞Metcxmet 20688  ballcbl 20690  fldccnfld 20703  intcnt 22274  cnccncf 24145   D cdv 25133
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 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050  ax-addf 11051  ax-mulf 11052
This theorem depends on definitions:  df-bi 206  df-an 397  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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-supp 8048  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-er 8569  df-map 8688  df-pm 8689  df-ixp 8757  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-fsupp 9227  df-fi 9268  df-sup 9299  df-inf 9300  df-oi 9367  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-5 12140  df-6 12141  df-7 12142  df-8 12143  df-9 12144  df-n0 12335  df-z 12421  df-dec 12539  df-uz 12684  df-q 12790  df-rp 12832  df-xneg 12949  df-xadd 12950  df-xmul 12951  df-ioo 13184  df-ico 13186  df-icc 13187  df-fz 13341  df-fzo 13484  df-fl 13613  df-seq 13823  df-exp 13884  df-hash 14146  df-shft 14877  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-limsup 15279  df-clim 15296  df-rlim 15297  df-sum 15497  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-starv 17074  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ds 17081  df-unif 17082  df-hom 17083  df-cco 17084  df-rest 17230  df-topn 17231  df-0g 17249  df-gsum 17250  df-topgen 17251  df-pt 17252  df-prds 17255  df-xrs 17310  df-qtop 17315  df-imas 17316  df-xps 17318  df-mre 17392  df-mrc 17393  df-acs 17395  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-submnd 18528  df-mulg 18797  df-cntz 19019  df-cmn 19483  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-cnfld 20704  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-lp 22393  df-perf 22394  df-cn 22484  df-cnp 22485  df-haus 22572  df-cmp 22644  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-xms 23579  df-ms 23580  df-tms 23581  df-cncf 24147  df-limc 25136  df-dv 25137  df-ulm 25642
This theorem is referenced by:  pserdv2  25695
  Copyright terms: Public domain W3C validator