dvmptre

Description: Function-builder for derivative, real 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	dvmptre	$⊢ φ \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	addcld	$⊢ (φ \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	addcld	$⊢ (φ \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	dvmptadd	$⊢ φ \to \frac{d (x \in X⟼ A + \overline{A})}{d_{ℝ} x} = (x \in X ⟼ B + \overline{B})$
13		halfcn	$⊢ \frac{1}{2} \in ℂ$
14	13	a1i	$⊢ φ \to \frac{1}{2} \in ℂ$
15	5 7 10 12 14	dvmptcmul	$⊢ φ \to \frac{d (x \in X⟼ (\frac{1}{2}) (A + \overline{A}))}{d_{ℝ} x} = (x \in X ⟼ (\frac{1}{2}) (B + \overline{B}))$
16		reval	$⊢ A \in ℂ \to ℜ (A) = \frac{A + \overline{A}}{2}$
17	1 16	syl	$⊢ (φ \land x \in X) \to ℜ (A) = \frac{A + \overline{A}}{2}$
18		2cn	$⊢ 2 \in ℂ$
19		2ne0	$⊢ 2 \neq 0$
20		divrec2	$⊢ (A + \overline{A} \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{A + \overline{A}}{2} = (\frac{1}{2}) (A + \overline{A})$
21	18 19 20	mp3an23	$⊢ A + \overline{A} \in ℂ \to \frac{A + \overline{A}}{2} = (\frac{1}{2}) (A + \overline{A})$
22	7 21	syl	$⊢ (φ \land x \in X) \to \frac{A + \overline{A}}{2} = (\frac{1}{2}) (A + \overline{A})$
23	17 22	eqtrd	$⊢ (φ \land x \in X) \to ℜ (A) = (\frac{1}{2}) (A + \overline{A})$
24	23	mpteq2dva	$⊢ φ \to (x \in X ⟼ ℜ (A)) = (x \in X ⟼ (\frac{1}{2}) (A + \overline{A}))$
25	24	oveq2d	$⊢ φ \to \frac{d (x \in X⟼ ℜ (A))}{d_{ℝ} x} = \frac{d (x \in X⟼ (\frac{1}{2}) (A + \overline{A}))}{d_{ℝ} x}$
26		reval	$⊢ B \in ℂ \to ℜ (B) = \frac{B + \overline{B}}{2}$
27	8 26	syl	$⊢ (φ \land x \in X) \to ℜ (B) = \frac{B + \overline{B}}{2}$
28		divrec2	$⊢ (B + \overline{B} \in ℂ \land 2 \in ℂ \land 2 \neq 0) \to \frac{B + \overline{B}}{2} = (\frac{1}{2}) (B + \overline{B})$
29	18 19 28	mp3an23	$⊢ B + \overline{B} \in ℂ \to \frac{B + \overline{B}}{2} = (\frac{1}{2}) (B + \overline{B})$
30	10 29	syl	$⊢ (φ \land x \in X) \to \frac{B + \overline{B}}{2} = (\frac{1}{2}) (B + \overline{B})$
31	27 30	eqtrd	$⊢ (φ \land x \in X) \to ℜ (B) = (\frac{1}{2}) (B + \overline{B})$
32	31	mpteq2dva	$⊢ φ \to (x \in X ⟼ ℜ (B)) = (x \in X ⟼ (\frac{1}{2}) (B + \overline{B}))$
33	15 25 32	3eqtr4d	$⊢ φ \to \frac{d (x \in X⟼ ℜ (A))}{d_{ℝ} x} = (x \in X ⟼ ℜ (B))$

Metamath Proof Explorer

Theorem dvmptre

Proof