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

Metamath Proof Explorer

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 ( 𝑥 ∈ 𝑋 ↦ ( ℜ ‘ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ℜ ‘ 𝐵 ) ) )