Metamath Proof Explorer


Theorem 9cn

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

Proof

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