Theorem mbfi1fseq 24993

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 𝐺 and "leaves the details as an exercise to the reader". (Contributed by Mario Carneiro, 16-Aug-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)

Hypotheses

Ref	Expression
mbfi1fseq.1	⊢ (𝜑 → 𝐹 ∈ MblFn)
mbfi1fseq.2	⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))

Assertion

Ref	Expression
mbfi1fseq	⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Distinct variable groups:   𝑔,𝑛,𝑥,𝐹   𝜑,𝑛,𝑥

Allowed substitution hint:   𝜑(𝑔)

Proof of Theorem mbfi1fseq

Dummy variables 𝑗 𝑘 𝑚 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mbfi1fseq.1	. 2 ⊢ (𝜑 → 𝐹 ∈ MblFn)
2		mbfi1fseq.2	. 2 ⊢ (𝜑 → 𝐹:ℝ⟶(0[,)+∞))
3		oveq2 7346	. . . . . 6 ⊢ (𝑗 = 𝑘 → (2↑𝑗) = (2↑𝑘))
4	3	oveq2d 7354	. . . . 5 ⊢ (𝑗 = 𝑘 → ((𝐹‘𝑧) · (2↑𝑗)) = ((𝐹‘𝑧) · (2↑𝑘)))
5	4	fveq2d 6830	. . . 4 ⊢ (𝑗 = 𝑘 → (⌊‘((𝐹‘𝑧) · (2↑𝑗))) = (⌊‘((𝐹‘𝑧) · (2↑𝑘))))
6	5, 3	oveq12d 7356	. . 3 ⊢ (𝑗 = 𝑘 → ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)) = ((⌊‘((𝐹‘𝑧) · (2↑𝑘))) / (2↑𝑘)))
7		fveq2 6826	. . . . 5 ⊢ (𝑧 = 𝑦 → (𝐹‘𝑧) = (𝐹‘𝑦))
8	7	fvoveq1d 7360	. . . 4 ⊢ (𝑧 = 𝑦 → (⌊‘((𝐹‘𝑧) · (2↑𝑘))) = (⌊‘((𝐹‘𝑦) · (2↑𝑘))))
9	8	oveq1d 7353	. . 3 ⊢ (𝑧 = 𝑦 → ((⌊‘((𝐹‘𝑧) · (2↑𝑘))) / (2↑𝑘)) = ((⌊‘((𝐹‘𝑦) · (2↑𝑘))) / (2↑𝑘)))
10	6, 9	cbvmpov 7433	. 2 ⊢ (𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗))) = (𝑘 ∈ ℕ, 𝑦 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑦) · (2↑𝑘))) / (2↑𝑘)))
11		eleq1w 2819	. . . . . 6 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ (-𝑚[,]𝑚) ↔ 𝑥 ∈ (-𝑚[,]𝑚)))
12		oveq2 7346	. . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦) = (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥))
13	12	breq1d 5103	. . . . . . 7 ⊢ (𝑦 = 𝑥 → ((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦) ≤ 𝑚 ↔ (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑚))
14	13, 12	ifbieq1d 4498	. . . . . 6 ⊢ (𝑦 = 𝑥 → if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦), 𝑚) = if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑚))
15	11, 14	ifbieq1d 4498	. . . . 5 ⊢ (𝑦 = 𝑥 → if(𝑦 ∈ (-𝑚[,]𝑚), if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦), 𝑚), 0) = if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑚), 0))
16	15	cbvmptv 5206	. . . 4 ⊢ (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (-𝑚[,]𝑚), if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦), 𝑚), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑚), 0))
17		negeq 11315	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → -𝑚 = -𝑘)
18		id 22	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘)
19	17, 18	oveq12d 7356	. . . . . . 7 ⊢ (𝑚 = 𝑘 → (-𝑚[,]𝑚) = (-𝑘[,]𝑘))
20	19	eleq2d 2822	. . . . . 6 ⊢ (𝑚 = 𝑘 → (𝑥 ∈ (-𝑚[,]𝑚) ↔ 𝑥 ∈ (-𝑘[,]𝑘)))
21		oveq1 7345	. . . . . . . 8 ⊢ (𝑚 = 𝑘 → (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) = (𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥))
22	21, 18	breq12d 5106	. . . . . . 7 ⊢ (𝑚 = 𝑘 → ((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑚 ↔ (𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑘))
23	22, 21, 18	ifbieq12d 4502	. . . . . 6 ⊢ (𝑚 = 𝑘 → if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑚) = if((𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑘, (𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑘))
24	20, 23	ifbieq1d 4498	. . . . 5 ⊢ (𝑚 = 𝑘 → if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑚), 0) = if(𝑥 ∈ (-𝑘[,]𝑘), if((𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑘, (𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑘), 0))
25	24	mpteq2dv 5195	. . . 4 ⊢ (𝑚 = 𝑘 → (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑚[,]𝑚), if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑚), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑘[,]𝑘), if((𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑘, (𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑘), 0)))
26	16, 25	eqtrid 2788	. . 3 ⊢ (𝑚 = 𝑘 → (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (-𝑚[,]𝑚), if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦), 𝑚), 0)) = (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑘[,]𝑘), if((𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑘, (𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑘), 0)))
27	26	cbvmptv 5206	. 2 ⊢ (𝑚 ∈ ℕ ↦ (𝑦 ∈ ℝ ↦ if(𝑦 ∈ (-𝑚[,]𝑚), if((𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦) ≤ 𝑚, (𝑚(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑦), 𝑚), 0))) = (𝑘 ∈ ℕ ↦ (𝑥 ∈ ℝ ↦ if(𝑥 ∈ (-𝑘[,]𝑘), if((𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥) ≤ 𝑘, (𝑘(𝑗 ∈ ℕ, 𝑧 ∈ ℝ ↦ ((⌊‘((𝐹‘𝑧) · (2↑𝑗))) / (2↑𝑗)))𝑥), 𝑘), 0)))
28	1, 2, 10, 27	mbfi1fseqlem6 24992	1 ⊢ (𝜑 → ∃𝑔(𝑔:ℕ⟶dom ∫1 ∧ ∀𝑛 ∈ ℕ (0𝑝 ∘r ≤ (𝑔‘𝑛) ∧ (𝑔‘𝑛) ∘r ≤ (𝑔‘(𝑛 + 1))) ∧ ∀𝑥 ∈ ℝ (𝑛 ∈ ℕ ↦ ((𝑔‘𝑛)‘𝑥)) ⇝ (𝐹‘𝑥)))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086  ∃wex 1780   ∈ wcel 2105  ∀wral 3061  ifcif 4474   class class class wbr 5093   ↦ cmpt 5176  dom cdm 5621  ⟶wf 6476  ‘cfv 6480  (class class class)co 7338   ∈ cmpo 7340   ∘_r cofr 7595  ℝcr 10972  0cc0 10973  1c1 10974   + caddc 10976   · cmul 10978  +∞cpnf 11108   ≤ cle 11112  -cneg 11308   / cdiv 11734  ℕcn 12075  2c2 12130  [,)cico 13183  [,]cicc 13184  ⌊cfl 13612  ↑cexp 13884   ⇝ cli 15293  MblFncmbf 24885  ∫₁citg1 24886  0_𝑝c0p 24940

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5230  ax-sep 5244  ax-nul 5251  ax-pow 5309  ax-pr 5373  ax-un 7651  ax-inf2 9499  ax-cnex 11029  ax-resscn 11030  ax-1cn 11031  ax-icn 11032  ax-addcl 11033  ax-addrcl 11034  ax-mulcl 11035  ax-mulrcl 11036  ax-mulcom 11037  ax-addass 11038  ax-mulass 11039  ax-distr 11040  ax-i2m1 11041  ax-1ne0 11042  ax-1rid 11043  ax-rnegex 11044  ax-rrecex 11045  ax-cnre 11046  ax-pre-lttri 11047  ax-pre-lttrn 11048  ax-pre-ltadd 11049  ax-pre-mulgt0 11050  ax-pre-sup 11051

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4271  df-if 4475  df-pw 4550  df-sn 4575  df-pr 4577  df-op 4581  df-uni 4854  df-int 4896  df-iun 4944  df-br 5094  df-opab 5156  df-mpt 5177  df-tr 5211  df-id 5519  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5576  df-se 5577  df-we 5578  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6239  df-ord 6306  df-on 6307  df-lim 6308  df-suc 6309  df-iota 6432  df-fun 6482  df-fn 6483  df-f 6484  df-f1 6485  df-fo 6486  df-f1o 6487  df-fv 6488  df-isom 6489  df-riota 7294  df-ov 7341  df-oprab 7342  df-mpo 7343  df-of 7596  df-ofr 7597  df-om 7782  df-1st 7900  df-2nd 7901  df-frecs 8168  df-wrecs 8199  df-recs 8273  df-rdg 8312  df-1o 8368  df-2o 8369  df-er 8570  df-map 8689  df-pm 8690  df-en 8806  df-dom 8807  df-sdom 8808  df-fin 8809  df-fi 9269  df-sup 9300  df-inf 9301  df-oi 9368  df-dju 9759  df-card 9797  df-pnf 11113  df-mnf 11114  df-xr 11115  df-ltxr 11116  df-le 11117  df-sub 11309  df-neg 11310  df-div 11735  df-nn 12076  df-2 12138  df-3 12139  df-n0 12336  df-z 12422  df-uz 12685  df-q 12791  df-rp 12833  df-xneg 12950  df-xadd 12951  df-xmul 12952  df-ioo 13185  df-ico 13187  df-icc 13188  df-fz 13342  df-fzo 13485  df-fl 13614  df-seq 13824  df-exp 13885  df-hash 14147  df-cj 14910  df-re 14911  df-im 14912  df-sqrt 15046  df-abs 15047  df-clim 15297  df-rlim 15298  df-sum 15498  df-rest 17231  df-topgen 17252  df-psmet 20696  df-xmet 20697  df-met 20698  df-bl 20699  df-mopn 20700  df-top 22150  df-topon 22167  df-bases 22203  df-cmp 22645  df-ovol 24735  df-vol 24736  df-mbf 24890  df-itg1 24891  df-0p 24941

This theorem is referenced by:  mbfi1flimlem  24994  itg2add  25031