Metamath Proof Explorer


Theorem iblabsr

Description: A measurable function is integrable iff its absolute value is integrable. (See iblabs for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses iblabsr.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
iblabsr.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
iblabsr.3 ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )
Assertion iblabsr ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 iblabsr.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
2 iblabsr.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ MblFn )
3 iblabsr.3 ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )
4 ifan if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
5 2 1 mbfmptcl ( ( 𝜑𝑥𝐴 ) → 𝐵 ∈ ℂ )
6 5 adantlr ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → 𝐵 ∈ ℂ )
7 ax-icn i ∈ ℂ
8 ine0 i ≠ 0
9 elfzelz ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
10 9 ad2antlr ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → 𝑘 ∈ ℤ )
11 expclz ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ∈ ℂ )
12 7 8 10 11 mp3an12i ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( i ↑ 𝑘 ) ∈ ℂ )
13 expne0i ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
14 7 8 10 13 mp3an12i ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( i ↑ 𝑘 ) ≠ 0 )
15 6 12 14 divcld ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( 𝐵 / ( i ↑ 𝑘 ) ) ∈ ℂ )
16 15 recld ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ ℝ )
17 0re 0 ∈ ℝ
18 ifcl ( ( ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
19 16 17 18 sylancl ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
20 19 rexrd ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* )
21 max1 ( ( 0 ∈ ℝ ∧ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) )
22 17 16 21 sylancr ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) )
23 elxrge0 ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) ↔ ( if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* ∧ 0 ≤ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
24 20 22 23 sylanbrc ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
25 0e0iccpnf 0 ∈ ( 0 [,] +∞ )
26 25 a1i ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
27 24 26 ifclda ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
28 4 27 eqeltrid ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
29 28 adantr ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
30 29 fmpttd ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
31 5 abscld ( ( 𝜑𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
32 5 absge0d ( ( 𝜑𝑥𝐴 ) → 0 ≤ ( abs ‘ 𝐵 ) )
33 31 32 iblpos ( 𝜑 → ( ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
34 3 33 mpbid ( 𝜑 → ( ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) )
35 34 simprd ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
36 35 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
37 31 rexrd ( ( 𝜑𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ* )
38 elxrge0 ( ( abs ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ 𝐵 ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ 𝐵 ) ) )
39 37 32 38 sylanbrc ( ( 𝜑𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
40 25 a1i ( ( 𝜑 ∧ ¬ 𝑥𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
41 39 40 ifclda ( 𝜑 → if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ ( 0 [,] +∞ ) )
42 41 adantr ( ( 𝜑𝑥 ∈ ℝ ) → if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ ( 0 [,] +∞ ) )
43 42 fmpttd ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
44 43 adantr ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
45 15 releabsd ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ≤ ( abs ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
46 6 12 14 absdivd ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( abs ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ( abs ‘ 𝐵 ) / ( abs ‘ ( i ↑ 𝑘 ) ) ) )
47 elfznn0 ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℕ0 )
48 47 ad2antlr ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → 𝑘 ∈ ℕ0 )
49 absexp ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( i ↑ 𝑘 ) ) = ( ( abs ‘ i ) ↑ 𝑘 ) )
50 7 48 49 sylancr ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( abs ‘ ( i ↑ 𝑘 ) ) = ( ( abs ‘ i ) ↑ 𝑘 ) )
51 absi ( abs ‘ i ) = 1
52 51 oveq1i ( ( abs ‘ i ) ↑ 𝑘 ) = ( 1 ↑ 𝑘 )
53 1exp ( 𝑘 ∈ ℤ → ( 1 ↑ 𝑘 ) = 1 )
54 10 53 syl ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( 1 ↑ 𝑘 ) = 1 )
55 52 54 syl5eq ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( ( abs ‘ i ) ↑ 𝑘 ) = 1 )
56 50 55 eqtrd ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( abs ‘ ( i ↑ 𝑘 ) ) = 1 )
57 56 oveq2d ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( ( abs ‘ 𝐵 ) / ( abs ‘ ( i ↑ 𝑘 ) ) ) = ( ( abs ‘ 𝐵 ) / 1 ) )
58 31 recnd ( ( 𝜑𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℂ )
59 58 adantlr ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℂ )
60 59 div1d ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( ( abs ‘ 𝐵 ) / 1 ) = ( abs ‘ 𝐵 ) )
61 46 57 60 3eqtrd ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( abs ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( abs ‘ 𝐵 ) )
62 45 61 breqtrd ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ≤ ( abs ‘ 𝐵 ) )
63 6 absge0d ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → 0 ≤ ( abs ‘ 𝐵 ) )
64 breq1 ( ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) → ( ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ≤ ( abs ‘ 𝐵 ) ↔ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( abs ‘ 𝐵 ) ) )
65 breq1 ( 0 = if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) → ( 0 ≤ ( abs ‘ 𝐵 ) ↔ if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( abs ‘ 𝐵 ) ) )
66 64 65 ifboth ( ( ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ≤ ( abs ‘ 𝐵 ) ∧ 0 ≤ ( abs ‘ 𝐵 ) ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( abs ‘ 𝐵 ) )
67 62 63 66 syl2anc ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( abs ‘ 𝐵 ) )
68 iftrue ( 𝑥𝐴 → if ( 𝑥𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) )
69 68 adantl ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → if ( 𝑥𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) )
70 iftrue ( 𝑥𝐴 → if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) = ( abs ‘ 𝐵 ) )
71 70 adantl ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) = ( abs ‘ 𝐵 ) )
72 67 69 71 3brtr4d ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → if ( 𝑥𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) )
73 72 ex ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥𝐴 → if ( 𝑥𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) )
74 0le0 0 ≤ 0
75 74 a1i ( ¬ 𝑥𝐴 → 0 ≤ 0 )
76 iffalse ( ¬ 𝑥𝐴 → if ( 𝑥𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
77 iffalse ( ¬ 𝑥𝐴 → if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) = 0 )
78 75 76 77 3brtr4d ( ¬ 𝑥𝐴 → if ( 𝑥𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) )
79 73 78 pm2.61d1 ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥𝐴 , if ( 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) )
80 4 79 eqbrtrid ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) )
81 80 ralrimivw ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ∀ 𝑥 ∈ ℝ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) )
82 reex ℝ ∈ V
83 82 a1i ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ℝ ∈ V )
84 37 adantlr ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ* )
85 84 63 38 sylanbrc ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥𝐴 ) → ( abs ‘ 𝐵 ) ∈ ( 0 [,] +∞ ) )
86 85 26 ifclda ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ ( 0 [,] +∞ ) )
87 86 adantr ( ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ ( 0 [,] +∞ ) )
88 eqidd ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
89 eqidd ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) )
90 83 29 87 88 89 ofrfval2 ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) )
91 81 90 mpbird ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) )
92 itg2le ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) )
93 30 44 91 92 syl3anc ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) )
94 itg2lecl ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
95 30 36 93 94 syl3anc ( ( 𝜑𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
96 95 ralrimiva ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
97 eqidd ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
98 eqidd ( ( 𝜑𝑥𝐴 ) → ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) )
99 97 98 1 isibl2 ( 𝜑 → ( ( 𝑥𝐴𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥𝐴𝐵 ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥𝐴 ∧ 0 ≤ ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( 𝐵 / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
100 2 96 99 mpbir2and ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )