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 23335

Description: Lemma for itgcn 23415. (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 11760	. . 3 ⊢ (𝜑 → (𝐶 / 2) ∈ ℝ⁺)
3		itg2cn.5	. . . 4 ⊢ (𝜑 → 𝑀 ∈ ℕ)
4	3	nnrpd 11746	. . 3 ⊢ (𝜑 → 𝑀 ∈ ℝ⁺)
5	2, 4	rpdivcld 11765	. 2 ⊢ (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ⁺)
6		simprl 790	. . . . . . . 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 12151	. . . . . . . . . . 11 ⊢ (0[,)+∞) ⊆ ℝ
11		fss 5969	. . . . . . . . . . 11 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ ℝ) → 𝐹:ℝ⟶ℝ)
12	9, 10, 11	sylancl 693	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹:ℝ⟶ℝ)
13	12	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶ℝ)
14		mbfima 23205	. . . . . . . . 9 ⊢ ((𝐹 ∈ MblFn ∧ 𝐹:ℝ⟶ℝ) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
15	8, 13, 14	syl2anc 691	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol)
16		inmbl 23117	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
17	6, 15, 16	syl2anc 691	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
18		difmbl 23118	. . . . . . . 8 ⊢ ((𝑢 ∈ dom vol ∧ (^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
19	6, 15, 18	syl2anc 691	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
20		inass 3785	. . . . . . . . . . 11 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
21		disjdif 3992	. . . . . . . . . . . 12 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
22	21	ineq2i 3773	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (𝑢 ∩ ∅)
23		in0 3920	. . . . . . . . . . 11 ⊢ (𝑢 ∩ ∅) = ∅
24	20, 22, 23	3eqtri 2636	. . . . . . . . . 10 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
25	24	fveq2i 6106	. . . . . . . . 9 ⊢ (vol‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
26		ovol0 23068	. . . . . . . . 9 ⊢ (vol*‘∅) = 0
27	25, 26	eqtri 2632	. . . . . . . 8 ⊢ (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
28	27	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∩ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
29		inundif 3998	. . . . . . . . 9 ⊢ ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = 𝑢
30	29	eqcomi 2619	. . . . . . . 8 ⊢ 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))))
31	30	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 = ((𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) ∪ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
32		mblss 23106	. . . . . . . . . 10 ⊢ (𝑢 ∈ dom vol → 𝑢 ⊆ ℝ)
33	6, 32	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑢 ⊆ ℝ)
34	33	sselda 3568	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → 𝑥 ∈ ℝ)
35	9	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,)+∞))
36	35	ffvelrnda 6267	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,)+∞))
37		elrege0 12149	. . . . . . . . . . . 12 ⊢ ((𝐹‘𝑥) ∈ (0[,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
38	36, 37	sylib 207	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)))
39	38	simpld 474	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ)
40	39	rexrd 9968	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ ℝ^*)
41	38	simprd 478	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ≤ (𝐹‘𝑥))
42		elxrge0 12152	. . . . . . . . 9 ⊢ ((𝐹‘𝑥) ∈ (0[,]+∞) ↔ ((𝐹‘𝑥) ∈ ℝ^* ∧ 0 ≤ (𝐹‘𝑥)))
43	40, 41, 42	sylanbrc 695	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ∈ (0[,]+∞))
44	34, 43	syldan 486	. . . . . . 7 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → (𝐹‘𝑥) ∈ (0[,]+∞))
45		eqid 2610	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
46		eqid 2610	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
47		eqid 2610	. . . . . . 7 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))
48		0e0iccpnf 12154	. . . . . . . . . 10 ⊢ 0 ∈ (0[,]+∞)
49		ifcl 4080	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
50	43, 48, 49	sylancl 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
51	50, 45	fmptd 6292	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
52		itg2cn.3	. . . . . . . . 9 ⊢ (𝜑 → (∫₂‘𝐹) ∈ ℝ)
53	52	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) ∈ ℝ)
54		icossicc 12131	. . . . . . . . . 10 ⊢ (0[,)+∞) ⊆ (0[,]+∞)
55		fss 5969	. . . . . . . . . 10 ⊢ ((𝐹:ℝ⟶(0[,)+∞) ∧ (0[,)+∞) ⊆ (0[,]+∞)) → 𝐹:ℝ⟶(0[,]+∞))
56	35, 54, 55	sylancl 693	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹:ℝ⟶(0[,]+∞))
57	39	leidd 10473	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝐹‘𝑥) ≤ (𝐹‘𝑥))
58		breq1 4586	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
59		breq1 4586	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
60	58, 59	ifboth 4074	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
61	57, 41, 60	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
62	61	ralrimiva 2949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
63		reex 9906	. . . . . . . . . . . 12 ⊢ ℝ ∈ V
64	63	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ ∈ V)
65		eqidd 2611	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
66	35	feqmptd 6159	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
67	64, 50, 39, 65, 66	ofrfval2 6813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
68	62, 67	mpbird 246	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹)
69		itg2le 23312	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
70	51, 56, 68, 69	syl3anc 1318	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
71		itg2lecl 23311	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
72	51, 53, 70, 71	syl3anc 1318	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
73		ifcl 4080	. . . . . . . . . 10 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
74	43, 48, 73	sylancl 693	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
75	74, 46	fmptd 6292	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
76		breq1 4586	. . . . . . . . . . . . 13 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
77		breq1 4586	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
78	76, 77	ifboth 4074	. . . . . . . . . . . 12 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
79	57, 41, 78	syl2anc 691	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
80	79	ralrimiva 2949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
81		eqidd 2611	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
82	64, 74, 39, 81, 66	ofrfval2 6813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
83	80, 82	mpbird 246	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹)
84		itg2le 23312	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
85	75, 56, 83, 84	syl3anc 1318	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
86		itg2lecl 23311	. . . . . . . 8 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
87	75, 53, 85, 86	syl3anc 1318	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
88	17, 19, 28, 31, 44, 45, 46, 47, 72, 87	itg2split 23322	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
89	1	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℝ⁺)
90	89	rphalfcld 11760	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ⁺)
91	90	rpred 11748	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝐶 / 2) ∈ ℝ)
92		ifcl 4080	. . . . . . . . . . 11 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
93	43, 48, 92	sylancl 693	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
94		eqid 2610	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
95	93, 94	fmptd 6292	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
96		breq1 4586	. . . . . . . . . . . . . 14 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
97		breq1 4586	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
98	96, 97	ifboth 4074	. . . . . . . . . . . . 13 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
99	57, 41, 98	syl2anc 691	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
100	99	ralrimiva 2949	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
101		eqidd 2611	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
102	64, 93, 43, 101, 66	ofrfval2 6813	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
103	100, 102	mpbird 246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹)
104		itg2le 23312	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
105	95, 56, 103, 104	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
106		itg2lecl 23311	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
107	95, 53, 105, 106	syl3anc 1318	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) ∈ ℝ)
108		0red 9920	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 0 ∈ ℝ)
109		elinel2 3762	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
110	109	a1i 11	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
111		ifle 11902	. . . . . . . . . . . 12 ⊢ ((((𝐹‘𝑥) ∈ ℝ ∧ 0 ∈ ℝ ∧ 0 ≤ (𝐹‘𝑥)) ∧ (𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))) → 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
112	39, 108, 41, 110, 111	syl31anc 1321	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
113	112	ralrimiva 2949	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))
114	64, 50, 93, 65, 101	ofrfval2 6813	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
115	113, 114	mpbird 246	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)))
116		itg2le 23312	. . . . . . . . 9 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
117	51, 95, 115, 116	syl3anc 1318	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))))
118	66	fveq2d 6107	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))))
119		cmmbl 23109	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
120	15, 119	syl 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ∈ dom vol)
121		disjdif 3992	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ∅
122	121	fveq2i 6106	. . . . . . . . . . . . . 14 ⊢ (vol‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = (vol‘∅)
123	122, 26	eqtri 2632	. . . . . . . . . . . . 13 ⊢ (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0
124	123	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘((^◡𝐹 “ (𝑀(,)+∞)) ∩ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))))) = 0)
125		undif2 3996	. . . . . . . . . . . . 13 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))) = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ)
126		mblss 23106	. . . . . . . . . . . . . . 15 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ∈ dom vol → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
127	15, 126	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ)
128		ssequn1 3745	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐹 “ (𝑀(,)+∞)) ⊆ ℝ ↔ ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
129	127, 128	sylib 207	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((^◡𝐹 “ (𝑀(,)+∞)) ∪ ℝ) = ℝ)
130	125, 129	syl5req 2657	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ℝ = ((^◡𝐹 “ (𝑀(,)+∞)) ∪ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞)))))
131		eqid 2610	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))
132		iftrue 4042	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0) = (𝐹‘𝑥))
133	132	mpteq2ia 4668	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥))
134	133	eqcomi 2619	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ ℝ, (𝐹‘𝑥), 0))
135		ifcl 4080	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘𝑥) ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
136	43, 48, 135	sylancl 693	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ∈ (0[,]+∞))
137	136, 131	fmptd 6292	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞))
138		breq1 4586	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐹‘𝑥) = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → ((𝐹‘𝑥) ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
139		breq1 4586	. . . . . . . . . . . . . . . . . 18 ⊢ (0 = if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) → (0 ≤ (𝐹‘𝑥) ↔ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
140	138, 139	ifboth 4074	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐹‘𝑥) ≤ (𝐹‘𝑥) ∧ 0 ≤ (𝐹‘𝑥)) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
141	57, 41, 140	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
142	141	ralrimiva 2949	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥))
143		eqidd 2611	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))
144	64, 136, 43, 143, 66	ofrfval2 6813	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹 ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ (𝐹‘𝑥)))
145	142, 144	mpbird 246	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹)
146		itg2le 23312	. . . . . . . . . . . . . 14 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ 𝐹:ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ 𝐹) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
147	137, 56, 145, 146	syl3anc 1318	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹))
148		itg2lecl 23311	. . . . . . . . . . . . 13 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (∫₂‘𝐹) ∈ ℝ ∧ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘𝐹)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
149	137, 53, 147, 148	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ∈ ℝ)
150	15, 120, 124, 130, 43, 94, 131, 134, 107, 149	itg2split 23322	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ (𝐹‘𝑥))) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
151	118, 150	eqtrd 2644	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) = ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
152		itg2cn.6	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
153	152	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
154		eldif 3550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ (𝑥 ∈ ℝ ∧ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
155	154	baib 942	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
156	155	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
157	9	ffnd 5959	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐹 Fn ℝ)
158	157	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn ℝ)
159		elpreima 6245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐹 Fn ℝ → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
160	158, 159	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
161	39	biantrurd 528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
162	3	nnred 10912	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑀 ∈ ℝ)
163	162	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ)
164	163	rexrd 9968	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑀 ∈ ℝ^*)
165		elioopnf 12138	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ ℝ^* → ((𝐹‘𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
166	164, 165	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (𝑀(,)+∞) ↔ ((𝐹‘𝑥) ∈ ℝ ∧ 𝑀 < (𝐹‘𝑥))))
167		simpr 476	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → 𝑥 ∈ ℝ)
168	167	biantrurd 528	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → ((𝐹‘𝑥) ∈ (𝑀(,)+∞) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
169	161, 166, 168	3bitr2d 295	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ (𝑥 ∈ ℝ ∧ (𝐹‘𝑥) ∈ (𝑀(,)+∞))))
170	163, 39	ltnled 10063	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑀 < (𝐹‘𝑥) ↔ ¬ (𝐹‘𝑥) ≤ 𝑀))
171	160, 169, 170	3bitr2rd 296	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
172	171	con1bid 344	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝐹‘𝑥) ≤ 𝑀))
173	156, 172	bitrd 267	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → (𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))) ↔ (𝐹‘𝑥) ≤ 𝑀))
174	173	ifbid 4058	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))
175	174	mpteq2dva 4672	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) = (𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0)))
176	175	fveq2d 6107	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) = (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))))
177	176	breq1d 4593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)) ↔ (∫₂‘(𝑥 ∈ ℝ ↦ if((𝐹‘𝑥) ≤ 𝑀, (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2))))
178	153, 177	mtbird 314	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2)))
179	53, 91	resubcld 10337	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘𝐹) − (𝐶 / 2)) ∈ ℝ)
180	179, 149	ltnled 10063	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫₂‘𝐹) − (𝐶 / 2)) < (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ↔ ¬ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ ((∫₂‘𝐹) − (𝐶 / 2))))
181	178, 180	mpbird 246	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘𝐹) − (𝐶 / 2)) < (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))))
182	53, 91, 149	ltsubadd2d 10504	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (((∫₂‘𝐹) − (𝐶 / 2)) < (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ↔ (∫₂‘𝐹) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))))))
183	181, 182	mpbid 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘𝐹) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
184	151, 183	eqbrtrrd 4607	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))))
185	107, 91, 149	ltadd1d 10499	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) < (𝐶 / 2) ↔ ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (ℝ ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))))))
186	184, 185	mpbird 246	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)), (𝐹‘𝑥), 0))) < (𝐶 / 2))
187	72, 107, 91, 117, 186	lelttrd 10074	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
188	162	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ)
189		mblvol 23105	. . . . . . . . . . 11 ⊢ (𝑢 ∈ dom vol → (vol‘𝑢) = (vol*‘𝑢))
190	6, 189	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) = (vol*‘𝑢))
191	5	rpred 11748	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐶 / 2) / 𝑀) ∈ ℝ)
192	191	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ)
193		simprr 792	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) < ((𝐶 / 2) / 𝑀))
194	190, 193	eqbrtrrd 4607	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) < ((𝐶 / 2) / 𝑀))
195		ovolcl 23053	. . . . . . . . . . . . . 14 ⊢ (𝑢 ⊆ ℝ → (vol‘𝑢) ∈ ℝ^)
196	33, 195	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ^)
197	192	rexrd 9968	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) / 𝑀) ∈ ℝ^*)
198		xrltle 11858	. . . . . . . . . . . . 13 ⊢ (((vol‘𝑢) ∈ ℝ^ ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ^) → ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀)))
199	196, 197, 198	syl2anc 691	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (vol‘𝑢) ≤ ((𝐶 / 2) / 𝑀)))
200	194, 199	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ≤ ((𝐶 / 2) / 𝑀))
201		ovollecl 23058	. . . . . . . . . . 11 ⊢ ((𝑢 ⊆ ℝ ∧ ((𝐶 / 2) / 𝑀) ∈ ℝ ∧ (vol‘𝑢) ≤ ((𝐶 / 2) / 𝑀)) → (vol‘𝑢) ∈ ℝ)
202	33, 192, 200, 201	syl3anc 1318	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol*‘𝑢) ∈ ℝ)
203	190, 202	eqeltrd 2688	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (vol‘𝑢) ∈ ℝ)
204	188, 203	remulcld 9949	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) ∈ ℝ)
205	188	rexrd 9968	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℝ^*)
206	3	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ)
207	206	nnnn0d 11228	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ ℕ₀)
208	207	nn0ge0d 11231	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ 𝑀)
209		elxrge0 12152	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ (0[,]+∞) ↔ (𝑀 ∈ ℝ^* ∧ 0 ≤ 𝑀))
210	205, 208, 209	sylanbrc 695	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,]+∞))
211		ifcl 4080	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ (0[,]+∞) ∧ 0 ∈ (0[,]+∞)) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
212	210, 48, 211	sylancl 693	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
213	212	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ ℝ) → if(𝑥 ∈ 𝑢, 𝑀, 0) ∈ (0[,]+∞))
214		eqid 2610	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))
215	213, 214	fmptd 6292	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞))
216		eldifn 3695	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
217	216	adantl 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → ¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)))
218		difssd 3700	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) ⊆ 𝑢)
219	218	sselda 3568	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → 𝑥 ∈ 𝑢)
220	34, 171	syldan 486	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ 𝑢) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
221	219, 220	syldan 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → (¬ (𝐹‘𝑥) ≤ 𝑀 ↔ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞))))
222	221	con1bid 344	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → (¬ 𝑥 ∈ (^◡𝐹 “ (𝑀(,)+∞)) ↔ (𝐹‘𝑥) ≤ 𝑀))
223	217, 222	mpbid 221	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → (𝐹‘𝑥) ≤ 𝑀)
224		iftrue 4042	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
225	224	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = (𝐹‘𝑥))
226	219	iftrued 4044	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ 𝑢, 𝑀, 0) = 𝑀)
227	223, 225, 226	3brtr4d 4615	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
228		iffalse 4045	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
229	228	adantl 481	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) = 0)
230		0le0 10987	. . . . . . . . . . . . . . . 16 ⊢ 0 ≤ 0
231		breq2 4587	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 𝑀 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
232		breq2 4587	. . . . . . . . . . . . . . . . 17 ⊢ (0 = if(𝑥 ∈ 𝑢, 𝑀, 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
233	231, 232	ifboth 4074	. . . . . . . . . . . . . . . 16 ⊢ ((0 ≤ 𝑀 ∧ 0 ≤ 0) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
234	208, 230, 233	sylancl 693	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
235	234	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → 0 ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
236	229, 235	eqbrtrd 4605	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) ∧ ¬ 𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞)))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
237	227, 236	pm2.61dan 828	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
238	237	ralrimivw 2950	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0))
239		eqidd 2611	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)))
240	64, 74, 213, 81, 239	ofrfval2 6813	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)) ↔ ∀𝑥 ∈ ℝ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0) ≤ if(𝑥 ∈ 𝑢, 𝑀, 0)))
241	238, 240	mpbird 246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)))
242		itg2le 23312	. . . . . . . . . 10 ⊢ (((𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0)):ℝ⟶(0[,]+∞) ∧ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)) ∘_𝑟 ≤ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
243	75, 215, 241, 242	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))))
244		elrege0 12149	. . . . . . . . . . 11 ⊢ (𝑀 ∈ (0[,)+∞) ↔ (𝑀 ∈ ℝ ∧ 0 ≤ 𝑀))
245	188, 208, 244	sylanbrc 695	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝑀 ∈ (0[,)+∞))
246		itg2const 23313	. . . . . . . . . 10 ⊢ ((𝑢 ∈ dom vol ∧ (vol‘𝑢) ∈ ℝ ∧ 𝑀 ∈ (0[,)+∞)) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
247	6, 203, 245, 246	syl3anc 1318	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, 𝑀, 0))) = (𝑀 · (vol‘𝑢)))
248	243, 247	breqtrd 4609	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) ≤ (𝑀 · (vol‘𝑢)))
249	206	nngt0d 10941	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 0 < 𝑀)
250		ltmuldiv2 10776	. . . . . . . . . 10 ⊢ (((vol‘𝑢) ∈ ℝ ∧ (𝐶 / 2) ∈ ℝ ∧ (𝑀 ∈ ℝ ∧ 0 < 𝑀)) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
251	203, 91, 188, 249, 250	syl112anc 1322	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝑀 · (vol‘𝑢)) < (𝐶 / 2) ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
252	193, 251	mpbird 246	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (𝑀 · (vol‘𝑢)) < (𝐶 / 2))
253	87, 204, 91, 248, 252	lelttrd 10074	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) < (𝐶 / 2))
254	72, 87, 91, 91, 187, 253	lt2addd 10529	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∩ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0))) + (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ (𝑢 ∖ (^◡𝐹 “ (𝑀(,)+∞))), (𝐹‘𝑥), 0)))) < ((𝐶 / 2) + (𝐶 / 2)))
255	88, 254	eqbrtrd 4605	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < ((𝐶 / 2) + (𝐶 / 2)))
256	89	rpcnd 11750	. . . . . 6 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → 𝐶 ∈ ℂ)
257	256	2halvesd 11155	. . . . 5 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → ((𝐶 / 2) + (𝐶 / 2)) = 𝐶)
258	255, 257	breqtrd 4609	. . . 4 ⊢ ((𝜑 ∧ (𝑢 ∈ dom vol ∧ (vol‘𝑢) < ((𝐶 / 2) / 𝑀))) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)
259	258	expr 641	. . 3 ⊢ ((𝜑 ∧ 𝑢 ∈ dom vol) → ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
260	259	ralrimiva 2949	. 2 ⊢ (𝜑 → ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
261		breq2 4587	. . . . 5 ⊢ (𝑑 = ((𝐶 / 2) / 𝑀) → ((vol‘𝑢) < 𝑑 ↔ (vol‘𝑢) < ((𝐶 / 2) / 𝑀)))
262	261	imbi1d 330	. . . 4 ⊢ (𝑑 = ((𝐶 / 2) / 𝑀) → (((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶) ↔ ((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)))
263	262	ralbidv 2969	. . 3 ⊢ (𝑑 = ((𝐶 / 2) / 𝑀) → (∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶) ↔ ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)))
264	263	rspcev 3282	. 2 ⊢ ((((𝐶 / 2) / 𝑀) ∈ ℝ⁺ ∧ ∀𝑢 ∈ dom vol((vol‘𝑢) < ((𝐶 / 2) / 𝑀) → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶)) → ∃𝑑 ∈ ℝ⁺ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))
265	5, 260, 264	syl2anc 691	1 ⊢ (𝜑 → ∃𝑑 ∈ ℝ⁺ ∀𝑢 ∈ dom vol((vol‘𝑢) < 𝑑 → (∫₂‘(𝑥 ∈ ℝ ↦ if(𝑥 ∈ 𝑢, (𝐹‘𝑥), 0))) < 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 ifcif 4036 class class class wbr 4583 ↦ cmpt 4643 ^◡ccnv 5037 dom cdm 5038 “ cima 5041 Fn wfn 5799 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ∘_𝑟 cofr 6794 ℝcr 9814 0cc0 9815 + caddc 9818 · cmul 9820 +∞cpnf 9950 ℝ^*cxr 9952 < clt 9953 ≤ cle 9954 − cmin 10145 / cdiv 10563 ℕcn 10897 2c2 10947 ℝ⁺crp 11708 (,)cioo 12046 [,)cico 12048 [,]cicc 12049 vol*covol 23038 volcvol 23039 MblFncmbf 23189 ∫₂citg2 23191

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-inf2 8421 ax-cnex 9871 ax-resscn 9872 ax-1cn 9873 ax-icn 9874 ax-addcl 9875 ax-addrcl 9876 ax-mulcl 9877 ax-mulrcl 9878 ax-mulcom 9879 ax-addass 9880 ax-mulass 9881 ax-distr 9882 ax-i2m1 9883 ax-1ne0 9884 ax-1rid 9885 ax-rnegex 9886 ax-rrecex 9887 ax-cnre 9888 ax-pre-lttri 9889 ax-pre-lttrn 9890 ax-pre-ltadd 9891 ax-pre-mulgt0 9892 ax-pre-sup 9893 ax-addf 9894

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3or 1032 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-nel 2783 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-pss 3556 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-tp 4130 df-op 4132 df-uni 4373 df-int 4411 df-iun 4457 df-disj 4554 df-br 4584 df-opab 4644 df-mpt 4645 df-tr 4681 df-eprel 4949 df-id 4953 df-po 4959 df-so 4960 df-fr 4997 df-se 4998 df-we 4999 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-pred 5597 df-ord 5643 df-on 5644 df-lim 5645 df-suc 5646 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-isom 5813 df-riota 6511 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-of 6795 df-ofr 6796 df-om 6958 df-1st 7059 df-2nd 7060 df-wrecs 7294 df-recs 7355 df-rdg 7393 df-1o 7447 df-2o 7448 df-oadd 7451 df-er 7629 df-map 7746 df-pm 7747 df-en 7842 df-dom 7843 df-sdom 7844 df-fin 7845 df-fi 8200 df-sup 8231 df-inf 8232 df-oi 8298 df-card 8648 df-cda 8873 df-pnf 9955 df-mnf 9956 df-xr 9957 df-ltxr 9958 df-le 9959 df-sub 10147 df-neg 10148 df-div 10564 df-nn 10898 df-2 10956 df-3 10957 df-n0 11170 df-z 11255 df-uz 11564 df-q 11665 df-rp 11709 df-xneg 11822 df-xadd 11823 df-xmul 11824 df-ioo 12050 df-ico 12052 df-icc 12053 df-fz 12198 df-fzo 12335 df-fl 12455 df-seq 12664 df-exp 12723 df-hash 12980 df-cj 13687 df-re 13688 df-im 13689 df-sqrt 13823 df-abs 13824 df-clim 14067 df-sum 14265 df-rest 15906 df-topgen 15927 df-psmet 19559 df-xmet 19560 df-met 19561 df-bl 19562 df-mopn 19563 df-top 20521 df-bases 20522 df-topon 20523 df-cmp 21000 df-ovol 23040 df-vol 23041 df-mbf 23194 df-itg1 23195 df-itg2 23196 df-0p 23243

This theorem is referenced by: itg2cn 23336

W3C validator