Theorem 3cn 9035

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

Syntax hints:   e. wcel 2160   CCcc 7849   3c3 9012

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-resscn 7943  ax-1re 7945  ax-addrcl 7948

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3154  df-ss 3161  df-2 9019  df-3 9020

This theorem is referenced by:  3ex  9036  3m1e2  9080  4m1e3  9081  3p2e5  9101  3p3e6  9102  4p4e8  9105  5p4e9  9108  3t1e3  9115  3t2e6  9116  3t3e9  9117  8th4div3  9179  halfpm6th  9180  6p4e10  9496  9t8e72  9552  halfthird  9567  fzo0to42pr  10262  sq3  10663  expnass  10672  fac3  10759  4bc3eq4  10800  ef01bndlem  11811  sin01bnd  11812  cos01bnd  11813  cos1bnd  11814  cos2bnd  11815  cos01gt0  11817  3dvdsdec  11917  3dvds2dec  11918  3lcm2e6woprm  12135  cosq23lt0  14792  tangtx  14797  sincos6thpi  14801  sincos3rdpi  14802  pigt3  14803  binom4  14935  lgsdir2lem1  14968  lgsdir2lem5  14972  2lgsoddprmlem3c  14996  2lgsoddprmlem3d  14997  ex-exp  15018  ex-dvds  15021  ex-gcd  15022