Metamath Proof Explorer

Theorem volcn

Description: The function formed by restricting a measurable set to a closed interval with a varying endpoint produces an increasing continuous function on the reals. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Hypothesis volcn.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) )
Assertion volcn ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) → 𝐹 ∈ ( ℝ –cn→ ℝ ) )

Proof

Step Hyp Ref Expression
1 volcn.1 ⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) )
2 simpll ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ dom vol )
3 iccmbl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝐵 [,] 𝑥 ) ∈ dom vol )
4 3 adantll ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐵 [,] 𝑥 ) ∈ dom vol )
5 inmbl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( 𝐵 [,] 𝑥 ) ∈ dom vol ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ∈ dom vol )
6 2 4 5 syl2anc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ∈ dom vol )
7 mblvol ⊢ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ∈ dom vol → ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) )
8 6 7 syl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) )
9 inss2 ⊢ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ⊆ ( 𝐵 [,] 𝑥 )
10 mblss ⊢ ( ( 𝐵 [,] 𝑥 ) ∈ dom vol → ( 𝐵 [,] 𝑥 ) ⊆ ℝ )
11 4 10 syl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐵 [,] 𝑥 ) ⊆ ℝ )
12 mblvol ⊢ ( ( 𝐵 [,] 𝑥 ) ∈ dom vol → ( vol ‘ ( 𝐵 [,] 𝑥 ) ) = ( vol* ‘ ( 𝐵 [,] 𝑥 ) ) )
13 4 12 syl ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( vol ‘ ( 𝐵 [,] 𝑥 ) ) = ( vol* ‘ ( 𝐵 [,] 𝑥 ) ) )
14 iccvolcl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( vol ‘ ( 𝐵 [,] 𝑥 ) ) ∈ ℝ )
15 14 adantll ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( vol ‘ ( 𝐵 [,] 𝑥 ) ) ∈ ℝ )
16 13 15 eqeltrrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( vol* ‘ ( 𝐵 [,] 𝑥 ) ) ∈ ℝ )
17 ovolsscl ⊢ ( ( ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ⊆ ( 𝐵 [,] 𝑥 ) ∧ ( 𝐵 [,] 𝑥 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐵 [,] 𝑥 ) ) ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) ∈ ℝ )
18 9 11 16 17 mp3an2i ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) ∈ ℝ )
19 8 18 eqeltrd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) ∈ ℝ )
20 19 1 fmptd ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
21 simprr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ) → 𝑒 ∈ ℝ+ )
22 oveq12 ⊢ ( ( 𝑣 = 𝑧 ∧ 𝑢 = 𝑦 ) → ( 𝑣 − 𝑢 ) = ( 𝑧 − 𝑦 ) )
23 22 ancoms ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( 𝑣 − 𝑢 ) = ( 𝑧 − 𝑦 ) )
24 23 fveq2d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( abs ‘ ( 𝑣 − 𝑢 ) ) = ( abs ‘ ( 𝑧 − 𝑦 ) ) )
25 24 breq1d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( ( abs ‘ ( 𝑣 − 𝑢 ) ) < 𝑒 ↔ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) )
26 fveq2 ⊢ ( 𝑣 = 𝑧 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑧 ) )
27 fveq2 ⊢ ( 𝑢 = 𝑦 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑦 ) )
28 26 27 oveqan12rd ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( ( 𝐹 ‘ 𝑣 ) − ( 𝐹 ‘ 𝑢 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) )
29 28 fveq2d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − ( 𝐹 ‘ 𝑢 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) )
30 29 breq1d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − ( 𝐹 ‘ 𝑢 ) ) ) < 𝑒 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
31 25 30 imbi12d ⊢ ( ( 𝑢 = 𝑦 ∧ 𝑣 = 𝑧 ) → ( ( ( abs ‘ ( 𝑣 − 𝑢 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − ( 𝐹 ‘ 𝑢 ) ) ) < 𝑒 ) ↔ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) ) )
32 oveq12 ⊢ ( ( 𝑣 = 𝑦 ∧ 𝑢 = 𝑧 ) → ( 𝑣 − 𝑢 ) = ( 𝑦 − 𝑧 ) )
33 32 ancoms ⊢ ( ( 𝑢 = 𝑧 ∧ 𝑣 = 𝑦 ) → ( 𝑣 − 𝑢 ) = ( 𝑦 − 𝑧 ) )
34 33 fveq2d ⊢ ( ( 𝑢 = 𝑧 ∧ 𝑣 = 𝑦 ) → ( abs ‘ ( 𝑣 − 𝑢 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
35 34 breq1d ⊢ ( ( 𝑢 = 𝑧 ∧ 𝑣 = 𝑦 ) → ( ( abs ‘ ( 𝑣 − 𝑢 ) ) < 𝑒 ↔ ( abs ‘ ( 𝑦 − 𝑧 ) ) < 𝑒 ) )
36 fveq2 ⊢ ( 𝑣 = 𝑦 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑦 ) )
37 fveq2 ⊢ ( 𝑢 = 𝑧 → ( 𝐹 ‘ 𝑢 ) = ( 𝐹 ‘ 𝑧 ) )
38 36 37 oveqan12rd ⊢ ( ( 𝑢 = 𝑧 ∧ 𝑣 = 𝑦 ) → ( ( 𝐹 ‘ 𝑣 ) − ( 𝐹 ‘ 𝑢 ) ) = ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) )
39 38 fveq2d ⊢ ( ( 𝑢 = 𝑧 ∧ 𝑣 = 𝑦 ) → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − ( 𝐹 ‘ 𝑢 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
40 39 breq1d ⊢ ( ( 𝑢 = 𝑧 ∧ 𝑣 = 𝑦 ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − ( 𝐹 ‘ 𝑢 ) ) ) < 𝑒 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) < 𝑒 ) )
41 35 40 imbi12d ⊢ ( ( 𝑢 = 𝑧 ∧ 𝑣 = 𝑦 ) → ( ( ( abs ‘ ( 𝑣 − 𝑢 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑣 ) − ( 𝐹 ‘ 𝑢 ) ) ) < 𝑒 ) ↔ ( ( abs ‘ ( 𝑦 − 𝑧 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) < 𝑒 ) ) )
42 ssidd ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) → ℝ ⊆ ℝ )
43 recn ⊢ ( 𝑧 ∈ ℝ → 𝑧 ∈ ℂ )
44 recn ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
45 abssub ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
46 43 44 45 syl2anr ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
47 46 adantl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( abs ‘ ( 𝑦 − 𝑧 ) ) )
48 47 breq1d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ↔ ( abs ‘ ( 𝑦 − 𝑧 ) ) < 𝑒 ) )
49 20 adantr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) → 𝐹 : ℝ ⟶ ℝ )
50 ffvelrn ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
51 ffvelrn ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
52 50 51 anim12dan ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) )
53 49 52 sylan ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) )
54 recn ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ℝ → ( 𝐹 ‘ 𝑧 ) ∈ ℂ )
55 recn ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
56 abssub ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℂ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
57 54 55 56 syl2anr ⊢ ( ( ( 𝐹 ‘ 𝑦 ) ∈ ℝ ∧ ( 𝐹 ‘ 𝑧 ) ∈ ℝ ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
58 53 57 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) )
59 58 breq1d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ↔ ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) < 𝑒 ) )
60 48 59 imbi12d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) ↔ ( ( abs ‘ ( 𝑦 − 𝑧 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑦 ) − ( 𝐹 ‘ 𝑧 ) ) ) < 𝑒 ) ) )
61 simpr2 ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → 𝑧 ∈ ℝ )
62 oveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐵 [,] 𝑥 ) = ( 𝐵 [,] 𝑧 ) )
63 62 ineq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) = ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) )
64 63 fveq2d ⊢ ( 𝑥 = 𝑧 → ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) = ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) )
65 fvex ⊢ ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) ∈ V
66 64 1 65 fvmpt ⊢ ( 𝑧 ∈ ℝ → ( 𝐹 ‘ 𝑧 ) = ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) )
67 61 66 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) = ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) )
68 simplll ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → 𝐴 ∈ dom vol )
69 simplr ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) → 𝐵 ∈ ℝ )
70 69 adantr ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → 𝐵 ∈ ℝ )
71 iccmbl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝐵 [,] 𝑧 ) ∈ dom vol )
72 70 61 71 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐵 [,] 𝑧 ) ∈ dom vol )
73 inmbl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( 𝐵 [,] 𝑧 ) ∈ dom vol ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ∈ dom vol )
74 68 72 73 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ∈ dom vol )
75 mblvol ⊢ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ∈ dom vol → ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) )
76 74 75 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) )
77 67 76 eqtrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) = ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) )
78 simpr1 ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → 𝑦 ∈ ℝ )
79 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐵 [,] 𝑥 ) = ( 𝐵 [,] 𝑦 ) )
80 79 ineq2d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) = ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) )
81 80 fveq2d ⊢ ( 𝑥 = 𝑦 → ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑥 ) ) ) = ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) )
82 fvex ⊢ ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) ∈ V
83 81 1 82 fvmpt ⊢ ( 𝑦 ∈ ℝ → ( 𝐹 ‘ 𝑦 ) = ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) )
84 78 83 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐹 ‘ 𝑦 ) = ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) )
85 simp1 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) → 𝑦 ∈ ℝ )
86 iccmbl ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐵 [,] 𝑦 ) ∈ dom vol )
87 69 85 86 syl2an ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐵 [,] 𝑦 ) ∈ dom vol )
88 inmbl ⊢ ( ( 𝐴 ∈ dom vol ∧ ( 𝐵 [,] 𝑦 ) ∈ dom vol ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∈ dom vol )
89 68 87 88 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∈ dom vol )
90 mblvol ⊢ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∈ dom vol → ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) )
91 89 90 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) = ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) )
92 84 91 eqtrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐹 ‘ 𝑦 ) = ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) )
93 77 92 oveq12d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) = ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) − ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) ) )
94 49 adantr ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → 𝐹 : ℝ ⟶ ℝ )
95 94 61 ffvelrnd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ℝ )
96 77 95 eqeltrrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) ∈ ℝ )
97 70 leidd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → 𝐵 ≤ 𝐵 )
98 simpr3 ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → 𝑦 ≤ 𝑧 )
99 iccss ⊢ ( ( ( 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝐵 ≤ 𝐵 ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐵 [,] 𝑦 ) ⊆ ( 𝐵 [,] 𝑧 ) )
100 70 61 97 98 99 syl22anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐵 [,] 𝑦 ) ⊆ ( 𝐵 [,] 𝑧 ) )
101 sslin ⊢ ( ( 𝐵 [,] 𝑦 ) ⊆ ( 𝐵 [,] 𝑧 ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ⊆ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) )
102 100 101 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ⊆ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) )
103 mblss ⊢ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ∈ dom vol → ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ⊆ ℝ )
104 74 103 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ⊆ ℝ )
105 102 104 sstrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ⊆ ℝ )
106 iccssre ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 [,] 𝑧 ) ⊆ ℝ )
107 78 61 106 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝑦 [,] 𝑧 ) ⊆ ℝ )
108 105 107 unssd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ⊆ ℝ )
109 94 78 ffvelrnd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ℝ )
110 92 109 eqeltrrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) ∈ ℝ )
111 61 78 resubcld ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝑧 − 𝑦 ) ∈ ℝ )
112 110 111 readdcld ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( 𝑧 − 𝑦 ) ) ∈ ℝ )
113 ovolicc ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) → ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) = ( 𝑧 − 𝑦 ) )
114 113 adantl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) = ( 𝑧 − 𝑦 ) )
115 114 111 eqeltrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) ∈ ℝ )
116 ovolun ⊢ ( ( ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ⊆ ℝ ∧ ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) ∈ ℝ ) ∧ ( ( 𝑦 [,] 𝑧 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) ) )
117 105 110 107 115 116 syl22anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) ) )
118 114 oveq2d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( vol* ‘ ( 𝑦 [,] 𝑧 ) ) ) = ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( 𝑧 − 𝑦 ) ) )
119 117 118 breqtrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( 𝑧 − 𝑦 ) ) )
120 ovollecl ⊢ ( ( ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ⊆ ℝ ∧ ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( 𝑧 − 𝑦 ) ) ∈ ℝ ∧ ( vol* ‘ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( 𝑧 − 𝑦 ) ) ) → ( vol* ‘ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ) ∈ ℝ )
121 108 112 119 120 syl3anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ) ∈ ℝ )
122 70 adantr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝐵 ≤ 𝑦 ) → 𝐵 ∈ ℝ )
123 61 adantr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝐵 ≤ 𝑦 ) → 𝑧 ∈ ℝ )
124 78 adantr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝐵 ≤ 𝑦 ) → 𝑦 ∈ ℝ )
125 simpr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝐵 ≤ 𝑦 ) → 𝐵 ≤ 𝑦 )
126 98 adantr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝐵 ≤ 𝑦 ) → 𝑦 ≤ 𝑧 )
127 simp2 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) → 𝑧 ∈ ℝ )
128 elicc2 ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐵 [,] 𝑧 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐵 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ) )
129 69 127 128 syl2an ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝑦 ∈ ( 𝐵 [,] 𝑧 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐵 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ) )
130 129 adantr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝐵 ≤ 𝑦 ) → ( 𝑦 ∈ ( 𝐵 [,] 𝑧 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐵 ≤ 𝑦 ∧ 𝑦 ≤ 𝑧 ) ) )
131 124 125 126 130 mpbir3and ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝐵 ≤ 𝑦 ) → 𝑦 ∈ ( 𝐵 [,] 𝑧 ) )
132 iccsplit ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ∈ ( 𝐵 [,] 𝑧 ) ) → ( 𝐵 [,] 𝑧 ) = ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) )
133 122 123 131 132 syl3anc ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝐵 ≤ 𝑦 ) → ( 𝐵 [,] 𝑧 ) = ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) )
134 eqimss ⊢ ( ( 𝐵 [,] 𝑧 ) = ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) → ( 𝐵 [,] 𝑧 ) ⊆ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) )
135 133 134 syl ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝐵 ≤ 𝑦 ) → ( 𝐵 [,] 𝑧 ) ⊆ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) )
136 78 adantr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑦 ≤ 𝐵 ) → 𝑦 ∈ ℝ )
137 61 adantr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑦 ≤ 𝐵 ) → 𝑧 ∈ ℝ )
138 simpr ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑦 ≤ 𝐵 ) → 𝑦 ≤ 𝐵 )
139 137 leidd ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑦 ≤ 𝐵 ) → 𝑧 ≤ 𝑧 )
140 iccss ⊢ ( ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ∧ ( 𝑦 ≤ 𝐵 ∧ 𝑧 ≤ 𝑧 ) ) → ( 𝐵 [,] 𝑧 ) ⊆ ( 𝑦 [,] 𝑧 ) )
141 136 137 138 139 140 syl22anc ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑦 ≤ 𝐵 ) → ( 𝐵 [,] 𝑧 ) ⊆ ( 𝑦 [,] 𝑧 ) )
142 ssun4 ⊢ ( ( 𝐵 [,] 𝑧 ) ⊆ ( 𝑦 [,] 𝑧 ) → ( 𝐵 [,] 𝑧 ) ⊆ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) )
143 141 142 syl ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) ∧ 𝑦 ≤ 𝐵 ) → ( 𝐵 [,] 𝑧 ) ⊆ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) )
144 70 78 135 143 lecasei ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐵 [,] 𝑧 ) ⊆ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) )
145 sslin ⊢ ( ( 𝐵 [,] 𝑧 ) ⊆ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ⊆ ( 𝐴 ∩ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) ) )
146 144 145 syl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ⊆ ( 𝐴 ∩ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) ) )
147 indi ⊢ ( 𝐴 ∩ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) ) = ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝐴 ∩ ( 𝑦 [,] 𝑧 ) ) )
148 inss2 ⊢ ( 𝐴 ∩ ( 𝑦 [,] 𝑧 ) ) ⊆ ( 𝑦 [,] 𝑧 )
149 unss2 ⊢ ( ( 𝐴 ∩ ( 𝑦 [,] 𝑧 ) ) ⊆ ( 𝑦 [,] 𝑧 ) → ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝐴 ∩ ( 𝑦 [,] 𝑧 ) ) ) ⊆ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) )
150 148 149 ax-mp ⊢ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝐴 ∩ ( 𝑦 [,] 𝑧 ) ) ) ⊆ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) )
151 147 150 eqsstri ⊢ ( 𝐴 ∩ ( ( 𝐵 [,] 𝑦 ) ∪ ( 𝑦 [,] 𝑧 ) ) ) ⊆ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) )
152 146 151 sstrdi ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ⊆ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) )
153 ovolss ⊢ ( ( ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ⊆ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ∧ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ⊆ ℝ ) → ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) ≤ ( vol* ‘ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ) )
154 152 108 153 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) ≤ ( vol* ‘ ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ∪ ( 𝑦 [,] 𝑧 ) ) ) )
155 96 121 112 154 119 letrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( 𝑧 − 𝑦 ) ) )
156 96 110 111 lesubadd2d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) − ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) ) ≤ ( 𝑧 − 𝑦 ) ↔ ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) ≤ ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) + ( 𝑧 − 𝑦 ) ) ) )
157 155 156 mpbird ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) − ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) ) ≤ ( 𝑧 − 𝑦 ) )
158 93 157 eqbrtrd ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝑧 − 𝑦 ) )
159 95 109 resubcld ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ )
160 simplr ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → 𝑒 ∈ ℝ+ )
161 160 rpred ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → 𝑒 ∈ ℝ )
162 lelttr ⊢ ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ∈ ℝ ∧ ( 𝑧 − 𝑦 ) ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝑧 − 𝑦 ) ∧ ( 𝑧 − 𝑦 ) < 𝑒 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) < 𝑒 ) )
163 159 111 161 162 syl3anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ≤ ( 𝑧 − 𝑦 ) ∧ ( 𝑧 − 𝑦 ) < 𝑒 ) → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) < 𝑒 ) )
164 158 163 mpand ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( 𝑧 − 𝑦 ) < 𝑒 → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) < 𝑒 ) )
165 abssubge0 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( 𝑧 − 𝑦 ) )
166 165 adantl ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( abs ‘ ( 𝑧 − 𝑦 ) ) = ( 𝑧 − 𝑦 ) )
167 166 breq1d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ↔ ( 𝑧 − 𝑦 ) < 𝑒 ) )
168 ovolss ⊢ ( ( ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ⊆ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ∧ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ⊆ ℝ ) → ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) ≤ ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) )
169 102 104 168 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑦 ) ) ) ≤ ( vol* ‘ ( 𝐴 ∩ ( 𝐵 [,] 𝑧 ) ) ) )
170 169 92 77 3brtr4d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( 𝐹 ‘ 𝑦 ) ≤ ( 𝐹 ‘ 𝑧 ) )
171 109 95 170 abssubge0d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) )
172 171 breq1d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ↔ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) < 𝑒 ) )
173 164 167 172 3imtr4d ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ∧ 𝑦 ≤ 𝑧 ) ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
174 31 41 42 60 173 wlogle ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑧 ∈ ℝ ) ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
175 174 anassrs ⊢ ( ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ ) ∧ 𝑧 ∈ ℝ ) → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
176 175 ralrimiva ⊢ ( ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑦 ∈ ℝ ) → ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
177 176 anasss ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑒 ∈ ℝ+ ∧ 𝑦 ∈ ℝ ) ) → ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
178 177 ancom2s ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ) → ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
179 breq2 ⊢ ( 𝑑 = 𝑒 → ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 ↔ ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 ) )
180 179 rspceaimv ⊢ ( ( 𝑒 ∈ ℝ+ ∧ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑒 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
181 21 178 180 syl2anc ⊢ ( ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) ∧ ( 𝑦 ∈ ℝ ∧ 𝑒 ∈ ℝ+ ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
182 181 ralrimivva ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) → ∀ 𝑦 ∈ ℝ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) )
183 ax-resscn ⊢ ℝ ⊆ ℂ
184 elcncf2 ⊢ ( ( ℝ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( 𝐹 ∈ ( ℝ –cn→ ℝ ) ↔ ( 𝐹 : ℝ ⟶ ℝ ∧ ∀ 𝑦 ∈ ℝ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) ) ) )
185 183 183 184 mp2an ⊢ ( 𝐹 ∈ ( ℝ –cn→ ℝ ) ↔ ( 𝐹 : ℝ ⟶ ℝ ∧ ∀ 𝑦 ∈ ℝ ∀ 𝑒 ∈ ℝ+ ∃ 𝑑 ∈ ℝ+ ∀ 𝑧 ∈ ℝ ( ( abs ‘ ( 𝑧 − 𝑦 ) ) < 𝑑 → ( abs ‘ ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑒 ) ) )
186 20 182 185 sylanbrc ⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ ℝ ) → 𝐹 ∈ ( ℝ –cn→ ℝ ) )