itg2cnlem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > itg2cnlem2		Structured version Visualization version GIF version

Theorem itg2cnlem2 24366

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

**Hypotheses**
Ref	Expression
itg2cn.1	⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
itg2cn.2	⊢ (𝜑 → 𝐹 ∈ MblFn)
itg2cn.3	⊢ (𝜑 → (∫₂‘𝐹) ∈ ℝ)
itg2cn.4	⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
itg2cn.5	⊢ (𝜑 → 𝑀 ∈ ℕ)
itg2cn.6	⊢ (𝜑 → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))

**Assertion**
Ref	Expression
itg2cnlem2	⊢ (𝜑 → ∃𝑑 ∈ ℝ⁺ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))

Distinct variable groups: 𝑢,𝑑,𝑥,𝐶 𝐹,𝑑,𝑢,𝑥 𝜑,𝑢,𝑥 𝑀,𝑑,𝑢,𝑥 Allowed substitution hint: 𝜑(𝑑)

**Proof of Theorem itg2cnlem2**
Step	Hyp	Ref	Expression
1		itg2cn.4	. . . 4 ⊢ (𝜑 → 𝐶 ∈ ℝ⁺)
2	1	rphalfcld 12446	. . 3 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ⁺)
3		itg2cn.5	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4	3	nnrpd 12432	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
5	2, 4	rpdivcld 12451	. 2 ⊢ (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ⁺)
6		simprl 769	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ∈ dom vol)
7		itg2cn.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ MblFn)
8	7	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 ∈ MblFn)
9		itg2cn.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
10		rge0ssre 12847	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ ℝ
11		fss 6530	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
12	9, 10, 11	sylancl 588	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
13	12	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶ℝ)
14		mbfima 24234	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
15	8, 13, 14	syl2anc 586	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
16		inmbl 24146	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
17	6, 15, 16	syl2anc 586	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
18		difmbl 24147	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
19	6, 15, 18	syl2anc 586	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
20		inass 4199	. . . . . . . . . . 11 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
21		disjdif 4424	. . . . . . . . . . . 12 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
22	21	ineq2i 4189	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (𝑢 ∩ ∅)
23		in0 4348	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ∅) = ∅
24	20, 22, 23	3eqtri 2851	. . . . . . . . . 10 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
25	24	fveq2i 6676	. . . . . . . . 9 ⊢ (vol‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
26		ovol0 24097	. . . . . . . . 9 ⊢ (vol*‘∅) = 0
27	25, 26	eqtri 2847	. . . . . . . 8 ⊢ (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
28	27	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
29		inundif 4430	. . . . . . . . 9 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = 𝑢
30	29	eqcomi 2833	. . . . . . . 8 ⊢ 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))
31	30	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
32		mblss 24135	. . . . . . . . . 10 ⊢ (𝑢 ∈ dom vol → 𝑢 ⊆ ℝ)
33	6, 32	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ⊆ ℝ)
34	33	sselda 3970	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ ℝ)
35	9	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,)+∞))
36	35	ffvelrnda 6854	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
37		elrege0 12845	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
38	36, 37	sylib 220	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
39	38	simpld 497	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
40	39	rexrd 10694	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ^*)
41	38	simprd 498	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥))
42		elxrge0 12848	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ (0[,]+∞) ↔ ((𝐹‘𝑥) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝑥)))
43	40, 41, 42	sylanbrc 585	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,]+∞))
44	34, 43	syldan 593	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → (𝐹‘𝑥) ∈ (0[,]+∞))
45		eqid 2824	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
46		eqid 2824	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
47		eqid 2824	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))
48		0e0iccpnf 12850	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
49		ifcl 4514	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
50	43, 48, 49	sylancl 588	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
51	50	fmpttd 6882	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
52		itg2cn.3	. . . . . . . . 9 ⊢ (𝜑 → (∫₂‘𝐹) ∈ ℝ)
53	52	adantr 483	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) ∈ ℝ)
54		icossicc 12827	. . . . . . . . . 10 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
55		fss 6530	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
56	35, 54, 55	sylancl 588	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,]+∞))
57	39	leidd 11209	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ (𝐹‘𝑥))
58		breq1 5072	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
59		breq1 5072	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
60	58, 59	ifboth 4508	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
61	57, 41, 60	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
62	61	ralrimiva 3185	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
63		reex 10631	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
64	63	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ ∈ V)
65		eqidd 2825	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
66	35	feqmptd 6736	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
67	64, 50, 39, 65, 66	ofrfval2 7430	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
68	62, 67	mpbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹)
69		itg2le 24343	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
70	51, 56, 68, 69	syl3anc 1367	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
71		itg2lecl 24342	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
72	51, 53, 70, 71	syl3anc 1367	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
73		ifcl 4514	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
74	43, 48, 73	sylancl 588	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
75	74	fmpttd 6882	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
76		breq1 5072	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
77		breq1 5072	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
78	76, 77	ifboth 4508	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
79	57, 41, 78	syl2anc 586	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
80	79	ralrimiva 3185	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
81		eqidd 2825	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
82	64, 74, 39, 81, 66	ofrfval2 7430	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
83	80, 82	mpbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹)
84		itg2le 24343	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
85	75, 56, 83, 84	syl3anc 1367	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
86		itg2lecl 24342	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
87	75, 53, 85, 86	syl3anc 1367	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 24353	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
89	1	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℝ⁺)
90	89	rphalfcld 12446	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ⁺)
91	90	rpred 12434	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ)
92		ifcl 4514	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
93	43, 48, 92	sylancl 588	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
94	93	fmpttd 6882	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
95		breq1 5072	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
96		breq1 5072	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
97	95, 96	ifboth 4508	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
98	57, 41, 97	syl2anc 586	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
99	98	ralrimiva 3185	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
100		eqidd 2825	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
101	64, 93, 43, 100, 66	ofrfval2 7430	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
102	99, 101	mpbird 259	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹)
103		itg2le 24343	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
104	94, 56, 102, 103	syl3anc 1367	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
105		itg2lecl 24342	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
106	94, 53, 104, 105	syl3anc 1367	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
107		0red 10647	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
108		elinel2 4176	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
109	108	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
110		ifle 12593	. . . . . . . . . . . 12 ⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
111	39, 107, 41, 109, 110	syl31anc 1369	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
112	111	ralrimiva 3185	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
113	64, 50, 93, 65, 100	ofrfval2 7430	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
114	112, 113	mpbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
115		itg2le 24343	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
116	51, 94, 114, 115	syl3anc 1367	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
117	66	fveq2d 6677	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))))
118		cmmbl 24138	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
119	15, 118	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
120		disjdif 4424	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
121	120	fveq2i 6676	. . . . . . . . . . . . . 14 ⊢ (vol‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
122	121, 26	eqtri 2847	. . . . . . . . . . . . 13 ⊢ (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
123	122	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
124		undif2 4428	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ)
125		mblss 24135	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
126	15, 125	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
127		ssequn1 4159	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ ↔ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
128	126, 127	sylib 220	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
129	124, 128	syl5req 2872	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
130		eqid 2824	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
131		eqid 2824	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
132		iftrue 4476	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0) = (𝐹‘𝑥))
133	132	mpteq2ia 5160	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))
134	133	eqcomi 2833	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0))
135		ifcl 4514	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
136	43, 48, 135	sylancl 588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
137	136	fmpttd 6882	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
138		breq1 5072	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
139		breq1 5072	. . . . . . . . . . . . . . . . . 18 ⊢ (0 = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
140	138, 139	ifboth 4508	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
141	57, 41, 140	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
142	141	ralrimiva 3185	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
143		eqidd 2825	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
144	64, 136, 43, 143, 66	ofrfval2 7430	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
145	142, 144	mpbird 259	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹)
146		itg2le 24343	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
147	137, 56, 145, 146	syl3anc 1367	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
148		itg2lecl 24342	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
149	137, 53, 147, 148	syl3anc 1367	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
150	15, 119, 123, 129, 43, 130, 131, 134, 106, 149	itg2split 24353	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
151	117, 150	eqtrd 2859	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
152		eldif 3949	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
153	152	baib 538	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
154	153	adantl 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
155	9	ffnd 6518	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 Fn ℝ)
156	155	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
157		elpreima 6831	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
158	156, 157	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
159	39	biantrurd 535	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
160	3	nnred 11656	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ ℝ)
161	160	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ)
162	161	rexrd 10694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ^*)
163		elioopnf 12834	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℝ^* → ((𝐹‘𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
165		simpr 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
166	165	biantrurd 535	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (𝑀(,)+∞) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
167	159, 164, 166	3bitr2d 309	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
168	161, 39	ltnled 10790	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) ≤ 𝑀))
169	158, 167, 168	3bitr2rd 310	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
170	169	con1bid 358	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝐹‘𝑥) ≤ 𝑀))
171	154, 170	bitrd 281	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ (𝐹‘𝑥) ≤ 𝑀))
172	171	ifbid 4492	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))
173	172	mpteq2dva 5164	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0)))
174	173	fveq2d 6677	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) = (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))))
175		itg2cn.6	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
176	175	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
177	174, 176	eqnbrtrd 5087	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
178	53, 91	resubcld 11071	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘𝐹) − (𝐶 / 2)) ∈ ℝ)
179	178, 149	ltnled 10790	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫₂‘𝐹) − (𝐶 / 2)) < (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ↔ ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2))))
180	177, 179	mpbird 259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘𝐹) − (𝐶 / 2)) < (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))))
181	53, 91, 149	ltsubadd2d 11241	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫₂‘𝐹) − (𝐶 / 2)) < (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ↔ (∫₂‘𝐹) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))))))
182	180, 181	mpbid 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
183	151, 182	eqbrtrrd 5093	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
184	106, 91, 149	ltadd1d 11236	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) < (𝐶 / 2) ↔ ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))))))
185	183, 184	mpbird 259	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) < (𝐶 / 2))
186	72, 106, 91, 116, 185	lelttrd 10801	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
187	160	adantr 483	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ)
188		mblvol 24134	. . . . . . . . . . 11 ⊢ (𝑢 ∈ dom vol → (vol‘𝑢) = (vol*‘𝑢))
189	6, 188	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) = (vol*‘𝑢))
190	5	rpred 12434	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ)
191	190	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ)
192		ovolcl 24082	. . . . . . . . . . . . 13 ⊢ (𝑢 ⊆ ℝ → (vol‘𝑢) ∈ ℝ^)
193	33, 192	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ^)
194	191	rexrd 10694	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ^*)
195		simprr 771	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) < ((𝐶 / 2) / 𝑀))
196	189, 195	eqbrtrrd 5093	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) < ((𝐶 / 2) / 𝑀))
197	193, 194, 196	xrltled 12546	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀))
198		ovollecl 24087	. . . . . . . . . . 11 ⊢ ((𝑢 ⊆ ℝ ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ ∧ (vol‘𝑢) ≤ ((𝐶 / 2) / 𝑀)) → (vol‘𝑢) ∈ ℝ)
199	33, 191, 197, 198	syl3anc 1367	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ∈ ℝ)
200	189, 199	eqeltrd 2916	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ)
201	187, 200	remulcld 10674	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) ∈ ℝ)
202	187	rexrd 10694	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ^*)
203	3	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ)
204	203	nnnn0d 11958	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ₀)
205	204	nn0ge0d 11961	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ 𝑀)
206		elxrge0 12848	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (0[,]+∞) ↔ (𝑀 ∈ ℝ^* ∧ 0 ≤ 𝑀))
207	202, 205, 206	sylanbrc 585	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,]+∞))
208		ifcl 4514	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
209	207, 48, 208	sylancl 588	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
210	209	adantr 483	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
211	210	fmpttd 6882	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞))
212		eldifn 4107	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
213	212	adantl 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
214		difssd 4112	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ⊆ 𝑢)
215	214	sselda 3970	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → 𝑥 ∈ 𝑢)
216	34, 169	syldan 593	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
217	215, 216	syldan 593	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
218	217	con1bid 358	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → (¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝐹‘𝑥) ≤ 𝑀))
219	213, 218	mpbid 234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → (𝐹‘𝑥) ≤ 𝑀)
220		iftrue 4476	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
221	220	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
222	215	iftrued 4478	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ 𝑢, 𝑀, 0) = 𝑀)
223	219, 221, 222	3brtr4d 5101	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
224		iffalse 4479	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
225	224	adantl 484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
226		0le0 11741	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
227		breq2 5073	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 𝑀 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
228		breq2 5073	. . . . . . . . . . . . . . . . 17 ⊢ (0 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
229	227, 228	ifboth 4508	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ 𝑀 ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
230	205, 226, 229	sylancl 588	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
231	230	adantr 483	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
232	225, 231	eqbrtrd 5091	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
233	223, 232	pm2.61dan 811	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
234	233	ralrimivw 3186	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
235		eqidd 2825	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)))
236	64, 74, 210, 81, 235	ofrfval2 7430	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
237	234, 236	mpbird 259	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)))
238		itg2le 24343	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
239	75, 211, 237, 238	syl3anc 1367	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
240		elrege0 12845	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0[,)+∞) ↔ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀))
241	187, 205, 240	sylanbrc 585	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,)+∞))
242		itg2const 24344	. . . . . . . . . 10 ⊢ ((𝑢 ∈ dom vol ∧ (vol‘𝑢) ∈ ℝ ∧ 𝑀 ∈ (0[,)+∞)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
243	6, 200, 241, 242	syl3anc 1367	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
244	239, 243	breqtrd 5095	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (𝑀 · (vol‘𝑢)))
245	203	nngt0d 11689	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 < 𝑀)
246		ltmuldiv2 11517	. . . . . . . . . 10 ⊢ (((vol‘𝑢) ∈ ℝ ∧ (𝐶 / 2) ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
247	200, 91, 187, 245, 246	syl112anc 1370	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
248	195, 247	mpbird 259	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) < (𝐶 / 2))
249	87, 201, 91, 244, 248	lelttrd 10801	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
250	72, 87, 91, 91, 186, 249	lt2addd 11266	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (𝐶 / 2)))
251	88, 250	eqbrtrd 5091	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < ((𝐶 / 2) + (𝐶 / 2)))
252	89	rpcnd 12436	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℂ)
253	252	2halvesd 11886	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
254	251, 253	breqtrd 5095	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)
255	254	expr 459	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ dom vol) → ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
256	255	ralrimiva 3185	. 2 ⊢ (𝜑 → ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
257		breq2 5073	. . 3 ⊢ (𝑑 = ((𝐶 / 2) / 𝑀) → ((vol‘𝑢) < 𝑑 ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
258	257	rspceaimv 3631	. 2 ⊢ ((((𝐶 / 2) / 𝑀) ∈ ℝ⁺ ∧ ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) → ∃𝑑 ∈ ℝ⁺ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
259	5, 256, 258	syl2anc 586	1 ⊢ (𝜑 → ∃𝑑 ∈ ℝ⁺ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 = wceq 1536 ∈ wcel 2113 ∀wral 3141 ∃wrex 3142 Vcvv 3497 ∖ cdif 3936 ∪ cun 3937 ∩ cin 3938 ⊆ wss 3939 ∅c0 4294 ifcif 4470 class class class wbr 5069 ↦ cmpt 5149 ^◡ccnv 5557 dom cdm 5558 “ cima 5561 Fn wfn 6353 ⟶wf 6354 ‘cfv 6358 (class class class)co 7159 ∘_r cofr 7411 ℝcr 10539 0cc0 10540 + caddc 10543 · cmul 10545 +∞cpnf 10675 ℝ^*cxr 10677 < clt 10678 ≤ cle 10679 − cmin 10873 / cdiv 11300 ℕcn 11641 2c2 11695 ℝ⁺crp 12392 (,)cioo 12741 [,)cico 12743 [,]cicc 12744 vol*covol 24066 volcvol 24067 MblFncmbf 24218 ∫₂citg2 24220

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-rep 5193 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 ax-inf2 9107 ax-cnex 10596 ax-resscn 10597 ax-1cn 10598 ax-icn 10599 ax-addcl 10600 ax-addrcl 10601 ax-mulcl 10602 ax-mulrcl 10603 ax-mulcom 10604 ax-addass 10605 ax-mulass 10606 ax-distr 10607 ax-i2m1 10608 ax-1ne0 10609 ax-1rid 10610 ax-rnegex 10611 ax-rrecex 10612 ax-cnre 10613 ax-pre-lttri 10614 ax-pre-lttrn 10615 ax-pre-ltadd 10616 ax-pre-mulgt0 10617 ax-pre-sup 10618 ax-addf 10619

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-fal 1549 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-nel 3127 df-ral 3146 df-rex 3147 df-reu 3148 df-rmo 3149 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-int 4880 df-iun 4924 df-disj 5035 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-se 5518 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-pred 6151 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-isom 6367 df-riota 7117 df-ov 7162 df-oprab 7163 df-mpo 7164 df-of 7412 df-ofr 7413 df-om 7584 df-1st 7692 df-2nd 7693 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-1o 8105 df-2o 8106 df-oadd 8109 df-er 8292 df-map 8411 df-pm 8412 df-en 8513 df-dom 8514 df-sdom 8515 df-fin 8516 df-fi 8878 df-sup 8909 df-inf 8910 df-oi 8977 df-dju 9333 df-card 9371 df-pnf 10680 df-mnf 10681 df-xr 10682 df-ltxr 10683 df-le 10684 df-sub 10875 df-neg 10876 df-div 11301 df-nn 11642 df-2 11703 df-3 11704 df-n0 11901 df-z 11985 df-uz 12247 df-q 12352 df-rp 12393 df-xneg 12510 df-xadd 12511 df-xmul 12512 df-ioo 12745 df-ico 12747 df-icc 12748 df-fz 12896 df-fzo 13037 df-fl 13165 df-seq 13373 df-exp 13433 df-hash 13694 df-cj 14461 df-re 14462 df-im 14463 df-sqrt 14597 df-abs 14598 df-clim 14848 df-sum 15046 df-rest 16699 df-topgen 16720 df-psmet 20540 df-xmet 20541 df-met 20542 df-bl 20543 df-mopn 20544 df-top 21505 df-topon 21522 df-bases 21557 df-cmp 21998 df-ovol 24068 df-vol 24069 df-mbf 24223 df-itg1 24224 df-itg2 24225 df-0p 24274

This theorem is referenced by: itg2cn 24367

W3C validator