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

Metamath Proof Explorer

Theorem cjreim2

Description: The conjugate of the representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005) (Proof shortened by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion cjreim2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∗ ‘ ( 𝐴 − ( i · 𝐵 ) ) ) = ( 𝐴 + ( i · 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cjreim ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) = ( 𝐴 − ( i · 𝐵 ) ) )
2 1 fveq2d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∗ ‘ ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( ∗ ‘ ( 𝐴 − ( i · 𝐵 ) ) ) )
3 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℝ )
4 3 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ )
5 ax-icn ⊢ i ∈ ℂ
6 5 a1i ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → i ∈ ℂ )
7 simpr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
8 7 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℂ )
9 6 8 mulcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( i · 𝐵 ) ∈ ℂ )
10 4 9 addcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ )
11 cjcj ⊢ ( ( 𝐴 + ( i · 𝐵 ) ) ∈ ℂ → ( ∗ ‘ ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( 𝐴 + ( i · 𝐵 ) ) )
12 10 11 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∗ ‘ ( ∗ ‘ ( 𝐴 + ( i · 𝐵 ) ) ) ) = ( 𝐴 + ( i · 𝐵 ) ) )
13 2 12 eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ∗ ‘ ( 𝐴 − ( i · 𝐵 ) ) ) = ( 𝐴 + ( i · 𝐵 ) ) )