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 · 𝐵 ) ) )