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

Metamath Proof Explorer

Theorem ftc1a

Description: The Fundamental Theorem of Calculus, part one. The function G formed by varying the right endpoint of an integral of F is continuous if F is integrable. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses ftc1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
ftc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ftc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ftc1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
ftc1.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
ftc1.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
ftc1.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
ftc1a.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
Assertion ftc1a ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 ftc1.g ⊢ 𝐺 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ∫ ( 𝐴 (,) 𝑥 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
2 ftc1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 ftc1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 ftc1.le ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 ftc1.s ⊢ ( 𝜑 → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
6 ftc1.d ⊢ ( 𝜑 → 𝐷 ⊆ ℝ )
7 ftc1.i ⊢ ( 𝜑 → 𝐹 ∈ 𝐿1 )
8 ftc1a.f ⊢ ( 𝜑 → 𝐹 : 𝐷 ⟶ ℂ )
9 1 2 3 4 5 6 7 8 ftc1lem2 ⊢ ( 𝜑 → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
10 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑤 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑤 ) ∈ V )
11 8 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑤 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑤 ) ) )
12 11 7 eqeltrrd ⊢ ( 𝜑 → ( 𝑤 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑤 ) ) ∈ 𝐿1 )
13 12 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( 𝑤 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑤 ) ) ∈ 𝐿1 )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑒 ∈ ℝ+ )
15 10 13 14 itgcn ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) )
16 oveq12 ⊢ ( ( 𝑠 = 𝑧 ∧ 𝑟 = 𝑦 ) → ( 𝑠 − 𝑟 ) = ( 𝑧 − 𝑦 ) )
17 16 fveq2d ⊢ ( ( 𝑠 = 𝑧 ∧ 𝑟 = 𝑦 ) → ( abs ‘ ( 𝑠 − 𝑟 ) ) = ( abs ‘ ( 𝑧 − 𝑦 ) ) )
18 17 breq1d ⊢ ( ( 𝑠 = 𝑧 ∧ 𝑟 = 𝑦 ) → ( ( abs ‘ ( 𝑠 − 𝑟 ) ) < 𝑑 ↔ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) )
19 fveq2 ⊢ ( 𝑠 = 𝑧 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑧 ) )
20 fveq2 ⊢ ( 𝑟 = 𝑦 → ( 𝐺 ‘ 𝑟 ) = ( 𝐺 ‘ 𝑦 ) )
21 19 20 oveqan12d ⊢ ( ( 𝑠 = 𝑧 ∧ 𝑟 = 𝑦 ) → ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) = ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) )
22 21 fveq2d ⊢ ( ( 𝑠 = 𝑧 ∧ 𝑟 = 𝑦 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) )
23 22 breq1d ⊢ ( ( 𝑠 = 𝑧 ∧ 𝑟 = 𝑦 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) ) < 𝑒 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
24 18 23 imbi12d ⊢ ( ( 𝑠 = 𝑧 ∧ 𝑟 = 𝑦 ) → ( ( ( abs ‘ ( 𝑠 − 𝑟 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) ) < 𝑒 ) ↔ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) ) )
25 24 ancoms ⊢ ( ( 𝑟 = 𝑦 ∧ 𝑠 = 𝑧 ) → ( ( ( abs ‘ ( 𝑠 − 𝑟 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) ) < 𝑒 ) ↔ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) ) )
26 oveq12 ⊢ ( ( 𝑠 = 𝑦 ∧ 𝑟 = 𝑧 ) → ( 𝑠 − 𝑟 ) = ( 𝑦 − 𝑧 ) )
27 26 fveq2d ⊢ ( ( 𝑠 = 𝑦 ∧ 𝑟 = 𝑧 ) → ( abs ‘ ( 𝑠 − 𝑟 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
28 27 breq1d ⊢ ( ( 𝑠 = 𝑦 ∧ 𝑟 = 𝑧 ) → ( ( abs ‘ ( 𝑠 − 𝑟 ) ) < 𝑑 ↔ ( abs ‘ ( 𝑦 − 𝑧 ) ) < 𝑑 ) )
29 fveq2 ⊢ ( 𝑠 = 𝑦 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑦 ) )
30 fveq2 ⊢ ( 𝑟 = 𝑧 → ( 𝐺 ‘ 𝑟 ) = ( 𝐺 ‘ 𝑧 ) )
31 29 30 oveqan12d ⊢ ( ( 𝑠 = 𝑦 ∧ 𝑟 = 𝑧 ) → ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) = ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) )
32 31 fveq2d ⊢ ( ( 𝑠 = 𝑦 ∧ 𝑟 = 𝑧 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) ) )
33 32 breq1d ⊢ ( ( 𝑠 = 𝑦 ∧ 𝑟 = 𝑧 ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) ) < 𝑒 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑒 ) )
34 28 33 imbi12d ⊢ ( ( 𝑠 = 𝑦 ∧ 𝑟 = 𝑧 ) → ( ( ( abs ‘ ( 𝑠 − 𝑟 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) ) < 𝑒 ) ↔ ( ( abs ‘ ( 𝑦 − 𝑧 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑒 ) ) )
35 34 ancoms ⊢ ( ( 𝑟 = 𝑧 ∧ 𝑠 = 𝑦 ) → ( ( ( abs ‘ ( 𝑠 − 𝑟 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑠 ) − ( 𝐺 ‘ 𝑟 ) ) ) < 𝑒 ) ↔ ( ( abs ‘ ( 𝑦 − 𝑧 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑒 ) ) )
36 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
37 2 3 36 syl2anc ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
38 37 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
39 37 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
40 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
41 39 40 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑧 ∈ ℝ )
42 41 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑧 ∈ ℂ )
43 simprl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
44 39 43 sseldd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑦 ∈ ℝ )
45 44 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝑦 ∈ ℂ )
46 42 45 abssubd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
47 46 breq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ↔ ( abs ‘ ( 𝑦 − 𝑧 ) ) < 𝑑 ) )
48 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
49 48 40 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐺 ‘ 𝑧 ) ∈ ℂ )
50 48 43 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ℂ )
51 49 50 abssubd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) ) )
52 51 breq1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ↔ ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑒 ) )
53 47 52 imbi12d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) ↔ ( ( abs ‘ ( 𝑦 − 𝑧 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑧 ) ) ) < 𝑒 ) ) )
54 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → 𝑦 ≤ 𝑧 )
55 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → 𝐴 ∈ ℝ )
56 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → 𝐵 ∈ ℝ )
57 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → 𝐴 ≤ 𝐵 )
58 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
59 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → 𝐷 ⊆ ℝ )
60 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → 𝐹 ∈ 𝐿1 )
61 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → 𝐹 : 𝐷 ⟶ ℂ )
62 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
63 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
64 1 55 56 57 58 59 60 61 62 63 ftc1lem1 ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑦 ≤ 𝑧 ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) = ∫ ( 𝑦 (,) 𝑧 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
65 54 64 mpdan ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) = ∫ ( 𝑦 (,) 𝑧 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
66 65 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) = ∫ ( 𝑦 (,) 𝑧 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
67 66 ad2ant2r ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) = ∫ ( 𝑦 (,) 𝑧 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 )
68 67 fveq2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) = ( abs ‘ ∫ ( 𝑦 (,) 𝑧 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) )
69 fvexd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) ∧ 𝑡 ∈ ( 𝑦 (,) 𝑧 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
70 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝐴 ∈ ℝ )
71 70 rexrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝐴 ∈ ℝ* )
72 simprl1 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
73 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝐵 ∈ ℝ )
74 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
75 70 73 74 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) ) )
76 72 75 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴 ≤ 𝑦 ∧ 𝑦 ≤ 𝐵 ) )
77 76 simp2d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝐴 ≤ 𝑦 )
78 iooss1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐴 ≤ 𝑦 ) → ( 𝑦 (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝑧 ) )
79 71 77 78 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑦 (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝑧 ) )
80 73 rexrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝐵 ∈ ℝ* )
81 simprl2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
82 elicc2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵 ) ) )
83 70 73 82 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵 ) ) )
84 81 83 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑧 ∈ ℝ ∧ 𝐴 ≤ 𝑧 ∧ 𝑧 ≤ 𝐵 ) )
85 84 simp3d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑧 ≤ 𝐵 )
86 iooss2 ⊢ ( ( 𝐵 ∈ ℝ* ∧ 𝑧 ≤ 𝐵 ) → ( 𝐴 (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝐵 ) )
87 80 85 86 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝐴 (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝐵 ) )
88 79 87 sstrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑦 (,) 𝑧 ) ⊆ ( 𝐴 (,) 𝐵 ) )
89 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝐴 (,) 𝐵 ) ⊆ 𝐷 )
90 88 89 sstrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑦 (,) 𝑧 ) ⊆ 𝐷 )
91 ioombl ⊢ ( 𝑦 (,) 𝑧 ) ∈ dom vol
92 91 a1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑦 (,) 𝑧 ) ∈ dom vol )
93 fvexd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) ∧ 𝑡 ∈ 𝐷 ) → ( 𝐹 ‘ 𝑡 ) ∈ V )
94 8 feqmptd ⊢ ( 𝜑 → 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) )
95 94 7 eqeltrrd ⊢ ( 𝜑 → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
96 95 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑡 ∈ 𝐷 ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
97 90 92 93 96 iblss ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑡 ∈ ( 𝑦 (,) 𝑧 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 )
98 69 97 itgcl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ∫ ( 𝑦 (,) 𝑧 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ∈ ℂ )
99 98 abscld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( abs ‘ ∫ ( 𝑦 (,) 𝑧 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ∈ ℝ )
100 iblmbf ⊢ ( ( 𝑡 ∈ ( 𝑦 (,) 𝑧 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ 𝐿1 → ( 𝑡 ∈ ( 𝑦 (,) 𝑧 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ MblFn )
101 97 100 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑡 ∈ ( 𝑦 (,) 𝑧 ) ↦ ( 𝐹 ‘ 𝑡 ) ) ∈ MblFn )
102 101 69 mbfmptcl ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) ∧ 𝑡 ∈ ( 𝑦 (,) 𝑧 ) ) → ( 𝐹 ‘ 𝑡 ) ∈ ℂ )
103 102 abscld ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) ∧ 𝑡 ∈ ( 𝑦 (,) 𝑧 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ∈ ℝ )
104 69 97 iblabs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑡 ∈ ( 𝑦 (,) 𝑧 ) ↦ ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) ) ∈ 𝐿1 )
105 103 104 itgrecl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ∫ ( 𝑦 (,) 𝑧 ) ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡 ∈ ℝ )
106 simprl ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 𝑒 ∈ ℝ+ )
107 106 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑒 ∈ ℝ+ )
108 107 rpred ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑒 ∈ ℝ )
109 69 97 itgabs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( abs ‘ ∫ ( 𝑦 (,) 𝑧 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) ≤ ∫ ( 𝑦 (,) 𝑧 ) ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡 )
110 mblvol ⊢ ( ( 𝑦 (,) 𝑧 ) ∈ dom vol → ( vol ‘ ( 𝑦 (,) 𝑧 ) ) = ( vol* ‘ ( 𝑦 (,) 𝑧 ) ) )
111 91 110 ax-mp ⊢ ( vol ‘ ( 𝑦 (,) 𝑧 ) ) = ( vol* ‘ ( 𝑦 (,) 𝑧 ) )
112 ioossre ⊢ ( 𝑦 (,) 𝑧 ) ⊆ ℝ
113 ovolcl ⊢ ( ( 𝑦 (,) 𝑧 ) ⊆ ℝ → ( vol* ‘ ( 𝑦 (,) 𝑧 ) ) ∈ ℝ* )
114 112 113 mp1i ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( vol* ‘ ( 𝑦 (,) 𝑧 ) ) ∈ ℝ* )
115 84 simp1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑧 ∈ ℝ )
116 76 simp1d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑦 ∈ ℝ )
117 115 116 resubcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑧 − 𝑦 ) ∈ ℝ )
118 117 rexrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑧 − 𝑦 ) ∈ ℝ* )
119 simprr ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → 𝑑 ∈ ℝ+ )
120 119 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑑 ∈ ℝ+ )
121 120 rpxrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑑 ∈ ℝ* )
122 ioossicc ⊢ ( 𝑦 (,) 𝑧 ) ⊆ ( 𝑦 [,] 𝑧 )
123 iccssre ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 [,] 𝑧 ) ⊆ ℝ )
124 116 115 123 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑦 [,] 𝑧 ) ⊆ ℝ )
125 ovolss ⊢ ( ( ( 𝑦 (,) 𝑧 ) ⊆ ( 𝑦 [,] 𝑧 ) ∧ ( 𝑦 [,] 𝑧 ) ⊆ ℝ ) → ( vol* ‘ ( 𝑦 (,) 𝑧 ) ) ≤ ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) )
126 122 124 125 sylancr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( vol* ‘ ( 𝑦 (,) 𝑧 ) ) ≤ ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) )
127 simprl3 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → 𝑦 ≤ 𝑧 )
128 ovolicc ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) → ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) = ( 𝑧 − 𝑦 ) )
129 116 115 127 128 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) = ( 𝑧 − 𝑦 ) )
130 126 129 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( vol* ‘ ( 𝑦 (,) 𝑧 ) ) ≤ ( 𝑧 − 𝑦 ) )
131 116 115 127 abssubge0d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( 𝑧 − 𝑦 ) )
132 simprr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 )
133 131 132 eqbrtrrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( 𝑧 − 𝑦 ) < 𝑑 )
134 114 118 121 130 133 xrlelttrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( vol* ‘ ( 𝑦 (,) 𝑧 ) ) < 𝑑 )
135 111 134 eqbrtrid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( vol ‘ ( 𝑦 (,) 𝑧 ) ) < 𝑑 )
136 sseq1 ⊢ ( 𝑢 = ( 𝑦 (,) 𝑧 ) → ( 𝑢 ⊆ 𝐷 ↔ ( 𝑦 (,) 𝑧 ) ⊆ 𝐷 ) )
137 fveq2 ⊢ ( 𝑢 = ( 𝑦 (,) 𝑧 ) → ( vol ‘ 𝑢 ) = ( vol ‘ ( 𝑦 (,) 𝑧 ) ) )
138 137 breq1d ⊢ ( 𝑢 = ( 𝑦 (,) 𝑧 ) → ( ( vol ‘ 𝑢 ) < 𝑑 ↔ ( vol ‘ ( 𝑦 (,) 𝑧 ) ) < 𝑑 ) )
139 136 138 anbi12d ⊢ ( 𝑢 = ( 𝑦 (,) 𝑧 ) → ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) ↔ ( ( 𝑦 (,) 𝑧 ) ⊆ 𝐷 ∧ ( vol ‘ ( 𝑦 (,) 𝑧 ) ) < 𝑑 ) ) )
140 2fveq3 ⊢ ( 𝑤 = 𝑡 → ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) )
141 140 cbvitgv ⊢ ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 = ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡
142 itgeq1 ⊢ ( 𝑢 = ( 𝑦 (,) 𝑧 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡 = ∫ ( 𝑦 (,) 𝑧 ) ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡 )
143 141 142 eqtrid ⊢ ( 𝑢 = ( 𝑦 (,) 𝑧 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 = ∫ ( 𝑦 (,) 𝑧 ) ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡 )
144 143 breq1d ⊢ ( 𝑢 = ( 𝑦 (,) 𝑧 ) → ( ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ↔ ∫ ( 𝑦 (,) 𝑧 ) ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡 < 𝑒 ) )
145 139 144 imbi12d ⊢ ( 𝑢 = ( 𝑦 (,) 𝑧 ) → ( ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ↔ ( ( ( 𝑦 (,) 𝑧 ) ⊆ 𝐷 ∧ ( vol ‘ ( 𝑦 (,) 𝑧 ) ) < 𝑑 ) → ∫ ( 𝑦 (,) 𝑧 ) ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡 < 𝑒 ) ) )
146 simplr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) )
147 145 146 92 rspcdva ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( ( ( 𝑦 (,) 𝑧 ) ⊆ 𝐷 ∧ ( vol ‘ ( 𝑦 (,) 𝑧 ) ) < 𝑑 ) → ∫ ( 𝑦 (,) 𝑧 ) ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡 < 𝑒 ) )
148 90 135 147 mp2and ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ∫ ( 𝑦 (,) 𝑧 ) ( abs ‘ ( 𝐹 ‘ 𝑡 ) ) d 𝑡 < 𝑒 )
149 99 105 108 109 148 lelttrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( abs ‘ ∫ ( 𝑦 (,) 𝑧 ) ( 𝐹 ‘ 𝑡 ) d 𝑡 ) < 𝑒 )
150 68 149 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ∧ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 )
151 150 expr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ≤ 𝑧 ) ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
152 25 35 38 53 151 wlogle ⊢ ( ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) ∧ ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
153 152 ralrimivva ⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) ∧ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
154 153 ex ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑑 ∈ ℝ+ ) ) → ( ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) ) )
155 154 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑑 ∈ ℝ+ ) → ( ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) ) )
156 155 reximdva ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( 𝑢 ⊆ 𝐷 ∧ ( vol ‘ 𝑢 ) < 𝑑 ) → ∫ 𝑢 ( abs ‘ ( 𝐹 ‘ 𝑤 ) ) d 𝑤 < 𝑒 ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) ) )
157 15 156 mpd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
158 r19.12 ⊢ ( ∃ 𝑑 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
159 157 158 syl ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
160 159 ralrimiva ⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
161 ralcom ⊢ ( ∀ 𝑒 ∈ ℝ+ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) ↔ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
162 160 161 sylib ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) )
163 ax-resscn ⊢ ℝ ⊆ ℂ
164 37 163 sstrdi ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ ℂ )
165 ssid ⊢ ℂ ⊆ ℂ
166 elcncf2 ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) ) ) )
167 164 165 166 sylancl ⊢ ( 𝜑 → ( 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ↔ ( 𝐺 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ∧ ∀ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐺 ‘ 𝑧 ) − ( 𝐺 ‘ 𝑦 ) ) ) < 𝑒 ) ) ) )
168 9 162 167 mpbir2and ⊢ ( 𝜑 → 𝐺 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )