Definition df-ibl

Description: Define the class of integrable functions on the reals. A function is integrable if it is measurable and the integrals of the pieces of the function are all finite. (Contributed by Mario Carneiro, 28-Jun-2014)

	Ref	Expression
Assertion	df-ibl	⊢ 𝐿1 = { 𝑓 ∈ MblFn ∣ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ∈ ℝ }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cibl	⊢ 𝐿1
1		vf	⊢ 𝑓
2		cmbf	⊢ MblFn
3		vk	⊢ 𝑘
4		cc0	⊢ 0
5		cfz	⊢ ...
6		c3	⊢ 3
7	4 6 5	co	⊢ ( 0 ... 3 )
8		citg2	⊢ ∫2
9		vx	⊢ 𝑥
10		cr	⊢ ℝ
11		cre	⊢ ℜ
12	1	cv	⊢ 𝑓
13	9	cv	⊢ 𝑥
14	13 12	cfv	⊢ ( 𝑓 ‘ 𝑥 )
15		cdiv	⊢ /
16		ci	⊢ i
17		cexp	⊢ ↑
18	3	cv	⊢ 𝑘
19	16 18 17	co	⊢ ( i ↑ 𝑘 )
20	14 19 15	co	⊢ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) )
21	20 11	cfv	⊢ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) )
22		vy	⊢ 𝑦
23	12	cdm	⊢ dom 𝑓
24	13 23	wcel	⊢ 𝑥 ∈ dom 𝑓
25		cle	⊢ ≤
26	22	cv	⊢ 𝑦
27	4 26 25	wbr	⊢ 0 ≤ 𝑦
28	24 27	wa	⊢ ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 )
29	28 26 4	cif	⊢ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 )
30	22 21 29	csb	⊢ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 )
31	9 10 30	cmpt	⊢ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) )
32	31 8	cfv	⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) )
33	32 10	wcel	⊢ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ∈ ℝ
34	33 3 7	wral	⊢ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ∈ ℝ
35	34 1 2	crab	⊢ { 𝑓 ∈ MblFn ∣ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ∈ ℝ }
36	0 35	wceq	⊢ 𝐿1 = { 𝑓 ∈ MblFn ∣ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ ⦋ ( ℜ ‘ ( ( 𝑓 ‘ 𝑥 ) / ( i ↑ 𝑘 ) ) ) / 𝑦 ⦌ if ( ( 𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦 ) , 𝑦 , 0 ) ) ) ∈ ℝ }