Theorem 6cn 9230

Description: The number 6 is complex. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
6cn	|- 6 e. CC

Proof of Theorem 6cn

Step	Hyp	Ref	Expression
1		6re 9229	. 2 |- 6 e. RR
2	1	recni 8196	1 |- 6 e. CC

Syntax hints:   e. wcel 2201   CCcc 8035   6c6 9203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2212  ax-resscn 8129  ax-1re 8131  ax-addrcl 8134

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-in 3205  df-ss 3212  df-2 9207  df-3 9208  df-4 9209  df-5 9210  df-6 9211

This theorem is referenced by:  7m1e6  9272  6p2e8  9298  6p3e9  9299  halfpm6th  9369  6p4e10  9687  6t2e12  9719  6t3e18  9720  6t5e30  9722  5recm6rec  9759  efi4p  12301  ef01bndlem  12340  cos01bnd  12342  3lcm2e6woprm  12681  6lcm4e12  12682  2exp8  13031  2exp11  13032  2exp16  13033  sincos6thpi  15595  sincos3rdpi  15596  2lgslem3d  15854  2lgsoddprmlem3d  15868  ex-exp  16380  ex-bc  16382  ex-gcd  16384