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

Metamath Proof Explorer

Theorem itg2cnlem2

Description: Lemma for itgcn . (Contributed by Mario Carneiro, 31-Aug-2014)

Ref Expression
Hypotheses itg2cn.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
itg2cn.2 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
itg2cn.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
itg2cn.4 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
itg2cn.5 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
itg2cn.6 ⊢ ( 𝜑 → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
Assertion itg2cnlem2 ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) )

Proof

Step Hyp Ref Expression
1 itg2cn.1 ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
2 itg2cn.2 ⊢ ( 𝜑 → 𝐹 ∈ MblFn )
3 itg2cn.3 ⊢ ( 𝜑 → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
4 itg2cn.4 ⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
5 itg2cn.5 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
6 itg2cn.6 ⊢ ( 𝜑 → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
7 4 rphalfcld ⊢ ( 𝜑 → ( 𝐶 / 2 ) ∈ ℝ+ )
8 5 nnrpd ⊢ ( 𝜑 → 𝑀 ∈ ℝ+ )
9 7 8 rpdivcld ⊢ ( 𝜑 → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ+ )
10 simprl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑢 ∈ dom vol )
11 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 ∈ MblFn )
12 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
13 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ℝ ) → 𝐹 : ℝ ⟶ ℝ )
14 1 12 13 sylancl ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
15 14 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 : ℝ ⟶ ℝ )
16 mbfima ⊢ ( ( 𝐹 ∈ MblFn ∧ 𝐹 : ℝ ⟶ ℝ ) → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol )
17 11 15 16 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol )
18 inmbl ⊢ ( ( 𝑢 ∈ dom vol ∧ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) → ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol )
19 10 17 18 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol )
20 difmbl ⊢ ( ( 𝑢 ∈ dom vol ∧ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol ) → ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol )
21 10 17 20 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol )
22 inass ⊢ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ( 𝑢 ∩ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) )
23 disjdif ⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ∅
24 23 ineq2i ⊢ ( 𝑢 ∩ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = ( 𝑢 ∩ ∅ )
25 in0 ⊢ ( 𝑢 ∩ ∅ ) = ∅
26 22 24 25 3eqtri ⊢ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ∅
27 26 fveq2i ⊢ ( vol* ‘ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = ( vol* ‘ ∅ )
28 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
29 27 28 eqtri ⊢ ( vol* ‘ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0
30 29 a1i ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∩ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 )
31 inundif ⊢ ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∪ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = 𝑢
32 31 eqcomi ⊢ 𝑢 = ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∪ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) )
33 32 a1i ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑢 = ( ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∪ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) )
34 mblss ⊢ ( 𝑢 ∈ dom vol → 𝑢 ⊆ ℝ )
35 10 34 syl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑢 ⊆ ℝ )
36 35 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑢 ) → 𝑥 ∈ ℝ )
37 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) )
38 37 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) )
39 elrege0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
40 38 39 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
41 40 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
42 41 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ* )
43 40 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 0 ≤ ( 𝐹 ‘ 𝑥 ) )
44 elxrge0 ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
45 42 43 44 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
46 36 45 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑢 ) → ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) )
47 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
48 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
49 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
50 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
51 ifcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
52 45 50 51 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
53 52 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
54 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) ∈ ℝ )
55 icossicc ⊢ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
56 fss ⊢ ( ( 𝐹 : ℝ ⟶ ( 0 [,) +∞ ) ∧ ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
57 37 55 56 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) )
58 41 leidd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) )
59 breq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
60 breq1 ⊢ ( 0 = if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
61 59 60 ifboth ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
62 58 43 61 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
63 62 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
64 reex ⊢ ℝ ∈ V
65 64 a1i ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ℝ ∈ V )
66 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
67 37 feqmptd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) )
68 65 52 41 66 67 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
69 63 68 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 )
70 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
71 53 57 69 70 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
72 itg2lecl ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
73 53 54 71 72 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
74 ifcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
75 45 50 74 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
76 75 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
77 breq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
78 breq1 ⊢ ( 0 = if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
79 77 78 ifboth ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
80 58 43 79 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
81 80 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
82 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
83 65 75 41 82 67 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
84 81 83 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 )
85 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
86 76 57 84 85 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
87 itg2lecl ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
88 76 54 86 87 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
89 19 21 30 33 46 47 48 49 73 88 itg2split ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) )
90 4 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐶 ∈ ℝ+ )
91 90 rphalfcld ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝐶 / 2 ) ∈ ℝ+ )
92 91 rpred ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝐶 / 2 ) ∈ ℝ )
93 ifcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
94 45 50 93 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
95 94 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
96 breq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
97 breq1 ⊢ ( 0 = if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
98 96 97 ifboth ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
99 58 43 98 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
100 99 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
101 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
102 65 94 45 101 67 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
103 100 102 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 )
104 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
105 95 57 103 104 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
106 itg2lecl ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
107 95 54 105 106 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
108 0red ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 0 ∈ ℝ )
109 elinel2 ⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) )
110 109 a1i ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) )
111 ifle ⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) ∧ ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
112 41 108 43 110 111 syl31anc ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
113 112 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
114 65 52 94 66 101 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
115 113 114 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
116 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
117 53 95 115 116 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
118 67 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) )
119 cmmbl ⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol → ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol )
120 17 119 syl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ∈ dom vol )
121 disjdif ⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ∅
122 121 fveq2i ⊢ ( vol* ‘ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = ( vol* ‘ ∅ )
123 122 28 eqtri ⊢ ( vol* ‘ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0
124 123 a1i ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∩ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) ) = 0 )
125 undif2 ⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) = ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ℝ )
126 mblss ⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∈ dom vol → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ⊆ ℝ )
127 17 126 syl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ⊆ ℝ )
128 ssequn1 ⊢ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ⊆ ℝ ↔ ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ℝ ) = ℝ )
129 127 128 sylib ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ℝ ) = ℝ )
130 125 129 eqtr2id ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ℝ = ( ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ∪ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) )
131 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
132 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) )
133 iftrue ⊢ ( 𝑥 ∈ ℝ → if ( 𝑥 ∈ ℝ , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
134 133 mpteq2ia ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ℝ , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) )
135 134 eqcomi ⊢ ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ℝ , ( 𝐹 ‘ 𝑥 ) , 0 ) )
136 ifcl ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
137 45 50 136 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ∈ ( 0 [,] +∞ ) )
138 137 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
139 breq1 ⊢ ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
140 breq1 ⊢ ( 0 = if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) → ( 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
141 139 140 ifboth ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑥 ) ∧ 0 ≤ ( 𝐹 ‘ 𝑥 ) ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
142 58 43 141 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
143 142 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) )
144 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
145 65 137 45 144 67 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ ( 𝐹 ‘ 𝑥 ) ) )
146 143 145 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 )
147 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ 𝐹 : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ 𝐹 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
148 138 57 146 147 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) )
149 itg2lecl ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ 𝐹 ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ 𝐹 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
150 138 54 148 149 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ∈ ℝ )
151 17 120 124 130 45 131 132 135 107 150 itg2split ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ( 𝐹 ‘ 𝑥 ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) )
152 118 151 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) )
153 eldif ⊢ ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) )
154 153 baib ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) )
155 154 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) )
156 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn ℝ )
157 156 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝐹 Fn ℝ )
158 elpreima ⊢ ( 𝐹 Fn ℝ → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) )
159 157 158 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) )
160 41 biantrurd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 < ( 𝐹 ‘ 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑀 < ( 𝐹 ‘ 𝑥 ) ) ) )
161 5 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
162 161 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑀 ∈ ℝ )
163 162 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑀 ∈ ℝ* )
164 elioopnf ⊢ ( 𝑀 ∈ ℝ* → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑀 < ( 𝐹 ‘ 𝑥 ) ) ) )
165 163 164 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ∧ 𝑀 < ( 𝐹 ‘ 𝑥 ) ) ) )
166 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
167 166 biantrurd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) )
168 160 165 167 3bitr2d ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 < ( 𝐹 ‘ 𝑥 ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝑀 (,) +∞ ) ) ) )
169 162 41 ltnled ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑀 < ( 𝐹 ‘ 𝑥 ) ↔ ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) )
170 159 168 169 3bitr2rd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) )
171 170 con1bid ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) )
172 155 171 bitrd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) )
173 172 ifbid ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) )
174 173 mpteq2dva ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) )
175 174 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
176 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
177 175 176 eqnbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) )
178 54 92 resubcld ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ∈ ℝ )
179 178 150 ltnled ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ↔ ¬ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) ) )
180 177 179 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) )
181 54 92 150 ltsubadd2d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ( ∫2 ‘ 𝐹 ) − ( 𝐶 / 2 ) ) < ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ↔ ( ∫2 ‘ 𝐹 ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) )
182 180 181 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ 𝐹 ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) )
183 152 182 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) )
184 107 92 150 ltadd1d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) ↔ ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) < ( ( 𝐶 / 2 ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ℝ ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) ) )
185 183 184 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) )
186 73 107 92 117 185 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) )
187 161 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℝ )
188 mblvol ⊢ ( 𝑢 ∈ dom vol → ( vol ‘ 𝑢 ) = ( vol* ‘ 𝑢 ) )
189 10 188 syl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol ‘ 𝑢 ) = ( vol* ‘ 𝑢 ) )
190 9 rpred ⊢ ( 𝜑 → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ )
191 190 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ )
192 ovolcl ⊢ ( 𝑢 ⊆ ℝ → ( vol* ‘ 𝑢 ) ∈ ℝ* )
193 35 192 syl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) ∈ ℝ* )
194 191 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ* )
195 simprr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) )
196 189 195 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) )
197 193 194 196 xrltled ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) ≤ ( ( 𝐶 / 2 ) / 𝑀 ) )
198 ovollecl ⊢ ( ( 𝑢 ⊆ ℝ ∧ ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ ∧ ( vol* ‘ 𝑢 ) ≤ ( ( 𝐶 / 2 ) / 𝑀 ) ) → ( vol* ‘ 𝑢 ) ∈ ℝ )
199 35 191 197 198 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol* ‘ 𝑢 ) ∈ ℝ )
200 189 199 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( vol ‘ 𝑢 ) ∈ ℝ )
201 187 200 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑀 · ( vol ‘ 𝑢 ) ) ∈ ℝ )
202 187 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℝ* )
203 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℕ )
204 203 nnnn0d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ℕ0 )
205 204 nn0ge0d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 0 ≤ 𝑀 )
206 elxrge0 ⊢ ( 𝑀 ∈ ( 0 [,] +∞ ) ↔ ( 𝑀 ∈ ℝ* ∧ 0 ≤ 𝑀 ) )
207 202 205 206 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ( 0 [,] +∞ ) )
208 ifcl ⊢ ( ( 𝑀 ∈ ( 0 [,] +∞ ) ∧ 0 ∈ ( 0 [,] +∞ ) ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ∈ ( 0 [,] +∞ ) )
209 207 50 208 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ∈ ( 0 [,] +∞ ) )
210 209 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ∈ ( 0 [,] +∞ ) )
211 210 fmpttd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
212 eldifn ⊢ ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) )
213 212 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) )
214 difssd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ⊆ 𝑢 )
215 214 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → 𝑥 ∈ 𝑢 )
216 36 170 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ 𝑢 ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) )
217 215 216 syldan ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ( ¬ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ↔ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) )
218 217 con1bid ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ( ¬ 𝑥 ∈ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ↔ ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 ) )
219 213 218 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → ( 𝐹 ‘ 𝑥 ) ≤ 𝑀 )
220 iftrue ⊢ ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
221 220 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = ( 𝐹 ‘ 𝑥 ) )
222 215 iftrued ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) = 𝑀 )
223 219 221 222 3brtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) )
224 iffalse ⊢ ( ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 )
225 224 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) = 0 )
226 0le0 ⊢ 0 ≤ 0
227 breq2 ⊢ ( 𝑀 = if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) → ( 0 ≤ 𝑀 ↔ 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) )
228 breq2 ⊢ ( 0 = if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) )
229 227 228 ifboth ⊢ ( ( 0 ≤ 𝑀 ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) )
230 205 226 229 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) )
231 230 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → 0 ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) )
232 225 231 eqbrtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) ∧ ¬ 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) )
233 223 232 pm2.61dan ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) )
234 233 ralrimivw ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) )
235 eqidd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) )
236 65 75 210 82 235 ofrfval2 ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ≤ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) )
237 234 236 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) )
238 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) )
239 76 211 237 238 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) )
240 elrege0 ⊢ ( 𝑀 ∈ ( 0 [,) +∞ ) ↔ ( 𝑀 ∈ ℝ ∧ 0 ≤ 𝑀 ) )
241 187 205 240 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝑀 ∈ ( 0 [,) +∞ ) )
242 itg2const ⊢ ( ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) ∈ ℝ ∧ 𝑀 ∈ ( 0 [,) +∞ ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) = ( 𝑀 · ( vol ‘ 𝑢 ) ) )
243 10 200 241 242 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , 𝑀 , 0 ) ) ) = ( 𝑀 · ( vol ‘ 𝑢 ) ) )
244 239 243 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ≤ ( 𝑀 · ( vol ‘ 𝑢 ) ) )
245 203 nngt0d ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 0 < 𝑀 )
246 ltmuldiv2 ⊢ ( ( ( vol ‘ 𝑢 ) ∈ ℝ ∧ ( 𝐶 / 2 ) ∈ ℝ ∧ ( 𝑀 ∈ ℝ ∧ 0 < 𝑀 ) ) → ( ( 𝑀 · ( vol ‘ 𝑢 ) ) < ( 𝐶 / 2 ) ↔ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) )
247 200 92 187 245 246 syl112anc ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝑀 · ( vol ‘ 𝑢 ) ) < ( 𝐶 / 2 ) ↔ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) )
248 195 247 mpbird ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( 𝑀 · ( vol ‘ 𝑢 ) ) < ( 𝐶 / 2 ) )
249 88 201 92 244 248 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( 𝐶 / 2 ) )
250 73 88 92 92 186 249 lt2addd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∩ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ ( 𝑢 ∖ ( ◡ 𝐹 “ ( 𝑀 (,) +∞ ) ) ) , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) ) < ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) )
251 89 250 eqbrtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) )
252 90 rpcnd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → 𝐶 ∈ ℂ )
253 252 2halvesd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ( 𝐶 / 2 ) + ( 𝐶 / 2 ) ) = 𝐶 )
254 251 253 breqtrd ⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ dom vol ∧ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 )
255 254 expr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ dom vol ) → ( ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) )
256 255 ralrimiva ⊢ ( 𝜑 → ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) )
257 breq2 ⊢ ( 𝑑 = ( ( 𝐶 / 2 ) / 𝑀 ) → ( ( vol ‘ 𝑢 ) < 𝑑 ↔ ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) ) )
258 257 rspceaimv ⊢ ( ( ( ( 𝐶 / 2 ) / 𝑀 ) ∈ ℝ+ ∧ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < ( ( 𝐶 / 2 ) / 𝑀 ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) ) → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) )
259 9 256 258 syl2anc ⊢ ( 𝜑 → ∃ 𝑑 ∈ ℝ+ ∀ 𝑢 ∈ dom vol ( ( vol ‘ 𝑢 ) < 𝑑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝑢 , ( 𝐹 ‘ 𝑥 ) , 0 ) ) ) < 𝐶 ) )