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

Theorem itgulm 24073
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 481 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → 𝑀 ∈ ℤ)
4 itgulm.f . . . . . . . 8 (𝜑𝐹:𝑍⟶𝐿1)
5 ffn 6004 . . . . . . . 8 (𝐹:𝑍⟶𝐿1𝐹 Fn 𝑍)
64, 5syl 17 . . . . . . 7 (𝜑𝐹 Fn 𝑍)
7 itgulm.u . . . . . . 7 (𝜑𝐹(⇝𝑢𝑆)𝐺)
8 ulmf2 24049 . . . . . . 7 ((𝐹 Fn 𝑍𝐹(⇝𝑢𝑆)𝐺) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
96, 7, 8syl2anc 692 . . . . . 6 (𝜑𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
109adantr 481 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → 𝐹:𝑍⟶(ℂ ↑𝑚 𝑆))
11 eqidd 2622 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍𝑧𝑆)) → ((𝐹𝑛)‘𝑧) = ((𝐹𝑛)‘𝑧))
12 eqidd 2622 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑧𝑆) → (𝐺𝑧) = (𝐺𝑧))
137adantr 481 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → 𝐹(⇝𝑢𝑆)𝐺)
14 simpr 477 . . . . . 6 ((𝜑𝑟 ∈ ℝ+) → 𝑟 ∈ ℝ+)
15 itgulm.s . . . . . . . 8 (𝜑 → (vol‘𝑆) ∈ ℝ)
1615adantr 481 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → (vol‘𝑆) ∈ ℝ)
17 ulmcl 24046 . . . . . . . . . . . 12 (𝐹(⇝𝑢𝑆)𝐺𝐺:𝑆⟶ℂ)
18 fdm 6010 . . . . . . . . . . . 12 (𝐺:𝑆⟶ℂ → dom 𝐺 = 𝑆)
197, 17, 183syl 18 . . . . . . . . . . 11 (𝜑 → dom 𝐺 = 𝑆)
201, 2, 4, 7, 15iblulm 24072 . . . . . . . . . . . 12 (𝜑𝐺 ∈ 𝐿1)
21 iblmbf 23447 . . . . . . . . . . . 12 (𝐺 ∈ 𝐿1𝐺 ∈ MblFn)
22 mbfdm 23308 . . . . . . . . . . . 12 (𝐺 ∈ MblFn → dom 𝐺 ∈ dom vol)
2320, 21, 223syl 18 . . . . . . . . . . 11 (𝜑 → dom 𝐺 ∈ dom vol)
2419, 23eqeltrrd 2699 . . . . . . . . . 10 (𝜑𝑆 ∈ dom vol)
25 mblss 23212 . . . . . . . . . 10 (𝑆 ∈ dom vol → 𝑆 ⊆ ℝ)
26 ovolge0 23162 . . . . . . . . . 10 (𝑆 ⊆ ℝ → 0 ≤ (vol*‘𝑆))
2724, 25, 263syl 18 . . . . . . . . 9 (𝜑 → 0 ≤ (vol*‘𝑆))
28 mblvol 23211 . . . . . . . . . 10 (𝑆 ∈ dom vol → (vol‘𝑆) = (vol*‘𝑆))
2924, 28syl 17 . . . . . . . . 9 (𝜑 → (vol‘𝑆) = (vol*‘𝑆))
3027, 29breqtrrd 4643 . . . . . . . 8 (𝜑 → 0 ≤ (vol‘𝑆))
3130adantr 481 . . . . . . 7 ((𝜑𝑟 ∈ ℝ+) → 0 ≤ (vol‘𝑆))
3216, 31ge0p1rpd 11849 . . . . . 6 ((𝜑𝑟 ∈ ℝ+) → ((vol‘𝑆) + 1) ∈ ℝ+)
3314, 32rpdivcld 11836 . . . . 5 ((𝜑𝑟 ∈ ℝ+) → (𝑟 / ((vol‘𝑆) + 1)) ∈ ℝ+)
341, 3, 10, 11, 12, 13, 33ulmi 24051 . . . 4 ((𝜑𝑟 ∈ ℝ+) → ∃𝑗𝑍𝑛 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))
351uztrn2 11652 . . . . . . . 8 ((𝑗𝑍𝑛 ∈ (ℤ𝑗)) → 𝑛𝑍)
369ffvelrnda 6317 . . . . . . . . . . . . . . . 16 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ (ℂ ↑𝑚 𝑆))
37 elmapi 7826 . . . . . . . . . . . . . . . 16 ((𝐹𝑛) ∈ (ℂ ↑𝑚 𝑆) → (𝐹𝑛):𝑆⟶ℂ)
3836, 37syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑛𝑍) → (𝐹𝑛):𝑆⟶ℂ)
3938ffvelrnda 6317 . . . . . . . . . . . . . 14 (((𝜑𝑛𝑍) ∧ 𝑥𝑆) → ((𝐹𝑛)‘𝑥) ∈ ℂ)
4039adantllr 754 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ 𝑛𝑍) ∧ 𝑥𝑆) → ((𝐹𝑛)‘𝑥) ∈ ℂ)
4140adantlrr 756 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥𝑆) → ((𝐹𝑛)‘𝑥) ∈ ℂ)
4238feqmptd 6208 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → (𝐹𝑛) = (𝑥𝑆 ↦ ((𝐹𝑛)‘𝑥)))
434ffvelrnda 6317 . . . . . . . . . . . . . 14 ((𝜑𝑛𝑍) → (𝐹𝑛) ∈ 𝐿1)
4442, 43eqeltrrd 2699 . . . . . . . . . . . . 13 ((𝜑𝑛𝑍) → (𝑥𝑆 ↦ ((𝐹𝑛)‘𝑥)) ∈ 𝐿1)
4544ad2ant2r 782 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥𝑆 ↦ ((𝐹𝑛)‘𝑥)) ∈ 𝐿1)
467, 17syl 17 . . . . . . . . . . . . . . 15 (𝜑𝐺:𝑆⟶ℂ)
4746ffvelrnda 6317 . . . . . . . . . . . . . 14 ((𝜑𝑥𝑆) → (𝐺𝑥) ∈ ℂ)
4847adantlr 750 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑥𝑆) → (𝐺𝑥) ∈ ℂ)
4948adantlr 750 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥𝑆) → (𝐺𝑥) ∈ ℂ)
5046feqmptd 6208 . . . . . . . . . . . . . 14 (𝜑𝐺 = (𝑥𝑆 ↦ (𝐺𝑥)))
5150, 20eqeltrrd 2699 . . . . . . . . . . . . 13 (𝜑 → (𝑥𝑆 ↦ (𝐺𝑥)) ∈ 𝐿1)
5251ad2antrr 761 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥𝑆 ↦ (𝐺𝑥)) ∈ 𝐿1)
5341, 45, 49, 52itgsub 23505 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(((𝐹𝑛)‘𝑥) − (𝐺𝑥)) d𝑥 = (∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥))
5453fveq2d 6154 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘∫𝑆(((𝐹𝑛)‘𝑥) − (𝐺𝑥)) d𝑥) = (abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)))
5541, 49subcld 10339 . . . . . . . . . . . . 13 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥𝑆) → (((𝐹𝑛)‘𝑥) − (𝐺𝑥)) ∈ ℂ)
5641, 45, 49, 52iblsub 23501 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥𝑆 ↦ (((𝐹𝑛)‘𝑥) − (𝐺𝑥))) ∈ 𝐿1)
5755, 56itgcl 23463 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(((𝐹𝑛)‘𝑥) − (𝐺𝑥)) d𝑥 ∈ ℂ)
5857abscld 14112 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘∫𝑆(((𝐹𝑛)‘𝑥) − (𝐺𝑥)) d𝑥) ∈ ℝ)
5955abscld 14112 . . . . . . . . . . . 12 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥𝑆) → (abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) ∈ ℝ)
6055, 56iblabs 23508 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥𝑆 ↦ (abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥)))) ∈ 𝐿1)
6159, 60itgrecl 23477 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) d𝑥 ∈ ℝ)
62 rpre 11786 . . . . . . . . . . . 12 (𝑟 ∈ ℝ+𝑟 ∈ ℝ)
6362ad2antlr 762 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → 𝑟 ∈ ℝ)
6455, 56itgabs 23514 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘∫𝑆(((𝐹𝑛)‘𝑥) − (𝐺𝑥)) d𝑥) ≤ ∫𝑆(abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) d𝑥)
6533adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 / ((vol‘𝑆) + 1)) ∈ ℝ+)
6665rpred 11819 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 / ((vol‘𝑆) + 1)) ∈ ℝ)
6715ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (vol‘𝑆) ∈ ℝ)
6866, 67remulcld 10017 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆)) ∈ ℝ)
69 fconstmpt 5125 . . . . . . . . . . . . . . 15 (𝑆 × {(𝑟 / ((vol‘𝑆) + 1))}) = (𝑥𝑆 ↦ (𝑟 / ((vol‘𝑆) + 1)))
7024ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → 𝑆 ∈ dom vol)
7165rpcnd 11821 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 / ((vol‘𝑆) + 1)) ∈ ℂ)
72 iblconst 23497 . . . . . . . . . . . . . . . 16 ((𝑆 ∈ dom vol ∧ (vol‘𝑆) ∈ ℝ ∧ (𝑟 / ((vol‘𝑆) + 1)) ∈ ℂ) → (𝑆 × {(𝑟 / ((vol‘𝑆) + 1))}) ∈ 𝐿1)
7370, 67, 71, 72syl3anc 1323 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑆 × {(𝑟 / ((vol‘𝑆) + 1))}) ∈ 𝐿1)
7469, 73syl5eqelr 2703 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑥𝑆 ↦ (𝑟 / ((vol‘𝑆) + 1))) ∈ 𝐿1)
7566adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥𝑆) → (𝑟 / ((vol‘𝑆) + 1)) ∈ ℝ)
76 simprr 795 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))
77 fveq2 6150 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → ((𝐹𝑛)‘𝑧) = ((𝐹𝑛)‘𝑥))
78 fveq2 6150 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → (𝐺𝑧) = (𝐺𝑥))
7977, 78oveq12d 6625 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑥 → (((𝐹𝑛)‘𝑧) − (𝐺𝑧)) = (((𝐹𝑛)‘𝑥) − (𝐺𝑥)))
8079fveq2d 6154 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑥 → (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) = (abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))))
8180breq1d 4625 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑥 → ((abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) ↔ (abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) < (𝑟 / ((vol‘𝑆) + 1))))
8281rspccva 3294 . . . . . . . . . . . . . . . 16 ((∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) ∧ 𝑥𝑆) → (abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) < (𝑟 / ((vol‘𝑆) + 1)))
8376, 82sylan 488 . . . . . . . . . . . . . . 15 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥𝑆) → (abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) < (𝑟 / ((vol‘𝑆) + 1)))
8459, 75, 83ltled 10132 . . . . . . . . . . . . . 14 ((((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) ∧ 𝑥𝑆) → (abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) ≤ (𝑟 / ((vol‘𝑆) + 1)))
8560, 74, 59, 75, 84itgle 23489 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) d𝑥 ≤ ∫𝑆(𝑟 / ((vol‘𝑆) + 1)) d𝑥)
86 itgconst 23498 . . . . . . . . . . . . . 14 ((𝑆 ∈ dom vol ∧ (vol‘𝑆) ∈ ℝ ∧ (𝑟 / ((vol‘𝑆) + 1)) ∈ ℂ) → ∫𝑆(𝑟 / ((vol‘𝑆) + 1)) d𝑥 = ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆)))
8770, 67, 71, 86syl3anc 1323 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(𝑟 / ((vol‘𝑆) + 1)) d𝑥 = ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆)))
8885, 87breqtrd 4641 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) d𝑥 ≤ ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆)))
8963recnd 10015 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → 𝑟 ∈ ℂ)
9067recnd 10015 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (vol‘𝑆) ∈ ℂ)
9132adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) + 1) ∈ ℝ+)
9291rpcnd 11821 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) + 1) ∈ ℂ)
9391rpne0d 11824 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) + 1) ≠ 0)
9489, 90, 92, 93div23d 10785 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((𝑟 · (vol‘𝑆)) / ((vol‘𝑆) + 1)) = ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆)))
9567ltp1d 10901 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (vol‘𝑆) < ((vol‘𝑆) + 1))
96 peano2re 10156 . . . . . . . . . . . . . . . . 17 ((vol‘𝑆) ∈ ℝ → ((vol‘𝑆) + 1) ∈ ℝ)
9767, 96syl 17 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) + 1) ∈ ℝ)
98 rpgt0 11791 . . . . . . . . . . . . . . . . 17 (𝑟 ∈ ℝ+ → 0 < 𝑟)
9998ad2antlr 762 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → 0 < 𝑟)
100 ltmul2 10821 . . . . . . . . . . . . . . . 16 (((vol‘𝑆) ∈ ℝ ∧ ((vol‘𝑆) + 1) ∈ ℝ ∧ (𝑟 ∈ ℝ ∧ 0 < 𝑟)) → ((vol‘𝑆) < ((vol‘𝑆) + 1) ↔ (𝑟 · (vol‘𝑆)) < (𝑟 · ((vol‘𝑆) + 1))))
10167, 97, 63, 99, 100syl112anc 1327 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((vol‘𝑆) < ((vol‘𝑆) + 1) ↔ (𝑟 · (vol‘𝑆)) < (𝑟 · ((vol‘𝑆) + 1))))
10295, 101mpbid 222 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 · (vol‘𝑆)) < (𝑟 · ((vol‘𝑆) + 1)))
10363, 67remulcld 10017 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (𝑟 · (vol‘𝑆)) ∈ ℝ)
104103, 63, 91ltdivmul2d 11871 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (((𝑟 · (vol‘𝑆)) / ((vol‘𝑆) + 1)) < 𝑟 ↔ (𝑟 · (vol‘𝑆)) < (𝑟 · ((vol‘𝑆) + 1))))
105102, 104mpbird 247 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((𝑟 · (vol‘𝑆)) / ((vol‘𝑆) + 1)) < 𝑟)
10694, 105eqbrtrrd 4639 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ((𝑟 / ((vol‘𝑆) + 1)) · (vol‘𝑆)) < 𝑟)
10761, 68, 63, 88, 106lelttrd 10142 . . . . . . . . . . 11 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → ∫𝑆(abs‘(((𝐹𝑛)‘𝑥) − (𝐺𝑥))) d𝑥 < 𝑟)
10858, 61, 63, 64, 107lelttrd 10142 . . . . . . . . . 10 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘∫𝑆(((𝐹𝑛)‘𝑥) − (𝐺𝑥)) d𝑥) < 𝑟)
10954, 108eqbrtrrd 4639 . . . . . . . . 9 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑛𝑍 ∧ ∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)))) → (abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)) < 𝑟)
110109expr 642 . . . . . . . 8 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑛𝑍) → (∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → (abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)) < 𝑟))
11135, 110sylan2 491 . . . . . . 7 (((𝜑𝑟 ∈ ℝ+) ∧ (𝑗𝑍𝑛 ∈ (ℤ𝑗))) → (∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → (abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)) < 𝑟))
112111anassrs 679 . . . . . 6 ((((𝜑𝑟 ∈ ℝ+) ∧ 𝑗𝑍) ∧ 𝑛 ∈ (ℤ𝑗)) → (∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → (abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)) < 𝑟))
113112ralimdva 2956 . . . . 5 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑗𝑍) → (∀𝑛 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → ∀𝑛 ∈ (ℤ𝑗)(abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)) < 𝑟))
114113reximdva 3011 . . . 4 ((𝜑𝑟 ∈ ℝ+) → (∃𝑗𝑍𝑛 ∈ (ℤ𝑗)∀𝑧𝑆 (abs‘(((𝐹𝑛)‘𝑧) − (𝐺𝑧))) < (𝑟 / ((vol‘𝑆) + 1)) → ∃𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)) < 𝑟))
11534, 114mpd 15 . . 3 ((𝜑𝑟 ∈ ℝ+) → ∃𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)) < 𝑟)
116115ralrimiva 2960 . 2 (𝜑 → ∀𝑟 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)) < 𝑟)
117 fvex 6160 . . . . . 6 (ℤ𝑀) ∈ V
1181, 117eqeltri 2694 . . . . 5 𝑍 ∈ V
119118mptex 6443 . . . 4 (𝑘𝑍 ↦ ∫𝑆((𝐹𝑘)‘𝑥) d𝑥) ∈ V
120119a1i 11 . . 3 (𝜑 → (𝑘𝑍 ↦ ∫𝑆((𝐹𝑘)‘𝑥) d𝑥) ∈ V)
121 fveq2 6150 . . . . . . . 8 (𝑘 = 𝑛 → (𝐹𝑘) = (𝐹𝑛))
122121fveq1d 6152 . . . . . . 7 (𝑘 = 𝑛 → ((𝐹𝑘)‘𝑥) = ((𝐹𝑛)‘𝑥))
123122adantr 481 . . . . . 6 ((𝑘 = 𝑛𝑥𝑆) → ((𝐹𝑘)‘𝑥) = ((𝐹𝑛)‘𝑥))
124123itgeq2dv 23461 . . . . 5 (𝑘 = 𝑛 → ∫𝑆((𝐹𝑘)‘𝑥) d𝑥 = ∫𝑆((𝐹𝑛)‘𝑥) d𝑥)
125 eqid 2621 . . . . 5 (𝑘𝑍 ↦ ∫𝑆((𝐹𝑘)‘𝑥) d𝑥) = (𝑘𝑍 ↦ ∫𝑆((𝐹𝑘)‘𝑥) d𝑥)
126 itgex 23450 . . . . 5 𝑆((𝐹𝑛)‘𝑥) d𝑥 ∈ V
127124, 125, 126fvmpt 6241 . . . 4 (𝑛𝑍 → ((𝑘𝑍 ↦ ∫𝑆((𝐹𝑘)‘𝑥) d𝑥)‘𝑛) = ∫𝑆((𝐹𝑛)‘𝑥) d𝑥)
128127adantl 482 . . 3 ((𝜑𝑛𝑍) → ((𝑘𝑍 ↦ ∫𝑆((𝐹𝑘)‘𝑥) d𝑥)‘𝑛) = ∫𝑆((𝐹𝑛)‘𝑥) d𝑥)
12947, 51itgcl 23463 . . 3 (𝜑 → ∫𝑆(𝐺𝑥) d𝑥 ∈ ℂ)
13039, 44itgcl 23463 . . 3 ((𝜑𝑛𝑍) → ∫𝑆((𝐹𝑛)‘𝑥) d𝑥 ∈ ℂ)
1311, 2, 120, 128, 129, 130clim2c 14173 . 2 (𝜑 → ((𝑘𝑍 ↦ ∫𝑆((𝐹𝑘)‘𝑥) d𝑥) ⇝ ∫𝑆(𝐺𝑥) d𝑥 ↔ ∀𝑟 ∈ ℝ+𝑗𝑍𝑛 ∈ (ℤ𝑗)(abs‘(∫𝑆((𝐹𝑛)‘𝑥) d𝑥 − ∫𝑆(𝐺𝑥) d𝑥)) < 𝑟))
132116, 131mpbird 247 1 (𝜑 → (𝑘𝑍 ↦ ∫𝑆((𝐹𝑘)‘𝑥) d𝑥) ⇝ ∫𝑆(𝐺𝑥) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2907  wrex 2908  Vcvv 3186  wss 3556  {csn 4150   class class class wbr 4615  cmpt 4675   × cxp 5074  dom cdm 5076   Fn wfn 5844  wf 5845  cfv 5849  (class class class)co 6607  𝑚 cmap 7805  cc 9881  cr 9882  0cc0 9883  1c1 9884   + caddc 9886   · cmul 9888   < clt 10021  cle 10022  cmin 10213   / cdiv 10631  cz 11324  cuz 11634  +crp 11779  abscabs 13911  cli 14152  vol*covol 23144  volcvol 23145  MblFncmbf 23296  𝐿1cibl 23299  citg 23300  𝑢culm 24041
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-cc 9204  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-disj 4586  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-ofr 6854  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-omul 7513  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-acn 8715  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-ioc 12125  df-ico 12126  df-icc 12127  df-fz 12272  df-fzo 12410  df-fl 12536  df-mod 12612  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-limsup 14139  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-cnfld 19669  df-top 20621  df-topon 20638  df-topsp 20651  df-bases 20664  df-cn 20944  df-cnp 20945  df-cmp 21103  df-tx 21278  df-hmeo 21471  df-xms 22038  df-ms 22039  df-tms 22040  df-cncf 22594  df-ovol 23146  df-vol 23147  df-mbf 23301  df-itg1 23302  df-itg2 23303  df-ibl 23304  df-itg 23305  df-0p 23350  df-ulm 24042
This theorem is referenced by:  itgulm2  24074
  Copyright terms: Public domain W3C validator