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 AA

Proof

Step Hyp Ref Expression
1 cjf *:
2 1 ffvelcdmi AA