Theorem 6cn 8974

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 8973	. 2 |- 6 e. RR
2	1	recni 7944	1 |- 6 e. CC

Syntax hints:   e. wcel 2146   CCcc 7784   6c6 8947

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-resscn 7878  ax-1re 7880  ax-addrcl 7883

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140  df-2 8951  df-3 8952  df-4 8953  df-5 8954  df-6 8955

This theorem is referenced by:  7m1e6  9016  6p2e8  9041  6p3e9  9042  halfpm6th  9112  6p4e10  9428  6t2e12  9460  6t3e18  9461  6t5e30  9463  5recm6rec  9500  efi4p  11693  ef01bndlem  11732  cos01bnd  11734  3lcm2e6woprm  12053  6lcm4e12  12054  sincos6thpi  13834  sincos3rdpi  13835  ex-exp  14039  ex-bc  14041  ex-gcd  14043