Database
REAL AND COMPLEX NUMBERS
Elementary real and complex functions
Real and imaginary parts; conjugate
cj0
Next ⟩
cji
Metamath Proof Explorer
Ascii
Unicode
Theorem
cj0
Description:
The conjugate of zero.
(Contributed by
NM
, 27-Jul-1999)
Ref
Expression
Assertion
cj0
⊢
0
‾
=
0
Proof
Step
Hyp
Ref
Expression
1
0re
⊢
0
∈
ℝ
2
cjre
⊢
0
∈
ℝ
→
0
‾
=
0
3
1
2
ax-mp
⊢
0
‾
=
0