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

Theorem pserdv 25028
 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 24515 . . . . 5 (ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ
2 ssidd 3941 . . . . . . . 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 25025 . . . . . . . . 9 (𝜑𝐹 ∈ (𝑆cn→ℂ))
10 cncff 23502 . . . . . . . . 9 (𝐹 ∈ (𝑆cn→ℂ) → 𝐹:𝑆⟶ℂ)
119, 10syl 17 . . . . . . . 8 (𝜑𝐹:𝑆⟶ℂ)
12 cnvimass 5920 . . . . . . . . . . 11 (abs “ (0[,)𝑅)) ⊆ dom abs
13 absf 14693 . . . . . . . . . . . 12 abs:ℂ⟶ℝ
1413fdmi 6502 . . . . . . . . . . 11 dom abs = ℂ
1512, 14sseqtri 3954 . . . . . . . . . 10 (abs “ (0[,)𝑅)) ⊆ ℂ
167, 15eqsstri 3952 . . . . . . . . 9 𝑆 ⊆ ℂ
1716a1i 11 . . . . . . . 8 (𝜑𝑆 ⊆ ℂ)
182, 11, 17dvbss 24508 . . . . . . 7 (𝜑 → dom (ℂ D 𝐹) ⊆ 𝑆)
19 ssidd 3941 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → ℂ ⊆ ℂ)
2011adantr 484 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝐹:𝑆⟶ℂ)
2116a1i 11 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝑆 ⊆ ℂ)
22 pserdv.b . . . . . . . . . . . 12 𝐵 = (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2))
23 cnxmet 23382 . . . . . . . . . . . . 13 (abs ∘ − ) ∈ (∞Met‘ℂ)
24 0cnd 10627 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → 0 ∈ ℂ)
2517sselda 3918 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎𝑆) → 𝑎 ∈ ℂ)
2625abscld 14792 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → (abs‘𝑎) ∈ ℝ)
273, 4, 5, 6, 7, 8psercnlem1 25024 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑎𝑆) → (𝑀 ∈ ℝ+ ∧ (abs‘𝑎) < 𝑀𝑀 < 𝑅))
2827simp1d 1139 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ+)
2928rpred 12423 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → 𝑀 ∈ ℝ)
3026, 29readdcld 10663 . . . . . . . . . . . . . . . 16 ((𝜑𝑎𝑆) → ((abs‘𝑎) + 𝑀) ∈ ℝ)
31 0red 10637 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → 0 ∈ ℝ)
3225absge0d 14800 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → 0 ≤ (abs‘𝑎))
3326, 28ltaddrpd 12456 . . . . . . . . . . . . . . . . 17 ((𝜑𝑎𝑆) → (abs‘𝑎) < ((abs‘𝑎) + 𝑀))
3431, 26, 30, 32, 33lelttrd 10791 . . . . . . . . . . . . . . . 16 ((𝜑𝑎𝑆) → 0 < ((abs‘𝑎) + 𝑀))
3530, 34elrpd 12420 . . . . . . . . . . . . . . 15 ((𝜑𝑎𝑆) → ((abs‘𝑎) + 𝑀) ∈ ℝ+)
3635rphalfcld 12435 . . . . . . . . . . . . . 14 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+)
3736rpxrd 12424 . . . . . . . . . . . . 13 ((𝜑𝑎𝑆) → (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*)
38 blssm 23029 . . . . . . . . . . . . 13 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ (((abs‘𝑎) + 𝑀) / 2) ∈ ℝ*) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
3923, 24, 37, 38mp3an2i 1463 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ ℂ)
4022, 39eqsstrid 3966 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → 𝐵 ⊆ ℂ)
41 eqid 2801 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4241cnfldtopon 23392 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
4342toponrestid 21530 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
4441, 43dvres 24518 . . . . . . . . . . 11 (((ℂ ⊆ ℂ ∧ 𝐹:𝑆⟶ℂ) ∧ (𝑆 ⊆ ℂ ∧ 𝐵 ⊆ ℂ)) → (ℂ D (𝐹𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)))
4519, 20, 21, 40, 44syl22anc 837 . . . . . . . . . 10 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) = ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)))
46 resss 5847 . . . . . . . . . 10 ((ℂ D 𝐹) ↾ ((int‘(TopOpen‘ℂfld))‘𝐵)) ⊆ (ℂ D 𝐹)
4745, 46eqsstrdi 3972 . . . . . . . . 9 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) ⊆ (ℂ D 𝐹))
48 dmss 5739 . . . . . . . . 9 ((ℂ D (𝐹𝐵)) ⊆ (ℂ D 𝐹) → dom (ℂ D (𝐹𝐵)) ⊆ dom (ℂ D 𝐹))
4947, 48syl 17 . . . . . . . 8 ((𝜑𝑎𝑆) → dom (ℂ D (𝐹𝐵)) ⊆ dom (ℂ D 𝐹))
503, 4, 5, 6, 7, 8pserdvlem1 25026 . . . . . . . . . . . 12 ((𝜑𝑎𝑆) → ((((abs‘𝑎) + 𝑀) / 2) ∈ ℝ+ ∧ (abs‘𝑎) < (((abs‘𝑎) + 𝑀) / 2) ∧ (((abs‘𝑎) + 𝑀) / 2) < 𝑅))
513, 4, 5, 6, 7, 50psercnlem2 25023 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (𝑎 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ∧ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)) ⊆ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ∧ (abs “ (0[,](((abs‘𝑎) + 𝑀) / 2))) ⊆ 𝑆))
5251simp1d 1139 . . . . . . . . . 10 ((𝜑𝑎𝑆) → 𝑎 ∈ (0(ball‘(abs ∘ − ))(((abs‘𝑎) + 𝑀) / 2)))
5352, 22eleqtrrdi 2904 . . . . . . . . 9 ((𝜑𝑎𝑆) → 𝑎𝐵)
543, 4, 5, 6, 7, 8, 22pserdvlem2 25027 . . . . . . . . . . 11 ((𝜑𝑎𝑆) → (ℂ D (𝐹𝐵)) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
5554dmeqd 5742 . . . . . . . . . 10 ((𝜑𝑎𝑆) → dom (ℂ D (𝐹𝐵)) = dom (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
56 dmmptg 6067 . . . . . . . . . . 11 (∀𝑦𝐵 Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) ∈ V → dom (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) = 𝐵)
57 sumex 15040 . . . . . . . . . . . 12 Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) ∈ V
5857a1i 11 . . . . . . . . . . 11 (𝑦𝐵 → Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) ∈ V)
5956, 58mprg 3123 . . . . . . . . . 10 dom (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) = 𝐵
6055, 59eqtrdi 2852 . . . . . . . . 9 ((𝜑𝑎𝑆) → dom (ℂ D (𝐹𝐵)) = 𝐵)
6153, 60eleqtrrd 2896 . . . . . . . 8 ((𝜑𝑎𝑆) → 𝑎 ∈ dom (ℂ D (𝐹𝐵)))
6249, 61sseldd 3919 . . . . . . 7 ((𝜑𝑎𝑆) → 𝑎 ∈ dom (ℂ D 𝐹))
6318, 62eqelssd 3939 . . . . . 6 (𝜑 → dom (ℂ D 𝐹) = 𝑆)
6463feq2d 6477 . . . . 5 (𝜑 → ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ ↔ (ℂ D 𝐹):𝑆⟶ℂ))
651, 64mpbii 236 . . . 4 (𝜑 → (ℂ D 𝐹):𝑆⟶ℂ)
6665feqmptd 6712 . . 3 (𝜑 → (ℂ D 𝐹) = (𝑎𝑆 ↦ ((ℂ D 𝐹)‘𝑎)))
67 ffun 6494 . . . . . . 7 ((ℂ D 𝐹):dom (ℂ D 𝐹)⟶ℂ → Fun (ℂ D 𝐹))
681, 67mp1i 13 . . . . . 6 ((𝜑𝑎𝑆) → Fun (ℂ D 𝐹))
69 funssfv 6670 . . . . . 6 ((Fun (ℂ D 𝐹) ∧ (ℂ D (𝐹𝐵)) ⊆ (ℂ D 𝐹) ∧ 𝑎 ∈ dom (ℂ D (𝐹𝐵))) → ((ℂ D 𝐹)‘𝑎) = ((ℂ D (𝐹𝐵))‘𝑎))
7068, 47, 61, 69syl3anc 1368 . . . . 5 ((𝜑𝑎𝑆) → ((ℂ D 𝐹)‘𝑎) = ((ℂ D (𝐹𝐵))‘𝑎))
7154fveq1d 6651 . . . . 5 ((𝜑𝑎𝑆) → ((ℂ D (𝐹𝐵))‘𝑎) = ((𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))‘𝑎))
72 oveq1 7146 . . . . . . . . 9 (𝑦 = 𝑎 → (𝑦𝑘) = (𝑎𝑘))
7372oveq2d 7155 . . . . . . . 8 (𝑦 = 𝑎 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
7473sumeq2sdv 15057 . . . . . . 7 (𝑦 = 𝑎 → Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
75 eqid 2801 . . . . . . 7 (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))) = (𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
76 sumex 15040 . . . . . . 7 Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)) ∈ V
7774, 75, 76fvmpt 6749 . . . . . 6 (𝑎𝐵 → ((𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))‘𝑎) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
7853, 77syl 17 . . . . 5 ((𝜑𝑎𝑆) → ((𝑦𝐵 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))‘𝑎) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
7970, 71, 783eqtrd 2840 . . . 4 ((𝜑𝑎𝑆) → ((ℂ D 𝐹)‘𝑎) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)))
8079mpteq2dva 5128 . . 3 (𝜑 → (𝑎𝑆 ↦ ((ℂ D 𝐹)‘𝑎)) = (𝑎𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘))))
8166, 80eqtrd 2836 . 2 (𝜑 → (ℂ D 𝐹) = (𝑎𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘))))
82 oveq1 7146 . . . . 5 (𝑎 = 𝑦 → (𝑎𝑘) = (𝑦𝑘))
8382oveq2d 7155 . . . 4 (𝑎 = 𝑦 → (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)) = (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
8483sumeq2sdv 15057 . . 3 (𝑎 = 𝑦 → Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘)) = Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
8584cbvmptv 5136 . 2 (𝑎𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑎𝑘))) = (𝑦𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘)))
8681, 85eqtrdi 2852 1 (𝜑 → (ℂ D 𝐹) = (𝑦𝑆 ↦ Σ𝑘 ∈ ℕ0 (((𝑘 + 1) · (𝐴‘(𝑘 + 1))) · (𝑦𝑘))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2112  {crab 3113  Vcvv 3444   ⊆ wss 3884  ifcif 4428   class class class wbr 5033   ↦ cmpt 5113  ◡ccnv 5522  dom cdm 5523   ↾ cres 5525   “ cima 5526   ∘ ccom 5527  Fun wfun 6322  ⟶wf 6324  ‘cfv 6328  (class class class)co 7139  supcsup 8892  ℂcc 10528  ℝcr 10529  0cc0 10530  1c1 10531   + caddc 10533   · cmul 10535  ℝ*cxr 10667   < clt 10668   − cmin 10863   / cdiv 11290  2c2 11684  ℕ0cn0 11889  ℝ+crp 12381  [,)cico 12732  [,]cicc 12733  seqcseq 13368  ↑cexp 13429  abscabs 14589   ⇝ cli 14837  Σcsu 15038  TopOpenctopn 16691  ∞Metcxmet 20080  ballcbl 20082  ℂfldccnfld 20095  intcnt 21626  –cn→ccncf 23485   D cdv 24470 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-addf 10609  ax-mulf 10610 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-fl 13161  df-seq 13369  df-exp 13430  df-hash 13691  df-shft 14422  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-limsup 14824  df-clim 14841  df-rlim 14842  df-sum 15039  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-rest 16692  df-topn 16693  df-0g 16711  df-gsum 16712  df-topgen 16713  df-pt 16714  df-prds 16717  df-xrs 16771  df-qtop 16776  df-imas 16777  df-xps 16779  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-submnd 17953  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-fbas 20092  df-fg 20093  df-cnfld 20096  df-top 21503  df-topon 21520  df-topsp 21542  df-bases 21555  df-cld 21628  df-ntr 21629  df-cls 21630  df-nei 21707  df-lp 21745  df-perf 21746  df-cn 21836  df-cnp 21837  df-haus 21924  df-cmp 21996  df-tx 22171  df-hmeo 22364  df-fil 22455  df-fm 22547  df-flim 22548  df-flf 22549  df-xms 22931  df-ms 22932  df-tms 22933  df-cncf 23487  df-limc 24473  df-dv 24474  df-ulm 24976 This theorem is referenced by:  pserdv2  25029
 Copyright terms: Public domain W3C validator