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

Theorem itgulm 26295
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 480 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ 𝑀 ∈ β„€)
4 itgulm.f . . . . . . . 8 (πœ‘ β†’ 𝐹:π‘βŸΆπΏ1)
54ffnd 6711 . . . . . . 7 (πœ‘ β†’ 𝐹 Fn 𝑍)
6 itgulm.u . . . . . . 7 (πœ‘ β†’ 𝐹(β‡π‘’β€˜π‘†)𝐺)
7 ulmf2 26271 . . . . . . 7 ((𝐹 Fn 𝑍 ∧ 𝐹(β‡π‘’β€˜π‘†)𝐺) β†’ 𝐹:π‘βŸΆ(β„‚ ↑m 𝑆))
85, 6, 7syl2anc 583 . . . . . 6 (πœ‘ β†’ 𝐹:π‘βŸΆ(β„‚ ↑m 𝑆))
98adantr 480 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐹:π‘βŸΆ(β„‚ ↑m 𝑆))
10 eqidd 2727 . . . . 5 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆)) β†’ ((πΉβ€˜π‘›)β€˜π‘§) = ((πΉβ€˜π‘›)β€˜π‘§))
11 eqidd 2727 . . . . 5 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑧 ∈ 𝑆) β†’ (πΊβ€˜π‘§) = (πΊβ€˜π‘§))
126adantr 480 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ 𝐹(β‡π‘’β€˜π‘†)𝐺)
13 simpr 484 . . . . . 6 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ π‘Ÿ ∈ ℝ+)
14 itgulm.s . . . . . . . 8 (πœ‘ β†’ (volβ€˜π‘†) ∈ ℝ)
1514adantr 480 . . . . . . 7 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (volβ€˜π‘†) ∈ ℝ)
16 ulmcl 26268 . . . . . . . . . . . 12 (𝐹(β‡π‘’β€˜π‘†)𝐺 β†’ 𝐺:π‘†βŸΆβ„‚)
17 fdm 6719 . . . . . . . . . . . 12 (𝐺:π‘†βŸΆβ„‚ β†’ dom 𝐺 = 𝑆)
186, 16, 173syl 18 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝐺 = 𝑆)
191, 2, 4, 6, 14iblulm 26294 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐺 ∈ 𝐿1)
20 iblmbf 25648 . . . . . . . . . . . 12 (𝐺 ∈ 𝐿1 β†’ 𝐺 ∈ MblFn)
21 mbfdm 25506 . . . . . . . . . . . 12 (𝐺 ∈ MblFn β†’ dom 𝐺 ∈ dom vol)
2219, 20, 213syl 18 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝐺 ∈ dom vol)
2318, 22eqeltrrd 2828 . . . . . . . . . 10 (πœ‘ β†’ 𝑆 ∈ dom vol)
24 mblss 25411 . . . . . . . . . 10 (𝑆 ∈ dom vol β†’ 𝑆 βŠ† ℝ)
25 ovolge0 25361 . . . . . . . . . 10 (𝑆 βŠ† ℝ β†’ 0 ≀ (vol*β€˜π‘†))
2623, 24, 253syl 18 . . . . . . . . 9 (πœ‘ β†’ 0 ≀ (vol*β€˜π‘†))
27 mblvol 25410 . . . . . . . . . 10 (𝑆 ∈ dom vol β†’ (volβ€˜π‘†) = (vol*β€˜π‘†))
2823, 27syl 17 . . . . . . . . 9 (πœ‘ β†’ (volβ€˜π‘†) = (vol*β€˜π‘†))
2926, 28breqtrrd 5169 . . . . . . . 8 (πœ‘ β†’ 0 ≀ (volβ€˜π‘†))
3029adantr 480 . . . . . . 7 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ 0 ≀ (volβ€˜π‘†))
3115, 30ge0p1rpd 13049 . . . . . 6 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ ((volβ€˜π‘†) + 1) ∈ ℝ+)
3213, 31rpdivcld 13036 . . . . 5 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ ℝ+)
331, 3, 9, 10, 11, 12, 32ulmi 26273 . . . 4 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))
341uztrn2 12842 . . . . . . . 8 ((𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘—)) β†’ 𝑛 ∈ 𝑍)
358ffvelcdmda 7079 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›) ∈ (β„‚ ↑m 𝑆))
36 elmapi 8842 . . . . . . . . . . . . . . . 16 ((πΉβ€˜π‘›) ∈ (β„‚ ↑m 𝑆) β†’ (πΉβ€˜π‘›):π‘†βŸΆβ„‚)
3735, 36syl 17 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›):π‘†βŸΆβ„‚)
3837ffvelcdmda 7079 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑛 ∈ 𝑍) ∧ π‘₯ ∈ 𝑆) β†’ ((πΉβ€˜π‘›)β€˜π‘₯) ∈ β„‚)
3938adantllr 716 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑛 ∈ 𝑍) ∧ π‘₯ ∈ 𝑆) β†’ ((πΉβ€˜π‘›)β€˜π‘₯) ∈ β„‚)
4039adantlrr 718 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ ((πΉβ€˜π‘›)β€˜π‘₯) ∈ β„‚)
4137feqmptd 6953 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›) = (π‘₯ ∈ 𝑆 ↦ ((πΉβ€˜π‘›)β€˜π‘₯)))
424ffvelcdmda 7079 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (πΉβ€˜π‘›) ∈ 𝐿1)
4341, 42eqeltrrd 2828 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ (π‘₯ ∈ 𝑆 ↦ ((πΉβ€˜π‘›)β€˜π‘₯)) ∈ 𝐿1)
4443ad2ant2r 744 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ ((πΉβ€˜π‘›)β€˜π‘₯)) ∈ 𝐿1)
456, 16syl 17 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐺:π‘†βŸΆβ„‚)
4645ffvelcdmda 7079 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘₯ ∈ 𝑆) β†’ (πΊβ€˜π‘₯) ∈ β„‚)
4746ad4ant14 749 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (πΊβ€˜π‘₯) ∈ β„‚)
4845feqmptd 6953 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐺 = (π‘₯ ∈ 𝑆 ↦ (πΊβ€˜π‘₯)))
4948, 19eqeltrrd 2828 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘₯ ∈ 𝑆 ↦ (πΊβ€˜π‘₯)) ∈ 𝐿1)
5049ad2antrr 723 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ (πΊβ€˜π‘₯)) ∈ 𝐿1)
5140, 44, 47, 50itgsub 25706 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯ = (βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯))
5251fveq2d 6888 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯) = (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)))
5340, 47subcld 11572 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) ∈ β„‚)
5440, 44, 47, 50iblsub 25702 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ (((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) ∈ 𝐿1)
5553, 54itgcl 25664 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯ ∈ β„‚)
5655abscld 15387 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯) ∈ ℝ)
5753abscld 15387 . . . . . . . . . . . 12 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) ∈ ℝ)
5853, 54iblabs 25709 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)))) ∈ 𝐿1)
5957, 58itgrecl 25678 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯ ∈ ℝ)
60 rpre 12985 . . . . . . . . . . . 12 (π‘Ÿ ∈ ℝ+ β†’ π‘Ÿ ∈ ℝ)
6160ad2antlr 724 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ π‘Ÿ ∈ ℝ)
6253, 54itgabs 25715 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯) ≀ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯)
6332adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ ℝ+)
6463rpred 13019 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ ℝ)
6514ad2antrr 723 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (volβ€˜π‘†) ∈ ℝ)
6664, 65remulcld 11245 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)) ∈ ℝ)
67 fconstmpt 5731 . . . . . . . . . . . . . . 15 (𝑆 Γ— {(π‘Ÿ / ((volβ€˜π‘†) + 1))}) = (π‘₯ ∈ 𝑆 ↦ (π‘Ÿ / ((volβ€˜π‘†) + 1)))
6823ad2antrr 723 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ 𝑆 ∈ dom vol)
6963rpcnd 13021 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ β„‚)
70 iblconst 25698 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ dom vol ∧ (volβ€˜π‘†) ∈ ℝ ∧ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ β„‚) β†’ (𝑆 Γ— {(π‘Ÿ / ((volβ€˜π‘†) + 1))}) ∈ 𝐿1)
7168, 65, 69, 70syl3anc 1368 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (𝑆 Γ— {(π‘Ÿ / ((volβ€˜π‘†) + 1))}) ∈ 𝐿1)
7267, 71eqeltrrid 2832 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘₯ ∈ 𝑆 ↦ (π‘Ÿ / ((volβ€˜π‘†) + 1))) ∈ 𝐿1)
7364adantr 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∈ ℝ)
74 simprr 770 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))
75 fveq2 6884 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = π‘₯ β†’ ((πΉβ€˜π‘›)β€˜π‘§) = ((πΉβ€˜π‘›)β€˜π‘₯))
76 fveq2 6884 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = π‘₯ β†’ (πΊβ€˜π‘§) = (πΊβ€˜π‘₯))
7775, 76oveq12d 7422 . . . . . . . . . . . . . . . . . . 19 (𝑧 = π‘₯ β†’ (((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§)) = (((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)))
7877fveq2d 6888 . . . . . . . . . . . . . . . . . 18 (𝑧 = π‘₯ β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) = (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))))
7978breq1d 5151 . . . . . . . . . . . . . . . . 17 (𝑧 = π‘₯ β†’ ((absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) ↔ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) < (π‘Ÿ / ((volβ€˜π‘†) + 1))))
8079rspccva 3605 . . . . . . . . . . . . . . . 16 ((βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) ∧ π‘₯ ∈ 𝑆) β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))
8174, 80sylan 579 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))
8257, 73, 81ltled 11363 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) ∧ π‘₯ ∈ 𝑆) β†’ (absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) ≀ (π‘Ÿ / ((volβ€˜π‘†) + 1)))
8358, 72, 57, 73, 82itgle 25690 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯ ≀ βˆ«π‘†(π‘Ÿ / ((volβ€˜π‘†) + 1)) dπ‘₯)
84 itgconst 25699 . . . . . . . . . . . . . 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 5167 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯ ≀ ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)))
8761recnd 11243 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ π‘Ÿ ∈ β„‚)
8865recnd 11243 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (volβ€˜π‘†) ∈ β„‚)
8931adantr 480 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((volβ€˜π‘†) + 1) ∈ ℝ+)
9089rpcnd 13021 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((volβ€˜π‘†) + 1) ∈ β„‚)
9189rpne0d 13024 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((volβ€˜π‘†) + 1) β‰  0)
9287, 88, 90, 91div23d 12028 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((π‘Ÿ Β· (volβ€˜π‘†)) / ((volβ€˜π‘†) + 1)) = ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)))
9365ltp1d 12145 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (volβ€˜π‘†) < ((volβ€˜π‘†) + 1))
94 peano2re 11388 . . . . . . . . . . . . . . . . 17 ((volβ€˜π‘†) ∈ ℝ β†’ ((volβ€˜π‘†) + 1) ∈ ℝ)
9565, 94syl 17 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((volβ€˜π‘†) + 1) ∈ ℝ)
96 rpgt0 12989 . . . . . . . . . . . . . . . . 17 (π‘Ÿ ∈ ℝ+ β†’ 0 < π‘Ÿ)
9796ad2antlr 724 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ 0 < π‘Ÿ)
98 ltmul2 12066 . . . . . . . . . . . . . . . 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 11245 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (π‘Ÿ Β· (volβ€˜π‘†)) ∈ ℝ)
102101, 61, 89ltdivmul2d 13071 . . . . . . . . . . . . . 14 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (((π‘Ÿ Β· (volβ€˜π‘†)) / ((volβ€˜π‘†) + 1)) < π‘Ÿ ↔ (π‘Ÿ Β· (volβ€˜π‘†)) < (π‘Ÿ Β· ((volβ€˜π‘†) + 1))))
103100, 102mpbird 257 . . . . . . . . . . . . 13 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((π‘Ÿ Β· (volβ€˜π‘†)) / ((volβ€˜π‘†) + 1)) < π‘Ÿ)
10492, 103eqbrtrrd 5165 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ ((π‘Ÿ / ((volβ€˜π‘†) + 1)) Β· (volβ€˜π‘†)) < π‘Ÿ)
10559, 66, 61, 86, 104lelttrd 11373 . . . . . . . . . . 11 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ βˆ«π‘†(absβ€˜(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯))) dπ‘₯ < π‘Ÿ)
10656, 59, 61, 62, 105lelttrd 11373 . . . . . . . . . 10 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜βˆ«π‘†(((πΉβ€˜π‘›)β€˜π‘₯) βˆ’ (πΊβ€˜π‘₯)) dπ‘₯) < π‘Ÿ)
10752, 106eqbrtrrd 5165 . . . . . . . . 9 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑛 ∈ 𝑍 ∧ βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)))) β†’ (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ)
108107expr 456 . . . . . . . 8 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑛 ∈ 𝑍) β†’ (βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
10934, 108sylan2 592 . . . . . . 7 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ (𝑗 ∈ 𝑍 ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘—))) β†’ (βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
110109anassrs 467 . . . . . 6 ((((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) ∧ 𝑛 ∈ (β„€β‰₯β€˜π‘—)) β†’ (βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ (absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
111110ralimdva 3161 . . . . 5 (((πœ‘ ∧ π‘Ÿ ∈ ℝ+) ∧ 𝑗 ∈ 𝑍) β†’ (βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
112111reximdva 3162 . . . 4 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ (βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)βˆ€π‘§ ∈ 𝑆 (absβ€˜(((πΉβ€˜π‘›)β€˜π‘§) βˆ’ (πΊβ€˜π‘§))) < (π‘Ÿ / ((volβ€˜π‘†) + 1)) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
11333, 112mpd 15 . . 3 ((πœ‘ ∧ π‘Ÿ ∈ ℝ+) β†’ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ)
114113ralrimiva 3140 . 2 (πœ‘ β†’ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ)
1151fvexi 6898 . . . . 5 𝑍 ∈ V
116115mptex 7219 . . . 4 (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) ∈ V
117116a1i 11 . . 3 (πœ‘ β†’ (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) ∈ V)
118 fveq2 6884 . . . . . . . 8 (π‘˜ = 𝑛 β†’ (πΉβ€˜π‘˜) = (πΉβ€˜π‘›))
119118fveq1d 6886 . . . . . . 7 (π‘˜ = 𝑛 β†’ ((πΉβ€˜π‘˜)β€˜π‘₯) = ((πΉβ€˜π‘›)β€˜π‘₯))
120119adantr 480 . . . . . 6 ((π‘˜ = 𝑛 ∧ π‘₯ ∈ 𝑆) β†’ ((πΉβ€˜π‘˜)β€˜π‘₯) = ((πΉβ€˜π‘›)β€˜π‘₯))
121120itgeq2dv 25662 . . . . 5 (π‘˜ = 𝑛 β†’ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯ = βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯)
122 eqid 2726 . . . . 5 (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) = (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯)
123 itgex 25651 . . . . 5 βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ ∈ V
124121, 122, 123fvmpt 6991 . . . 4 (𝑛 ∈ 𝑍 β†’ ((π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯)β€˜π‘›) = βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯)
125124adantl 481 . . 3 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ ((π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯)β€˜π‘›) = βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯)
12646, 49itgcl 25664 . . 3 (πœ‘ β†’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯ ∈ β„‚)
12738, 43itgcl 25664 . . 3 ((πœ‘ ∧ 𝑛 ∈ 𝑍) β†’ βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ ∈ β„‚)
1281, 2, 117, 125, 126, 127clim2c 15453 . 2 (πœ‘ β†’ ((π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) ⇝ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯ ↔ βˆ€π‘Ÿ ∈ ℝ+ βˆƒπ‘— ∈ 𝑍 βˆ€π‘› ∈ (β„€β‰₯β€˜π‘—)(absβ€˜(βˆ«π‘†((πΉβ€˜π‘›)β€˜π‘₯) dπ‘₯ βˆ’ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)) < π‘Ÿ))
129114, 128mpbird 257 1 (πœ‘ β†’ (π‘˜ ∈ 𝑍 ↦ βˆ«π‘†((πΉβ€˜π‘˜)β€˜π‘₯) dπ‘₯) ⇝ βˆ«π‘†(πΊβ€˜π‘₯) dπ‘₯)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  βˆ€wral 3055  βˆƒwrex 3064  Vcvv 3468   βŠ† wss 3943  {csn 4623   class class class wbr 5141   ↦ cmpt 5224   Γ— cxp 5667  dom cdm 5669   Fn wfn 6531  βŸΆwf 6532  β€˜cfv 6536  (class class class)co 7404   ↑m cmap 8819  β„‚cc 11107  β„cr 11108  0cc0 11109  1c1 11110   + caddc 11112   Β· cmul 11114   < clt 11249   ≀ cle 11250   βˆ’ cmin 11445   / cdiv 11872  β„€cz 12559  β„€β‰₯cuz 12823  β„+crp 12977  abscabs 15185   ⇝ cli 15432  vol*covol 25342  volcvol 25343  MblFncmbf 25494  πΏ1cibl 25497  βˆ«citg 25498  β‡π‘’culm 26263
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 2163  ax-ext 2697  ax-rep 5278  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7721  ax-inf2 9635  ax-cc 10429  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187  ax-addf 11188
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2704  df-cleq 2718  df-clel 2804  df-nfc 2879  df-ne 2935  df-nel 3041  df-ral 3056  df-rex 3065  df-rmo 3370  df-reu 3371  df-rab 3427  df-v 3470  df-sbc 3773  df-csb 3889  df-dif 3946  df-un 3948  df-in 3950  df-ss 3960  df-pss 3962  df-nul 4318  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4944  df-iun 4992  df-iin 4993  df-disj 5107  df-br 5142  df-opab 5204  df-mpt 5225  df-tr 5259  df-id 5567  df-eprel 5573  df-po 5581  df-so 5582  df-fr 5624  df-se 5625  df-we 5626  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680  df-res 5681  df-ima 5682  df-pred 6293  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6488  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7360  df-ov 7407  df-oprab 7408  df-mpo 7409  df-of 7666  df-ofr 7667  df-om 7852  df-1st 7971  df-2nd 7972  df-supp 8144  df-frecs 8264  df-wrecs 8295  df-recs 8369  df-rdg 8408  df-1o 8464  df-2o 8465  df-oadd 8468  df-omul 8469  df-er 8702  df-map 8821  df-pm 8822  df-ixp 8891  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-fsupp 9361  df-fi 9405  df-sup 9436  df-inf 9437  df-oi 9504  df-dju 9895  df-card 9933  df-acn 9936  df-pnf 11251  df-mnf 11252  df-xr 11253  df-ltxr 11254  df-le 11255  df-sub 11447  df-neg 11448  df-div 11873  df-nn 12214  df-2 12276  df-3 12277  df-4 12278  df-5 12279  df-6 12280  df-7 12281  df-8 12282  df-9 12283  df-n0 12474  df-z 12560  df-dec 12679  df-uz 12824  df-q 12934  df-rp 12978  df-xneg 13095  df-xadd 13096  df-xmul 13097  df-ioo 13331  df-ioc 13332  df-ico 13333  df-icc 13334  df-fz 13488  df-fzo 13631  df-fl 13760  df-mod 13838  df-seq 13970  df-exp 14031  df-hash 14294  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-limsup 15419  df-clim 15436  df-rlim 15437  df-sum 15637  df-struct 17087  df-sets 17104  df-slot 17122  df-ndx 17134  df-base 17152  df-ress 17181  df-plusg 17217  df-mulr 17218  df-starv 17219  df-sca 17220  df-vsca 17221  df-ip 17222  df-tset 17223  df-ple 17224  df-ds 17226  df-unif 17227  df-hom 17228  df-cco 17229  df-rest 17375  df-topn 17376  df-0g 17394  df-gsum 17395  df-topgen 17396  df-pt 17397  df-prds 17400  df-xrs 17455  df-qtop 17460  df-imas 17461  df-xps 17463  df-mre 17537  df-mrc 17538  df-acs 17540  df-mgm 18571  df-sgrp 18650  df-mnd 18666  df-submnd 18712  df-mulg 18994  df-cntz 19231  df-cmn 19700  df-psmet 21228  df-xmet 21229  df-met 21230  df-bl 21231  df-mopn 21232  df-cnfld 21237  df-top 22747  df-topon 22764  df-topsp 22786  df-bases 22800  df-cn 23082  df-cnp 23083  df-cmp 23242  df-tx 23417  df-hmeo 23610  df-xms 24177  df-ms 24178  df-tms 24179  df-cncf 24749  df-ovol 25344  df-vol 25345  df-mbf 25499  df-itg1 25500  df-itg2 25501  df-ibl 25502  df-itg 25503  df-0p 25550  df-ulm 26264
This theorem is referenced by:  itgulm2  26296
  Copyright terms: Public domain W3C validator