Theorem itg2cn

Description: A sort of absolute continuity of the Lebesgue integral (this is the core of ftc1a which is about actual absolute continuity). (Contributed by Mario Carneiro, 1-Sep-2014)

	Ref	Expression
Hypotheses	itg2cn.1	$$⊢\phi \to F:ℝ⟶\left[0,\mathrm{+\infty }\right)$$
	itg2cn.2	$$⊢\phi \to F\in MblFn$$
	itg2cn.3	$$⊢\phi \to {\int }^2\left(F\right)\in ℝ$$
	itg2cn.4	$$⊢\phi \to C\in {ℝ}^{+}$$
Assertion	itg2cn	$$⊢\phi \to \exists d\in {ℝ}^{+}\forall u\in \mathrm{dom}vol\left(vol\left(u\right)<d\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in u,F\left(x\right),0\right)\right)\right)<C\right)$$

Proof

Step	Hyp	Ref	Expression
1		itg2cn.1	$$⊢\phi \to F:ℝ⟶\left[0,\mathrm{+\infty }\right)$$
2		itg2cn.2	$$⊢\phi \to F\in MblFn$$
3		itg2cn.3	$$⊢\phi \to {\int }^2\left(F\right)\in ℝ$$
4		itg2cn.4	$$⊢\phi \to C\in {ℝ}^{+}$$
5	4	rphalfcld	$$⊢\phi \to \frac{C}{2}\in {ℝ}^{+}$$
6	3 5	ltsubrpd	$$⊢\phi \to {\int }^2\left(F\right)-\left(\frac{C}{2}\right)<{\int }^2\left(F\right)$$
7	5	rpred	$$⊢\phi \to \frac{C}{2}\in ℝ$$
8	3 7	resubcld	$$⊢\phi \to {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\in ℝ$$
9	8 3	ltnled	$$⊢\phi \to \left({\int }^2\left(F\right)-\left(\frac{C}{2}\right)<{\int }^2\left(F\right)\leftrightarrow \neg {\int }^2\left(F\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
10	6 9	mpbid	$$⊢\phi \to \neg {\int }^2\left(F\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)$$
11	1	ffvelrnda	$$⊢\left(\phi \wedge x\in ℝ\right)\to F\left(x\right)\in \left[0,\mathrm{+\infty }\right)$$
12		elrege0	$$⊢F\left(x\right)\in \left[0,\mathrm{+\infty }\right)\leftrightarrow \left(F\left(x\right)\in ℝ\wedge 0\le F\left(x\right)\right)$$
13	11 12	sylib	$$⊢\left(\phi \wedge x\in ℝ\right)\to \left(F\left(x\right)\in ℝ\wedge 0\le F\left(x\right)\right)$$
14	13	simpld	$$⊢\left(\phi \wedge x\in ℝ\right)\to F\left(x\right)\in ℝ$$
15	14	rexrd	$$⊢\left(\phi \wedge x\in ℝ\right)\to F\left(x\right)\in {ℝ}^{*}$$
16	13	simprd	$$⊢\left(\phi \wedge x\in ℝ\right)\to 0\le F\left(x\right)$$
17		elxrge0	$$⊢F\left(x\right)\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(F\left(x\right)\in {ℝ}^{*}\wedge 0\le F\left(x\right)\right)$$
18	15 16 17	sylanbrc	$$⊢\left(\phi \wedge x\in ℝ\right)\to F\left(x\right)\in \left[0,\mathrm{+\infty }\right]$$
19		0e0iccpnf	$$⊢0\in \left[0,\mathrm{+\infty }\right]$$
20		ifcl	$$⊢\left(F\left(x\right)\in \left[0,\mathrm{+\infty }\right]\wedge 0\in \left[0,\mathrm{+\infty }\right]\right)\to if\left(F\left(x\right)\le n,F\left(x\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
21	18 19 20	sylancl	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(F\left(x\right)\le n,F\left(x\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
22	21	adantlr	$$⊢\left(\left(\phi \wedge n\in \mathbb{N}\right)\wedge x\in ℝ\right)\to if\left(F\left(x\right)\le n,F\left(x\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
23	22	fmpttd	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to \left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]$$
24		itg2cl	$$⊢\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]\to {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\in {ℝ}^{*}$$
25	23 24	syl	$$⊢\left(\phi \wedge n\in \mathbb{N}\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\in {ℝ}^{*}$$
26	25	fmpttd	$$⊢\phi \to \left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right):\mathbb{N}⟶{ℝ}^{*}$$
27	26	frnd	$$⊢\phi \to \mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)\subseteq {ℝ}^{*}$$
28	8	rexrd	$$⊢\phi \to {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\in {ℝ}^{*}$$
29		supxrleub	$$⊢\left(\mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)\subseteq {ℝ}^{*}\wedge {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\in {ℝ}^{*}\right)\to \left(sup\left(\mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right),{ℝ}^{*},<\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow \forall z\in \mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)z\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
30	27 28 29	syl2anc	$$⊢\phi \to \left(sup\left(\mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right),{ℝ}^{*},<\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow \forall z\in \mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)z\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
31	1 2 3	itg2cnlem1	$$⊢\phi \to sup\left(\mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right),{ℝ}^{*},<\right)={\int }^2\left(F\right)$$
32	31	breq1d	$$⊢\phi \to \left(sup\left(\mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right),{ℝ}^{*},<\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow {\int }^2\left(F\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
33	26	ffnd	$$⊢\phi \to \left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)Fn\mathbb{N}$$
34		breq1	$$⊢z=\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)\left(m\right)\to \left(z\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow \left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)\left(m\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
35	34	ralrn	$$⊢\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)Fn\mathbb{N}\to \left(\forall z\in \mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)z\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow \forall m\in \mathbb{N}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)\left(m\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
36		breq2	$$⊢n=m\to \left(F\left(x\right)\le n\leftrightarrow F\left(x\right)\le m\right)$$
37	36	ifbid	$$⊢n=m\to if\left(F\left(x\right)\le n,F\left(x\right),0\right)=if\left(F\left(x\right)\le m,F\left(x\right),0\right)$$
38	37	mpteq2dv	$$⊢n=m\to \left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)=\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)$$
39	38	fveq2d	$$⊢n=m\to {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)$$
40		eqid	$$⊢\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)=\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)$$
41		fvex	$$⊢{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\in \mathrm{V}$$
42	39 40 41	fvmpt	$$⊢m\in \mathbb{N}\to \left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)\left(m\right)={\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)$$
43	42	breq1d	$$⊢m\in \mathbb{N}\to \left(\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)\left(m\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
44	43	ralbiia	$$⊢\forall m\in \mathbb{N}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)\left(m\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow \forall m\in \mathbb{N}{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)$$
45	35 44	bitrdi	$$⊢\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)Fn\mathbb{N}\to \left(\forall z\in \mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)z\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow \forall m\in \mathbb{N}{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
46	33 45	syl	$$⊢\phi \to \left(\forall z\in \mathrm{ran}\left(n\in \mathbb{N}⟼{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le n,F\left(x\right),0\right)\right)\right)\right)z\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow \forall m\in \mathbb{N}{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
47	30 32 46	3bitr3d	$$⊢\phi \to \left({\int }^2\left(F\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow \forall m\in \mathbb{N}{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)$$
48	10 47	mtbid	$$⊢\phi \to \neg \forall m\in \mathbb{N}{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)$$
49		rexnal	$$⊢\exists m\in \mathbb{N}\neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow \neg \forall m\in \mathbb{N}{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)$$
50	48 49	sylibr	$$⊢\phi \to \exists m\in \mathbb{N}\neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)$$
51	1	adantr	$$⊢\left(\phi \wedge \left(m\in \mathbb{N}\wedge \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)\right)\to F:ℝ⟶\left[0,\mathrm{+\infty }\right)$$
52	2	adantr	$$⊢\left(\phi \wedge \left(m\in \mathbb{N}\wedge \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)\right)\to F\in MblFn$$
53	3	adantr	$$⊢\left(\phi \wedge \left(m\in \mathbb{N}\wedge \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)\right)\to {\int }^2\left(F\right)\in ℝ$$
54	4	adantr	$$⊢\left(\phi \wedge \left(m\in \mathbb{N}\wedge \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)\right)\to C\in {ℝ}^{+}$$
55		simprl	$$⊢\left(\phi \wedge \left(m\in \mathbb{N}\wedge \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)\right)\to m\in \mathbb{N}$$
56		simprr	$$⊢\left(\phi \wedge \left(m\in \mathbb{N}\wedge \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)\right)\to \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)$$
57		fveq2	$$⊢x=y\to F\left(x\right)=F\left(y\right)$$
58	57	breq1d	$$⊢x=y\to \left(F\left(x\right)\le m\leftrightarrow F\left(y\right)\le m\right)$$
59	58 57	ifbieq1d	$$⊢x=y\to if\left(F\left(x\right)\le m,F\left(x\right),0\right)=if\left(F\left(y\right)\le m,F\left(y\right),0\right)$$
60	59	cbvmptv	$$⊢\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)=\left(y\in ℝ⟼if\left(F\left(y\right)\le m,F\left(y\right),0\right)\right)$$
61	60	fveq2i	$$⊢{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)={\int }^2\left(\left(y\in ℝ⟼if\left(F\left(y\right)\le m,F\left(y\right),0\right)\right)\right)$$
62	61	breq1i	$$⊢{\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\leftrightarrow {\int }^2\left(\left(y\in ℝ⟼if\left(F\left(y\right)\le m,F\left(y\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)$$
63	56 62	sylnib	$$⊢\left(\phi \wedge \left(m\in \mathbb{N}\wedge \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)\right)\to \neg {\int }^2\left(\left(y\in ℝ⟼if\left(F\left(y\right)\le m,F\left(y\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)$$
64	51 52 53 54 55 63	itg2cnlem2	$$⊢\left(\phi \wedge \left(m\in \mathbb{N}\wedge \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)\right)\to \exists d\in {ℝ}^{+}\forall u\in \mathrm{dom}vol\left(vol\left(u\right)<d\to {\int }^2\left(\left(y\in ℝ⟼if\left(y\in u,F\left(y\right),0\right)\right)\right)<C\right)$$
65		elequ1	$$⊢x=y\to \left(x\in u\leftrightarrow y\in u\right)$$
66	65 57	ifbieq1d	$$⊢x=y\to if\left(x\in u,F\left(x\right),0\right)=if\left(y\in u,F\left(y\right),0\right)$$
67	66	cbvmptv	$$⊢\left(x\in ℝ⟼if\left(x\in u,F\left(x\right),0\right)\right)=\left(y\in ℝ⟼if\left(y\in u,F\left(y\right),0\right)\right)$$
68	67	fveq2i	$$⊢{\int }^2\left(\left(x\in ℝ⟼if\left(x\in u,F\left(x\right),0\right)\right)\right)={\int }^2\left(\left(y\in ℝ⟼if\left(y\in u,F\left(y\right),0\right)\right)\right)$$
69	68	breq1i	$$⊢{\int }^2\left(\left(x\in ℝ⟼if\left(x\in u,F\left(x\right),0\right)\right)\right)<C\leftrightarrow {\int }^2\left(\left(y\in ℝ⟼if\left(y\in u,F\left(y\right),0\right)\right)\right)<C$$
70	69	imbi2i	$$⊢\left(vol\left(u\right)<d\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in u,F\left(x\right),0\right)\right)\right)<C\right)\leftrightarrow \left(vol\left(u\right)<d\to {\int }^2\left(\left(y\in ℝ⟼if\left(y\in u,F\left(y\right),0\right)\right)\right)<C\right)$$
71	70	ralbii	$$⊢\forall u\in \mathrm{dom}vol\left(vol\left(u\right)<d\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in u,F\left(x\right),0\right)\right)\right)<C\right)\leftrightarrow \forall u\in \mathrm{dom}vol\left(vol\left(u\right)<d\to {\int }^2\left(\left(y\in ℝ⟼if\left(y\in u,F\left(y\right),0\right)\right)\right)<C\right)$$
72	71	rexbii	$$⊢\exists d\in {ℝ}^{+}\forall u\in \mathrm{dom}vol\left(vol\left(u\right)<d\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in u,F\left(x\right),0\right)\right)\right)<C\right)\leftrightarrow \exists d\in {ℝ}^{+}\forall u\in \mathrm{dom}vol\left(vol\left(u\right)<d\to {\int }^2\left(\left(y\in ℝ⟼if\left(y\in u,F\left(y\right),0\right)\right)\right)<C\right)$$
73	64 72	sylibr	$$⊢\left(\phi \wedge \left(m\in \mathbb{N}\wedge \neg {\int }^2\left(\left(x\in ℝ⟼if\left(F\left(x\right)\le m,F\left(x\right),0\right)\right)\right)\le {\int }^2\left(F\right)-\left(\frac{C}{2}\right)\right)\right)\to \exists d\in {ℝ}^{+}\forall u\in \mathrm{dom}vol\left(vol\left(u\right)<d\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in u,F\left(x\right),0\right)\right)\right)<C\right)$$
74	50 73	rexlimddv	$$⊢\phi \to \exists d\in {ℝ}^{+}\forall u\in \mathrm{dom}vol\left(vol\left(u\right)<d\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in u,F\left(x\right),0\right)\right)\right)<C\right)$$