Theorem dvmptre

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

	Ref	Expression
Hypotheses	dvmptcj.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
	dvmptcj.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
	dvmptcj.da	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
Assertion	dvmptre	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ℜ ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℜ ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvmptcj.a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
2		dvmptcj.b	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
3		dvmptcj.da	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
4		reelprrecn	⊢ ℝ ∈ { ℝ , ℂ }
5	4	a1i	⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
6	1	cjcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
7	1 6	addcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℂ )
8	5 1 2 3	dvmptcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ ℂ )
9	8	cjcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ∗ ‘ 𝐵 ) ∈ ℂ )
10	8 9	addcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ∈ ℂ )
11	1 2 3	dvmptcj	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ∗ ‘ 𝐵 ) ) )
12	5 1 2 3 6 9 11	dvmptadd	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ) )
13		halfcn	⊢ ( 1 / 2 ) ∈ ℂ
14	13	a1i	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
15	5 7 10 12 14	dvmptcmul	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 2 ) · ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 2 ) · ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ) ) )
16		reval	⊢ ( 𝐴 ∈ ℂ → ( ℜ ‘ 𝐴 ) = ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) )
17	1 16	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ℜ ‘ 𝐴 ) = ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) )
18		2cn	⊢ 2 ∈ ℂ
19		2ne0	⊢ 2 ≠ 0
20		divrec2	⊢ ( ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) = ( ( 1 / 2 ) · ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ) )
21	18 19 20	mp3an23	⊢ ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ∈ ℂ → ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) = ( ( 1 / 2 ) · ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ) )
22	7 21	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐴 + ( ∗ ‘ 𝐴 ) ) / 2 ) = ( ( 1 / 2 ) · ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ) )
23	17 22	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ℜ ‘ 𝐴 ) = ( ( 1 / 2 ) · ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ) )
24	23	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ℜ ‘ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 2 ) · ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ) ) )
25	24	oveq2d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ℜ ‘ 𝐴 ) ) ) = ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 2 ) · ( 𝐴 + ( ∗ ‘ 𝐴 ) ) ) ) ) )
26		reval	⊢ ( 𝐵 ∈ ℂ → ( ℜ ‘ 𝐵 ) = ( ( 𝐵 + ( ∗ ‘ 𝐵 ) ) / 2 ) )
27	8 26	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ℜ ‘ 𝐵 ) = ( ( 𝐵 + ( ∗ ‘ 𝐵 ) ) / 2 ) )
28		divrec2	⊢ ( ( ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( 𝐵 + ( ∗ ‘ 𝐵 ) ) / 2 ) = ( ( 1 / 2 ) · ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ) )
29	18 19 28	mp3an23	⊢ ( ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ∈ ℂ → ( ( 𝐵 + ( ∗ ‘ 𝐵 ) ) / 2 ) = ( ( 1 / 2 ) · ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ) )
30	10 29	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐵 + ( ∗ ‘ 𝐵 ) ) / 2 ) = ( ( 1 / 2 ) · ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ) )
31	27 30	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ℜ ‘ 𝐵 ) = ( ( 1 / 2 ) · ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ) )
32	31	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ℜ ‘ 𝐵 ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 1 / 2 ) · ( 𝐵 + ( ∗ ‘ 𝐵 ) ) ) ) )
33	15 25 32	3eqtr4d	⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑋 ↦ ( ℜ ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℜ ‘ 𝐵 ) ) )