This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem itgcl

Description: The integral of an integrable function is a complex number. This is Metamath 100 proof #86. (Contributed by Mario Carneiro, 29-Jun-2014)

Ref Expression
Hypotheses itgmpt.1 ⊢ φ ∧ x ∈ A → B ∈ V
itgcl.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
Assertion itgcl ⊢ φ → ∫ A B dx ∈ ℂ

Proof

Step Hyp Ref Expression
1 itgmpt.1 ⊢ φ ∧ x ∈ A → B ∈ V
2 itgcl.2 ⊢ φ → x ∈ A ⟼ B ∈ 𝐿 1
3 eqid ⊢ ℜ ⁡ B i k = ℜ ⁡ B i k
4 3 dfitg ⊢ ∫ A B dx = ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
5 fzfid ⊢ φ → 0 … 3 ∈ Fin
6 ax-icn ⊢ i ∈ ℂ
7 elfznn0 ⊢ k ∈ 0 … 3 → k ∈ ℕ 0
8 7 adantl ⊢ φ ∧ k ∈ 0 … 3 → k ∈ ℕ 0
9 expcl ⊢ i ∈ ℂ ∧ k ∈ ℕ 0 → i k ∈ ℂ
10 6 8 9 sylancr ⊢ φ ∧ k ∈ 0 … 3 → i k ∈ ℂ
11 elfzelz ⊢ k ∈ 0 … 3 → k ∈ ℤ
12 eqidd ⊢ φ → x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 = x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0
13 eqidd ⊢ φ ∧ x ∈ A → ℜ ⁡ B i k = ℜ ⁡ B i k
14 12 13 2 1 iblitg ⊢ φ ∧ k ∈ ℤ → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℝ
15 11 14 sylan2 ⊢ φ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℝ
16 15 recnd ⊢ φ ∧ k ∈ 0 … 3 → ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℂ
17 10 16 mulcld ⊢ φ ∧ k ∈ 0 … 3 → i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℂ
18 5 17 fsumcl ⊢ φ → ∑ k = 0 3 i k ⁢ ∫ 2 ⁡ x ∈ ℝ ⟼ if x ∈ A ∧ 0 ≤ ℜ ⁡ B i k ℜ ⁡ B i k 0 ∈ ℂ
19 4 18 eqeltrid ⊢ φ → ∫ A B dx ∈ ℂ