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 25729

Description: Lemma for itgcn 25812. (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 12998	. . 3 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ⁺)
3		itg2cn.5	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4	3	nnrpd 12984	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
5	2, 4	rpdivcld 13003	. 2 ⊢ (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ⁺)
6		simprl 771	. . . . . . . 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 13409	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ ℝ
11		fss 6685	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
12	9, 10, 11	sylancl 587	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
13	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶ℝ)
14		mbfima 25597	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
15	8, 13, 14	syl2anc 585	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
16		inmbl 25509	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
17	6, 15, 16	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
18		difmbl 25510	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
19	6, 15, 18	syl2anc 585	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
20		inass 4169	. . . . . . . . . . 11 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
21		disjdif 4413	. . . . . . . . . . . 12 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
22	21	ineq2i 4158	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (𝑢 ∩ ∅)
23		in0 4336	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ∅) = ∅
24	20, 22, 23	3eqtri 2764	. . . . . . . . . 10 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
25	24	fveq2i 6844	. . . . . . . . 9 ⊢ (vol‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
26		ovol0 25460	. . . . . . . . 9 ⊢ (vol*‘∅) = 0
27	25, 26	eqtri 2760	. . . . . . . 8 ⊢ (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
28	27	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
29		inundif 4420	. . . . . . . . 9 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = 𝑢
30	29	eqcomi 2746	. . . . . . . 8 ⊢ 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))
31	30	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
32		mblss 25498	. . . . . . . . . 10 ⊢ (𝑢 ∈ dom vol → 𝑢 ⊆ ℝ)
33	6, 32	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ⊆ ℝ)
34	33	sselda 3922	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ ℝ)
35	9	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,)+∞))
36	35	ffvelcdmda 7037	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
37		elrege0 13407	. . . . . . . . . . . 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 11195	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ^*)
41	38	simprd 495	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥))
42		elxrge0 13410	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ (0[,]+∞) ↔ ((𝐹‘𝑥) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝑥)))
43	40, 41, 42	sylanbrc 584	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,]+∞))
44	34, 43	syldan 592	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → (𝐹‘𝑥) ∈ (0[,]+∞))
45		eqid 2737	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
46		eqid 2737	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
47		eqid 2737	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))
48		0e0iccpnf 13412	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
49		ifcl 4513	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
50	43, 48, 49	sylancl 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
51	50	fmpttd 7068	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
52		itg2cn.3	. . . . . . . . 9 ⊢ (𝜑 → (∫₂‘𝐹) ∈ ℝ)
53	52	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) ∈ ℝ)
54		icossicc 13389	. . . . . . . . . 10 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
55		fss 6685	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
56	35, 54, 55	sylancl 587	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,]+∞))
57	39	leidd 11716	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ (𝐹‘𝑥))
58		breq1 5089	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
59		breq1 5089	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
60	58, 59	ifboth 4507	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
61	57, 41, 60	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
62	61	ralrimiva 3130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
63		reex 11129	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
64	63	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ ∈ V)
65		eqidd 2738	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
66	35	feqmptd 6909	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
67	64, 50, 39, 65, 66	ofrfval2 7652	. . . . . . . . . 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 25706	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
70	51, 56, 68, 69	syl3anc 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
71		itg2lecl 25705	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
72	51, 53, 70, 71	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
73		ifcl 4513	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
74	43, 48, 73	sylancl 587	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
75	74	fmpttd 7068	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
76		breq1 5089	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
77		breq1 5089	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
78	76, 77	ifboth 4507	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
79	57, 41, 78	syl2anc 585	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
80	79	ralrimiva 3130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
81		eqidd 2738	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
82	64, 74, 39, 81, 66	ofrfval2 7652	. . . . . . . . . 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 25706	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
85	75, 56, 83, 84	syl3anc 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
86		itg2lecl 25705	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
87	75, 53, 85, 86	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 25716	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
89	1	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℝ⁺)
90	89	rphalfcld 12998	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ⁺)
91	90	rpred 12986	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ)
92		ifcl 4513	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
93	43, 48, 92	sylancl 587	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
94	93	fmpttd 7068	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
95		breq1 5089	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
96		breq1 5089	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
97	95, 96	ifboth 4507	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
98	57, 41, 97	syl2anc 585	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
99	98	ralrimiva 3130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
100		eqidd 2738	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
101	64, 93, 43, 100, 66	ofrfval2 7652	. . . . . . . . . . 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 25706	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
104	94, 56, 102, 103	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
105		itg2lecl 25705	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
106	94, 53, 104, 105	syl3anc 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
107		0red 11147	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
108		elinel2 4143	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
109	108	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
110		ifle 13149	. . . . . . . . . . . 12 ⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
111	39, 107, 41, 109, 110	syl31anc 1376	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
112	111	ralrimiva 3130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
113	64, 50, 93, 65, 100	ofrfval2 7652	. . . . . . . . . 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 25706	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
116	51, 94, 114, 115	syl3anc 1374	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
117	66	fveq2d 6845	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))))
118		cmmbl 25501	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
119	15, 118	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
120		disjdif 4413	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
121	120	fveq2i 6844	. . . . . . . . . . . . . 14 ⊢ (vol‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
122	121, 26	eqtri 2760	. . . . . . . . . . . . 13 ⊢ (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
123	122	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
124		undif2 4418	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ)
125		mblss 25498	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
126	15, 125	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
127		ssequn1 4127	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ ↔ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
128	126, 127	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
129	124, 128	eqtr2id 2785	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
130		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
131		eqid 2737	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
132		iftrue 4473	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0) = (𝐹‘𝑥))
133	132	mpteq2ia 5181	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))
134	133	eqcomi 2746	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0))
135		ifcl 4513	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
136	43, 48, 135	sylancl 587	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
137	136	fmpttd 7068	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
138		breq1 5089	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
139		breq1 5089	. . . . . . . . . . . . . . . . . 18 ⊢ (0 = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
140	138, 139	ifboth 4507	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
141	57, 41, 140	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
142	141	ralrimiva 3130	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
143		eqidd 2738	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
144	64, 136, 43, 143, 66	ofrfval2 7652	. . . . . . . . . . . . . . 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 25706	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
147	137, 56, 145, 146	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
148		itg2lecl 25705	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
149	137, 53, 147, 148	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
150	15, 119, 123, 129, 43, 130, 131, 134, 106, 149	itg2split 25716	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
151	117, 150	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
152		eldif 3900	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
153	152	baib 535	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
154	153	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
155	9	ffnd 6670	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 Fn ℝ)
156	155	ad2antrr 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
157		elpreima 7011	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
158	156, 157	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
159	39	biantrurd 532	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
160	3	nnred 12189	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ ℝ)
161	160	ad2antrr 727	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ)
162	161	rexrd 11195	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ^*)
163		elioopnf 13396	. . . . . . . . . . . . . . . . . . . . 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 11293	. . . . . . . . . . . . . . . . . . 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 4491	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))
173	172	mpteq2dva 5179	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0)))
174	173	fveq2d 6845	. . . . . . . . . . . . 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 5104	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
178	53, 91	resubcld 11578	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘𝐹) − (𝐶 / 2)) ∈ ℝ)
179	178, 149	ltnled 11293	. . . . . . . . . . . 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 11748	. . . . . . . . . . 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 5110	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
184	106, 91, 149	ltadd1d 11743	. . . . . . . . 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 11304	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
187	160	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ)
188		mblvol 25497	. . . . . . . . . . 11 ⊢ (𝑢 ∈ dom vol → (vol‘𝑢) = (vol*‘𝑢))
189	6, 188	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) = (vol*‘𝑢))
190	5	rpred 12986	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ)
191	190	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ)
192		ovolcl 25445	. . . . . . . . . . . . 13 ⊢ (𝑢 ⊆ ℝ → (vol‘𝑢) ∈ ℝ^)
193	33, 192	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ^)
194	191	rexrd 11195	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ^*)
195		simprr 773	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) < ((𝐶 / 2) / 𝑀))
196	189, 195	eqbrtrrd 5110	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) < ((𝐶 / 2) / 𝑀))
197	193, 194, 196	xrltled 13101	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀))
198		ovollecl 25450	. . . . . . . . . . 11 ⊢ ((𝑢 ⊆ ℝ ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ ∧ (vol‘𝑢) ≤ ((𝐶 / 2) / 𝑀)) → (vol‘𝑢) ∈ ℝ)
199	33, 191, 197, 198	syl3anc 1374	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ∈ ℝ)
200	189, 199	eqeltrd 2837	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ)
201	187, 200	remulcld 11175	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) ∈ ℝ)
202	187	rexrd 11195	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ^*)
203	3	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ)
204	203	nnnn0d 12498	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ₀)
205	204	nn0ge0d 12501	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ 𝑀)
206		elxrge0 13410	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (0[,]+∞) ↔ (𝑀 ∈ ℝ^* ∧ 0 ≤ 𝑀))
207	202, 205, 206	sylanbrc 584	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,]+∞))
208		ifcl 4513	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
209	207, 48, 208	sylancl 587	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
210	209	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
211	210	fmpttd 7068	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞))
212		eldifn 4073	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
213	212	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
214		difssd 4078	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ⊆ 𝑢)
215	214	sselda 3922	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → 𝑥 ∈ 𝑢)
216	34, 169	syldan 592	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
217	215, 216	syldan 592	. . . . . . . . . . . . . . . 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 4473	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
221	220	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
222	215	iftrued 4475	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ 𝑢, 𝑀, 0) = 𝑀)
223	219, 221, 222	3brtr4d 5118	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
224		iffalse 4476	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
225	224	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
226		0le0 12282	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
227		breq2 5090	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 𝑀 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
228		breq2 5090	. . . . . . . . . . . . . . . . 17 ⊢ (0 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
229	227, 228	ifboth 4507	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ 𝑀 ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
230	205, 226, 229	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
231	230	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
232	225, 231	eqbrtrd 5108	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
233	223, 232	pm2.61dan 813	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
234	233	ralrimivw 3134	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
235		eqidd 2738	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)))
236	64, 74, 210, 81, 235	ofrfval2 7652	. . . . . . . . . . 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 25706	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
239	75, 211, 237, 238	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
240		elrege0 13407	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0[,)+∞) ↔ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀))
241	187, 205, 240	sylanbrc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,)+∞))
242		itg2const 25707	. . . . . . . . . 10 ⊢ ((𝑢 ∈ dom vol ∧ (vol‘𝑢) ∈ ℝ ∧ 𝑀 ∈ (0[,)+∞)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
243	6, 200, 241, 242	syl3anc 1374	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
244	239, 243	breqtrd 5112	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (𝑀 · (vol‘𝑢)))
245	203	nngt0d 12226	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 < 𝑀)
246		ltmuldiv2 12030	. . . . . . . . . 10 ⊢ (((vol‘𝑢) ∈ ℝ ∧ (𝐶 / 2) ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
247	200, 91, 187, 245, 246	syl112anc 1377	. . . . . . . . 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 11304	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
250	72, 87, 91, 91, 186, 249	lt2addd 11773	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (𝐶 / 2)))
251	88, 250	eqbrtrd 5108	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < ((𝐶 / 2) + (𝐶 / 2)))
252	89	rpcnd 12988	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℂ)
253	252	2halvesd 12423	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
254	251, 253	breqtrd 5112	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)
255	254	expr 456	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ dom vol) → ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
256	255	ralrimiva 3130	. 2 ⊢ (𝜑 → ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
257		breq2 5090	. . 3 ⊢ (𝑑 = ((𝐶 / 2) / 𝑀) → ((vol‘𝑢) < 𝑑 ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
258	257	rspceaimv 3571	. 2 ⊢ ((((𝐶 / 2) / 𝑀) ∈ ℝ⁺ ∧ ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) → ∃𝑑 ∈ ℝ⁺ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
259	5, 256, 258	syl2anc 585	1 ⊢ (𝜑 → ∃𝑑 ∈ ℝ⁺ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 ∃wrex 3062 Vcvv 3430 ∖ cdif 3887 ∪ cun 3888 ∩ cin 3889 ⊆ wss 3890 ∅c0 4274 ifcif 4467 class class class wbr 5086 ↦ cmpt 5167 ^◡ccnv 5630 dom cdm 5631 “ cima 5634 Fn wfn 6494 ⟶wf 6495 ‘cfv 6499 (class class class)co 7367 ∘_r cofr 7630 ℝcr 11037 0cc0 11038 + caddc 11041 · cmul 11043 +∞cpnf 11176 ℝ^*cxr 11178 < clt 11179 ≤ cle 11180 − cmin 11377 / cdiv 11807 ℕcn 12174 2c2 12236 ℝ⁺crp 12942 (,)cioo 13298 [,)cico 13300 [,]cicc 13301 vol*covol 25429 volcvol 25430 MblFncmbf 25581 ∫₂citg2 25583

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5213 ax-sep 5232 ax-nul 5242 ax-pow 5308 ax-pr 5376 ax-un 7689 ax-inf2 9562 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116 ax-addf 11117

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-disj 5054 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-se 5585 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6266 df-ord 6327 df-on 6328 df-lim 6329 df-suc 6330 df-iota 6455 df-fun 6501 df-fn 6502 df-f 6503 df-f1 6504 df-fo 6505 df-f1o 6506 df-fv 6507 df-isom 6508 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-of 7631 df-ofr 7632 df-om 7818 df-1st 7942 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-1o 8405 df-2o 8406 df-er 8643 df-map 8775 df-pm 8776 df-en 8894 df-dom 8895 df-sdom 8896 df-fin 8897 df-fi 9324 df-sup 9355 df-inf 9356 df-oi 9425 df-dju 9825 df-card 9863 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-n0 12438 df-z 12525 df-uz 12789 df-q 12899 df-rp 12943 df-xneg 13063 df-xadd 13064 df-xmul 13065 df-ioo 13302 df-ico 13304 df-icc 13305 df-fz 13462 df-fzo 13609 df-fl 13751 df-seq 13964 df-exp 14024 df-hash 14293 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198 df-clim 15450 df-sum 15649 df-rest 17385 df-topgen 17406 df-psmet 21344 df-xmet 21345 df-met 21346 df-bl 21347 df-mopn 21348 df-top 22859 df-topon 22876 df-bases 22911 df-cmp 23352 df-ovol 25431 df-vol 25432 df-mbf 25586 df-itg1 25587 df-itg2 25588 df-0p 25637

This theorem is referenced by: itg2cn 25730

W3C validator