Metamath Proof Explorer

Theorem dvmptim

Description: Function-builder for derivative, imaginary part. (Contributed by Mario Carneiro, 1-Sep-2014)

Ref Expression
Hypotheses dvmptcj.a ⊢ φ ∧ x ∈ X → A ∈ ℂ
dvmptcj.b ⊢ φ ∧ x ∈ X → B ∈ V
dvmptcj.da ⊢ φ → dx ∈ X A d ℝ x = x ∈ X ⟼ B
Assertion dvmptim ⊢ φ → dx ∈ X ℑ ⁡ A d ℝ x = x ∈ X ⟼ ℑ ⁡ B

Proof

Step Hyp Ref Expression
1 dvmptcj.a ⊢ φ ∧ x ∈ X → A ∈ ℂ
2 dvmptcj.b ⊢ φ ∧ x ∈ X → B ∈ V
3 dvmptcj.da ⊢ φ → dx ∈ X A d ℝ x = x ∈ X ⟼ B
4 reelprrecn ⊢ ℝ ∈ ℝ ℂ
5 4 a1i ⊢ φ → ℝ ∈ ℝ ℂ
6 1 cjcld ⊢ φ ∧ x ∈ X → A ‾ ∈ ℂ
7 1 6 subcld ⊢ φ ∧ x ∈ X → A − A ‾ ∈ ℂ
8 5 1 2 3 dvmptcl ⊢ φ ∧ x ∈ X → B ∈ ℂ
9 8 cjcld ⊢ φ ∧ x ∈ X → B ‾ ∈ ℂ
10 8 9 subcld ⊢ φ ∧ x ∈ X → B − B ‾ ∈ ℂ
11 1 2 3 dvmptcj ⊢ φ → dx ∈ X A ‾ d ℝ x = x ∈ X ⟼ B ‾
12 5 1 2 3 6 9 11 dvmptsub ⊢ φ → dx ∈ X A − A ‾ d ℝ x = x ∈ X ⟼ B − B ‾
13 2mulicn ⊢ 2 ⁢ i ∈ ℂ
14 2muline0 ⊢ 2 ⁢ i ≠ 0
15 13 14 reccli ⊢ 1 2 ⁢ i ∈ ℂ
16 15 a1i ⊢ φ → 1 2 ⁢ i ∈ ℂ
17 5 7 10 12 16 dvmptcmul ⊢ φ → dx ∈ X 1 2 ⁢ i ⁢ A − A ‾ d ℝ x = x ∈ X ⟼ 1 2 ⁢ i ⁢ B − B ‾
18 imval2 ⊢ A ∈ ℂ → ℑ ⁡ A = A − A ‾ 2 ⁢ i
19 1 18 syl ⊢ φ ∧ x ∈ X → ℑ ⁡ A = A − A ‾ 2 ⁢ i
20 divrec2 ⊢ A − A ‾ ∈ ℂ ∧ 2 ⁢ i ∈ ℂ ∧ 2 ⁢ i ≠ 0 → A − A ‾ 2 ⁢ i = 1 2 ⁢ i ⁢ A − A ‾
21 13 14 20 mp3an23 ⊢ A − A ‾ ∈ ℂ → A − A ‾ 2 ⁢ i = 1 2 ⁢ i ⁢ A − A ‾
22 7 21 syl ⊢ φ ∧ x ∈ X → A − A ‾ 2 ⁢ i = 1 2 ⁢ i ⁢ A − A ‾
23 19 22 eqtrd ⊢ φ ∧ x ∈ X → ℑ ⁡ A = 1 2 ⁢ i ⁢ A − A ‾
24 23 mpteq2dva ⊢ φ → x ∈ X ⟼ ℑ ⁡ A = x ∈ X ⟼ 1 2 ⁢ i ⁢ A − A ‾
25 24 oveq2d ⊢ φ → dx ∈ X ℑ ⁡ A d ℝ x = dx ∈ X 1 2 ⁢ i ⁢ A − A ‾ d ℝ x
26 imval2 ⊢ B ∈ ℂ → ℑ ⁡ B = B − B ‾ 2 ⁢ i
27 8 26 syl ⊢ φ ∧ x ∈ X → ℑ ⁡ B = B − B ‾ 2 ⁢ i
28 divrec2 ⊢ B − B ‾ ∈ ℂ ∧ 2 ⁢ i ∈ ℂ ∧ 2 ⁢ i ≠ 0 → B − B ‾ 2 ⁢ i = 1 2 ⁢ i ⁢ B − B ‾
29 13 14 28 mp3an23 ⊢ B − B ‾ ∈ ℂ → B − B ‾ 2 ⁢ i = 1 2 ⁢ i ⁢ B − B ‾
30 10 29 syl ⊢ φ ∧ x ∈ X → B − B ‾ 2 ⁢ i = 1 2 ⁢ i ⁢ B − B ‾
31 27 30 eqtrd ⊢ φ ∧ x ∈ X → ℑ ⁡ B = 1 2 ⁢ i ⁢ B − B ‾
32 31 mpteq2dva ⊢ φ → x ∈ X ⟼ ℑ ⁡ B = x ∈ X ⟼ 1 2 ⁢ i ⁢ B − B ‾
33 17 25 32 3eqtr4d ⊢ φ → dx ∈ X ℑ ⁡ A d ℝ x = x ∈ X ⟼ ℑ ⁡ B