dvmptim

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

	Ref	Expression
Hypotheses	dvmptcj.a	$⊢ (φ \land x \in X) \to A \in ℂ$
	dvmptcj.b	$⊢ (φ \land x \in X) \to B \in V$
	dvmptcj.da	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{ℝ} x} = (x \in X ⟼ B)$
Assertion	dvmptim	$⊢ φ \to \frac{d (x \in X⟼ ℑ (A))}{d_{ℝ} x} = (x \in X ⟼ ℑ (B))$

Proof

Step	Hyp	Ref	Expression
1		dvmptcj.a	$⊢ (φ \land x \in X) \to A \in ℂ$
2		dvmptcj.b	$⊢ (φ \land x \in X) \to B \in V$
3		dvmptcj.da	$⊢ φ \to \frac{d (x \in X⟼ A)}{d_{ℝ} x} = (x \in X ⟼ B)$
4		reelprrecn	$⊢ ℝ \in \{ℝ, ℂ\}$
5	4	a1i	$⊢ φ \to ℝ \in \{ℝ, ℂ\}$
6	1	cjcld	$⊢ (φ \land x \in X) \to \overline{A} \in ℂ$
7	1 6	subcld	$⊢ (φ \land x \in X) \to A - \overline{A} \in ℂ$
8	5 1 2 3	dvmptcl	$⊢ (φ \land x \in X) \to B \in ℂ$
9	8	cjcld	$⊢ (φ \land x \in X) \to \overline{B} \in ℂ$
10	8 9	subcld	$⊢ (φ \land x \in X) \to B - \overline{B} \in ℂ$
11	1 2 3	dvmptcj	$⊢ φ \to \frac{d (x \in X⟼ \overline{A})}{d_{ℝ} x} = (x \in X ⟼ \overline{B})$
12	5 1 2 3 6 9 11	dvmptsub	$⊢ φ \to \frac{d (x \in X⟼ A - \overline{A})}{d_{ℝ} x} = (x \in X ⟼ B - \overline{B})$
13		2mulicn	$⊢ 2 i \in ℂ$
14		2muline0	$⊢ 2 i \neq 0$
15	13 14	reccli	$⊢ \frac{1}{2 i} \in ℂ$
16	15	a1i	$⊢ φ \to \frac{1}{2 i} \in ℂ$
17	5 7 10 12 16	dvmptcmul	$⊢ φ \to \frac{d (x \in X⟼ (\frac{1}{2 i}) (A - \overline{A}))}{d_{ℝ} x} = (x \in X ⟼ (\frac{1}{2 i}) (B - \overline{B}))$
18		imval2	$⊢ A \in ℂ \to ℑ (A) = \frac{A - \overline{A}}{2 i}$
19	1 18	syl	$⊢ (φ \land x \in X) \to ℑ (A) = \frac{A - \overline{A}}{2 i}$
20		divrec2	$⊢ (A - \overline{A} \in ℂ \land 2 i \in ℂ \land 2 i \neq 0) \to \frac{A - \overline{A}}{2 i} = (\frac{1}{2 i}) (A - \overline{A})$
21	13 14 20	mp3an23	$⊢ A - \overline{A} \in ℂ \to \frac{A - \overline{A}}{2 i} = (\frac{1}{2 i}) (A - \overline{A})$
22	7 21	syl	$⊢ (φ \land x \in X) \to \frac{A - \overline{A}}{2 i} = (\frac{1}{2 i}) (A - \overline{A})$
23	19 22	eqtrd	$⊢ (φ \land x \in X) \to ℑ (A) = (\frac{1}{2 i}) (A - \overline{A})$
24	23	mpteq2dva	$⊢ φ \to (x \in X ⟼ ℑ (A)) = (x \in X ⟼ (\frac{1}{2 i}) (A - \overline{A}))$
25	24	oveq2d	$⊢ φ \to \frac{d (x \in X⟼ ℑ (A))}{d_{ℝ} x} = \frac{d (x \in X⟼ (\frac{1}{2 i}) (A - \overline{A}))}{d_{ℝ} x}$
26		imval2	$⊢ B \in ℂ \to ℑ (B) = \frac{B - \overline{B}}{2 i}$
27	8 26	syl	$⊢ (φ \land x \in X) \to ℑ (B) = \frac{B - \overline{B}}{2 i}$
28		divrec2	$⊢ (B - \overline{B} \in ℂ \land 2 i \in ℂ \land 2 i \neq 0) \to \frac{B - \overline{B}}{2 i} = (\frac{1}{2 i}) (B - \overline{B})$
29	13 14 28	mp3an23	$⊢ B - \overline{B} \in ℂ \to \frac{B - \overline{B}}{2 i} = (\frac{1}{2 i}) (B - \overline{B})$
30	10 29	syl	$⊢ (φ \land x \in X) \to \frac{B - \overline{B}}{2 i} = (\frac{1}{2 i}) (B - \overline{B})$
31	27 30	eqtrd	$⊢ (φ \land x \in X) \to ℑ (B) = (\frac{1}{2 i}) (B - \overline{B})$
32	31	mpteq2dva	$⊢ φ \to (x \in X ⟼ ℑ (B)) = (x \in X ⟼ (\frac{1}{2 i}) (B - \overline{B}))$
33	17 25 32	3eqtr4d	$⊢ φ \to \frac{d (x \in X⟼ ℑ (A))}{d_{ℝ} x} = (x \in X ⟼ ℑ (B))$

Metamath Proof Explorer

Theorem dvmptim

Proof