This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) ∈ ℝ }