itg2cnlem2

	Ref	Expression
Hypotheses	itg2cn.1	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
	itg2cn.2	$⊢ φ \to F \in MblFn$
	itg2cn.3	$⊢ φ \to \int^{2} (F) \in ℝ$
	itg2cn.4	$⊢ φ \to C \in ℝ^{+}$
	itg2cn.5	$⊢ φ \to M \in ℕ$
	itg2cn.6	$⊢ φ \to \neg \int^{2} ((x \in ℝ ⟼ if (F (x) \leq M, F (x), 0))) \leq \int^{2} (F) - (\frac{C}{2})$
Assertion	itg2cnlem2	$⊢ φ \to \exists d \in ℝ^{+} \forall u \in dom vol (vol (u) < d \to \int^{2} ((x \in ℝ ⟼ if (x \in u, F (x), 0))) < C)$

Proof

Step	Hyp	Ref	Expression
1		itg2cn.1	$⊢ φ \to F : ℝ ⟶ [0, +∞)$
2		itg2cn.2	$⊢ φ \to F \in MblFn$
3		itg2cn.3	$⊢ φ \to \int^{2} (F) \in ℝ$
4		itg2cn.4	$⊢ φ \to C \in ℝ^{+}$
5		itg2cn.5	$⊢ φ \to M \in ℕ$
6		itg2cn.6	$⊢ φ \to \neg \int^{2} ((x \in ℝ ⟼ if (F (x) \leq M, F (x), 0))) \leq \int^{2} (F) - (\frac{C}{2})$
7	4	rphalfcld	$⊢ φ \to \frac{C}{2} \in ℝ^{+}$
8	5	nnrpd	$⊢ φ \to M \in ℝ^{+}$
9	7 8	rpdivcld	$⊢ φ \to \frac{\frac{C}{2}}{M} \in ℝ^{+}$
10		simprl	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to u \in dom vol$
11	2	adantr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to F \in MblFn$
12		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
13		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq ℝ) \to F : ℝ ⟶ ℝ$
14	1 12 13	sylancl	$⊢ φ \to F : ℝ ⟶ ℝ$
15	14	adantr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to F : ℝ ⟶ ℝ$
16		mbfima	$⊢ (F \in MblFn \land F : ℝ ⟶ ℝ) \to F^{-1} [(M, +∞)] \in dom vol$
17	11 15 16	syl2anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to F^{-1} [(M, +∞)] \in dom vol$
18		inmbl	$⊢ (u \in dom vol \land F^{-1} [(M, +∞)] \in dom vol) \to u \cap F^{-1} [(M, +∞)] \in dom vol$
19	10 17 18	syl2anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to u \cap F^{-1} [(M, +∞)] \in dom vol$
20		difmbl	$⊢ (u \in dom vol \land F^{-1} [(M, +∞)] \in dom vol) \to u ∖ F^{-1} [(M, +∞)] \in dom vol$
21	10 17 20	syl2anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to u ∖ F^{-1} [(M, +∞)] \in dom vol$
22		inass	$⊢ (u \cap F^{-1} [(M, +∞)]) \cap (u ∖ F^{-1} [(M, +∞)]) = u \cap (F^{-1} [(M, +∞)] \cap (u ∖ F^{-1} [(M, +∞)]))$
23		disjdif	$⊢ F^{-1} [(M, +∞)] \cap (u ∖ F^{-1} [(M, +∞)]) = \emptyset$
24	23	ineq2i	$⊢ u \cap (F^{-1} [(M, +∞)] \cap (u ∖ F^{-1} [(M, +∞)])) = u \cap \emptyset$
25		in0	$⊢ u \cap \emptyset = \emptyset$
26	22 24 25	3eqtri	$⊢ (u \cap F^{-1} [(M, +∞)]) \cap (u ∖ F^{-1} [(M, +∞)]) = \emptyset$
27	26	fveq2i	$⊢ {vol}^{} ((u \cap F^{-1} [(M, +∞)]) \cap (u ∖ F^{-1} [(M, +∞)])) = {vol}^{} (\emptyset)$
28		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
29	27 28	eqtri	$⊢ {vol}^{*} ((u \cap F^{-1} [(M, +∞)]) \cap (u ∖ F^{-1} [(M, +∞)])) = 0$
30	29	a1i	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to {vol}^{*} ((u \cap F^{-1} [(M, +∞)]) \cap (u ∖ F^{-1} [(M, +∞)])) = 0$
31		inundif	$⊢ (u \cap F^{-1} [(M, +∞)]) \cup (u ∖ F^{-1} [(M, +∞)]) = u$
32	31	eqcomi	$⊢ u = (u \cap F^{-1} [(M, +∞)]) \cup (u ∖ F^{-1} [(M, +∞)])$
33	32	a1i	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to u = (u \cap F^{-1} [(M, +∞)]) \cup (u ∖ F^{-1} [(M, +∞)])$
34		mblss	$⊢ u \in dom vol \to u \subseteq ℝ$
35	10 34	syl	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to u \subseteq ℝ$
36	35	sselda	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in u) \to x \in ℝ$
37	1	adantr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to F : ℝ ⟶ [0, +∞)$
38	37	ffvelcdmda	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to F (x) \in [0, +∞)$
39		elrege0	$⊢ F (x) \in [0, +∞) \leftrightarrow (F (x) \in ℝ \land 0 \leq F (x))$
40	38 39	sylib	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (F (x) \in ℝ \land 0 \leq F (x))$
41	40	simpld	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to F (x) \in ℝ$
42	41	rexrd	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to F (x) \in ℝ^{*}$
43	40	simprd	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to 0 \leq F (x)$
44		elxrge0	$⊢ F (x) \in [0, +∞] \leftrightarrow (F (x) \in ℝ^{*} \land 0 \leq F (x))$
45	42 43 44	sylanbrc	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to F (x) \in [0, +∞]$
46	36 45	syldan	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in u) \to F (x) \in [0, +∞]$
47		eqid	$⊢ (x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) = (x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))$
48		eqid	$⊢ (x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) = (x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))$
49		eqid	$⊢ (x \in ℝ ⟼ if (x \in u, F (x), 0)) = (x \in ℝ ⟼ if (x \in u, F (x), 0))$
50		0e0iccpnf	$⊢ 0 \in [0, +∞]$
51		ifcl	$⊢ (F (x) \in [0, +∞] \land 0 \in [0, +∞]) \to if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \in [0, +∞]$
52	45 50 51	sylancl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \in [0, +∞]$
53	52	fmpttd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞]$
54	3	adantr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} (F) \in ℝ$
55		icossicc	$⊢ [0, +∞) \subseteq [0, +∞]$
56		fss	$⊢ (F : ℝ ⟶ [0, +∞) \land [0, +∞) \subseteq [0, +∞]) \to F : ℝ ⟶ [0, +∞]$
57	37 55 56	sylancl	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to F : ℝ ⟶ [0, +∞]$
58	41	leidd	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to F (x) \leq F (x)$
59		breq1	$⊢ F (x) = if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \to (F (x) \leq F (x) \leftrightarrow if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq F (x))$
60		breq1	$⊢ 0 = if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \to (0 \leq F (x) \leftrightarrow if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq F (x))$
61	59 60	ifboth	$⊢ (F (x) \leq F (x) \land 0 \leq F (x)) \to if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq F (x)$
62	58 43 61	syl2anc	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq F (x)$
63	62	ralrimiva	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \forall x \in ℝ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq F (x)$
64		reex	$⊢ ℝ \in V$
65	64	a1i	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to ℝ \in V$
66		eqidd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) = (x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))$
67	37	feqmptd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to F = (x \in ℝ ⟼ F (x))$
68	65 52 41 66 67	ofrfval2	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} F \leftrightarrow \forall x \in ℝ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq F (x))$
69	63 68	mpbird	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} F$
70		itg2le	$⊢ ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞] \land F : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} F) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F)$
71	53 57 69 70	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F)$
72		itg2lecl	$⊢ ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞] \land \int^{2} (F) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F)) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) \in ℝ$
73	53 54 71 72	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) \in ℝ$
74		ifcl	$⊢ (F (x) \in [0, +∞] \land 0 \in [0, +∞]) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \in [0, +∞]$
75	45 50 74	sylancl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \in [0, +∞]$
76	75	fmpttd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞]$
77		breq1	$⊢ F (x) = if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \to (F (x) \leq F (x) \leftrightarrow if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x))$
78		breq1	$⊢ 0 = if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \to (0 \leq F (x) \leftrightarrow if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x))$
79	77 78	ifboth	$⊢ (F (x) \leq F (x) \land 0 \leq F (x)) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x)$
80	58 43 79	syl2anc	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x)$
81	80	ralrimiva	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \forall x \in ℝ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x)$
82		eqidd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) = (x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))$
83	65 75 41 82 67	ofrfval2	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} F \leftrightarrow \forall x \in ℝ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x))$
84	81 83	mpbird	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} F$
85		itg2le	$⊢ ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞] \land F : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} F) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F)$
86	76 57 84 85	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F)$
87		itg2lecl	$⊢ ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞] \land \int^{2} (F) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F)) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) \in ℝ$
88	76 54 86 87	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) \in ℝ$
89	19 21 30 33 46 47 48 49 73 88	itg2split	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in u, F (x), 0))) = \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) + \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)))$
90	4	adantr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to C \in ℝ^{+}$
91	90	rphalfcld	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \frac{C}{2} \in ℝ^{+}$
92	91	rpred	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \frac{C}{2} \in ℝ$
93		ifcl	$⊢ (F (x) \in [0, +∞] \land 0 \in [0, +∞]) \to if (x \in F^{-1} [(M, +∞)], F (x), 0) \in [0, +∞]$
94	45 50 93	sylancl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in F^{-1} [(M, +∞)], F (x), 0) \in [0, +∞]$
95	94	fmpttd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) : ℝ ⟶ [0, +∞]$
96		breq1	$⊢ F (x) = if (x \in F^{-1} [(M, +∞)], F (x), 0) \to (F (x) \leq F (x) \leftrightarrow if (x \in F^{-1} [(M, +∞)], F (x), 0) \leq F (x))$
97		breq1	$⊢ 0 = if (x \in F^{-1} [(M, +∞)], F (x), 0) \to (0 \leq F (x) \leftrightarrow if (x \in F^{-1} [(M, +∞)], F (x), 0) \leq F (x))$
98	96 97	ifboth	$⊢ (F (x) \leq F (x) \land 0 \leq F (x)) \to if (x \in F^{-1} [(M, +∞)], F (x), 0) \leq F (x)$
99	58 43 98	syl2anc	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in F^{-1} [(M, +∞)], F (x), 0) \leq F (x)$
100	99	ralrimiva	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \forall x \in ℝ if (x \in F^{-1} [(M, +∞)], F (x), 0) \leq F (x)$
101		eqidd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) = (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))$
102	65 94 45 101 67	ofrfval2	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) \leq_{f} F \leftrightarrow \forall x \in ℝ if (x \in F^{-1} [(M, +∞)], F (x), 0) \leq F (x))$
103	100 102	mpbird	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) \leq_{f} F$
104		itg2le	$⊢ ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) : ℝ ⟶ [0, +∞] \land F : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) \leq_{f} F) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) \leq \int^{2} (F)$
105	95 57 103 104	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) \leq \int^{2} (F)$
106		itg2lecl	$⊢ ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) : ℝ ⟶ [0, +∞] \land \int^{2} (F) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) \leq \int^{2} (F)) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) \in ℝ$
107	95 54 105 106	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) \in ℝ$
108		0red	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to 0 \in ℝ$
109		elinel2	$⊢ x \in (u \cap F^{-1} [(M, +∞)]) \to x \in F^{-1} [(M, +∞)]$
110	109	a1i	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (x \in (u \cap F^{-1} [(M, +∞)]) \to x \in F^{-1} [(M, +∞)])$
111		ifle	$⊢ ((F (x) \in ℝ \land 0 \in ℝ \land 0 \leq F (x)) \land (x \in (u \cap F^{-1} [(M, +∞)]) \to x \in F^{-1} [(M, +∞)])) \to if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq if (x \in F^{-1} [(M, +∞)], F (x), 0)$
112	41 108 43 110 111	syl31anc	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq if (x \in F^{-1} [(M, +∞)], F (x), 0)$
113	112	ralrimiva	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \forall x \in ℝ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq if (x \in F^{-1} [(M, +∞)], F (x), 0)$
114	65 52 94 66 101	ofrfval2	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) \leftrightarrow \forall x \in ℝ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0) \leq if (x \in F^{-1} [(M, +∞)], F (x), 0))$
115	113 114	mpbird	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))$
116		itg2le	$⊢ ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)))$
117	53 95 115 116	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)))$
118	67	fveq2d	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} (F) = \int^{2} ((x \in ℝ ⟼ F (x)))$
119		cmmbl	$⊢ F^{-1} [(M, +∞)] \in dom vol \to ℝ ∖ F^{-1} [(M, +∞)] \in dom vol$
120	17 119	syl	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to ℝ ∖ F^{-1} [(M, +∞)] \in dom vol$
121		disjdif	$⊢ F^{-1} [(M, +∞)] \cap (ℝ ∖ F^{-1} [(M, +∞)]) = \emptyset$
122	121	fveq2i	$⊢ {vol}^{} (F^{-1} [(M, +∞)] \cap (ℝ ∖ F^{-1} [(M, +∞)])) = {vol}^{} (\emptyset)$
123	122 28	eqtri	$⊢ {vol}^{*} (F^{-1} [(M, +∞)] \cap (ℝ ∖ F^{-1} [(M, +∞)])) = 0$
124	123	a1i	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to {vol}^{*} (F^{-1} [(M, +∞)] \cap (ℝ ∖ F^{-1} [(M, +∞)])) = 0$
125		undif2	$⊢ F^{-1} [(M, +∞)] \cup (ℝ ∖ F^{-1} [(M, +∞)]) = F^{-1} [(M, +∞)] \cup ℝ$
126		mblss	$⊢ F^{-1} [(M, +∞)] \in dom vol \to F^{-1} [(M, +∞)] \subseteq ℝ$
127	17 126	syl	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to F^{-1} [(M, +∞)] \subseteq ℝ$
128		ssequn1	$⊢ F^{-1} [(M, +∞)] \subseteq ℝ \leftrightarrow F^{-1} [(M, +∞)] \cup ℝ = ℝ$
129	127 128	sylib	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to F^{-1} [(M, +∞)] \cup ℝ = ℝ$
130	125 129	eqtr2id	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to ℝ = F^{-1} [(M, +∞)] \cup (ℝ ∖ F^{-1} [(M, +∞)])$
131		eqid	$⊢ (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0)) = (x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))$
132		eqid	$⊢ (x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)) = (x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))$
133		iftrue	$⊢ x \in ℝ \to if (x \in ℝ, F (x), 0) = F (x)$
134	133	mpteq2ia	$⊢ (x \in ℝ ⟼ if (x \in ℝ, F (x), 0)) = (x \in ℝ ⟼ F (x))$
135	134	eqcomi	$⊢ (x \in ℝ ⟼ F (x)) = (x \in ℝ ⟼ if (x \in ℝ, F (x), 0))$
136		ifcl	$⊢ (F (x) \in [0, +∞] \land 0 \in [0, +∞]) \to if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \in [0, +∞]$
137	45 50 136	sylancl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \in [0, +∞]$
138	137	fmpttd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞]$
139		breq1	$⊢ F (x) = if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \to (F (x) \leq F (x) \leftrightarrow if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x))$
140		breq1	$⊢ 0 = if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \to (0 \leq F (x) \leftrightarrow if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x))$
141	139 140	ifboth	$⊢ (F (x) \leq F (x) \land 0 \leq F (x)) \to if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x)$
142	58 43 141	syl2anc	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x)$
143	142	ralrimiva	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \forall x \in ℝ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x)$
144		eqidd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)) = (x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))$
145	65 137 45 144 67	ofrfval2	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} F \leftrightarrow \forall x \in ℝ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq F (x))$
146	143 145	mpbird	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} F$
147		itg2le	$⊢ ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞] \land F : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} F) \to \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F)$
148	138 57 146 147	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F)$
149		itg2lecl	$⊢ ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞] \land \int^{2} (F) \in ℝ \land \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F)) \to \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) \in ℝ$
150	138 54 148 149	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) \in ℝ$
151	17 120 124 130 45 131 132 135 107 150	itg2split	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ F (x))) = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) + \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)))$
152	118 151	eqtrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} (F) = \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) + \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)))$
153		eldif	$⊢ x \in (ℝ ∖ F^{-1} [(M, +∞)]) \leftrightarrow (x \in ℝ \land \neg x \in F^{-1} [(M, +∞)])$
154	153	baib	$⊢ x \in ℝ \to (x \in (ℝ ∖ F^{-1} [(M, +∞)]) \leftrightarrow \neg x \in F^{-1} [(M, +∞)])$
155	154	adantl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (x \in (ℝ ∖ F^{-1} [(M, +∞)]) \leftrightarrow \neg x \in F^{-1} [(M, +∞)])$
156	1	ffnd	$⊢ φ \to F Fn ℝ$
157	156	ad2antrr	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to F Fn ℝ$
158		elpreima	$⊢ F Fn ℝ \to (x \in F^{-1} [(M, +∞)] \leftrightarrow (x \in ℝ \land F (x) \in (M, +∞)))$
159	157 158	syl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (x \in F^{-1} [(M, +∞)] \leftrightarrow (x \in ℝ \land F (x) \in (M, +∞)))$
160	41	biantrurd	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (M < F (x) \leftrightarrow (F (x) \in ℝ \land M < F (x)))$
161	5	nnred	$⊢ φ \to M \in ℝ$
162	161	ad2antrr	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to M \in ℝ$
163	162	rexrd	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to M \in ℝ^{*}$
164		elioopnf	$⊢ M \in ℝ^{*} \to (F (x) \in (M, +∞) \leftrightarrow (F (x) \in ℝ \land M < F (x)))$
165	163 164	syl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (F (x) \in (M, +∞) \leftrightarrow (F (x) \in ℝ \land M < F (x)))$
166		simpr	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to x \in ℝ$
167	166	biantrurd	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (F (x) \in (M, +∞) \leftrightarrow (x \in ℝ \land F (x) \in (M, +∞)))$
168	160 165 167	3bitr2d	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (M < F (x) \leftrightarrow (x \in ℝ \land F (x) \in (M, +∞)))$
169	162 41	ltnled	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (M < F (x) \leftrightarrow \neg F (x) \leq M)$
170	159 168 169	3bitr2rd	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (\neg F (x) \leq M \leftrightarrow x \in F^{-1} [(M, +∞)])$
171	170	con1bid	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (\neg x \in F^{-1} [(M, +∞)] \leftrightarrow F (x) \leq M)$
172	155 171	bitrd	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to (x \in (ℝ ∖ F^{-1} [(M, +∞)]) \leftrightarrow F (x) \leq M)$
173	172	ifbid	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0) = if (F (x) \leq M, F (x), 0)$
174	173	mpteq2dva	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)) = (x \in ℝ ⟼ if (F (x) \leq M, F (x), 0))$
175	174	fveq2d	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) = \int^{2} ((x \in ℝ ⟼ if (F (x) \leq M, F (x), 0)))$
176	6	adantr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \neg \int^{2} ((x \in ℝ ⟼ if (F (x) \leq M, F (x), 0))) \leq \int^{2} (F) - (\frac{C}{2})$
177	175 176	eqnbrtrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \neg \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F) - (\frac{C}{2})$
178	54 92	resubcld	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} (F) - (\frac{C}{2}) \in ℝ$
179	178 150	ltnled	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (\int^{2} (F) - (\frac{C}{2}) < \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leftrightarrow \neg \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} (F) - (\frac{C}{2}))$
180	177 179	mpbird	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} (F) - (\frac{C}{2}) < \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)))$
181	54 92 150	ltsubadd2d	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (\int^{2} (F) - (\frac{C}{2}) < \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leftrightarrow \int^{2} (F) < (\frac{C}{2}) + \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))))$
182	180 181	mpbid	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} (F) < (\frac{C}{2}) + \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)))$
183	152 182	eqbrtrrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) + \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) < (\frac{C}{2}) + \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0)))$
184	107 92 150	ltadd1d	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (\int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) < \frac{C}{2} \leftrightarrow \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) + \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))) < (\frac{C}{2}) + \int^{2} ((x \in ℝ ⟼ if (x \in (ℝ ∖ F^{-1} [(M, +∞)]), F (x), 0))))$
185	183 184	mpbird	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in F^{-1} [(M, +∞)], F (x), 0))) < \frac{C}{2}$
186	73 107 92 117 185	lelttrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) < \frac{C}{2}$
187	161	adantr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to M \in ℝ$
188		mblvol	$⊢ u \in dom vol \to vol (u) = {vol}^{*} (u)$
189	10 188	syl	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to vol (u) = {vol}^{*} (u)$
190	9	rpred	$⊢ φ \to \frac{\frac{C}{2}}{M} \in ℝ$
191	190	adantr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \frac{\frac{C}{2}}{M} \in ℝ$
192		ovolcl	$⊢ u \subseteq ℝ \to {vol}^{} (u) \in ℝ^{}$
193	35 192	syl	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to {vol}^{} (u) \in ℝ^{}$
194	191	rexrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \frac{\frac{C}{2}}{M} \in ℝ^{*}$
195		simprr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to vol (u) < \frac{\frac{C}{2}}{M}$
196	189 195	eqbrtrrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to {vol}^{*} (u) < \frac{\frac{C}{2}}{M}$
197	193 194 196	xrltled	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to {vol}^{*} (u) \leq \frac{\frac{C}{2}}{M}$
198		ovollecl	$⊢ (u \subseteq ℝ \land \frac{\frac{C}{2}}{M} \in ℝ \land {vol}^{} (u) \leq \frac{\frac{C}{2}}{M}) \to {vol}^{} (u) \in ℝ$
199	35 191 197 198	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to {vol}^{*} (u) \in ℝ$
200	189 199	eqeltrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to vol (u) \in ℝ$
201	187 200	remulcld	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to M vol (u) \in ℝ$
202	187	rexrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to M \in ℝ^{*}$
203	5	adantr	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to M \in ℕ$
204	203	nnnn0d	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to M \in ℕ_{0}$
205	204	nn0ge0d	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to 0 \leq M$
206		elxrge0	$⊢ M \in [0, +∞] \leftrightarrow (M \in ℝ^{*} \land 0 \leq M)$
207	202 205 206	sylanbrc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to M \in [0, +∞]$
208		ifcl	$⊢ (M \in [0, +∞] \land 0 \in [0, +∞]) \to if (x \in u, M, 0) \in [0, +∞]$
209	207 50 208	sylancl	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to if (x \in u, M, 0) \in [0, +∞]$
210	209	adantr	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in ℝ) \to if (x \in u, M, 0) \in [0, +∞]$
211	210	fmpttd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in u, M, 0)) : ℝ ⟶ [0, +∞]$
212		eldifn	$⊢ x \in (u ∖ F^{-1} [(M, +∞)]) \to \neg x \in F^{-1} [(M, +∞)]$
213	212	adantl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in (u ∖ F^{-1} [(M, +∞)])) \to \neg x \in F^{-1} [(M, +∞)]$
214		difssd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to u ∖ F^{-1} [(M, +∞)] \subseteq u$
215	214	sselda	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in (u ∖ F^{-1} [(M, +∞)])) \to x \in u$
216	36 170	syldan	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in u) \to (\neg F (x) \leq M \leftrightarrow x \in F^{-1} [(M, +∞)])$
217	215 216	syldan	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in (u ∖ F^{-1} [(M, +∞)])) \to (\neg F (x) \leq M \leftrightarrow x \in F^{-1} [(M, +∞)])$
218	217	con1bid	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in (u ∖ F^{-1} [(M, +∞)])) \to (\neg x \in F^{-1} [(M, +∞)] \leftrightarrow F (x) \leq M)$
219	213 218	mpbid	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in (u ∖ F^{-1} [(M, +∞)])) \to F (x) \leq M$
220		iftrue	$⊢ x \in (u ∖ F^{-1} [(M, +∞)]) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) = F (x)$
221	220	adantl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in (u ∖ F^{-1} [(M, +∞)])) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) = F (x)$
222	215	iftrued	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in (u ∖ F^{-1} [(M, +∞)])) \to if (x \in u, M, 0) = M$
223	219 221 222	3brtr4d	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land x \in (u ∖ F^{-1} [(M, +∞)])) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq if (x \in u, M, 0)$
224		iffalse	$⊢ \neg x \in (u ∖ F^{-1} [(M, +∞)]) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) = 0$
225	224	adantl	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land \neg x \in (u ∖ F^{-1} [(M, +∞)])) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) = 0$
226		0le0	$⊢ 0 \leq 0$
227		breq2	$⊢ M = if (x \in u, M, 0) \to (0 \leq M \leftrightarrow 0 \leq if (x \in u, M, 0))$
228		breq2	$⊢ 0 = if (x \in u, M, 0) \to (0 \leq 0 \leftrightarrow 0 \leq if (x \in u, M, 0))$
229	227 228	ifboth	$⊢ (0 \leq M \land 0 \leq 0) \to 0 \leq if (x \in u, M, 0)$
230	205 226 229	sylancl	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to 0 \leq if (x \in u, M, 0)$
231	230	adantr	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land \neg x \in (u ∖ F^{-1} [(M, +∞)])) \to 0 \leq if (x \in u, M, 0)$
232	225 231	eqbrtrd	$⊢ ((φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \land \neg x \in (u ∖ F^{-1} [(M, +∞)])) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq if (x \in u, M, 0)$
233	223 232	pm2.61dan	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq if (x \in u, M, 0)$
234	233	ralrimivw	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \forall x \in ℝ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq if (x \in u, M, 0)$
235		eqidd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in u, M, 0)) = (x \in ℝ ⟼ if (x \in u, M, 0))$
236	65 75 210 82 235	ofrfval2	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} (x \in ℝ ⟼ if (x \in u, M, 0)) \leftrightarrow \forall x \in ℝ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0) \leq if (x \in u, M, 0))$
237	234 236	mpbird	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} (x \in ℝ ⟼ if (x \in u, M, 0))$
238		itg2le	$⊢ ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in u, M, 0)) : ℝ ⟶ [0, +∞] \land (x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0)) \leq_{f} (x \in ℝ ⟼ if (x \in u, M, 0))) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} ((x \in ℝ ⟼ if (x \in u, M, 0)))$
239	76 211 237 238	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq \int^{2} ((x \in ℝ ⟼ if (x \in u, M, 0)))$
240		elrege0	$⊢ M \in [0, +∞) \leftrightarrow (M \in ℝ \land 0 \leq M)$
241	187 205 240	sylanbrc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to M \in [0, +∞)$
242		itg2const	$⊢ (u \in dom vol \land vol (u) \in ℝ \land M \in [0, +∞)) \to \int^{2} ((x \in ℝ ⟼ if (x \in u, M, 0))) = M vol (u)$
243	10 200 241 242	syl3anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in u, M, 0))) = M vol (u)$
244	239 243	breqtrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) \leq M vol (u)$
245	203	nngt0d	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to 0 < M$
246		ltmuldiv2	$⊢ (vol (u) \in ℝ \land \frac{C}{2} \in ℝ \land (M \in ℝ \land 0 < M)) \to (M vol (u) < \frac{C}{2} \leftrightarrow vol (u) < \frac{\frac{C}{2}}{M})$
247	200 92 187 245 246	syl112anc	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (M vol (u) < \frac{C}{2} \leftrightarrow vol (u) < \frac{\frac{C}{2}}{M})$
248	195 247	mpbird	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to M vol (u) < \frac{C}{2}$
249	88 201 92 244 248	lelttrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) < \frac{C}{2}$
250	73 88 92 92 186 249	lt2addd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in (u \cap F^{-1} [(M, +∞)]), F (x), 0))) + \int^{2} ((x \in ℝ ⟼ if (x \in (u ∖ F^{-1} [(M, +∞)]), F (x), 0))) < (\frac{C}{2}) + (\frac{C}{2})$
251	89 250	eqbrtrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in u, F (x), 0))) < (\frac{C}{2}) + (\frac{C}{2})$
252	90	rpcnd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to C \in ℂ$
253	252	2halvesd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to (\frac{C}{2}) + (\frac{C}{2}) = C$
254	251 253	breqtrd	$⊢ (φ \land (u \in dom vol \land vol (u) < \frac{\frac{C}{2}}{M})) \to \int^{2} ((x \in ℝ ⟼ if (x \in u, F (x), 0))) < C$
255	254	expr	$⊢ (φ \land u \in dom vol) \to (vol (u) < \frac{\frac{C}{2}}{M} \to \int^{2} ((x \in ℝ ⟼ if (x \in u, F (x), 0))) < C)$
256	255	ralrimiva	$⊢ φ \to \forall u \in dom vol (vol (u) < \frac{\frac{C}{2}}{M} \to \int^{2} ((x \in ℝ ⟼ if (x \in u, F (x), 0))) < C)$
257		breq2	$⊢ d = \frac{\frac{C}{2}}{M} \to (vol (u) < d \leftrightarrow vol (u) < \frac{\frac{C}{2}}{M})$
258	257	rspceaimv	$⊢ (\frac{\frac{C}{2}}{M} \in ℝ^{+} \land \forall u \in dom vol (vol (u) < \frac{\frac{C}{2}}{M} \to \int^{2} ((x \in ℝ ⟼ if (x \in u, F (x), 0))) < C)) \to \exists d \in ℝ^{+} \forall u \in dom vol (vol (u) < d \to \int^{2} ((x \in ℝ ⟼ if (x \in u, F (x), 0))) < C)$
259	9 256 258	syl2anc	$⊢ φ \to \exists d \in ℝ^{+} \forall u \in dom vol (vol (u) < d \to \int^{2} ((x \in ℝ ⟼ if (x \in u, F (x), 0))) < C)$

Metamath Proof Explorer

Theorem itg2cnlem2

Proof