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 ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
re0cj.2 ⊢ ( 𝜑 → ( ℜ ‘ 𝐴 ) = 0 )
Assertion re0cj ( 𝜑 → ( ∗ ‘ 𝐴 ) = - 𝐴 )

Proof

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