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

Metamath Proof Explorer

Theorem cji

Description: The complex conjugate of the imaginary unit. (Contributed by NM, 26-Mar-2005)

Ref Expression
Assertion cji ⊢ i ‾ = − i

Proof

Step Hyp Ref Expression
1 rei ⊢ ℜ ⁡ i = 0
2 imi ⊢ ℑ ⁡ i = 1
3 2 oveq2i ⊢ i ⁢ ℑ ⁡ i = i ⋅ 1
4 ax-icn ⊢ i ∈ ℂ
5 4 mulridi ⊢ i ⋅ 1 = i
6 3 5 eqtri ⊢ i ⁢ ℑ ⁡ i = i
7 1 6 oveq12i ⊢ ℜ ⁡ i − i ⁢ ℑ ⁡ i = 0 − i
8 remim ⊢ i ∈ ℂ → i ‾ = ℜ ⁡ i − i ⁢ ℑ ⁡ i
9 4 8 ax-mp ⊢ i ‾ = ℜ ⁡ i − i ⁢ ℑ ⁡ i
10 df-neg ⊢ − i = 0 − i
11 7 9 10 3eqtr4i ⊢ i ‾ = − i