Metamath Proof Explorer

Theorem iblmulc2nc

Description: Choice-free analogue of iblmulc2 . (Contributed by Brendan Leahy, 17-Nov-2017)

Ref Expression
Hypotheses itgmulc2nc.1 ⊢ φ → C ∈ ℂ
itgmulc2nc.2 ⊢ φ ∧ x ∈ A → B ∈ V
itgmulc2nc.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
itgmulc2nc.m ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ MblFn
Assertion iblmulc2nc ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 itgmulc2nc.1 ⊢ φ → C ∈ ℂ
2 itgmulc2nc.2 ⊢ φ ∧ x ∈ A → B ∈ V
3 itgmulc2nc.3 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
4 itgmulc2nc.m ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ MblFn
5 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
6 1 adantr ⊢ φ ∧ x ∈ A → C ∈ ℂ
7 iblmbf ⊢ x ∈ A ⟼ B ∈ 𝐿 1 → x ∈ A ⟼ B ∈ MblFn
8 3 7 syl ⊢ φ → x ∈ A ⟼ B ∈ MblFn
9 8 2 mbfmptcl ⊢ φ ∧ x ∈ A → B ∈ ℂ
10 6 9 mulcld ⊢ φ ∧ x ∈ A → C ⁢ B ∈ ℂ
11 10 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B ∈ ℂ
12 elfzelz ⊢ k ∈ 0 … 3 → k ∈ ℤ
13 12 ad2antlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → k ∈ ℤ
14 ax-icn ⊢ i ∈ ℂ
15 ine0 ⊢ i ≠ 0
16 expclz ⊢ i ∈ ℂ ∧ i ≠ 0 ∧ k ∈ ℤ → i k ∈ ℂ
17 14 15 16 mp3an12 ⊢ k ∈ ℤ → i k ∈ ℂ
18 13 17 syl ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → i k ∈ ℂ
19 expne0i ⊢ i ∈ ℂ ∧ i ≠ 0 ∧ k ∈ ℤ → i k ≠ 0
20 14 15 19 mp3an12 ⊢ k ∈ ℤ → i k ≠ 0
21 13 20 syl ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → i k ≠ 0
22 11 18 21 divcld ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B i k ∈ ℂ
23 22 recld ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → ℜ ⁡ C ⁢ B i k ∈ ℝ
24 0re ⊢ 0 ∈ ℝ
25 ifcl ⊢ ℜ ⁡ C ⁢ B i k ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
26 23 24 25 sylancl ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
27 26 rexrd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ *
28 max1 ⊢ 0 ∈ ℝ ∧ ℜ ⁡ C ⁢ B i k ∈ ℝ → 0 ≤ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0
29 24 23 28 sylancr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → 0 ≤ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0
30 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
31 27 29 30 sylanbrc ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ 0 +∞
32 0e0iccpnf ⊢ 0 ∈ 0 +∞
33 32 a1i ⊢ φ ∧ k ∈ 0 … 3 ∧ ¬ x ∈ A → 0 ∈ 0 +∞
34 31 33 ifclda ⊢ φ ∧ k ∈ 0 … 3 → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 ∈ 0 +∞
35 34 adantr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ ℝ → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 ∈ 0 +∞
36 5 35 eqeltrid ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ ℝ → if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ 0 +∞
37 36 fmpttd ⊢ φ ∧ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 : ℝ ⟶ 0 +∞
38 9 recld ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ ℝ
39 38 recnd ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ ℂ
40 39 abscld ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ ℝ
41 9 imcld ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℝ
42 41 recnd ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℂ
43 42 abscld ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℝ
44 40 43 readdcld ⊢ φ ∧ x ∈ A → ℜ ⁡ B + ℑ ⁡ B ∈ ℝ
45 39 absge0d ⊢ φ ∧ x ∈ A → 0 ≤ ℜ ⁡ B
46 42 absge0d ⊢ φ ∧ x ∈ A → 0 ≤ ℑ ⁡ B
47 40 43 45 46 addge0d ⊢ φ ∧ x ∈ A → 0 ≤ ℜ ⁡ B + ℑ ⁡ B
48 elrege0 ⊢ ℜ ⁡ B + ℑ ⁡ B ∈ 0 +∞ ↔ ℜ ⁡ B + ℑ ⁡ B ∈ ℝ ∧ 0 ≤ ℜ ⁡ B + ℑ ⁡ B
49 44 47 48 sylanbrc ⊢ φ ∧ x ∈ A → ℜ ⁡ B + ℑ ⁡ B ∈ 0 +∞
50 0e0icopnf ⊢ 0 ∈ 0 +∞
51 50 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
52 49 51 ifclda ⊢ φ → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 ∈ 0 +∞
53 52 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 ∈ 0 +∞
54 53 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 : ℝ ⟶ 0 +∞
55 reex ⊢ ℝ ∈ V
56 55 a1i ⊢ φ → ℝ ∈ V
57 elrege0 ⊢ ℜ ⁡ B ∈ 0 +∞ ↔ ℜ ⁡ B ∈ ℝ ∧ 0 ≤ ℜ ⁡ B
58 40 45 57 sylanbrc ⊢ φ ∧ x ∈ A → ℜ ⁡ B ∈ 0 +∞
59 58 51 ifclda ⊢ φ → if x ∈ A ℜ ⁡ B 0 ∈ 0 +∞
60 59 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ℜ ⁡ B 0 ∈ 0 +∞
61 elrege0 ⊢ ℑ ⁡ B ∈ 0 +∞ ↔ ℑ ⁡ B ∈ ℝ ∧ 0 ≤ ℑ ⁡ B
62 43 46 61 sylanbrc ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ 0 +∞
63 62 51 ifclda ⊢ φ → if x ∈ A ℑ ⁡ B 0 ∈ 0 +∞
64 63 adantr ⊢ φ ∧ x ∈ ℝ → if x ∈ A ℑ ⁡ B 0 ∈ 0 +∞
65 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0
66 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
67 56 60 64 65 66 offval2 ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + f x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0
68 iftrue ⊢ x ∈ A → if x ∈ A ℜ ⁡ B 0 = ℜ ⁡ B
69 iftrue ⊢ x ∈ A → if x ∈ A ℑ ⁡ B 0 = ℑ ⁡ B
70 68 69 oveq12d ⊢ x ∈ A → if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = ℜ ⁡ B + ℑ ⁡ B
71 iftrue ⊢ x ∈ A → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = ℜ ⁡ B + ℑ ⁡ B
72 70 71 eqtr4d ⊢ x ∈ A → if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
73 00id ⊢ 0 + 0 = 0
74 iffalse ⊢ ¬ x ∈ A → if x ∈ A ℜ ⁡ B 0 = 0
75 iffalse ⊢ ¬ x ∈ A → if x ∈ A ℑ ⁡ B 0 = 0
76 74 75 oveq12d ⊢ ¬ x ∈ A → if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = 0 + 0
77 iffalse ⊢ ¬ x ∈ A → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = 0
78 73 76 77 3eqtr4a ⊢ ¬ x ∈ A → if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
79 72 78 pm2.61i ⊢ if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
80 79 mpteq2i ⊢ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + if x ∈ A ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
81 67 80 syl6req ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + f x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
82 81 fveq2d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + f x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
83 eqid ⊢ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0
84 9 iblcn ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
85 3 84 mpbid ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1 ∧ x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
86 85 simpld ⊢ φ → x ∈ A ⟼ ℜ ⁡ B ∈ 𝐿 1
87 2 3 83 86 38 iblabsnclem ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 ∈ ℝ
88 87 simpld ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 ∈ MblFn
89 60 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 : ℝ ⟶ 0 +∞
90 87 simprd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 ∈ ℝ
91 64 fmpttd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 : ℝ ⟶ 0 +∞
92 eqid ⊢ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
93 85 simprd ⊢ φ → x ∈ A ⟼ ℑ ⁡ B ∈ 𝐿 1
94 2 3 92 93 41 iblabsnclem ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 ∈ MblFn ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 ∈ ℝ
95 94 simprd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 ∈ ℝ
96 88 89 90 91 95 itg2addnc ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + f x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
97 82 96 eqtrd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
98 90 95 readdcld ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 ∈ ℝ
99 97 98 eqeltrd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 ∈ ℝ
100 1 abscld ⊢ φ → C ∈ ℝ
101 1 absge0d ⊢ φ → 0 ≤ C
102 elrege0 ⊢ C ∈ 0 +∞ ↔ C ∈ ℝ ∧ 0 ≤ C
103 100 101 102 sylanbrc ⊢ φ → C ∈ 0 +∞
104 54 99 103 itg2mulc ⊢ φ → ∫ 2 ⁡ ℝ × C × f x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
105 100 adantr ⊢ φ ∧ x ∈ ℝ → C ∈ ℝ
106 fconstmpt ⊢ ℝ × C = x ∈ ℝ ⟼ C
107 106 a1i ⊢ φ → ℝ × C = x ∈ ℝ ⟼ C
108 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
109 56 105 53 107 108 offval2 ⊢ φ → ℝ × C × f x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = x ∈ ℝ ⟼ C ⁢ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0
110 71 oveq2d ⊢ x ∈ A → C ⁢ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = C ⁢ ℜ ⁡ B + ℑ ⁡ B
111 iftrue ⊢ x ∈ A → if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 = C ⁢ ℜ ⁡ B + ℑ ⁡ B
112 110 111 eqtr4d ⊢ x ∈ A → C ⁢ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
113 112 adantl ⊢ φ ∧ x ∈ A → C ⁢ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
114 100 recnd ⊢ φ → C ∈ ℂ
115 114 mul01d ⊢ φ → C ⋅ 0 = 0
116 115 adantr ⊢ φ ∧ ¬ x ∈ A → C ⋅ 0 = 0
117 77 adantl ⊢ φ ∧ ¬ x ∈ A → if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = 0
118 117 oveq2d ⊢ φ ∧ ¬ x ∈ A → C ⁢ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = C ⋅ 0
119 iffalse ⊢ ¬ x ∈ A → if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 = 0
120 119 adantl ⊢ φ ∧ ¬ x ∈ A → if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 = 0
121 116 118 120 3eqtr4d ⊢ φ ∧ ¬ x ∈ A → C ⁢ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
122 113 121 pm2.61dan ⊢ φ → C ⁢ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
123 122 mpteq2dv ⊢ φ → x ∈ ℝ ⟼ C ⁢ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
124 109 123 eqtrd ⊢ φ → ℝ × C × f x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
125 124 fveq2d ⊢ φ → ∫ 2 ⁡ ℝ × C × f x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
126 97 oveq2d ⊢ φ → C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B + ℑ ⁡ B 0 = C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
127 104 125 126 3eqtr3d ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 = C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0
128 100 98 remulcld ⊢ φ → C ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℜ ⁡ B 0 + ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ℑ ⁡ B 0 ∈ ℝ
129 127 128 eqeltrd ⊢ φ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 ∈ ℝ
130 129 adantr ⊢ φ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 ∈ ℝ
131 100 adantr ⊢ φ ∧ x ∈ A → C ∈ ℝ
132 131 44 remulcld ⊢ φ ∧ x ∈ A → C ⁢ ℜ ⁡ B + ℑ ⁡ B ∈ ℝ
133 132 rexrd ⊢ φ ∧ x ∈ A → C ⁢ ℜ ⁡ B + ℑ ⁡ B ∈ ℝ *
134 101 adantr ⊢ φ ∧ x ∈ A → 0 ≤ C
135 131 44 134 47 mulge0d ⊢ φ ∧ x ∈ A → 0 ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
136 elxrge0 ⊢ C ⁢ ℜ ⁡ B + ℑ ⁡ B ∈ 0 +∞ ↔ C ⁢ ℜ ⁡ B + ℑ ⁡ B ∈ ℝ * ∧ 0 ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
137 133 135 136 sylanbrc ⊢ φ ∧ x ∈ A → C ⁢ ℜ ⁡ B + ℑ ⁡ B ∈ 0 +∞
138 32 a1i ⊢ φ ∧ ¬ x ∈ A → 0 ∈ 0 +∞
139 137 138 ifclda ⊢ φ → if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 ∈ 0 +∞
140 139 ad2antrr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ ℝ → if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 ∈ 0 +∞
141 140 fmpttd ⊢ φ ∧ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 : ℝ ⟶ 0 +∞
142 9 abscld ⊢ φ ∧ x ∈ A → B ∈ ℝ
143 131 142 remulcld ⊢ φ ∧ x ∈ A → C ⁢ B ∈ ℝ
144 143 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B ∈ ℝ
145 132 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ ℜ ⁡ B + ℑ ⁡ B ∈ ℝ
146 22 releabsd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → ℜ ⁡ C ⁢ B i k ≤ C ⁢ B i k
147 11 18 21 absdivd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B i k = C ⁢ B i k
148 elfznn0 ⊢ k ∈ 0 … 3 → k ∈ ℕ 0
149 absexp ⊢ i ∈ ℂ ∧ k ∈ ℕ 0 → i k = i k
150 14 148 149 sylancr ⊢ k ∈ 0 … 3 → i k = i k
151 absi ⊢ i = 1
152 151 oveq1i ⊢ i k = 1 k
153 1exp ⊢ k ∈ ℤ → 1 k = 1
154 12 153 syl ⊢ k ∈ 0 … 3 → 1 k = 1
155 152 154 syl5eq ⊢ k ∈ 0 … 3 → i k = 1
156 150 155 eqtrd ⊢ k ∈ 0 … 3 → i k = 1
157 156 oveq2d ⊢ k ∈ 0 … 3 → C ⁢ B i k = C ⁢ B 1
158 157 ad2antlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B i k = C ⁢ B 1
159 10 abscld ⊢ φ ∧ x ∈ A → C ⁢ B ∈ ℝ
160 159 recnd ⊢ φ ∧ x ∈ A → C ⁢ B ∈ ℂ
161 160 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B ∈ ℂ
162 161 div1d ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B 1 = C ⁢ B
163 147 158 162 3eqtrd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B i k = C ⁢ B
164 6 9 absmuld ⊢ φ ∧ x ∈ A → C ⁢ B = C ⁢ B
165 164 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B = C ⁢ B
166 163 165 eqtrd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B i k = C ⁢ B
167 146 166 breqtrd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → ℜ ⁡ C ⁢ B i k ≤ C ⁢ B
168 mulcl ⊢ i ∈ ℂ ∧ ℑ ⁡ B ∈ ℂ → i ⁢ ℑ ⁡ B ∈ ℂ
169 14 42 168 sylancr ⊢ φ ∧ x ∈ A → i ⁢ ℑ ⁡ B ∈ ℂ
170 39 169 abstrid ⊢ φ ∧ x ∈ A → ℜ ⁡ B + i ⁢ ℑ ⁡ B ≤ ℜ ⁡ B + i ⁢ ℑ ⁡ B
171 9 replimd ⊢ φ ∧ x ∈ A → B = ℜ ⁡ B + i ⁢ ℑ ⁡ B
172 171 fveq2d ⊢ φ ∧ x ∈ A → B = ℜ ⁡ B + i ⁢ ℑ ⁡ B
173 absmul ⊢ i ∈ ℂ ∧ ℑ ⁡ B ∈ ℂ → i ⁢ ℑ ⁡ B = i ⁢ ℑ ⁡ B
174 14 42 173 sylancr ⊢ φ ∧ x ∈ A → i ⁢ ℑ ⁡ B = i ⁢ ℑ ⁡ B
175 151 oveq1i ⊢ i ⁢ ℑ ⁡ B = 1 ⁢ ℑ ⁡ B
176 174 175 syl6eq ⊢ φ ∧ x ∈ A → i ⁢ ℑ ⁡ B = 1 ⁢ ℑ ⁡ B
177 43 recnd ⊢ φ ∧ x ∈ A → ℑ ⁡ B ∈ ℂ
178 177 mulid2d ⊢ φ ∧ x ∈ A → 1 ⁢ ℑ ⁡ B = ℑ ⁡ B
179 176 178 eqtr2d ⊢ φ ∧ x ∈ A → ℑ ⁡ B = i ⁢ ℑ ⁡ B
180 179 oveq2d ⊢ φ ∧ x ∈ A → ℜ ⁡ B + ℑ ⁡ B = ℜ ⁡ B + i ⁢ ℑ ⁡ B
181 170 172 180 3brtr4d ⊢ φ ∧ x ∈ A → B ≤ ℜ ⁡ B + ℑ ⁡ B
182 142 44 131 134 181 lemul2ad ⊢ φ ∧ x ∈ A → C ⁢ B ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
183 182 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → C ⁢ B ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
184 23 144 145 167 183 letrd ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → ℜ ⁡ C ⁢ B i k ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
185 135 adantlr ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → 0 ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
186 breq1 ⊢ ℜ ⁡ C ⁢ B i k = if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 → ℜ ⁡ C ⁢ B i k ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B ↔ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
187 breq1 ⊢ 0 = if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 → 0 ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B ↔ if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
188 186 187 ifboth ⊢ ℜ ⁡ C ⁢ B i k ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B ∧ 0 ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
189 184 185 188 syl2anc ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ C ⁢ ℜ ⁡ B + ℑ ⁡ B
190 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
191 190 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
192 111 adantl ⊢ φ ∧ k ∈ 0 … 3 ∧ x ∈ A → if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 = C ⁢ ℜ ⁡ B + ℑ ⁡ B
193 189 191 192 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 + ℑ ⁡ B 0
194 193 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 + ℑ ⁡ B 0
195 0le0 ⊢ 0 ≤ 0
196 195 a1i ⊢ ¬ x ∈ A → 0 ≤ 0
197 iffalse ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 = 0
198 196 197 119 3brtr4d ⊢ ¬ x ∈ A → if x ∈ A if 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 0 ≤ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
199 194 198 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 + ℑ ⁡ B 0
200 5 199 eqbrtrid ⊢ φ ∧ k ∈ 0 … 3 → if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
201 200 ralrimivw ⊢ φ ∧ k ∈ 0 … 3 → ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
202 55 a1i ⊢ φ ∧ k ∈ 0 … 3 → ℝ ∈ V
203 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
204 eqidd ⊢ φ ∧ k ∈ 0 … 3 → x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 = x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
205 202 36 140 203 204 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 + ℑ ⁡ B 0 ↔ ∀ x ∈ ℝ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
206 201 205 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 + ℑ ⁡ B 0
207 itg2le ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 : ℝ ⟶ 0 +∞ ∧ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ f x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0
208 37 141 206 207 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 + ℑ ⁡ B 0
209 itg2lecl ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 : ℝ ⟶ 0 +∞ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 ∈ ℝ ∧ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ≤ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A C ⁢ ℜ ⁡ B + ℑ ⁡ B 0 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
210 37 130 208 209 syl3anc ⊢ φ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
211 210 ralrimiva ⊢ φ → ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ C ⁢ B i k ℜ ⁡ C ⁢ B i k 0 ∈ ℝ
212 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
213 eqidd ⊢ φ ∧ x ∈ A → ℜ ⁡ C ⁢ B i k = ℜ ⁡ C ⁢ B i k
214 212 213 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 ∈ ℝ
215 4 211 214 mpbir2and ⊢ φ → x ∈ A ⟼ C ⁢ B ∈ 𝐿 1