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

Theorem itgulm 26362
Description: A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015.)
Hypotheses
Ref Expression
itgulm.z 𝑍 = (β„€β‰₯β€˜π‘€)
itgulm.m (πœ‘ β†’ 𝑀 ∈ β„€)
itgulm.f (πœ‘ β†’ 𝐹:π‘βŸΆπΏ1)
itgulm.u (πœ‘ β†’ 𝐹(β‡π‘’β€˜π‘†)𝐺)
itgulm.s (πœ‘ β†’ (volβ€˜π‘†) ∈ ℝ)
Assertion
Ref Expression
itgulm (πœ‘ β†’ (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) ⇝ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)
Distinct variable groups:   π‘₯,π‘˜,𝐹   π‘˜,𝐺,π‘₯   πœ‘,π‘˜,π‘₯   π‘˜,𝑀,π‘₯   𝑆,π‘˜,π‘₯   π‘˜,𝑍,π‘₯

Proof of Theorem itgulm
Dummy variables 𝑗 𝑛 π‘Ÿ 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 itgulm.z . . . . 5 𝑍 = (β„€β‰₯β€˜π‘€)
2 itgulm.m . . . . . 6 (πœ‘ β†’ 𝑀 ∈ β„€)
32adantr 479 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑀 ∈ β„€)
4 itgulm.f . . . . . . . 8 (πœ‘ β†’ 𝐹:π‘βŸΆπΏ1)
54ffnd 6726 . . . . . . 7 (πœ‘ β†’ 𝐹 Fn 𝑍)
6 itgulm.u . . . . . . 7 (πœ‘ β†’ 𝐹(β‡π‘’β€˜π‘†)𝐺)
7 ulmf2 26338 . . . . . . 7 ((𝐹 Fn 𝑍 ∧ 𝐹(β‡π‘’β€˜π‘†)𝐺) β†’ 𝐹:π‘βŸΆ(β„‚ ↑m 𝑆))
85, 6, 7syl2anc 582 . . . . . 6 (πœ‘ β†’ 𝐹:π‘βŸΆ(β„‚ ↑m 𝑆))
98adantr 479 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐹:π‘βŸΆ(β„‚ ↑m 𝑆))
10 eqidd 2728 . . . . 5 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) β†’ ((πΉβ€˜π‘›)β€˜π‘§) = ((πΉβ€˜π‘›)β€˜π‘§))
11 eqidd 2728 . . . . 5 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑧 ∈ 𝑆) β†’ (πΊβ€˜π‘§) = (πΊβ€˜π‘§))
126adantr 479 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐹(β‡π‘’β€˜π‘†)𝐺)
13 simpr 483 . . . . . 6 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ π‘Ÿ ∈ ℝ+)
14 itgulm.s . . . . . . . 8 (πœ‘ β†’ (volβ€˜π‘†) ∈ ℝ)
1514adantr 479 . . . . . . 7 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (volβ€˜π‘†) ∈ ℝ)
16 ulmcl 26335 . . . . . . . . . . . 12 (𝐹(β‡π‘’β€˜π‘†)𝐺 β†’ 𝐺:π‘†βŸΆβ„‚)
17 fdm 6734 . . . . . . . . . . . 12 (𝐺:π‘†βŸΆβ„‚ β†’ dom 𝐺 = 𝑆)
186, 16, 173syl 18 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝐺 = 𝑆)
191, 2, 4, 6, 14iblulm 26361 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐺 ∈ 𝐿1)
20 iblmbf 25715 . . . . . . . . . . . 12 (𝐺 ∈ 𝐿1 β†’ 𝐺 ∈ MblFn)
21 mbfdm 25573 . . . . . . . . . . . 12 (𝐺 ∈ MblFn β†’ dom 𝐺 ∈ dom vol)
2219, 20, 213syl 18 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝐺 ∈ dom vol)
2318, 22eqeltrrd 2829 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 ∈ dom vol)
24 mblss 25478 . . . . . . . . . 10 (𝑆 ∈ dom vol β†’ 𝑆 βŠ† ℝ)
25 ovolge0 25428 . . . . . . . . . 10 (𝑆 βŠ† ℝ β†’ 0 ≀ (vol*β€˜π‘†))
2623, 24, 253syl 18 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ (vol*β€˜π‘†))
27 mblvol 25477 . . . . . . . . . 10 (𝑆 ∈ dom vol β†’ (volβ€˜π‘†) = (vol*β€˜π‘†))
2823, 27syl 17 . . . . . . . . 9 (πœ‘ β†’ (volβ€˜π‘†) = (vol*β€˜π‘†))
2926, 28breqtrrd 5178 . . . . . . . 8 (πœ‘ β†’ 0 ≀ (volβ€˜π‘†))
3029adantr 479 . . . . . . 7 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ 0 ≀ (volβ€˜π‘†))
3115, 30ge0p1rpd 13084 . . . . . 6 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ ((volβ€˜π‘†) + 1) ∈ ℝ+)
3213, 31rpdivcld 13071 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ ℝ+)
331, 3, 9, 10, 11, 12, 32ulmi 26340 . . . 4 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))
341uztrn2 12877 . . . . . . . 8 ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘—)) β†’ 𝑛 ∈ 𝑍)
358ffvelcdmda 7097 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›) ∈ (β„‚ ↑m 𝑆))
36 elmapi 8872 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘›) ∈ (β„‚ ↑m 𝑆) β†’ (πΉβ€˜π‘›):π‘†βŸΆβ„‚)
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›):π‘†βŸΆβ„‚)
3837ffvelcdmda 7097 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ 𝑍) ∧ π‘₯ ∈ 𝑆) β†’ ((πΉβ€˜π‘›)β€˜π‘₯) ∈ β„‚)
3938adantllr 717 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑛 ∈ 𝑍) ∧ π‘₯ ∈ 𝑆) β†’ ((πΉβ€˜π‘›)β€˜π‘₯) ∈ β„‚)
4039adantlrr 719 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ ((πΉβ€˜π‘›)β€˜π‘₯) ∈ β„‚)
4137feqmptd 6970 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›) = (π‘₯ ∈ 𝑆 ↦ ((πΉβ€˜π‘›)β€˜π‘₯)))
424ffvelcdmda 7097 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›) ∈ 𝐿1)
4341, 42eqeltrrd 2829 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (π‘₯ ∈ 𝑆 ↦ ((πΉβ€˜π‘›)β€˜π‘₯)) ∈ 𝐿1)
4443ad2ant2r 745 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ ((πΉβ€˜π‘›)β€˜π‘₯)) ∈ 𝐿1)
456, 16syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐺:π‘†βŸΆβ„‚)
4645ffvelcdmda 7097 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ (πΊβ€˜π‘₯) ∈ β„‚)
4746ad4ant14 750 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (πΊβ€˜π‘₯) ∈ β„‚)
4845feqmptd 6970 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐺 = (π‘₯ ∈ 𝑆 ↦ (πΊβ€˜π‘₯)))
4948, 19eqeltrrd 2829 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ (πΊβ€˜π‘₯)) ∈ 𝐿1)
5049ad2antrr 724 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ (πΊβ€˜π‘₯)) ∈ 𝐿1)
5140, 44, 47, 50itgsub 25773 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯ = (βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯))
5251fveq2d 6904 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯) = (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)))
5340, 47subcld 11607 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) ∈ β„‚)
5440, 44, 47, 50iblsub 25769 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ (((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) ∈ 𝐿1)
5553, 54itgcl 25731 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯ ∈ β„‚)
5655abscld 15421 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯) ∈ ℝ)
5753abscld 15421 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) ∈ ℝ)
5853, 54iblabs 25776 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)))) ∈ 𝐿1)
5957, 58itgrecl 25745 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯ ∈ ℝ)
60 rpre 13020 . . . . . . . . . . . 12 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ)
6160ad2antlr 725 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ π‘Ÿ ∈ ℝ)
6253, 54itgabs 25782 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯) ≀ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯)
6332adantr 479 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ ℝ+)
6463rpred 13054 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ ℝ)
6514ad2antrr 724 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (volβ€˜π‘†) ∈ ℝ)
6664, 65remulcld 11280 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)) ∈ ℝ)
67 fconstmpt 5742 . . . . . . . . . . . . . . 15 (𝑆 Γ— {(π‘Ÿ / ((volβ€˜π‘†) + 1))}) = (π‘₯ ∈ 𝑆 ↦ (π‘Ÿ / ((volβ€˜π‘†) + 1)))
6823ad2antrr 724 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ 𝑆 ∈ dom vol)
6963rpcnd 13056 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ β„‚)
70 iblconst 25765 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ dom vol ∧ (volβ€˜π‘†) ∈ ℝ ∧ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ β„‚) β†’ (𝑆 Γ— {(π‘Ÿ / ((volβ€˜π‘†) + 1))}) ∈ 𝐿1)
7168, 65, 69, 70syl3anc 1368 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (𝑆 Γ— {(π‘Ÿ / ((volβ€˜π‘†) + 1))}) ∈ 𝐿1)
7267, 71eqeltrrid 2833 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ (π‘Ÿ / ((volβ€˜π‘†) + 1))) ∈ 𝐿1)
7364adantr 479 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ ℝ)
74 simprr 771 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))
75 fveq2 6900 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = π‘₯ β†’ ((πΉβ€˜π‘›)β€˜π‘§) = ((πΉβ€˜π‘›)β€˜π‘₯))
76 fveq2 6900 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = π‘₯ β†’ (πΊβ€˜π‘§) = (πΊβ€˜π‘₯))
7775, 76oveq12d 7442 . . . . . . . . . . . . . . . . . . 19 (𝑧 = π‘₯ β†’ (((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§)) = (((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)))
7877fveq2d 6904 . . . . . . . . . . . . . . . . . 18 (𝑧 = π‘₯ β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) = (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))))
7978breq1d 5160 . . . . . . . . . . . . . . . . 17 (𝑧 = π‘₯ β†’ ((absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) ↔ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) < (π‘Ÿ / ((volβ€˜π‘†) + 1))))
8079rspccva 3608 . . . . . . . . . . . . . . . 16 ((βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∧ π‘₯ ∈ 𝑆) β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))
8174, 80sylan 578 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))
8257, 73, 81ltled 11398 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) ≀ (π‘Ÿ / ((volβ€˜π‘†) + 1)))
8358, 72, 57, 73, 82itgle 25757 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯ ≀ βˆ«π‘†(π‘Ÿ / ((volβ€˜π‘†) + 1)) dπ‘₯)
84 itgconst 25766 . . . . . . . . . . . . . 14 ((𝑆 ∈ dom vol ∧ (volβ€˜π‘†) ∈ ℝ ∧ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ β„‚) β†’ βˆ«π‘†(π‘Ÿ / ((volβ€˜π‘†) + 1)) dπ‘₯ = ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)))
8568, 65, 69, 84syl3anc 1368 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(π‘Ÿ / ((volβ€˜π‘†) + 1)) dπ‘₯ = ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)))
8683, 85breqtrd 5176 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯ ≀ ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)))
8761recnd 11278 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ π‘Ÿ ∈ β„‚)
8865recnd 11278 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (volβ€˜π‘†) ∈ β„‚)
8931adantr 479 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((volβ€˜π‘†) + 1) ∈ ℝ+)
9089rpcnd 13056 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((volβ€˜π‘†) + 1) ∈ β„‚)
9189rpne0d 13059 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((volβ€˜π‘†) + 1) β‰  0)
9287, 88, 90, 91div23d 12063 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((π‘Ÿ Β· (volβ€˜π‘†)) / ((volβ€˜π‘†) + 1)) = ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)))
9365ltp1d 12180 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (volβ€˜π‘†) < ((volβ€˜π‘†) + 1))
94 peano2re 11423 . . . . . . . . . . . . . . . . 17 ((volβ€˜π‘†) ∈ ℝ β†’ ((volβ€˜π‘†) + 1) ∈ ℝ)
9565, 94syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((volβ€˜π‘†) + 1) ∈ ℝ)
96 rpgt0 13024 . . . . . . . . . . . . . . . . 17 (π‘Ÿ ∈ ℝ+ β†’ 0 < π‘Ÿ)
9796ad2antlr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ 0 < π‘Ÿ)
98 ltmul2 12101 . . . . . . . . . . . . . . . 16 (((volβ€˜π‘†) ∈ ℝ ∧ ((volβ€˜π‘†) + 1) ∈ ℝ ∧ (π‘Ÿ ∈ ℝ ∧ 0 < π‘Ÿ)) β†’ ((volβ€˜π‘†) < ((volβ€˜π‘†) + 1) ↔ (π‘Ÿ Β· (volβ€˜π‘†)) < (π‘Ÿ Β· ((volβ€˜π‘†) + 1))))
9965, 95, 61, 97, 98syl112anc 1371 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((volβ€˜π‘†) < ((volβ€˜π‘†) + 1) ↔ (π‘Ÿ Β· (volβ€˜π‘†)) < (π‘Ÿ Β· ((volβ€˜π‘†) + 1))))
10093, 99mpbid 231 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘Ÿ Β· (volβ€˜π‘†)) < (π‘Ÿ Β· ((volβ€˜π‘†) + 1)))
10161, 65remulcld 11280 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘Ÿ Β· (volβ€˜π‘†)) ∈ ℝ)
102101, 61, 89ltdivmul2d 13106 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (((π‘Ÿ Β· (volβ€˜π‘†)) / ((volβ€˜π‘†) + 1)) < π‘Ÿ ↔ (π‘Ÿ Β· (volβ€˜π‘†)) < (π‘Ÿ Β· ((volβ€˜π‘†) + 1))))
103100, 102mpbird 256 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((π‘Ÿ Β· (volβ€˜π‘†)) / ((volβ€˜π‘†) + 1)) < π‘Ÿ)
10492, 103eqbrtrrd 5174 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)) < π‘Ÿ)
10559, 66, 61, 86, 104lelttrd 11408 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯ < π‘Ÿ)
10656, 59, 61, 62, 105lelttrd 11408 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯) < π‘Ÿ)
10752, 106eqbrtrrd 5174 . . . . . . . . 9 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ)
108107expr 455 . . . . . . . 8 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑛 ∈ 𝑍) β†’ (βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
10934, 108sylan2 591 . . . . . . 7 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘—))) β†’ (βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
110109anassrs 466 . . . . . 6 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘—)) β†’ (βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
111110ralimdva 3163 . . . . 5 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
112111reximdva 3164 . . . 4 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
11333, 112mpd 15 . . 3 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ)
114113ralrimiva 3142 . 2 (πœ‘ β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ)
1151fvexi 6914 . . . . 5 𝑍 ∈ V
116115mptex 7239 . . . 4 (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) ∈ V
117116a1i 11 . . 3 (πœ‘ β†’ (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) ∈ V)
118 fveq2 6900 . . . . . . . 8 (π‘˜ = 𝑛 β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘›))
119118fveq1d 6902 . . . . . . 7 (π‘˜ = 𝑛 β†’ ((πΉβ€˜π‘˜)β€˜π‘₯) = ((πΉβ€˜π‘›)β€˜π‘₯))
120119adantr 479 . . . . . 6 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝑆) β†’ ((πΉβ€˜π‘˜)β€˜π‘₯) = ((πΉβ€˜π‘›)β€˜π‘₯))
121120itgeq2dv 25729 . . . . 5 (π‘˜ = 𝑛 β†’ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯ = βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯)
122 eqid 2727 . . . . 5 (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) = (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯)
123 itgex 25718 . . . . 5 βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ ∈ V
124121, 122, 123fvmpt 7008 . . . 4 (𝑛 ∈ 𝑍 β†’ ((π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯)β€˜π‘›) = βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯)
125124adantl 480 . . 3 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ ((π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯)β€˜π‘›) = βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯)
12646, 49itgcl 25731 . . 3 (πœ‘ β†’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯ ∈ β„‚)
12738, 43itgcl 25731 . . 3 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ ∈ β„‚)
1281, 2, 117, 125, 126, 127clim2c 15487 . 2 (πœ‘ β†’ ((π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) ⇝ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯ ↔ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
129114, 128mpbird 256 1 (πœ‘ β†’ (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) ⇝ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  βˆ€wral 3057  βˆƒwrex 3066  Vcvv 3471   βŠ† wss 3947  {csn 4630   class class class wbr 5150   ↦ cmpt 5233   Γ— cxp 5678  dom cdm 5680   Fn wfn 6546  βŸΆwf 6547  β€˜cfv 6551  (class class class)co 7424   ↑m cmap 8849  β„‚cc 11142  β„cr 11143  0cc0 11144  1c1 11145   + caddc 11147   Β· cmul 11149   < clt 11284   ≀ cle 11285   βˆ’ cmin 11480   / cdiv 11907  β„€cz 12594  β„€β‰₯cuz 12858  β„+crp 13012  abscabs 15219   ⇝ cli 15466  vol*covol 25409  volcvol 25410  MblFncmbf 25561  πΏ1cibl 25564  βˆ«citg 25565  β‡π‘’culm 26330
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-rep 5287  ax-sep 5301  ax-nul 5308  ax-pow 5367  ax-pr 5431  ax-un 7744  ax-inf2 9670  ax-cc 10464  ax-cnex 11200  ax-resscn 11201  ax-1cn 11202  ax-icn 11203  ax-addcl 11204  ax-addrcl 11205  ax-mulcl 11206  ax-mulrcl 11207  ax-mulcom 11208  ax-addass 11209  ax-mulass 11210  ax-distr 11211  ax-i2m1 11212  ax-1ne0 11213  ax-1rid 11214  ax-rnegex 11215  ax-rrecex 11216  ax-cnre 11217  ax-pre-lttri 11218  ax-pre-lttrn 11219  ax-pre-ltadd 11220  ax-pre-mulgt0 11221  ax-pre-sup 11222  ax-addf 11223
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4325  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4911  df-int 4952  df-iun 5000  df-iin 5001  df-disj 5116  df-br 5151  df-opab 5213  df-mpt 5234  df-tr 5268  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5635  df-se 5636  df-we 5637  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-pred 6308  df-ord 6375  df-on 6376  df-lim 6377  df-suc 6378  df-iota 6503  df-fun 6553  df-fn 6554  df-f 6555  df-f1 6556  df-fo 6557  df-f1o 6558  df-fv 6559  df-isom 6560  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-of 7689  df-ofr 7690  df-om 7875  df-1st 7997  df-2nd 7998  df-supp 8170  df-frecs 8291  df-wrecs 8322  df-recs 8396  df-rdg 8435  df-1o 8491  df-2o 8492  df-oadd 8495  df-omul 8496  df-er 8729  df-map 8851  df-pm 8852  df-ixp 8921  df-en 8969  df-dom 8970  df-sdom 8971  df-fin 8972  df-fsupp 9392  df-fi 9440  df-sup 9471  df-inf 9472  df-oi 9539  df-dju 9930  df-card 9968  df-acn 9971  df-pnf 11286  df-mnf 11287  df-xr 11288  df-ltxr 11289  df-le 11290  df-sub 11482  df-neg 11483  df-div 11908  df-nn 12249  df-2 12311  df-3 12312  df-4 12313  df-5 12314  df-6 12315  df-7 12316  df-8 12317  df-9 12318  df-n0 12509  df-z 12595  df-dec 12714  df-uz 12859  df-q 12969  df-rp 13013  df-xneg 13130  df-xadd 13131  df-xmul 13132  df-ioo 13366  df-ioc 13367  df-ico 13368  df-icc 13369  df-fz 13523  df-fzo 13666  df-fl 13795  df-mod 13873  df-seq 14005  df-exp 14065  df-hash 14328  df-cj 15084  df-re 15085  df-im 15086  df-sqrt 15220  df-abs 15221  df-limsup 15453  df-clim 15470  df-rlim 15471  df-sum 15671  df-struct 17121  df-sets 17138  df-slot 17156  df-ndx 17168  df-base 17186  df-ress 17215  df-plusg 17251  df-mulr 17252  df-starv 17253  df-sca 17254  df-vsca 17255  df-ip 17256  df-tset 17257  df-ple 17258  df-ds 17260  df-unif 17261  df-hom 17262  df-cco 17263  df-rest 17409  df-topn 17410  df-0g 17428  df-gsum 17429  df-topgen 17430  df-pt 17431  df-prds 17434  df-xrs 17489  df-qtop 17494  df-imas 17495  df-xps 17497  df-mre 17571  df-mrc 17572  df-acs 17574  df-mgm 18605  df-sgrp 18684  df-mnd 18700  df-submnd 18746  df-mulg 19029  df-cntz 19273  df-cmn 19742  df-psmet 21276  df-xmet 21277  df-met 21278  df-bl 21279  df-mopn 21280  df-cnfld 21285  df-top 22814  df-topon 22831  df-topsp 22853  df-bases 22867  df-cn 23149  df-cnp 23150  df-cmp 23309  df-tx 23484  df-hmeo 23677  df-xms 24244  df-ms 24245  df-tms 24246  df-cncf 24816  df-ovol 25411  df-vol 25412  df-mbf 25566  df-itg1 25567  df-itg2 25568  df-ibl 25569  df-itg 25570  df-0p 25617  df-ulm 26331
This theorem is referenced by:  itgulm2  26363
  Copyright terms: Public domain W3C validator