Theorem 6cn 9340

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

Syntax hints:   e. wcel 2205   CCcc 8142   6c6 9313

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8236  ax-1re 8238  ax-addrcl 8241

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227  df-2 9317  df-3 9318  df-4 9319  df-5 9320  df-6 9321

This theorem is referenced by:  7m1e6  9382  6p2e8  9408  6p3e9  9409  halfpm6th  9479  6p4e10  9802  6t2e12  9834  6t3e18  9835  6t5e30  9837  5recm6rec  9874  efi4p  12433  ef01bndlem  12472  cos01bnd  12474  3lcm2e6woprm  12813  6lcm4e12  12814  2exp8  13163  2exp11  13164  2exp16  13165  sincos6thpi  15838  sincos3rdpi  15839  2lgslem3d  16100  2lgsoddprmlem3d  16114  ex-exp  16626  ex-bc  16628  ex-gcd  16630