Metamath Proof Explorer


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 φFMblFn
mbfi1fseq.2 φF:0+∞
Assertion mbfi1fseq φgg:dom1n0𝑝fgngnfgn+1xngnxFx

Proof

Step Hyp Ref Expression
1 mbfi1fseq.1 φFMblFn
2 mbfi1fseq.2 φF:0+∞
3 oveq2 j=k2j=2k
4 3 oveq2d j=kFz2j=Fz2k
5 4 fveq2d j=kFz2j=Fz2k
6 5 3 oveq12d j=kFz2j2j=Fz2k2k
7 fveq2 z=yFz=Fy
8 7 fvoveq1d z=yFz2k=Fy2k
9 8 oveq1d z=yFz2k2k=Fy2k2k
10 6 9 cbvmpov j,zFz2j2j=k,yFy2k2k
11 eleq1w y=xymmxmm
12 oveq2 y=xmj,zFz2j2jy=mj,zFz2j2jx
13 12 breq1d y=xmj,zFz2j2jymmj,zFz2j2jxm
14 13 12 ifbieq1d y=xifmj,zFz2j2jymmj,zFz2j2jym=ifmj,zFz2j2jxmmj,zFz2j2jxm
15 11 14 ifbieq1d y=xifymmifmj,zFz2j2jymmj,zFz2j2jym0=ifxmmifmj,zFz2j2jxmmj,zFz2j2jxm0
16 15 cbvmptv yifymmifmj,zFz2j2jymmj,zFz2j2jym0=xifxmmifmj,zFz2j2jxmmj,zFz2j2jxm0
17 negeq m=km=k
18 id m=km=k
19 17 18 oveq12d m=kmm=kk
20 19 eleq2d m=kxmmxkk
21 oveq1 m=kmj,zFz2j2jx=kj,zFz2j2jx
22 21 18 breq12d m=kmj,zFz2j2jxmkj,zFz2j2jxk
23 22 21 18 ifbieq12d m=kifmj,zFz2j2jxmmj,zFz2j2jxm=ifkj,zFz2j2jxkkj,zFz2j2jxk
24 20 23 ifbieq1d m=kifxmmifmj,zFz2j2jxmmj,zFz2j2jxm0=ifxkkifkj,zFz2j2jxkkj,zFz2j2jxk0
25 24 mpteq2dv m=kxifxmmifmj,zFz2j2jxmmj,zFz2j2jxm0=xifxkkifkj,zFz2j2jxkkj,zFz2j2jxk0
26 16 25 eqtrid m=kyifymmifmj,zFz2j2jymmj,zFz2j2jym0=xifxkkifkj,zFz2j2jxkkj,zFz2j2jxk0
27 26 cbvmptv myifymmifmj,zFz2j2jymmj,zFz2j2jym0=kxifxkkifkj,zFz2j2jxkkj,zFz2j2jxk0
28 1 2 10 27 mbfi1fseqlem6 φgg:dom1n0𝑝fgngnfgn+1xngnxFx