Theorem 6cn 9160

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

Syntax hints:   e. wcel 2180   CCcc 7965   6c6 9133

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 1473  ax-7 1474  ax-gen 1475  ax-ie1 1519  ax-ie2 1520  ax-8 1530  ax-11 1532  ax-4 1536  ax-17 1552  ax-i9 1556  ax-ial 1560  ax-i5r 1561  ax-ext 2191  ax-resscn 8059  ax-1re 8061  ax-addrcl 8064

This theorem depends on definitions:  df-bi 117  df-nf 1487  df-sb 1789  df-clab 2196  df-cleq 2202  df-clel 2205  df-in 3183  df-ss 3190  df-2 9137  df-3 9138  df-4 9139  df-5 9140  df-6 9141

This theorem is referenced by:  7m1e6  9202  6p2e8  9228  6p3e9  9229  halfpm6th  9299  6p4e10  9617  6t2e12  9649  6t3e18  9650  6t5e30  9652  5recm6rec  9689  efi4p  12194  ef01bndlem  12233  cos01bnd  12235  3lcm2e6woprm  12574  6lcm4e12  12575  2exp8  12924  2exp11  12925  2exp16  12926  sincos6thpi  15481  sincos3rdpi  15482  2lgslem3d  15740  2lgsoddprmlem3d  15754  ex-exp  16001  ex-bc  16003  ex-gcd  16005