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 25798

Description: Lemma for itgcn 25881. (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 13090	. . 3 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ⁺)
3		itg2cn.5	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4	3	nnrpd 13076	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
5	2, 4	rpdivcld 13095	. 2 ⊢ (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ⁺)
6		simprl 770	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ∈ dom vol)
7		itg2cn.2	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ MblFn)
8	7	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 ∈ MblFn)
9		itg2cn.1	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
10		rge0ssre 13497	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ ℝ
11		fss 6751	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
12	9, 10, 11	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
13	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶ℝ)
14		mbfima 25666	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
15	8, 13, 14	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
16		inmbl 25578	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
17	6, 15, 16	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
18		difmbl 25579	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
19	6, 15, 18	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
20		inass 4227	. . . . . . . . . . 11 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
21		disjdif 4471	. . . . . . . . . . . 12 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
22	21	ineq2i 4216	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (𝑢 ∩ ∅)
23		in0 4394	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ∅) = ∅
24	20, 22, 23	3eqtri 2768	. . . . . . . . . 10 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
25	24	fveq2i 6908	. . . . . . . . 9 ⊢ (vol‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
26		ovol0 25529	. . . . . . . . 9 ⊢ (vol*‘∅) = 0
27	25, 26	eqtri 2764	. . . . . . . 8 ⊢ (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
28	27	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
29		inundif 4478	. . . . . . . . 9 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = 𝑢
30	29	eqcomi 2745	. . . . . . . 8 ⊢ 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))
31	30	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
32		mblss 25567	. . . . . . . . . 10 ⊢ (𝑢 ∈ dom vol → 𝑢 ⊆ ℝ)
33	6, 32	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ⊆ ℝ)
34	33	sselda 3982	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ ℝ)
35	9	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,)+∞))
36	35	ffvelcdmda 7103	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
37		elrege0 13495	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
38	36, 37	sylib 218	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
39	38	simpld 494	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
40	39	rexrd 11312	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ^*)
41	38	simprd 495	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥))
42		elxrge0 13498	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ (0[,]+∞) ↔ ((𝐹‘𝑥) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝑥)))
43	40, 41, 42	sylanbrc 583	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,]+∞))
44	34, 43	syldan 591	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → (𝐹‘𝑥) ∈ (0[,]+∞))
45		eqid 2736	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
46		eqid 2736	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
47		eqid 2736	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))
48		0e0iccpnf 13500	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
49		ifcl 4570	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
50	43, 48, 49	sylancl 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
51	50	fmpttd 7134	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
52		itg2cn.3	. . . . . . . . 9 ⊢ (𝜑 → (∫₂‘𝐹) ∈ ℝ)
53	52	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) ∈ ℝ)
54		icossicc 13477	. . . . . . . . . 10 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
55		fss 6751	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
56	35, 54, 55	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,]+∞))
57	39	leidd 11830	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ (𝐹‘𝑥))
58		breq1 5145	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
59		breq1 5145	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
60	58, 59	ifboth 4564	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
61	57, 41, 60	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
62	61	ralrimiva 3145	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
63		reex 11247	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
64	63	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ ∈ V)
65		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
66	35	feqmptd 6976	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
67	64, 50, 39, 65, 66	ofrfval2 7719	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
68	62, 67	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹)
69		itg2le 25775	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
70	51, 56, 68, 69	syl3anc 1372	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
71		itg2lecl 25774	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
72	51, 53, 70, 71	syl3anc 1372	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
73		ifcl 4570	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
74	43, 48, 73	sylancl 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
75	74	fmpttd 7134	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
76		breq1 5145	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
77		breq1 5145	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
78	76, 77	ifboth 4564	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
79	57, 41, 78	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
80	79	ralrimiva 3145	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
81		eqidd 2737	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
82	64, 74, 39, 81, 66	ofrfval2 7719	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
83	80, 82	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹)
84		itg2le 25775	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
85	75, 56, 83, 84	syl3anc 1372	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
86		itg2lecl 25774	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
87	75, 53, 85, 86	syl3anc 1372	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 25785	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
89	1	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℝ⁺)
90	89	rphalfcld 13090	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ⁺)
91	90	rpred 13078	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ)
92		ifcl 4570	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
93	43, 48, 92	sylancl 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
94	93	fmpttd 7134	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
95		breq1 5145	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
96		breq1 5145	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
97	95, 96	ifboth 4564	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
98	57, 41, 97	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
99	98	ralrimiva 3145	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
100		eqidd 2737	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
101	64, 93, 43, 100, 66	ofrfval2 7719	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
102	99, 101	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹)
103		itg2le 25775	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
104	94, 56, 102, 103	syl3anc 1372	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
105		itg2lecl 25774	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
106	94, 53, 104, 105	syl3anc 1372	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
107		0red 11265	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
108		elinel2 4201	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
109	108	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
110		ifle 13240	. . . . . . . . . . . 12 ⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
111	39, 107, 41, 109, 110	syl31anc 1374	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
112	111	ralrimiva 3145	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
113	64, 50, 93, 65, 100	ofrfval2 7719	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
114	112, 113	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
115		itg2le 25775	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
116	51, 94, 114, 115	syl3anc 1372	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
117	66	fveq2d 6909	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))))
118		cmmbl 25570	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
119	15, 118	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
120		disjdif 4471	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
121	120	fveq2i 6908	. . . . . . . . . . . . . 14 ⊢ (vol‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
122	121, 26	eqtri 2764	. . . . . . . . . . . . 13 ⊢ (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
123	122	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
124		undif2 4476	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ)
125		mblss 25567	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
126	15, 125	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
127		ssequn1 4185	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ ↔ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
128	126, 127	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
129	124, 128	eqtr2id 2789	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
130		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
131		eqid 2736	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
132		iftrue 4530	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0) = (𝐹‘𝑥))
133	132	mpteq2ia 5244	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))
134	133	eqcomi 2745	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0))
135		ifcl 4570	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
136	43, 48, 135	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
137	136	fmpttd 7134	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
138		breq1 5145	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
139		breq1 5145	. . . . . . . . . . . . . . . . . 18 ⊢ (0 = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
140	138, 139	ifboth 4564	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
141	57, 41, 140	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
142	141	ralrimiva 3145	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
143		eqidd 2737	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
144	64, 136, 43, 143, 66	ofrfval2 7719	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
145	142, 144	mpbird 257	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹)
146		itg2le 25775	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
147	137, 56, 145, 146	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
148		itg2lecl 25774	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
149	137, 53, 147, 148	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
150	15, 119, 123, 129, 43, 130, 131, 134, 106, 149	itg2split 25785	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
151	117, 150	eqtrd 2776	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
152		eldif 3960	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
153	152	baib 535	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
154	153	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
155	9	ffnd 6736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 Fn ℝ)
156	155	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
157		elpreima 7077	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
158	156, 157	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
159	39	biantrurd 532	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
160	3	nnred 12282	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ ℝ)
161	160	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ)
162	161	rexrd 11312	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ^*)
163		elioopnf 13484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ ℝ^* → ((𝐹‘𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
164	162, 163	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
165		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
166	165	biantrurd 532	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (𝑀(,)+∞) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
167	159, 164, 166	3bitr2d 307	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
168	161, 39	ltnled 11409	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) ≤ 𝑀))
169	158, 167, 168	3bitr2rd 308	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
170	169	con1bid 355	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝐹‘𝑥) ≤ 𝑀))
171	154, 170	bitrd 279	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ (𝐹‘𝑥) ≤ 𝑀))
172	171	ifbid 4548	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))
173	172	mpteq2dva 5241	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0)))
174	173	fveq2d 6909	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) = (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))))
175		itg2cn.6	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
176	175	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
177	174, 176	eqnbrtrd 5160	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
178	53, 91	resubcld 11692	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘𝐹) − (𝐶 / 2)) ∈ ℝ)
179	178, 149	ltnled 11409	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫₂‘𝐹) − (𝐶 / 2)) < (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ↔ ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2))))
180	177, 179	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘𝐹) − (𝐶 / 2)) < (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))))
181	53, 91, 149	ltsubadd2d 11862	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫₂‘𝐹) − (𝐶 / 2)) < (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ↔ (∫₂‘𝐹) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))))))
182	180, 181	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
183	151, 182	eqbrtrrd 5166	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
184	106, 91, 149	ltadd1d 11857	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) < (𝐶 / 2) ↔ ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))))))
185	183, 184	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) < (𝐶 / 2))
186	72, 106, 91, 116, 185	lelttrd 11420	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
187	160	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ)
188		mblvol 25566	. . . . . . . . . . 11 ⊢ (𝑢 ∈ dom vol → (vol‘𝑢) = (vol*‘𝑢))
189	6, 188	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) = (vol*‘𝑢))
190	5	rpred 13078	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ)
191	190	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ)
192		ovolcl 25514	. . . . . . . . . . . . 13 ⊢ (𝑢 ⊆ ℝ → (vol‘𝑢) ∈ ℝ^)
193	33, 192	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ^)
194	191	rexrd 11312	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ^*)
195		simprr 772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) < ((𝐶 / 2) / 𝑀))
196	189, 195	eqbrtrrd 5166	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) < ((𝐶 / 2) / 𝑀))
197	193, 194, 196	xrltled 13193	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀))
198		ovollecl 25519	. . . . . . . . . . 11 ⊢ ((𝑢 ⊆ ℝ ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ ∧ (vol‘𝑢) ≤ ((𝐶 / 2) / 𝑀)) → (vol‘𝑢) ∈ ℝ)
199	33, 191, 197, 198	syl3anc 1372	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ∈ ℝ)
200	189, 199	eqeltrd 2840	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ)
201	187, 200	remulcld 11292	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) ∈ ℝ)
202	187	rexrd 11312	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ^*)
203	3	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ)
204	203	nnnn0d 12589	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ₀)
205	204	nn0ge0d 12592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ 𝑀)
206		elxrge0 13498	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (0[,]+∞) ↔ (𝑀 ∈ ℝ^* ∧ 0 ≤ 𝑀))
207	202, 205, 206	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,]+∞))
208		ifcl 4570	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
209	207, 48, 208	sylancl 586	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
210	209	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
211	210	fmpttd 7134	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞))
212		eldifn 4131	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
213	212	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
214		difssd 4136	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ⊆ 𝑢)
215	214	sselda 3982	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → 𝑥 ∈ 𝑢)
216	34, 169	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
217	215, 216	syldan 591	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
218	217	con1bid 355	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → (¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝐹‘𝑥) ≤ 𝑀))
219	213, 218	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → (𝐹‘𝑥) ≤ 𝑀)
220		iftrue 4530	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
221	220	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
222	215	iftrued 4532	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ 𝑢, 𝑀, 0) = 𝑀)
223	219, 221, 222	3brtr4d 5174	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
224		iffalse 4533	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
225	224	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
226		0le0 12368	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
227		breq2 5146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 𝑀 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
228		breq2 5146	. . . . . . . . . . . . . . . . 17 ⊢ (0 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
229	227, 228	ifboth 4564	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ 𝑀 ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
230	205, 226, 229	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
231	230	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
232	225, 231	eqbrtrd 5164	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
233	223, 232	pm2.61dan 812	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
234	233	ralrimivw 3149	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
235		eqidd 2737	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)))
236	64, 74, 210, 81, 235	ofrfval2 7719	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
237	234, 236	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)))
238		itg2le 25775	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
239	75, 211, 237, 238	syl3anc 1372	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
240		elrege0 13495	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0[,)+∞) ↔ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀))
241	187, 205, 240	sylanbrc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,)+∞))
242		itg2const 25776	. . . . . . . . . 10 ⊢ ((𝑢 ∈ dom vol ∧ (vol‘𝑢) ∈ ℝ ∧ 𝑀 ∈ (0[,)+∞)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
243	6, 200, 241, 242	syl3anc 1372	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
244	239, 243	breqtrd 5168	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (𝑀 · (vol‘𝑢)))
245	203	nngt0d 12316	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 < 𝑀)
246		ltmuldiv2 12143	. . . . . . . . . 10 ⊢ (((vol‘𝑢) ∈ ℝ ∧ (𝐶 / 2) ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
247	200, 91, 187, 245, 246	syl112anc 1375	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
248	195, 247	mpbird 257	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) < (𝐶 / 2))
249	87, 201, 91, 244, 248	lelttrd 11420	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
250	72, 87, 91, 91, 186, 249	lt2addd 11887	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (𝐶 / 2)))
251	88, 250	eqbrtrd 5164	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < ((𝐶 / 2) + (𝐶 / 2)))
252	89	rpcnd 13080	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℂ)
253	252	2halvesd 12514	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
254	251, 253	breqtrd 5168	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)
255	254	expr 456	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ dom vol) → ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
256	255	ralrimiva 3145	. 2 ⊢ (𝜑 → ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
257		breq2 5146	. . 3 ⊢ (𝑑 = ((𝐶 / 2) / 𝑀) → ((vol‘𝑢) < 𝑑 ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
258	257	rspceaimv 3627	. 2 ⊢ ((((𝐶 / 2) / 𝑀) ∈ ℝ⁺ ∧ ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) → ∃𝑑 ∈ ℝ⁺ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
259	5, 256, 258	syl2anc 584	1 ⊢ (𝜑 → ∃𝑑 ∈ ℝ⁺ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1539 ∈ wcel 2107 ∀wral 3060 ∃wrex 3069 Vcvv 3479 ∖ cdif 3947 ∪ cun 3948 ∩ cin 3949 ⊆ wss 3950 ∅c0 4332 ifcif 4524 class class class wbr 5142 ↦ cmpt 5224 ^◡ccnv 5683 dom cdm 5684 “ cima 5687 Fn wfn 6555 ⟶wf 6556 ‘cfv 6560 (class class class)co 7432 ∘_r cofr 7697 ℝcr 11155 0cc0 11156 + caddc 11159 · cmul 11161 +∞cpnf 11293 ℝ^*cxr 11295 < clt 11296 ≤ cle 11297 − cmin 11493 / cdiv 11921 ℕcn 12267 2c2 12322 ℝ⁺crp 13035 (,)cioo 13388 [,)cico 13390 [,]cicc 13391 vol*covol 25498 volcvol 25499 MblFncmbf 25650 ∫₂citg2 25652

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-rep 5278 ax-sep 5295 ax-nul 5305 ax-pow 5364 ax-pr 5431 ax-un 7756 ax-inf2 9682 ax-cnex 11212 ax-resscn 11213 ax-1cn 11214 ax-icn 11215 ax-addcl 11216 ax-addrcl 11217 ax-mulcl 11218 ax-mulrcl 11219 ax-mulcom 11220 ax-addass 11221 ax-mulass 11222 ax-distr 11223 ax-i2m1 11224 ax-1ne0 11225 ax-1rid 11226 ax-rnegex 11227 ax-rrecex 11228 ax-cnre 11229 ax-pre-lttri 11230 ax-pre-lttrn 11231 ax-pre-ltadd 11232 ax-pre-mulgt0 11233 ax-pre-sup 11234 ax-addf 11235

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3379 df-reu 3380 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-pss 3970 df-nul 4333 df-if 4525 df-pw 4601 df-sn 4626 df-pr 4628 df-op 4632 df-uni 4907 df-int 4946 df-iun 4992 df-disj 5110 df-br 5143 df-opab 5205 df-mpt 5225 df-tr 5259 df-id 5577 df-eprel 5583 df-po 5591 df-so 5592 df-fr 5636 df-se 5637 df-we 5638 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-ord 6386 df-on 6387 df-lim 6388 df-suc 6389 df-iota 6513 df-fun 6562 df-fn 6563 df-f 6564 df-f1 6565 df-fo 6566 df-f1o 6567 df-fv 6568 df-isom 6569 df-riota 7389 df-ov 7435 df-oprab 7436 df-mpo 7437 df-of 7698 df-ofr 7699 df-om 7889 df-1st 8015 df-2nd 8016 df-frecs 8307 df-wrecs 8338 df-recs 8412 df-rdg 8451 df-1o 8507 df-2o 8508 df-er 8746 df-map 8869 df-pm 8870 df-en 8987 df-dom 8988 df-sdom 8989 df-fin 8990 df-fi 9452 df-sup 9483 df-inf 9484 df-oi 9551 df-dju 9942 df-card 9980 df-pnf 11298 df-mnf 11299 df-xr 11300 df-ltxr 11301 df-le 11302 df-sub 11495 df-neg 11496 df-div 11922 df-nn 12268 df-2 12330 df-3 12331 df-n0 12529 df-z 12616 df-uz 12880 df-q 12992 df-rp 13036 df-xneg 13155 df-xadd 13156 df-xmul 13157 df-ioo 13392 df-ico 13394 df-icc 13395 df-fz 13549 df-fzo 13696 df-fl 13833 df-seq 14044 df-exp 14104 df-hash 14371 df-cj 15139 df-re 15140 df-im 15141 df-sqrt 15275 df-abs 15276 df-clim 15525 df-sum 15724 df-rest 17468 df-topgen 17489 df-psmet 21357 df-xmet 21358 df-met 21359 df-bl 21360 df-mopn 21361 df-top 22901 df-topon 22918 df-bases 22954 df-cmp 23396 df-ovol 25500 df-vol 25501 df-mbf 25655 df-itg1 25656 df-itg2 25657 df-0p 25706

This theorem is referenced by: itg2cn 25799

W3C validator