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 ) ) ) < 𝐶 ) )