Definition df-ibl 25657

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.)

Assertion

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

Distinct variable group:   𝑦,𝑘,𝑓,𝑥

Detailed syntax breakdown of Definition df-ibl

Step	Hyp	Ref	Expression
1		cibl 25652	. 2 class 𝐿1
2		vx	. . . . . . 7 setvar 𝑥
3		cr 11154	. . . . . . 7 class ℝ
4		vy	. . . . . . . 8 setvar 𝑦
5	2	cv 1539	. . . . . . . . . . 11 class 𝑥
6		vf	. . . . . . . . . . . 12 setvar 𝑓
7	6	cv 1539	. . . . . . . . . . 11 class 𝑓
8	5, 7	cfv 6561	. . . . . . . . . 10 class (𝑓‘𝑥)
9		ci 11157	. . . . . . . . . . 11 class i
10		vk	. . . . . . . . . . . 12 setvar 𝑘
11	10	cv 1539	. . . . . . . . . . 11 class 𝑘
12		cexp 14102	. . . . . . . . . . 11 class ↑
13	9, 11, 12	co 7431	. . . . . . . . . 10 class (i↑𝑘)
14		cdiv 11920	. . . . . . . . . 10 class /
15	8, 13, 14	co 7431	. . . . . . . . 9 class ((𝑓‘𝑥) / (i↑𝑘))
16		cre 15136	. . . . . . . . 9 class ℜ
17	15, 16	cfv 6561	. . . . . . . 8 class (ℜ‘((𝑓‘𝑥) / (i↑𝑘)))
18	7	cdm 5685	. . . . . . . . . . 11 class dom 𝑓
19	5, 18	wcel 2108	. . . . . . . . . 10 wff 𝑥 ∈ dom 𝑓
20		cc0 11155	. . . . . . . . . . 11 class 0
21	4	cv 1539	. . . . . . . . . . 11 class 𝑦
22		cle 11296	. . . . . . . . . . 11 class ≤
23	20, 21, 22	wbr 5143	. . . . . . . . . 10 wff 0 ≤ 𝑦
24	19, 23	wa 395	. . . . . . . . 9 wff (𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦)
25	24, 21, 20	cif 4525	. . . . . . . 8 class if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
26	4, 17, 25	csb 3899	. . . . . . 7 class ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)
27	2, 3, 26	cmpt 5225	. . . . . 6 class (𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))
28		citg2 25651	. . . . . 6 class ∫2
29	27, 28	cfv 6561	. . . . 5 class (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0)))
30	29, 3	wcel 2108	. . . 4 wff (∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
31		c3 12322	. . . . 5 class 3
32		cfz 13547	. . . . 5 class ...
33	20, 31, 32	co 7431	. . . 4 class (0...3)
34	30, 10, 33	wral 3061	. . 3 wff ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ
35		cmbf 25649	. . 3 class MblFn
36	34, 6, 35	crab 3436	. 2 class {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}
37	1, 36	wceq 1540	1 wff 𝐿1 = {𝑓 ∈ MblFn ∣ ∀𝑘 ∈ (0...3)(∫2‘(𝑥 ∈ ℝ ↦ ⦋(ℜ‘((𝑓‘𝑥) / (i↑𝑘))) / 𝑦⦌if((𝑥 ∈ dom 𝑓 ∧ 0 ≤ 𝑦), 𝑦, 0))) ∈ ℝ}

This definition is referenced by:  isibl  25800  iblmbf  25802