Theorem 3cn 9146

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 9145	. 2 |- 3 e. RR
2	1	recni 8119	1 |- 3 e. CC

Syntax hints:   e. wcel 2178   CCcc 7958   3c3 9123

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189  ax-resscn 8052  ax-1re 8054  ax-addrcl 8057

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187  df-2 9130  df-3 9131

This theorem is referenced by:  3ex  9147  3m1e2  9191  4m1e3  9192  3p2e5  9213  3p3e6  9214  4p4e8  9217  5p4e9  9220  3t1e3  9227  3t2e6  9228  3t3e9  9229  8th4div3  9291  halfpm6th  9292  6p4e10  9610  9t8e72  9666  halfthird  9681  fzo0to42pr  10386  sq3  10818  expnass  10827  fac3  10914  4bc3eq4  10955  ef01bndlem  12182  sin01bnd  12183  cos01bnd  12184  cos1bnd  12185  cos2bnd  12186  cos01gt0  12189  3dvdsdec  12291  3dvds2dec  12292  5ndvds3  12360  3lcm2e6woprm  12523  2exp6  12871  2exp16  12875  cosq23lt0  15420  tangtx  15425  sincos6thpi  15429  sincos3rdpi  15430  pigt3  15431  binom4  15566  lgsdir2lem1  15620  lgsdir2lem5  15624  2lgslem3b  15686  2lgslem3d  15688  2lgsoddprmlem3c  15701  2lgsoddprmlem3d  15702  ex-exp  15863  ex-dvds  15866  ex-gcd  15867