Metamath Proof Explorer

Theorem iblss2

Description: Change the domain of an integrability predicate. (Contributed by Mario Carneiro, 13-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses iblss2.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
iblss2.2 ⊢ ( 𝜑 → 𝐵 ∈ dom vol )
iblss2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
iblss2.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
iblss2.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
Assertion iblss2 ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 iblss2.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2 iblss2.2 ⊢ ( 𝜑 → 𝐵 ∈ dom vol )
3 iblss2.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ 𝑉 )
4 iblss2.4 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 = 0 )
5 iblss2.5 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 )
6 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
7 5 6 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐶 ) ∈ MblFn )
8 1 2 3 4 7 mbfss ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn )
9 1 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → 𝐴 ⊆ 𝐵 )
10 9 sselda ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
11 10 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
12 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
13 12 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
14 11 13 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
15 ifid ⊢ if ( 𝑥 ∈ 𝐵 , 0 , 0 ) = 0
16 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → 𝜑 )
17 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
18 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ¬ 𝑥 ∈ 𝐴 )
19 17 18 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) )
20 16 19 4 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐶 = 0 )
21 20 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐶 / ( i ↑ 𝑘 ) ) = ( 0 / ( i ↑ 𝑘 ) ) )
22 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑘 ∈ ( 0 ... 3 ) )
23 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
24 ax-icn ⊢ i ∈ ℂ
25 ine0 ⊢ i ≠ 0
26 expclz ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ∈ ℂ )
27 expne0i ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
28 26 27 div0d ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( 0 / ( i ↑ 𝑘 ) ) = 0 )
29 24 25 28 mp3an12 ⊢ ( 𝑘 ∈ ℤ → ( 0 / ( i ↑ 𝑘 ) ) = 0 )
30 22 23 29 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 0 / ( i ↑ 𝑘 ) ) = 0 )
31 21 30 eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝐶 / ( i ↑ 𝑘 ) ) = 0 )
32 31 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ 0 ) )
33 re0 ⊢ ( ℜ ‘ 0 ) = 0
34 32 33 eqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = 0 )
35 34 ifeq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 , 0 ) )
36 ifid ⊢ if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 , 0 ) = 0
37 35 36 eqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = 0 )
38 37 ifeq1da ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 𝑥 ∈ 𝐵 , 0 , 0 ) )
39 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
40 39 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
41 15 38 40 3eqtr4a ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
42 14 41 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) )
43 ifan ⊢ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐵 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
44 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
45 42 43 44 3eqtr4g ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) )
46 45 mpteq2dv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
47 46 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) )
48 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
49 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) )
50 48 49 5 3 iblitg ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℤ ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
51 23 50 sylan2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
52 47 51 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
53 52 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
54 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
55 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) )
56 elun ⊢ ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) )
57 undif2 ⊢ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐵 )
58 ssequn1 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ 𝐵 ) = 𝐵 )
59 1 58 sylib ⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) = 𝐵 )
60 57 59 eqtrid ⊢ ( 𝜑 → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
61 60 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ↔ 𝑥 ∈ 𝐵 ) )
62 56 61 bitr3id ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) ↔ 𝑥 ∈ 𝐵 ) )
63 62 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) )
64 7 3 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
65 0cn ⊢ 0 ∈ ℂ
66 4 65 eqeltrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) → 𝐶 ∈ ℂ )
67 64 66 jaodan ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) ) ) → 𝐶 ∈ ℂ )
68 63 67 syldan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
69 54 55 68 isibl2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐵 ∧ 0 ≤ ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐶 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
70 8 53 69 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ∈ 𝐿1 )