Metamath Proof Explorer


Theorem 4cn

Description: The number 4 is a complex number. (Contributed by David A. Wheeler, 7-Jul-2016) Reduce dependencies on axioms. (Revised by Steven Nguyen, 4-Oct-2022)

Ref Expression
Assertion 4cn 4

Proof

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