Metamath Proof Explorer


Theorem 6cn

Description: The number 6 is a complex number. (Contributed by David A. Wheeler, 8-Dec-2018) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022)

Ref Expression
Assertion 6cn 6

Proof

Step Hyp Ref Expression
1 df-6 6 = 5 + 1
2 5cn 5
3 ax-1cn 1
4 2 3 addcli 5 + 1
5 1 4 eqeltri 6