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 25700

Description: Lemma for itgcn 25783. (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 12956	. . 3 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ⁺)
3		itg2cn.5	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4	3	nnrpd 12942	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
5	2, 4	rpdivcld 12961	. 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 13366	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ ℝ
11		fss 6675	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
12	9, 10, 11	sylancl 586	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
13	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶ℝ)
14		mbfima 25568	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
15	8, 13, 14	syl2anc 584	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
16		inmbl 25480	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
17	6, 15, 16	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
18		difmbl 25481	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
19	6, 15, 18	syl2anc 584	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
20		inass 4179	. . . . . . . . . . 11 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
21		disjdif 4423	. . . . . . . . . . . 12 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
22	21	ineq2i 4168	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (𝑢 ∩ ∅)
23		in0 4346	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ∅) = ∅
24	20, 22, 23	3eqtri 2760	. . . . . . . . . 10 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
25	24	fveq2i 6834	. . . . . . . . 9 ⊢ (vol‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
26		ovol0 25431	. . . . . . . . 9 ⊢ (vol*‘∅) = 0
27	25, 26	eqtri 2756	. . . . . . . 8 ⊢ (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
28	27	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
29		inundif 4430	. . . . . . . . 9 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = 𝑢
30	29	eqcomi 2742	. . . . . . . 8 ⊢ 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))
31	30	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
32		mblss 25469	. . . . . . . . . 10 ⊢ (𝑢 ∈ dom vol → 𝑢 ⊆ ℝ)
33	6, 32	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ⊆ ℝ)
34	33	sselda 3931	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ ℝ)
35	9	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,)+∞))
36	35	ffvelcdmda 7026	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
37		elrege0 13364	. . . . . . . . . . . 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 11172	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ^*)
41	38	simprd 495	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥))
42		elxrge0 13367	. . . . . . . . 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 2733	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
46		eqid 2733	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
47		eqid 2733	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))
48		0e0iccpnf 13369	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
49		ifcl 4522	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
50	43, 48, 49	sylancl 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
51	50	fmpttd 7057	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
52		itg2cn.3	. . . . . . . . 9 ⊢ (𝜑 → (∫₂‘𝐹) ∈ ℝ)
53	52	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) ∈ ℝ)
54		icossicc 13346	. . . . . . . . . 10 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
55		fss 6675	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
56	35, 54, 55	sylancl 586	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,]+∞))
57	39	leidd 11693	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ (𝐹‘𝑥))
58		breq1 5098	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
59		breq1 5098	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
60	58, 59	ifboth 4516	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
61	57, 41, 60	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
62	61	ralrimiva 3126	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
63		reex 11107	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
64	63	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ ∈ V)
65		eqidd 2734	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
66	35	feqmptd 6899	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
67	64, 50, 39, 65, 66	ofrfval2 7640	. . . . . . . . . 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 25677	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
70	51, 56, 68, 69	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
71		itg2lecl 25676	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
72	51, 53, 70, 71	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
73		ifcl 4522	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
74	43, 48, 73	sylancl 586	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
75	74	fmpttd 7057	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
76		breq1 5098	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
77		breq1 5098	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
78	76, 77	ifboth 4516	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
79	57, 41, 78	syl2anc 584	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
80	79	ralrimiva 3126	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
81		eqidd 2734	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
82	64, 74, 39, 81, 66	ofrfval2 7640	. . . . . . . . . 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 25677	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
85	75, 56, 83, 84	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
86		itg2lecl 25676	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
87	75, 53, 85, 86	syl3anc 1373	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 25687	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
89	1	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℝ⁺)
90	89	rphalfcld 12956	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ⁺)
91	90	rpred 12944	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ)
92		ifcl 4522	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
93	43, 48, 92	sylancl 586	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
94	93	fmpttd 7057	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
95		breq1 5098	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
96		breq1 5098	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
97	95, 96	ifboth 4516	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
98	57, 41, 97	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
99	98	ralrimiva 3126	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
100		eqidd 2734	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
101	64, 93, 43, 100, 66	ofrfval2 7640	. . . . . . . . . . 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 25677	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
104	94, 56, 102, 103	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
105		itg2lecl 25676	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
106	94, 53, 104, 105	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
107		0red 11125	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
108		elinel2 4153	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
109	108	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
110		ifle 13106	. . . . . . . . . . . 12 ⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
111	39, 107, 41, 109, 110	syl31anc 1375	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
112	111	ralrimiva 3126	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
113	64, 50, 93, 65, 100	ofrfval2 7640	. . . . . . . . . 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 25677	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
116	51, 94, 114, 115	syl3anc 1373	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
117	66	fveq2d 6835	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))))
118		cmmbl 25472	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
119	15, 118	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
120		disjdif 4423	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
121	120	fveq2i 6834	. . . . . . . . . . . . . 14 ⊢ (vol‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
122	121, 26	eqtri 2756	. . . . . . . . . . . . 13 ⊢ (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
123	122	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
124		undif2 4428	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ)
125		mblss 25469	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
126	15, 125	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
127		ssequn1 4137	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ ↔ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
128	126, 127	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
129	124, 128	eqtr2id 2781	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
130		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
131		eqid 2733	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
132		iftrue 4482	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0) = (𝐹‘𝑥))
133	132	mpteq2ia 5190	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))
134	133	eqcomi 2742	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0))
135		ifcl 4522	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
136	43, 48, 135	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
137	136	fmpttd 7057	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
138		breq1 5098	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
139		breq1 5098	. . . . . . . . . . . . . . . . . 18 ⊢ (0 = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
140	138, 139	ifboth 4516	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
141	57, 41, 140	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
142	141	ralrimiva 3126	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
143		eqidd 2734	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
144	64, 136, 43, 143, 66	ofrfval2 7640	. . . . . . . . . . . . . . 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 25677	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
147	137, 56, 145, 146	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
148		itg2lecl 25676	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
149	137, 53, 147, 148	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
150	15, 119, 123, 129, 43, 130, 131, 134, 106, 149	itg2split 25687	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
151	117, 150	eqtrd 2768	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
152		eldif 3909	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
153	152	baib 535	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
154	153	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
155	9	ffnd 6660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝐹 Fn ℝ)
156	155	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
157		elpreima 7000	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
158	156, 157	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
159	39	biantrurd 532	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
160	3	nnred 12150	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑀 ∈ ℝ)
161	160	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ)
162	161	rexrd 11172	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ^*)
163		elioopnf 13353	. . . . . . . . . . . . . . . . . . . . 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 11270	. . . . . . . . . . . . . . . . . . 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 4500	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))
173	172	mpteq2dva 5188	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0)))
174	173	fveq2d 6835	. . . . . . . . . . . . 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 5113	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
178	53, 91	resubcld 11555	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘𝐹) − (𝐶 / 2)) ∈ ℝ)
179	178, 149	ltnled 11270	. . . . . . . . . . . 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 11725	. . . . . . . . . . 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 5119	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
184	106, 91, 149	ltadd1d 11720	. . . . . . . . 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 11281	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
187	160	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ)
188		mblvol 25468	. . . . . . . . . . 11 ⊢ (𝑢 ∈ dom vol → (vol‘𝑢) = (vol*‘𝑢))
189	6, 188	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) = (vol*‘𝑢))
190	5	rpred 12944	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ)
191	190	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ)
192		ovolcl 25416	. . . . . . . . . . . . 13 ⊢ (𝑢 ⊆ ℝ → (vol‘𝑢) ∈ ℝ^)
193	33, 192	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ^)
194	191	rexrd 11172	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ^*)
195		simprr 772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) < ((𝐶 / 2) / 𝑀))
196	189, 195	eqbrtrrd 5119	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) < ((𝐶 / 2) / 𝑀))
197	193, 194, 196	xrltled 13059	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀))
198		ovollecl 25421	. . . . . . . . . . 11 ⊢ ((𝑢 ⊆ ℝ ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ ∧ (vol‘𝑢) ≤ ((𝐶 / 2) / 𝑀)) → (vol‘𝑢) ∈ ℝ)
199	33, 191, 197, 198	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ∈ ℝ)
200	189, 199	eqeltrd 2833	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ)
201	187, 200	remulcld 11152	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) ∈ ℝ)
202	187	rexrd 11172	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ^*)
203	3	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ)
204	203	nnnn0d 12452	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ₀)
205	204	nn0ge0d 12455	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ 𝑀)
206		elxrge0 13367	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (0[,]+∞) ↔ (𝑀 ∈ ℝ^* ∧ 0 ≤ 𝑀))
207	202, 205, 206	sylanbrc 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,]+∞))
208		ifcl 4522	. . . . . . . . . . . . 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 7057	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞))
212		eldifn 4083	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
213	212	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
214		difssd 4088	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ⊆ 𝑢)
215	214	sselda 3931	. . . . . . . . . . . . . . . . 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 4482	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
221	220	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
222	215	iftrued 4484	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ 𝑢, 𝑀, 0) = 𝑀)
223	219, 221, 222	3brtr4d 5127	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
224		iffalse 4485	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
225	224	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
226		0le0 12236	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
227		breq2 5099	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 𝑀 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
228		breq2 5099	. . . . . . . . . . . . . . . . 17 ⊢ (0 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
229	227, 228	ifboth 4516	. . . . . . . . . . . . . . . 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 5117	. . . . . . . . . . . . 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 3130	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
235		eqidd 2734	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)))
236	64, 74, 210, 81, 235	ofrfval2 7640	. . . . . . . . . . 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 25677	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_r ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
239	75, 211, 237, 238	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
240		elrege0 13364	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0[,)+∞) ↔ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀))
241	187, 205, 240	sylanbrc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,)+∞))
242		itg2const 25678	. . . . . . . . . 10 ⊢ ((𝑢 ∈ dom vol ∧ (vol‘𝑢) ∈ ℝ ∧ 𝑀 ∈ (0[,)+∞)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
243	6, 200, 241, 242	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
244	239, 243	breqtrd 5121	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (𝑀 · (vol‘𝑢)))
245	203	nngt0d 12184	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 < 𝑀)
246		ltmuldiv2 12006	. . . . . . . . . 10 ⊢ (((vol‘𝑢) ∈ ℝ ∧ (𝐶 / 2) ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
247	200, 91, 187, 245, 246	syl112anc 1376	. . . . . . . . 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 11281	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
250	72, 87, 91, 91, 186, 249	lt2addd 11750	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (𝐶 / 2)))
251	88, 250	eqbrtrd 5117	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < ((𝐶 / 2) + (𝐶 / 2)))
252	89	rpcnd 12946	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℂ)
253	252	2halvesd 12377	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
254	251, 253	breqtrd 5121	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)
255	254	expr 456	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ dom vol) → ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
256	255	ralrimiva 3126	. 2 ⊢ (𝜑 → ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
257		breq2 5099	. . 3 ⊢ (𝑑 = ((𝐶 / 2) / 𝑀) → ((vol‘𝑢) < 𝑑 ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
258	257	rspceaimv 3580	. 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 1541 ∈ wcel 2113 ∀wral 3049 ∃wrex 3058 Vcvv 3438 ∖ cdif 3896 ∪ cun 3897 ∩ cin 3898 ⊆ wss 3899 ∅c0 4284 ifcif 4476 class class class wbr 5095 ↦ cmpt 5176 ^◡ccnv 5620 dom cdm 5621 “ cima 5624 Fn wfn 6484 ⟶wf 6485 ‘cfv 6489 (class class class)co 7355 ∘_r cofr 7618 ℝcr 11015 0cc0 11016 + caddc 11019 · cmul 11021 +∞cpnf 11153 ℝ^*cxr 11155 < clt 11156 ≤ cle 11157 − cmin 11354 / cdiv 11784 ℕcn 12135 2c2 12190 ℝ⁺crp 12900 (,)cioo 13255 [,)cico 13257 [,]cicc 13258 vol*covol 25400 volcvol 25401 MblFncmbf 25552 ∫₂citg2 25554

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-inf2 9541 ax-cnex 11072 ax-resscn 11073 ax-1cn 11074 ax-icn 11075 ax-addcl 11076 ax-addrcl 11077 ax-mulcl 11078 ax-mulrcl 11079 ax-mulcom 11080 ax-addass 11081 ax-mulass 11082 ax-distr 11083 ax-i2m1 11084 ax-1ne0 11085 ax-1rid 11086 ax-rnegex 11087 ax-rrecex 11088 ax-cnre 11089 ax-pre-lttri 11090 ax-pre-lttrn 11091 ax-pre-ltadd 11092 ax-pre-mulgt0 11093 ax-pre-sup 11094 ax-addf 11095

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-disj 5063 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-isom 6498 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-of 7619 df-ofr 7620 df-om 7806 df-1st 7930 df-2nd 7931 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-2o 8395 df-er 8631 df-map 8761 df-pm 8762 df-en 8879 df-dom 8880 df-sdom 8881 df-fin 8882 df-fi 9305 df-sup 9336 df-inf 9337 df-oi 9406 df-dju 9804 df-card 9842 df-pnf 11158 df-mnf 11159 df-xr 11160 df-ltxr 11161 df-le 11162 df-sub 11356 df-neg 11357 df-div 11785 df-nn 12136 df-2 12198 df-3 12199 df-n0 12392 df-z 12479 df-uz 12743 df-q 12857 df-rp 12901 df-xneg 13021 df-xadd 13022 df-xmul 13023 df-ioo 13259 df-ico 13261 df-icc 13262 df-fz 13418 df-fzo 13565 df-fl 13706 df-seq 13919 df-exp 13979 df-hash 14248 df-cj 15016 df-re 15017 df-im 15018 df-sqrt 15152 df-abs 15153 df-clim 15405 df-sum 15604 df-rest 17336 df-topgen 17357 df-psmet 21293 df-xmet 21294 df-met 21295 df-bl 21296 df-mopn 21297 df-top 22819 df-topon 22836 df-bases 22871 df-cmp 23312 df-ovol 25402 df-vol 25403 df-mbf 25557 df-itg1 25558 df-itg2 25559 df-0p 25608

This theorem is referenced by: itg2cn 25701

W3C validator