Metamath Proof Explorer

Theorem iblmulc2

Description: Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses itgmulc2.1 ⊢ φ → C ∈ ℂ
itgmulc2.2 ⊢ φ ∧ x ∈ A → B ∈ V
itgmulc2.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
Assertion iblmulc2 ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 itgmulc2.1 ⊢ φ → C ∈ ℂ
2 itgmulc2.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 itgmulc2.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
4 iblmbf ⊢ x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
5 3 4 syl ⊢ φ → x ∈ A ⟼ B ∈ MblFn
6 1 2 5 mbfmulc2 ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ MblFn
7 ifan ⊢ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 = if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0
8 1 adantr ⊢ φ ∧ x ∈ A → C ∈ ℂ
9 5 2 mbfmptcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
10 8 9 mulcld ⊢ φ ∧ x ∈ A → C ⁢ B ∈ ℂ
11 10 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B ∈ ℂ
12 ax-icn ⊢ i ∈ ℂ
13 ine0 ⊢ i ≠ 0
14 elfzelz ⊢ k ∈ 0 … 3 → k ∈ ℤ
15 14 ad2antlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → k ∈ ℤ
16 expclz ⊢ i ∈ ℂ ∧ i ≠ 0 ∧ k ∈ ℤ → i k ∈ ℂ
17 12 13 15 16 mp3an12i ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → i k ∈ ℂ
18 expne0i ⊢ i ∈ ℂ ∧ i ≠ 0 ∧ k ∈ ℤ → i k ≠ 0
19 12 13 15 18 mp3an12i ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → i k ≠ 0
20 11 17 19 divcld ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B i k ∈ ℂ
21 20 recld ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → ℜ ⁡ C ⁢ B i k ∈ ℝ
22 0re ⊢ 0 ∈ ℝ
23 ifcl ⊢ ℜ ⁡ C ⁢ B i k ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
24 21 22 23 sylancl ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
25 24 rexrd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ *
26 max1 ⊢ 0 ∈ ℝ ∧ ℜ ⁡ C ⁢ B i k ∈ ℝ → 0 ≤ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0
27 22 21 26 sylancr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → 0 ≤ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0
28 elxrge0 ⊢ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ 0 +∞ ↔ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ * ∧ 0 ≤ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0
29 25 27 28 sylanbrc ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ 0 +∞
30 0e0iccpnf ⊢ 0 ∈ 0 +∞
31 30 a1i ⊢ φ ∧ k ∈ 0 … 3 ∧ ¬ x ∈ A → 0 ∈ 0 +∞
32 29 31 ifclda ⊢ φ ∧ k ∈ 0 … 3 → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 ∈ 0 +∞
33 32 adantr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ ℝ → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 ∈ 0 +∞
34 7 33 eqeltrid ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ 0 +∞
35 34 fmpttd ⊢ φ ∧ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 : ℝ ⟶ 0 +∞
36 reex ⊢ ℝ ∈ V
37 36 a1i ⊢ φ → ℝ ∈ V
38 1 abscld ⊢ φ → C ∈ ℝ
39 38 adantr ⊢ φ ∧ x ∈ ℝ → C ∈ ℝ
40 9 abscld ⊢ φ ∧ x ∈ A → B ∈ ℝ
41 9 absge0d ⊢ φ ∧ x ∈ A → 0 ≤ B
42 elrege0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ ∧ 0 ≤ B
43 40 41 42 sylanbrc ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
44 0e0icopnf ⊢ 0 ∈ 0 +∞
45 44 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
46 43 45 ifclda ⊢ φ → if x ∈ A B 0 ∈ 0 +∞
47 46 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A B 0 ∈ 0 +∞
48 fconstmpt ⊢ ℝ × C = x ∈ ℝ ⟼ C
49 48 a1i ⊢ φ → ℝ × C = x ∈ ℝ ⟼ C
50 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 = x ∈ ℝ ⟼ if x ∈ A B 0
51 37 39 47 49 50 offval2 ⊢ φ → ℝ × C × f x ∈ ℝ ⟼ if x ∈ A B 0 = x ∈ ℝ ⟼ C ⁢ if x ∈ A B 0
52 ovif2 ⊢ C ⁢ if x ∈ A B 0 = if x ∈ A C ⁢ B C ⋅ 0
53 8 9 absmuld ⊢ φ ∧ x ∈ A → C ⁢ B = C ⁢ B
54 53 ifeq1da ⊢ φ → if x ∈ A C ⁢ B C ⋅ 0 = if x ∈ A C ⁢ B C ⋅ 0
55 38 recnd ⊢ φ → C ∈ ℂ
56 55 mul01d ⊢ φ → C ⋅ 0 = 0
57 56 ifeq2d ⊢ φ → if x ∈ A C ⁢ B C ⋅ 0 = if x ∈ A C ⁢ B 0
58 54 57 eqtr3d ⊢ φ → if x ∈ A C ⁢ B C ⋅ 0 = if x ∈ A C ⁢ B 0
59 52 58 syl5eq ⊢ φ → C ⁢ if x ∈ A B 0 = if x ∈ A C ⁢ B 0
60 59 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ C ⁢ if x ∈ A B 0 = x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
61 51 60 eqtrd ⊢ φ → ℝ × C × f x ∈ ℝ ⟼ if x ∈ A B 0 = x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
62 61 fveq2d ⊢ φ → ∫ 2 ⁡ ℝ × C × f x ∈ ℝ ⟼ if x ∈ A B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
63 47 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A B 0 : ℝ ⟶ 0 +∞
64 2 3 iblabs ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
65 40 41 iblpos ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
66 64 65 mpbid ⊢ φ → x ∈ A ⟼ B ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
67 66 simprd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
68 abscl ⊢ C ∈ ℂ → C ∈ ℝ
69 absge0 ⊢ C ∈ ℂ → 0 ≤ C
70 elrege0 ⊢ C ∈ 0 +∞ ↔ C ∈ ℝ ∧ 0 ≤ C
71 68 69 70 sylanbrc ⊢ C ∈ ℂ → C ∈ 0 +∞
72 1 71 syl ⊢ φ → C ∈ 0 +∞
73 63 67 72 itg2mulc ⊢ φ → ∫ 2 ⁡ ℝ × C × f x ∈ ℝ ⟼ if x ∈ A B 0 = C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0
74 62 73 eqtr3d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 = C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0
75 38 67 remulcld ⊢ φ → C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A B 0 ∈ ℝ
76 74 75 eqeltrd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 ∈ ℝ
77 76 adantr ⊢ φ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 ∈ ℝ
78 10 abscld ⊢ φ ∧ x ∈ A → C ⁢ B ∈ ℝ
79 78 rexrd ⊢ φ ∧ x ∈ A → C ⁢ B ∈ ℝ *
80 10 absge0d ⊢ φ ∧ x ∈ A → 0 ≤ C ⁢ B
81 elxrge0 ⊢ C ⁢ B ∈ 0 +∞ ↔ C ⁢ B ∈ ℝ * ∧ 0 ≤ C ⁢ B
82 79 80 81 sylanbrc ⊢ φ ∧ x ∈ A → C ⁢ B ∈ 0 +∞
83 30 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
84 82 83 ifclda ⊢ φ → if x ∈ A C ⁢ B 0 ∈ 0 +∞
85 84 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A C ⁢ B 0 ∈ 0 +∞
86 85 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 : ℝ ⟶ 0 +∞
87 86 adantr ⊢ φ ∧ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 : ℝ ⟶ 0 +∞
88 20 releabsd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → ℜ ⁡ C ⁢ B i k ≤ C ⁢ B i k
89 11 17 19 absdivd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B i k = C ⁢ B i k
90 elfznn0 ⊢ k ∈ 0 … 3 → k ∈ ℕ 0
91 90 ad2antlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → k ∈ ℕ 0
92 absexp ⊢ i ∈ ℂ ∧ k ∈ ℕ 0 → i k = i k
93 12 91 92 sylancr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → i k = i k
94 absi ⊢ i = 1
95 94 oveq1i ⊢ i k = 1 k
96 1exp ⊢ k ∈ ℤ → 1 k = 1
97 15 96 syl ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → 1 k = 1
98 95 97 syl5eq ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → i k = 1
99 93 98 eqtrd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → i k = 1
100 99 oveq2d ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B i k = C ⁢ B 1
101 78 recnd ⊢ φ ∧ x ∈ A → C ⁢ B ∈ ℂ
102 101 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B ∈ ℂ
103 102 div1d ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B 1 = C ⁢ B
104 89 100 103 3eqtrd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B i k = C ⁢ B
105 88 104 breqtrd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → ℜ ⁡ C ⁢ B i k ≤ C ⁢ B
106 80 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → 0 ≤ C ⁢ B
107 breq1 ⊢ ℜ ⁡ C ⁢ B i k = if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 → ℜ ⁡ C ⁢ B i k ≤ C ⁢ B ↔ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ C ⁢ B
108 breq1 ⊢ 0 = if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 → 0 ≤ C ⁢ B ↔ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ C ⁢ B
109 107 108 ifboth ⊢ ℜ ⁡ C ⁢ B i k ≤ C ⁢ B ∧ 0 ≤ C ⁢ B → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ C ⁢ B
110 105 106 109 syl2anc ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ C ⁢ B
111 iftrue ⊢ x ∈ A → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 = if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0
112 111 adantl ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 = if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0
113 iftrue ⊢ x ∈ A → if x ∈ A C ⁢ B 0 = C ⁢ B
114 113 adantl ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if x ∈ A C ⁢ B 0 = C ⁢ B
115 110 112 114 3brtr4d ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 ≤ if x ∈ A C ⁢ B 0
116 115 ex ⊢ φ ∧ k ∈ 0 … 3 → x ∈ A → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 ≤ if x ∈ A C ⁢ B 0
117 0le0 ⊢ 0 ≤ 0
118 117 a1i ⊢ ¬ x ∈ A → 0 ≤ 0
119 iffalse ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 = 0
120 iffalse ⊢ ¬ x ∈ A → if x ∈ A C ⁢ B 0 = 0
121 118 119 120 3brtr4d ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 ≤ if x ∈ A C ⁢ B 0
122 116 121 pm2.61d1 ⊢ φ ∧ k ∈ 0 … 3 → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 ≤ if x ∈ A C ⁢ B 0
123 7 122 eqbrtrid ⊢ φ ∧ k ∈ 0 … 3 → if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ if x ∈ A C ⁢ B 0
124 123 ralrimivw ⊢ φ ∧ k ∈ 0 … 3 → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ if x ∈ A C ⁢ B 0
125 36 a1i ⊢ φ ∧ k ∈ 0 … 3 → ℝ ∈ V
126 85 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ ℝ → if x ∈ A C ⁢ B 0 ∈ 0 +∞
127 eqidd ⊢ φ ∧ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0
128 eqidd ⊢ φ ∧ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 = x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
129 125 34 126 127 128 ofrfval2 ⊢ φ ∧ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ f x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 ↔ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ if x ∈ A C ⁢ B 0
130 124 129 mpbird ⊢ φ ∧ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ f x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
131 itg2le ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ f x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
132 35 87 130 131 syl3anc ⊢ φ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0
133 itg2lecl ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 : ℝ ⟶ 0 +∞ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ B 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
134 35 77 132 133 syl3anc ⊢ φ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
135 134 ralrimiva ⊢ φ → ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
136 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0
137 eqidd ⊢ φ ∧ x ∈ A → ℜ ⁡ C ⁢ B i k = ℜ ⁡ C ⁢ B i k
138 136 137 10 isibl2 ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ 𝐿 1 ↔ x ∈ A ⟼ C ⁢ B ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
139 6 135 138 mpbir2and ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ 𝐿 1