Metamath Proof Explorer


Theorem cjcl

Description: The conjugate of a complex number is a complex number (closure law). (Contributed by NM, 10-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

Ref Expression
Assertion cjcl A A

Proof

Step Hyp Ref Expression
1 cjf * :
2 1 ffvelrni A A