Metamath Proof Explorer


Theorem 5cn

Description: The number 5 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 5cn
|- 5 e. CC

Proof

Step Hyp Ref Expression
1 df-5
 |-  5 = ( 4 + 1 )
2 4cn
 |-  4 e. CC
3 ax-1cn
 |-  1 e. CC
4 2 3 addcli
 |-  ( 4 + 1 ) e. CC
5 1 4 eqeltri
 |-  5 e. CC