Theorem mbfi1fseq

Description: A characterization of measurability in terms of simple functions (this is an if and only if for nonnegative functions, although we don't prove it). Any nonnegative measurable function is the limit of an increasing sequence of nonnegative simple functions. This proof is an example of a poor de Bruijn factor - the formalized proof is much longer than an average hand proof, which usually just describes the function G and "leaves the details as an exercise to the reader". (Contributed by Mario Carneiro, 16-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	mbfi1fseq.1	$$⊢\phi \to F\in MblFn$$
	mbfi1fseq.2	$$⊢\phi \to F:ℝ⟶\left[0,\mathrm{+\infty }\right)$$
Assertion	mbfi1fseq	$$⊢\phi \to \exists g\left(g:\mathbb{N}⟶\mathrm{dom}{\int }^1\wedge \forall n\in \mathbb{N}\left(0_{𝑝}{\le }_{f}g\left(n\right)\wedge g\left(n\right){\le }_{f}g\left(n+1\right)\right)\wedge \forall x\in ℝ\left(n\in \mathbb{N}⟼g\left(n\right)\left(x\right)\right)⇝F\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		mbfi1fseq.1	$$⊢\phi \to F\in MblFn$$
2		mbfi1fseq.2	$$⊢\phi \to F:ℝ⟶\left[0,\mathrm{+\infty }\right)$$
3		oveq2	$$⊢j=k\to 2^j=2^k$$
4	3	oveq2d	$$⊢j=k\to F\left(z\right)2^j=F\left(z\right)2^k$$
5	4	fveq2d	$$⊢j=k\to ⌊F\left(z\right)2^j⌋=⌊F\left(z\right)2^k⌋$$
6	5 3	oveq12d	$$⊢j=k\to \frac{⌊F\left(z\right)2^j⌋}{2^j}=\frac{⌊F\left(z\right)2^k⌋}{2^k}$$
7		fveq2	$$⊢z=y\to F\left(z\right)=F\left(y\right)$$
8	7	fvoveq1d	$$⊢z=y\to ⌊F\left(z\right)2^k⌋=⌊F\left(y\right)2^k⌋$$
9	8	oveq1d	$$⊢z=y\to \frac{⌊F\left(z\right)2^k⌋}{2^k}=\frac{⌊F\left(y\right)2^k⌋}{2^k}$$
10	6 9	cbvmpov	$$⊢\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)=\left(k\in \mathbb{N},y\in ℝ⟼\frac{⌊F\left(y\right)2^k⌋}{2^k}\right)$$
11		eleq1w	$$⊢y=x\to \left(y\in \left[-m,m\right]\leftrightarrow x\in \left[-m,m\right]\right)$$
12		oveq2	$$⊢y=x\to m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y=m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x$$
13	12	breq1d	$$⊢y=x\to \left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y\le m\leftrightarrow m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le m\right)$$
14	13 12	ifbieq1d	$$⊢y=x\to if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y,m\right)=if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,m\right)$$
15	11 14	ifbieq1d	$$⊢y=x\to if\left(y\in \left[-m,m\right],if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y,m\right),0\right)=if\left(x\in \left[-m,m\right],if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,m\right),0\right)$$
16	15	cbvmptv	$$⊢\left(y\in ℝ⟼if\left(y\in \left[-m,m\right],if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y,m\right),0\right)\right)=\left(x\in ℝ⟼if\left(x\in \left[-m,m\right],if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,m\right),0\right)\right)$$
17		negeq	$$⊢m=k\to -m=-k$$
18		id	$$⊢m=k\to m=k$$
19	17 18	oveq12d	$$⊢m=k\to \left[-m,m\right]=\left[-k,k\right]$$
20	19	eleq2d	$$⊢m=k\to \left(x\in \left[-m,m\right]\leftrightarrow x\in \left[-k,k\right]\right)$$
21		oveq1	$$⊢m=k\to m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x=k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x$$
22	21 18	breq12d	$$⊢m=k\to \left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le m\leftrightarrow k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le k\right)$$
23	22 21 18	ifbieq12d	$$⊢m=k\to if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,m\right)=if\left(k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le k,k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,k\right)$$
24	20 23	ifbieq1d	$$⊢m=k\to if\left(x\in \left[-m,m\right],if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,m\right),0\right)=if\left(x\in \left[-k,k\right],if\left(k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le k,k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,k\right),0\right)$$
25	24	mpteq2dv	$$⊢m=k\to \left(x\in ℝ⟼if\left(x\in \left[-m,m\right],if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,m\right),0\right)\right)=\left(x\in ℝ⟼if\left(x\in \left[-k,k\right],if\left(k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le k,k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,k\right),0\right)\right)$$
26	16 25	syl5eq	$$⊢m=k\to \left(y\in ℝ⟼if\left(y\in \left[-m,m\right],if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y,m\right),0\right)\right)=\left(x\in ℝ⟼if\left(x\in \left[-k,k\right],if\left(k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le k,k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,k\right),0\right)\right)$$
27	26	cbvmptv	$$⊢\left(m\in \mathbb{N}⟼\left(y\in ℝ⟼if\left(y\in \left[-m,m\right],if\left(m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y\le m,m\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)y,m\right),0\right)\right)\right)=\left(k\in \mathbb{N}⟼\left(x\in ℝ⟼if\left(x\in \left[-k,k\right],if\left(k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x\le k,k\left(j\in \mathbb{N},z\in ℝ⟼\frac{⌊F\left(z\right)2^j⌋}{2^j}\right)x,k\right),0\right)\right)\right)$$
28	1 2 10 27	mbfi1fseqlem6	$$⊢\phi \to \exists g\left(g:\mathbb{N}⟶\mathrm{dom}{\int }^1\wedge \forall n\in \mathbb{N}\left(0_{𝑝}{\le }_{f}g\left(n\right)\wedge g\left(n\right){\le }_{f}g\left(n+1\right)\right)\wedge \forall x\in ℝ\left(n\in \mathbb{N}⟼g\left(n\right)\left(x\right)\right)⇝F\left(x\right)\right)$$