Metamath Proof Explorer

Theorem cjreim

Description: The conjugate of a representation of a complex number in terms of real and imaginary parts. (Contributed by NM, 1-Jul-2005)

Ref Expression
Assertion cjreim ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B ‾ = A − i ⁢ B

Proof

Step Hyp Ref Expression
1 recn ⊢ A ∈ ℝ → A ∈ ℂ
2 ax-icn ⊢ i ∈ ℂ
3 recn ⊢ B ∈ ℝ → B ∈ ℂ
4 mulcl ⊢ i ∈ ℂ ∧ B ∈ ℂ → i ⁢ B ∈ ℂ
5 2 3 4 sylancr ⊢ B ∈ ℝ → i ⁢ B ∈ ℂ
6 cjadd ⊢ A ∈ ℂ ∧ i ⁢ B ∈ ℂ → A + i ⁢ B ‾ = A ‾ + i ⁢ B ‾
7 1 5 6 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B ‾ = A ‾ + i ⁢ B ‾
8 cjre ⊢ A ∈ ℝ → A ‾ = A
9 cjmul ⊢ i ∈ ℂ ∧ B ∈ ℂ → i ⁢ B ‾ = i ‾ ⁢ B ‾
10 2 3 9 sylancr ⊢ B ∈ ℝ → i ⁢ B ‾ = i ‾ ⁢ B ‾
11 cji ⊢ i ‾ = − i
12 11 a1i ⊢ B ∈ ℝ → i ‾ = − i
13 cjre ⊢ B ∈ ℝ → B ‾ = B
14 12 13 oveq12d ⊢ B ∈ ℝ → i ‾ ⁢ B ‾ = − i ⁢ B
15 mulneg1 ⊢ i ∈ ℂ ∧ B ∈ ℂ → − i ⁢ B = − i ⁢ B
16 2 3 15 sylancr ⊢ B ∈ ℝ → − i ⁢ B = − i ⁢ B
17 10 14 16 3eqtrd ⊢ B ∈ ℝ → i ⁢ B ‾ = − i ⁢ B
18 8 17 oveqan12d ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ‾ + i ⁢ B ‾ = A + − i ⁢ B
19 negsub ⊢ A ∈ ℂ ∧ i ⁢ B ∈ ℂ → A + − i ⁢ B = A − i ⁢ B
20 1 5 19 syl2an ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + − i ⁢ B = A − i ⁢ B
21 7 18 20 3eqtrd ⊢ A ∈ ℝ ∧ B ∈ ℝ → A + i ⁢ B ‾ = A − i ⁢ B