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

Theorem dvfsumrlim2 23706
 Description: Compare a finite sum to an integral (the integral here is given as a function with a known derivative). The statement here says that if 𝑥 ∈ 𝑆 ↦ 𝐵 is a decreasing function with antiderivative 𝐴 converging to zero, then the difference between Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐵(𝑘) and ∫𝑢 ∈ (𝑀[,]𝑥)𝐵(𝑢) d𝑢 = 𝐴(𝑥) converges to a constant limit value, with the remainder term bounded by 𝐵(𝑥). (Contributed by Mario Carneiro, 18-May-2016.)
Hypotheses
Ref Expression
dvfsum.s 𝑆 = (𝑇(,)+∞)
dvfsum.z 𝑍 = (ℤ𝑀)
dvfsum.m (𝜑𝑀 ∈ ℤ)
dvfsum.d (𝜑𝐷 ∈ ℝ)
dvfsum.md (𝜑𝑀 ≤ (𝐷 + 1))
dvfsum.t (𝜑𝑇 ∈ ℝ)
dvfsum.a ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
dvfsum.b1 ((𝜑𝑥𝑆) → 𝐵𝑉)
dvfsum.b2 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
dvfsum.b3 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
dvfsum.c (𝑥 = 𝑘𝐵 = 𝐶)
dvfsumrlim.l ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘)) → 𝐶𝐵)
dvfsumrlim.g 𝐺 = (𝑥𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴))
dvfsumrlim.k (𝜑 → (𝑥𝑆𝐵) ⇝𝑟 0)
dvfsumrlim2.1 (𝜑𝑋𝑆)
dvfsumrlim2.2 (𝜑𝐷𝑋)
Assertion
Ref Expression
dvfsumrlim2 ((𝜑𝐺𝑟 𝐿) → (abs‘((𝐺𝑋) − 𝐿)) ≤ 𝑋 / 𝑥𝐵)
Distinct variable groups:   𝐵,𝑘   𝑥,𝐶   𝑥,𝑘,𝐷   𝜑,𝑘,𝑥   𝑆,𝑘,𝑥   𝑘,𝑀,𝑥   𝑥,𝑇   𝑥,𝑍   𝑘,𝑋,𝑥
Allowed substitution hints:   𝐴(𝑥,𝑘)   𝐵(𝑥)   𝐶(𝑘)   𝑇(𝑘)   𝐺(𝑥,𝑘)   𝐿(𝑥,𝑘)   𝑉(𝑥,𝑘)   𝑍(𝑘)

Proof of Theorem dvfsumrlim2
Dummy variables 𝑦 𝑧 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dvfsum.s . . . . . . 7 𝑆 = (𝑇(,)+∞)
2 ioossre 12180 . . . . . . 7 (𝑇(,)+∞) ⊆ ℝ
31, 2eqsstri 3616 . . . . . 6 𝑆 ⊆ ℝ
4 dvfsumrlim2.1 . . . . . 6 (𝜑𝑋𝑆)
53, 4sseldi 3582 . . . . 5 (𝜑𝑋 ∈ ℝ)
65rexrd 10036 . . . 4 (𝜑𝑋 ∈ ℝ*)
75renepnfd 10037 . . . 4 (𝜑𝑋 ≠ +∞)
8 icopnfsup 12607 . . . 4 ((𝑋 ∈ ℝ*𝑋 ≠ +∞) → sup((𝑋[,)+∞), ℝ*, < ) = +∞)
96, 7, 8syl2anc 692 . . 3 (𝜑 → sup((𝑋[,)+∞), ℝ*, < ) = +∞)
109adantr 481 . 2 ((𝜑𝐺𝑟 𝐿) → sup((𝑋[,)+∞), ℝ*, < ) = +∞)
11 dvfsum.z . . . . . . . 8 𝑍 = (ℤ𝑀)
12 dvfsum.m . . . . . . . 8 (𝜑𝑀 ∈ ℤ)
13 dvfsum.d . . . . . . . 8 (𝜑𝐷 ∈ ℝ)
14 dvfsum.md . . . . . . . 8 (𝜑𝑀 ≤ (𝐷 + 1))
15 dvfsum.t . . . . . . . 8 (𝜑𝑇 ∈ ℝ)
16 dvfsum.a . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐴 ∈ ℝ)
17 dvfsum.b1 . . . . . . . 8 ((𝜑𝑥𝑆) → 𝐵𝑉)
18 dvfsum.b2 . . . . . . . 8 ((𝜑𝑥𝑍) → 𝐵 ∈ ℝ)
19 dvfsum.b3 . . . . . . . 8 (𝜑 → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
20 dvfsum.c . . . . . . . 8 (𝑥 = 𝑘𝐵 = 𝐶)
21 dvfsumrlim.g . . . . . . . 8 𝐺 = (𝑥𝑆 ↦ (Σ𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴))
221, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21dvfsumrlimf 23699 . . . . . . 7 (𝜑𝐺:𝑆⟶ℝ)
2322ad2antrr 761 . . . . . 6 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝐺:𝑆⟶ℝ)
244ad2antrr 761 . . . . . 6 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑋𝑆)
2523, 24ffvelrnd 6318 . . . . 5 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (𝐺𝑋) ∈ ℝ)
2625recnd 10015 . . . 4 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (𝐺𝑋) ∈ ℂ)
2715rexrd 10036 . . . . . . . . . 10 (𝜑𝑇 ∈ ℝ*)
284, 1syl6eleq 2708 . . . . . . . . . . . 12 (𝜑𝑋 ∈ (𝑇(,)+∞))
29 elioopnf 12212 . . . . . . . . . . . . 13 (𝑇 ∈ ℝ* → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
3027, 29syl 17 . . . . . . . . . . . 12 (𝜑 → (𝑋 ∈ (𝑇(,)+∞) ↔ (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋)))
3128, 30mpbid 222 . . . . . . . . . . 11 (𝜑 → (𝑋 ∈ ℝ ∧ 𝑇 < 𝑋))
3231simprd 479 . . . . . . . . . 10 (𝜑𝑇 < 𝑋)
33 df-ioo 12124 . . . . . . . . . . 11 (,) = (𝑢 ∈ ℝ*, 𝑣 ∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢 < 𝑤𝑤 < 𝑣)})
34 df-ico 12126 . . . . . . . . . . 11 [,) = (𝑢 ∈ ℝ*, 𝑣 ∈ ℝ* ↦ {𝑤 ∈ ℝ* ∣ (𝑢𝑤𝑤 < 𝑣)})
35 xrltletr 11935 . . . . . . . . . . 11 ((𝑇 ∈ ℝ*𝑋 ∈ ℝ*𝑧 ∈ ℝ*) → ((𝑇 < 𝑋𝑋𝑧) → 𝑇 < 𝑧))
3633, 34, 35ixxss1 12138 . . . . . . . . . 10 ((𝑇 ∈ ℝ*𝑇 < 𝑋) → (𝑋[,)+∞) ⊆ (𝑇(,)+∞))
3727, 32, 36syl2anc 692 . . . . . . . . 9 (𝜑 → (𝑋[,)+∞) ⊆ (𝑇(,)+∞))
3837, 1syl6sseqr 3633 . . . . . . . 8 (𝜑 → (𝑋[,)+∞) ⊆ 𝑆)
3938adantr 481 . . . . . . 7 ((𝜑𝐺𝑟 𝐿) → (𝑋[,)+∞) ⊆ 𝑆)
4039sselda 3584 . . . . . 6 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑦𝑆)
4123, 40ffvelrnd 6318 . . . . 5 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (𝐺𝑦) ∈ ℝ)
4241recnd 10015 . . . 4 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (𝐺𝑦) ∈ ℂ)
4326, 42subcld 10339 . . 3 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → ((𝐺𝑋) − (𝐺𝑦)) ∈ ℂ)
44 pnfxr 10039 . . . . . . 7 +∞ ∈ ℝ*
45 icossre 12199 . . . . . . 7 ((𝑋 ∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑋[,)+∞) ⊆ ℝ)
465, 44, 45sylancl 693 . . . . . 6 (𝜑 → (𝑋[,)+∞) ⊆ ℝ)
4746adantr 481 . . . . 5 ((𝜑𝐺𝑟 𝐿) → (𝑋[,)+∞) ⊆ ℝ)
48 rlimf 14169 . . . . . . . 8 (𝐺𝑟 𝐿𝐺:dom 𝐺⟶ℂ)
4948adantl 482 . . . . . . 7 ((𝜑𝐺𝑟 𝐿) → 𝐺:dom 𝐺⟶ℂ)
50 ovex 6635 . . . . . . . . 9 𝑘 ∈ (𝑀...(⌊‘𝑥))𝐶𝐴) ∈ V
5150, 21dmmpti 5982 . . . . . . . 8 dom 𝐺 = 𝑆
5251feq2i 5996 . . . . . . 7 (𝐺:dom 𝐺⟶ℂ ↔ 𝐺:𝑆⟶ℂ)
5349, 52sylib 208 . . . . . 6 ((𝜑𝐺𝑟 𝐿) → 𝐺:𝑆⟶ℂ)
544adantr 481 . . . . . 6 ((𝜑𝐺𝑟 𝐿) → 𝑋𝑆)
5553, 54ffvelrnd 6318 . . . . 5 ((𝜑𝐺𝑟 𝐿) → (𝐺𝑋) ∈ ℂ)
56 rlimconst 14212 . . . . 5 (((𝑋[,)+∞) ⊆ ℝ ∧ (𝐺𝑋) ∈ ℂ) → (𝑦 ∈ (𝑋[,)+∞) ↦ (𝐺𝑋)) ⇝𝑟 (𝐺𝑋))
5747, 55, 56syl2anc 692 . . . 4 ((𝜑𝐺𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ (𝐺𝑋)) ⇝𝑟 (𝐺𝑋))
5853feqmptd 6208 . . . . . 6 ((𝜑𝐺𝑟 𝐿) → 𝐺 = (𝑦𝑆 ↦ (𝐺𝑦)))
59 simpr 477 . . . . . 6 ((𝜑𝐺𝑟 𝐿) → 𝐺𝑟 𝐿)
6058, 59eqbrtrrd 4639 . . . . 5 ((𝜑𝐺𝑟 𝐿) → (𝑦𝑆 ↦ (𝐺𝑦)) ⇝𝑟 𝐿)
6139, 60rlimres2 14229 . . . 4 ((𝜑𝐺𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ (𝐺𝑦)) ⇝𝑟 𝐿)
6226, 42, 57, 61rlimsub 14311 . . 3 ((𝜑𝐺𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ ((𝐺𝑋) − (𝐺𝑦))) ⇝𝑟 ((𝐺𝑋) − 𝐿))
6343, 62rlimabs 14276 . 2 ((𝜑𝐺𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ (abs‘((𝐺𝑋) − (𝐺𝑦)))) ⇝𝑟 (abs‘((𝐺𝑋) − 𝐿)))
643a1i 11 . . . . . . . 8 (𝜑𝑆 ⊆ ℝ)
6564, 16, 17, 19dvmptrecl 23698 . . . . . . 7 ((𝜑𝑥𝑆) → 𝐵 ∈ ℝ)
6665ralrimiva 2960 . . . . . 6 (𝜑 → ∀𝑥𝑆 𝐵 ∈ ℝ)
67 nfcsb1v 3531 . . . . . . . 8 𝑥𝑋 / 𝑥𝐵
6867nfel1 2775 . . . . . . 7 𝑥𝑋 / 𝑥𝐵 ∈ ℝ
69 csbeq1a 3524 . . . . . . . 8 (𝑥 = 𝑋𝐵 = 𝑋 / 𝑥𝐵)
7069eleq1d 2683 . . . . . . 7 (𝑥 = 𝑋 → (𝐵 ∈ ℝ ↔ 𝑋 / 𝑥𝐵 ∈ ℝ))
7168, 70rspc 3289 . . . . . 6 (𝑋𝑆 → (∀𝑥𝑆 𝐵 ∈ ℝ → 𝑋 / 𝑥𝐵 ∈ ℝ))
724, 66, 71sylc 65 . . . . 5 (𝜑𝑋 / 𝑥𝐵 ∈ ℝ)
7372recnd 10015 . . . 4 (𝜑𝑋 / 𝑥𝐵 ∈ ℂ)
74 rlimconst 14212 . . . 4 (((𝑋[,)+∞) ⊆ ℝ ∧ 𝑋 / 𝑥𝐵 ∈ ℂ) → (𝑦 ∈ (𝑋[,)+∞) ↦ 𝑋 / 𝑥𝐵) ⇝𝑟 𝑋 / 𝑥𝐵)
7546, 73, 74syl2anc 692 . . 3 (𝜑 → (𝑦 ∈ (𝑋[,)+∞) ↦ 𝑋 / 𝑥𝐵) ⇝𝑟 𝑋 / 𝑥𝐵)
7675adantr 481 . 2 ((𝜑𝐺𝑟 𝐿) → (𝑦 ∈ (𝑋[,)+∞) ↦ 𝑋 / 𝑥𝐵) ⇝𝑟 𝑋 / 𝑥𝐵)
7743abscld 14112 . 2 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺𝑋) − (𝐺𝑦))) ∈ ℝ)
7872ad2antrr 761 . 2 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → 𝑋 / 𝑥𝐵 ∈ ℝ)
7926, 42abssubd 14129 . . 3 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺𝑋) − (𝐺𝑦))) = (abs‘((𝐺𝑦) − (𝐺𝑋))))
8012adantr 481 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝑀 ∈ ℤ)
8113adantr 481 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝐷 ∈ ℝ)
8214adantr 481 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝑀 ≤ (𝐷 + 1))
8315adantr 481 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝑇 ∈ ℝ)
8416adantlr 750 . . . . 5 (((𝜑𝑦 ∈ (𝑋[,)+∞)) ∧ 𝑥𝑆) → 𝐴 ∈ ℝ)
8517adantlr 750 . . . . 5 (((𝜑𝑦 ∈ (𝑋[,)+∞)) ∧ 𝑥𝑆) → 𝐵𝑉)
8618adantlr 750 . . . . 5 (((𝜑𝑦 ∈ (𝑋[,)+∞)) ∧ 𝑥𝑍) → 𝐵 ∈ ℝ)
8719adantr 481 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → (ℝ D (𝑥𝑆𝐴)) = (𝑥𝑆𝐵))
8844a1i 11 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → +∞ ∈ ℝ*)
89 3simpa 1056 . . . . . . 7 ((𝐷𝑥𝑥𝑘𝑘 ≤ +∞) → (𝐷𝑥𝑥𝑘))
90 dvfsumrlim.l . . . . . . 7 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘)) → 𝐶𝐵)
9189, 90syl3an3 1358 . . . . . 6 ((𝜑 ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘 ≤ +∞)) → 𝐶𝐵)
92913adant1r 1316 . . . . 5 (((𝜑𝑦 ∈ (𝑋[,)+∞)) ∧ (𝑥𝑆𝑘𝑆) ∧ (𝐷𝑥𝑥𝑘𝑘 ≤ +∞)) → 𝐶𝐵)
93 dvfsumrlim.k . . . . . . . 8 (𝜑 → (𝑥𝑆𝐵) ⇝𝑟 0)
941, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 90, 21, 93dvfsumrlimge0 23704 . . . . . . 7 ((𝜑 ∧ (𝑥𝑆𝐷𝑥)) → 0 ≤ 𝐵)
95943adantr3 1220 . . . . . 6 ((𝜑 ∧ (𝑥𝑆𝐷𝑥𝑥 ≤ +∞)) → 0 ≤ 𝐵)
9695adantlr 750 . . . . 5 (((𝜑𝑦 ∈ (𝑋[,)+∞)) ∧ (𝑥𝑆𝐷𝑥𝑥 ≤ +∞)) → 0 ≤ 𝐵)
974adantr 481 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝑋𝑆)
9838sselda 3584 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝑦𝑆)
99 dvfsumrlim2.2 . . . . . 6 (𝜑𝐷𝑋)
10099adantr 481 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝐷𝑋)
101 elicopnf 12214 . . . . . . 7 (𝑋 ∈ ℝ → (𝑦 ∈ (𝑋[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑋𝑦)))
1025, 101syl 17 . . . . . 6 (𝜑 → (𝑦 ∈ (𝑋[,)+∞) ↔ (𝑦 ∈ ℝ ∧ 𝑋𝑦)))
103102simplbda 653 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝑋𝑦)
104102simprbda 652 . . . . . . 7 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝑦 ∈ ℝ)
105104rexrd 10036 . . . . . 6 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝑦 ∈ ℝ*)
106 pnfge 11911 . . . . . 6 (𝑦 ∈ ℝ*𝑦 ≤ +∞)
107105, 106syl 17 . . . . 5 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → 𝑦 ≤ +∞)
1081, 11, 80, 81, 82, 83, 84, 85, 86, 87, 20, 88, 92, 21, 96, 97, 98, 100, 103, 107dvfsumlem4 23703 . . . 4 ((𝜑𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺𝑦) − (𝐺𝑋))) ≤ 𝑋 / 𝑥𝐵)
109108adantlr 750 . . 3 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺𝑦) − (𝐺𝑋))) ≤ 𝑋 / 𝑥𝐵)
11079, 109eqbrtrd 4637 . 2 (((𝜑𝐺𝑟 𝐿) ∧ 𝑦 ∈ (𝑋[,)+∞)) → (abs‘((𝐺𝑋) − (𝐺𝑦))) ≤ 𝑋 / 𝑥𝐵)
11110, 63, 76, 77, 78, 110rlimle 14315 1 ((𝜑𝐺𝑟 𝐿) → (abs‘((𝐺𝑋) − 𝐿)) ≤ 𝑋 / 𝑥𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 384   ∧ w3a 1036   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  ∀wral 2907  ⦋csb 3515   ⊆ wss 3556   class class class wbr 4615   ↦ cmpt 4675  dom cdm 5076  ⟶wf 5845  ‘cfv 5849  (class class class)co 6607  supcsup 8293  ℂcc 9881  ℝcr 9882  0cc0 9883  1c1 9884   + caddc 9886  +∞cpnf 10018  ℝ*cxr 10020   < clt 10021   ≤ cle 10022   − cmin 10213  ℤcz 11324  ℤ≥cuz 11634  (,)cioo 12120  [,)cico 12122  ...cfz 12271  ⌊cfl 12534  abscabs 13911   ⇝𝑟 crli 14153  Σcsu 14353   D cdv 23540 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-inf2 8485  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960  ax-pre-sup 9961  ax-addf 9962  ax-mulf 9963 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-iin 4490  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-se 5036  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-isom 5858  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-of 6853  df-om 7016  df-1st 7116  df-2nd 7117  df-supp 7244  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-2o 7509  df-oadd 7512  df-er 7690  df-map 7807  df-pm 7808  df-ixp 7856  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-fsupp 8223  df-fi 8264  df-sup 8295  df-inf 8296  df-oi 8362  df-card 8712  df-cda 8937  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-div 10632  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-5 11029  df-6 11030  df-7 11031  df-8 11032  df-9 11033  df-n0 11240  df-z 11325  df-dec 11441  df-uz 11635  df-q 11736  df-rp 11780  df-xneg 11893  df-xadd 11894  df-xmul 11895  df-ioo 12124  df-ico 12126  df-icc 12127  df-fz 12272  df-fzo 12410  df-fl 12536  df-seq 12745  df-exp 12804  df-hash 13061  df-cj 13776  df-re 13777  df-im 13778  df-sqrt 13912  df-abs 13913  df-clim 14156  df-rlim 14157  df-sum 14354  df-struct 15786  df-ndx 15787  df-slot 15788  df-base 15789  df-sets 15790  df-ress 15791  df-plusg 15878  df-mulr 15879  df-starv 15880  df-sca 15881  df-vsca 15882  df-ip 15883  df-tset 15884  df-ple 15885  df-ds 15888  df-unif 15889  df-hom 15890  df-cco 15891  df-rest 16007  df-topn 16008  df-0g 16026  df-gsum 16027  df-topgen 16028  df-pt 16029  df-prds 16032  df-xrs 16086  df-qtop 16091  df-imas 16092  df-xps 16094  df-mre 16170  df-mrc 16171  df-acs 16173  df-mgm 17166  df-sgrp 17208  df-mnd 17219  df-submnd 17260  df-mulg 17465  df-cntz 17674  df-cmn 18119  df-psmet 19660  df-xmet 19661  df-met 19662  df-bl 19663  df-mopn 19664  df-fbas 19665  df-fg 19666  df-cnfld 19669  df-top 20621  df-topon 20638  df-topsp 20651  df-bases 20664  df-cld 20736  df-ntr 20737  df-cls 20738  df-nei 20815  df-lp 20853  df-perf 20854  df-cn 20944  df-cnp 20945  df-haus 21032  df-cmp 21103  df-tx 21278  df-hmeo 21471  df-fil 21563  df-fm 21655  df-flim 21656  df-flf 21657  df-xms 22038  df-ms 22039  df-tms 22040  df-cncf 22594  df-limc 23543  df-dv 23544 This theorem is referenced by:  dvfsumrlim3  23707
 Copyright terms: Public domain W3C validator