This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgulm

Description: A uniform limit of integrals of integrable functions converges to the integral of the limit function. (Contributed by Mario Carneiro, 18-Mar-2015)

Ref Expression
Hypotheses itgulm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
itgulm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
itgulm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝐿1 )
itgulm.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
itgulm.s ⊢ ( 𝜑 → ( vol ‘ 𝑆 ) ∈ ℝ )
Assertion itgulm ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 ) ⇝ ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 itgulm.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 itgulm.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 itgulm.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ 𝐿1 )
4 itgulm.u ⊢ ( 𝜑 → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
5 itgulm.s ⊢ ( 𝜑 → ( vol ‘ 𝑆 ) ∈ ℝ )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑀 ∈ ℤ )
7 3 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝑍 )
8 ulmf2 ⊢ ( ( 𝐹 Fn 𝑍 ∧ 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
9 7 4 8 syl2anc ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
10 9 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝐹 : 𝑍 ⟶ ( ℂ ↑m 𝑆 ) )
11 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ 𝑧 ∈ 𝑆 ) ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) )
12 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑧 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑧 ) )
13 4 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝑟 ∈ ℝ+ )
15 5 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( vol ‘ 𝑆 ) ∈ ℝ )
16 ulmcl ⊢ ( 𝐹 ( ⇝𝑢 ‘ 𝑆 ) 𝐺 → 𝐺 : 𝑆 ⟶ ℂ )
17 fdm ⊢ ( 𝐺 : 𝑆 ⟶ ℂ → dom 𝐺 = 𝑆 )
18 4 16 17 3syl ⊢ ( 𝜑 → dom 𝐺 = 𝑆 )
19 1 2 3 4 5 iblulm ⊢ ( 𝜑 → 𝐺 ∈ 𝐿1 )
20 iblmbf ⊢ ( 𝐺 ∈ 𝐿1 → 𝐺 ∈ MblFn )
21 mbfdm ⊢ ( 𝐺 ∈ MblFn → dom 𝐺 ∈ dom vol )
22 19 20 21 3syl ⊢ ( 𝜑 → dom 𝐺 ∈ dom vol )
23 18 22 eqeltrrd ⊢ ( 𝜑 → 𝑆 ∈ dom vol )
24 mblss ⊢ ( 𝑆 ∈ dom vol → 𝑆 ⊆ ℝ )
25 ovolge0 ⊢ ( 𝑆 ⊆ ℝ → 0 ≤ ( vol* ‘ 𝑆 ) )
26 23 24 25 3syl ⊢ ( 𝜑 → 0 ≤ ( vol* ‘ 𝑆 ) )
27 mblvol ⊢ ( 𝑆 ∈ dom vol → ( vol ‘ 𝑆 ) = ( vol* ‘ 𝑆 ) )
28 23 27 syl ⊢ ( 𝜑 → ( vol ‘ 𝑆 ) = ( vol* ‘ 𝑆 ) )
29 26 28 breqtrrd ⊢ ( 𝜑 → 0 ≤ ( vol ‘ 𝑆 ) )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 0 ≤ ( vol ‘ 𝑆 ) )
31 15 30 ge0p1rpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ( vol ‘ 𝑆 ) + 1 ) ∈ ℝ+ )
32 14 31 rpdivcld ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ∈ ℝ+ )
33 1 6 10 11 12 13 32 ulmi ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) )
34 1 uztrn2 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → 𝑛 ∈ 𝑍 )
35 9 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑆 ) )
36 elmapi ⊢ ( ( 𝐹 ‘ 𝑛 ) ∈ ( ℂ ↑m 𝑆 ) → ( 𝐹 ‘ 𝑛 ) : 𝑆 ⟶ ℂ )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) : 𝑆 ⟶ ℂ )
38 37 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ )
39 38 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ )
40 39 adantlrr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ∈ ℂ )
41 37 feqmptd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) )
42 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑛 ) ∈ 𝐿1 )
43 41 42 eqeltrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ 𝐿1 )
44 43 ad2ant2r ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) ) ∈ 𝐿1 )
45 4 16 syl ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
46 45 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
47 46 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℂ )
48 45 feqmptd ⊢ ( 𝜑 → 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑥 ) ) )
49 48 19 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐿1 )
50 49 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑥 ) ) ∈ 𝐿1 )
51 40 44 47 50 itgsub ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ∫ 𝑆 ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) d 𝑥 = ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) )
52 51 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( abs ‘ ∫ 𝑆 ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) d 𝑥 ) = ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) )
53 40 47 subcld ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ∈ ℂ )
54 40 44 47 50 iblsub ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ∈ 𝐿1 )
55 53 54 itgcl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ∫ 𝑆 ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) d 𝑥 ∈ ℂ )
56 55 abscld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( abs ‘ ∫ 𝑆 ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) d 𝑥 ) ∈ ℝ )
57 53 abscld ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ∈ ℝ )
58 53 54 iblabs ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑥 ∈ 𝑆 ↦ ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ) ∈ 𝐿1 )
59 57 58 itgrecl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ∫ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) d 𝑥 ∈ ℝ )
60 rpre ⊢ ( 𝑟 ∈ ℝ+ → 𝑟 ∈ ℝ )
61 60 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → 𝑟 ∈ ℝ )
62 53 54 itgabs ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( abs ‘ ∫ 𝑆 ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) d 𝑥 ) ≤ ∫ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) d 𝑥 )
63 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ∈ ℝ+ )
64 63 rpred ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ∈ ℝ )
65 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( vol ‘ 𝑆 ) ∈ ℝ )
66 64 65 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) · ( vol ‘ 𝑆 ) ) ∈ ℝ )
67 fconstmpt ⊢ ( 𝑆 × { ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) } ) = ( 𝑥 ∈ 𝑆 ↦ ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) )
68 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → 𝑆 ∈ dom vol )
69 63 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ∈ ℂ )
70 iblconst ⊢ ( ( 𝑆 ∈ dom vol ∧ ( vol ‘ 𝑆 ) ∈ ℝ ∧ ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ∈ ℂ ) → ( 𝑆 × { ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) } ) ∈ 𝐿1 )
71 68 65 69 70 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑆 × { ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) } ) ∈ 𝐿1 )
72 67 71 eqeltrrid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑥 ∈ 𝑆 ↦ ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ∈ 𝐿1 )
73 64 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ∈ ℝ )
74 simprr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) )
75 fveq2 ⊢ ( 𝑧 = 𝑥 → ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
76 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑥 ) )
77 75 76 oveq12d ⊢ ( 𝑧 = 𝑥 → ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) = ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) )
78 77 fveq2d ⊢ ( 𝑧 = 𝑥 → ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) = ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) )
79 78 breq1d ⊢ ( 𝑧 = 𝑥 → ( ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ↔ ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) )
80 79 rspccva ⊢ ( ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) )
81 74 80 sylan ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) )
82 57 73 81 ltled ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) ≤ ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) )
83 58 72 57 73 82 itgle ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ∫ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) d 𝑥 ≤ ∫ 𝑆 ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) d 𝑥 )
84 itgconst ⊢ ( ( 𝑆 ∈ dom vol ∧ ( vol ‘ 𝑆 ) ∈ ℝ ∧ ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ∈ ℂ ) → ∫ 𝑆 ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) d 𝑥 = ( ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) · ( vol ‘ 𝑆 ) ) )
85 68 65 69 84 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ∫ 𝑆 ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) d 𝑥 = ( ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) · ( vol ‘ 𝑆 ) ) )
86 83 85 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ∫ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) d 𝑥 ≤ ( ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) · ( vol ‘ 𝑆 ) ) )
87 61 recnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → 𝑟 ∈ ℂ )
88 65 recnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( vol ‘ 𝑆 ) ∈ ℂ )
89 31 adantr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( vol ‘ 𝑆 ) + 1 ) ∈ ℝ+ )
90 89 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( vol ‘ 𝑆 ) + 1 ) ∈ ℂ )
91 89 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( vol ‘ 𝑆 ) + 1 ) ≠ 0 )
92 87 88 90 91 div23d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( 𝑟 · ( vol ‘ 𝑆 ) ) / ( ( vol ‘ 𝑆 ) + 1 ) ) = ( ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) · ( vol ‘ 𝑆 ) ) )
93 65 ltp1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( vol ‘ 𝑆 ) < ( ( vol ‘ 𝑆 ) + 1 ) )
94 peano2re ⊢ ( ( vol ‘ 𝑆 ) ∈ ℝ → ( ( vol ‘ 𝑆 ) + 1 ) ∈ ℝ )
95 65 94 syl ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( vol ‘ 𝑆 ) + 1 ) ∈ ℝ )
96 rpgt0 ⊢ ( 𝑟 ∈ ℝ+ → 0 < 𝑟 )
97 96 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → 0 < 𝑟 )
98 ltmul2 ⊢ ( ( ( vol ‘ 𝑆 ) ∈ ℝ ∧ ( ( vol ‘ 𝑆 ) + 1 ) ∈ ℝ ∧ ( 𝑟 ∈ ℝ ∧ 0 < 𝑟 ) ) → ( ( vol ‘ 𝑆 ) < ( ( vol ‘ 𝑆 ) + 1 ) ↔ ( 𝑟 · ( vol ‘ 𝑆 ) ) < ( 𝑟 · ( ( vol ‘ 𝑆 ) + 1 ) ) ) )
99 65 95 61 97 98 syl112anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( vol ‘ 𝑆 ) < ( ( vol ‘ 𝑆 ) + 1 ) ↔ ( 𝑟 · ( vol ‘ 𝑆 ) ) < ( 𝑟 · ( ( vol ‘ 𝑆 ) + 1 ) ) ) )
100 93 99 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑟 · ( vol ‘ 𝑆 ) ) < ( 𝑟 · ( ( vol ‘ 𝑆 ) + 1 ) ) )
101 61 65 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( 𝑟 · ( vol ‘ 𝑆 ) ) ∈ ℝ )
102 101 61 89 ltdivmul2d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( ( 𝑟 · ( vol ‘ 𝑆 ) ) / ( ( vol ‘ 𝑆 ) + 1 ) ) < 𝑟 ↔ ( 𝑟 · ( vol ‘ 𝑆 ) ) < ( 𝑟 · ( ( vol ‘ 𝑆 ) + 1 ) ) ) )
103 100 102 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( 𝑟 · ( vol ‘ 𝑆 ) ) / ( ( vol ‘ 𝑆 ) + 1 ) ) < 𝑟 )
104 92 103 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) · ( vol ‘ 𝑆 ) ) < 𝑟 )
105 59 66 61 86 104 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ∫ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) ) d 𝑥 < 𝑟 )
106 56 59 61 62 105 lelttrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( abs ‘ ∫ 𝑆 ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) − ( 𝐺 ‘ 𝑥 ) ) d 𝑥 ) < 𝑟 )
107 52 106 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑛 ∈ 𝑍 ∧ ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) ) ) → ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) < 𝑟 )
108 107 expr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑛 ∈ 𝑍 ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) → ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) < 𝑟 ) )
109 34 108 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ ( 𝑗 ∈ 𝑍 ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) → ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) < 𝑟 ) )
110 109 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) ∧ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ) → ( ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) → ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) < 𝑟 ) )
111 110 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑗 ∈ 𝑍 ) → ( ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) → ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) < 𝑟 ) )
112 111 reximdva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ∀ 𝑧 ∈ 𝑆 ( abs ‘ ( ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑧 ) − ( 𝐺 ‘ 𝑧 ) ) ) < ( 𝑟 / ( ( vol ‘ 𝑆 ) + 1 ) ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) < 𝑟 ) )
113 33 112 mpd ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) < 𝑟 )
114 113 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) < 𝑟 )
115 1 fvexi ⊢ 𝑍 ∈ V
116 115 mptex ⊢ ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 ) ∈ V
117 116 a1i ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 ) ∈ V )
118 fveq2 ⊢ ( 𝑘 = 𝑛 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑛 ) )
119 118 fveq1d ⊢ ( 𝑘 = 𝑛 → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
120 119 adantr ⊢ ( ( 𝑘 = 𝑛 ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) = ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) )
121 120 itgeq2dv ⊢ ( 𝑘 = 𝑛 → ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 = ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 )
122 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 ) = ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 )
123 itgex ⊢ ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 ∈ V
124 121 122 123 fvmpt ⊢ ( 𝑛 ∈ 𝑍 → ( ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 ) ‘ 𝑛 ) = ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 )
125 124 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 ) ‘ 𝑛 ) = ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 )
126 46 49 itgcl ⊢ ( 𝜑 → ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ∈ ℂ )
127 38 43 itgcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝑍 ) → ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 ∈ ℂ )
128 1 2 117 125 126 127 clim2c ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 ) ⇝ ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ↔ ∀ 𝑟 ∈ ℝ+ ∃ 𝑗 ∈ 𝑍 ∀ 𝑛 ∈ ( ℤ≥ ‘ 𝑗 ) ( abs ‘ ( ∫ 𝑆 ( ( 𝐹 ‘ 𝑛 ) ‘ 𝑥 ) d 𝑥 − ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 ) ) < 𝑟 ) )
129 114 128 mpbird ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ∫ 𝑆 ( ( 𝐹 ‘ 𝑘 ) ‘ 𝑥 ) d 𝑥 ) ⇝ ∫ 𝑆 ( 𝐺 ‘ 𝑥 ) d 𝑥 )