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

Metamath Proof Explorer

Theorem re0cj

Description: The conjugate of a pure imaginary number is its negative. (Contributed by Thierry Arnoux, 25-Jun-2025)

Ref Expression
Hypotheses re0cj.1 ⊢ φ → A ∈ ℂ
re0cj.2 ⊢ φ → ℜ ⁡ A = 0
Assertion re0cj ⊢ φ → A ‾ = − A

Proof

Step Hyp Ref Expression
1 re0cj.1 ⊢ φ → A ∈ ℂ
2 re0cj.2 ⊢ φ → ℜ ⁡ A = 0
3 2 oveq1d ⊢ φ → ℜ ⁡ A − i ⁢ ℑ ⁡ A = 0 − i ⁢ ℑ ⁡ A
4 df-neg ⊢ − i ⁢ ℑ ⁡ A = 0 − i ⁢ ℑ ⁡ A
5 3 4 eqtr4di ⊢ φ → ℜ ⁡ A − i ⁢ ℑ ⁡ A = − i ⁢ ℑ ⁡ A
6 1 remimd ⊢ φ → A ‾ = ℜ ⁡ A − i ⁢ ℑ ⁡ A
7 1 replimd ⊢ φ → A = ℜ ⁡ A + i ⁢ ℑ ⁡ A
8 2 oveq1d ⊢ φ → ℜ ⁡ A + i ⁢ ℑ ⁡ A = 0 + i ⁢ ℑ ⁡ A
9 ax-icn ⊢ i ∈ ℂ
10 9 a1i ⊢ φ → i ∈ ℂ
11 1 imcld ⊢ φ → ℑ ⁡ A ∈ ℝ
12 11 recnd ⊢ φ → ℑ ⁡ A ∈ ℂ
13 10 12 mulcld ⊢ φ → i ⁢ ℑ ⁡ A ∈ ℂ
14 13 addlidd ⊢ φ → 0 + i ⁢ ℑ ⁡ A = i ⁢ ℑ ⁡ A
15 7 8 14 3eqtrd ⊢ φ → A = i ⁢ ℑ ⁡ A
16 15 negeqd ⊢ φ → − A = − i ⁢ ℑ ⁡ A
17 5 6 16 3eqtr4d ⊢ φ → A ‾ = − A