Metamath Proof Explorer

Theorem iblconst

Description: A constant function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Assertion iblconst ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ → A × B ∈ 𝐿 1

Proof

Step Hyp Ref Expression
1 fconstmpt ⊢ A × B = x ∈ A ⟼ B
2 mbfconst ⊢ A ∈ dom ⁡ vol ∧ B ∈ ℂ → A × B ∈ MblFn
3 2 3adant2 ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ → A × B ∈ MblFn
4 1 3 eqeltrrid ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ → x ∈ A ⟼ B ∈ MblFn
5 ifan ⊢ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = if x ∈ A if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 0
6 5 mpteq2i ⊢ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = x ∈ ℝ ⟼ if x ∈ A if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 0
7 6 fveq2i ⊢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 0
8 simpl1 ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → A ∈ dom ⁡ vol
9 simpl2 ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → vol ⁡ A ∈ ℝ
10 simpl3 ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → B ∈ ℂ
11 ax-icn ⊢ i ∈ ℂ
12 ine0 ⊢ i ≠ 0
13 elfzelz ⊢ k ∈ 0 … 3 → k ∈ ℤ
14 13 adantl ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → k ∈ ℤ
15 expclz ⊢ i ∈ ℂ ∧ i ≠ 0 ∧ k ∈ ℤ → i k ∈ ℂ
16 11 12 14 15 mp3an12i ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → i k ∈ ℂ
17 expne0i ⊢ i ∈ ℂ ∧ i ≠ 0 ∧ k ∈ ℤ → i k ≠ 0
18 11 12 14 17 mp3an12i ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → i k ≠ 0
19 10 16 18 divcld ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → B i k ∈ ℂ
20 19 recld ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → ℜ ⁡ B i k ∈ ℝ
21 0re ⊢ 0 ∈ ℝ
22 ifcl ⊢ ℜ ⁡ B i k ∈ ℝ ∧ 0 ∈ ℝ → if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℝ
23 20 21 22 sylancl ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℝ
24 max1 ⊢ 0 ∈ ℝ ∧ ℜ ⁡ B i k ∈ ℝ → 0 ≤ if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
25 21 20 24 sylancr ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → 0 ≤ if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
26 elrege0 ⊢ if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ 0 +∞ ↔ if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℝ ∧ 0 ≤ if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
27 23 25 26 sylanbrc ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ 0 +∞
28 itg2const ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ 0 +∞ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 0 = if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ⁢ vol ⁡ A
29 8 9 27 28 syl3anc ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 0 = if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ⁢ vol ⁡ A
30 7 29 eqtrid ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ⁢ vol ⁡ A
31 23 9 remulcld ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → if 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ⁢ vol ⁡ A ∈ ℝ
32 30 31 eqeltrd ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℝ
33 32 ralrimiva ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ → ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℝ
34 eqidd ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
35 eqidd ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ x ∈ A → ℜ ⁡ B i k = ℜ ⁡ B i k
36 simpl3 ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ ∧ x ∈ A → B ∈ ℂ
37 34 35 36 isibl2 ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ → x ∈ A ⟼ B ∈ 𝐿 1 ↔ x ∈ A ⟼ B ∈ MblFn ∧ ∀ k ∈ 0 … 3 ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℝ
38 4 33 37 mpbir2and ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ → x ∈ A ⟼ B ∈ 𝐿 1
39 1 38 eqeltrid ⊢ A ∈ dom ⁡ vol ∧ vol ⁡ A ∈ ℝ ∧ B ∈ ℂ → A × B ∈ 𝐿 1