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 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑢 ∈ 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 ) ) ) < 𝐶 ) )