Theorem 3cn 9065

Description: The number 3 is a complex number. (Contributed by FL, 17-Oct-2010.)

Assertion

Ref	Expression
3cn	|- 3 e. CC

Proof of Theorem 3cn

Step	Hyp	Ref	Expression
1		3re 9064	. 2 |- 3 e. RR
2	1	recni 8038	1 |- 3 e. CC

Syntax hints:   e. wcel 2167   CCcc 7877   3c3 9042

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-resscn 7971  ax-1re 7973  ax-addrcl 7976

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170  df-2 9049  df-3 9050

This theorem is referenced by:  3ex  9066  3m1e2  9110  4m1e3  9111  3p2e5  9132  3p3e6  9133  4p4e8  9136  5p4e9  9139  3t1e3  9146  3t2e6  9147  3t3e9  9148  8th4div3  9210  halfpm6th  9211  6p4e10  9528  9t8e72  9584  halfthird  9599  fzo0to42pr  10296  sq3  10728  expnass  10737  fac3  10824  4bc3eq4  10865  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos1bnd  11924  cos2bnd  11925  cos01gt0  11928  3dvdsdec  12030  3dvds2dec  12031  5ndvds3  12099  3lcm2e6woprm  12254  2exp6  12602  2exp16  12606  cosq23lt0  15069  tangtx  15074  sincos6thpi  15078  sincos3rdpi  15079  pigt3  15080  binom4  15215  lgsdir2lem1  15269  lgsdir2lem5  15273  2lgslem3b  15335  2lgslem3d  15337  2lgsoddprmlem3c  15350  2lgsoddprmlem3d  15351  ex-exp  15373  ex-dvds  15376  ex-gcd  15377