Theorem 2cn 8898

Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)

Assertion

Ref	Expression
2cn	|- 2 e. CC

Proof of Theorem 2cn

Step	Hyp	Ref	Expression
1		2re 8897	. 2 |- 2 e. RR
2	1	recni 7884	1 |- 2 e. CC

Syntax hints:   e. wcel 2128   CCcc 7724   2c2 8878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139  ax-resscn 7818  ax-1re 7820  ax-addrcl 7823

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115  df-2 8886

This theorem is referenced by:  2ex  8899  2cnd  8900  2m1e1  8945  3m1e2  8947  2p2e4  8954  times2  8956  2div2e1  8959  1p2e3  8961  3p3e6  8969  4p3e7  8971  5p3e8  8974  6p3e9  8977  2t1e2  8980  2t2e4  8981  3t3e9  8984  2t0e0  8986  4d2e2  8987  2cnne0  9036  1mhlfehlf  9045  8th4div3  9046  halfpm6th  9047  2mulicn  9049  2muliap0  9051  halfcl  9053  half0  9055  2halves  9056  halfaddsub  9061  div4p1lem1div2  9080  3halfnz  9255  zneo  9259  nneoor  9260  zeo  9263  7p3e10  9363  4t4e16  9387  6t3e18  9393  7t7e49  9402  8t5e40  9406  9t9e81  9417  decbin0  9428  decbin2  9429  halfthird  9431  fztpval  9978  fz0tp  10016  fzo0to3tp  10111  2tnp1ge0ge0  10193  expubnd  10469  sq2  10507  sq4e2t8  10509  cu2  10510  subsq2  10519  binom2sub  10524  binom3  10528  zesq  10529  fac2  10598  fac3  10599  faclbnd2  10609  bcn2  10631  4bc2eq6  10641  crre  10750  addcj  10784  imval2  10787  resqrexlemover  10903  resqrexlemcalc1  10907  resqrexlemnm  10911  resqrexlemcvg  10912  amgm2  11011  arisum  11388  arisum2  11389  geo2sum2  11405  geo2lim  11406  geoihalfsum  11412  efcllemp  11548  ege2le3  11561  tanval2ap  11603  tanval3ap  11604  efi4p  11607  efival  11622  sinadd  11626  cosadd  11627  sinmul  11634  cosmul  11635  cos2tsin  11641  ef01bndlem  11646  sin01bnd  11647  cos01bnd  11648  cos1bnd  11649  cos2bnd  11650  cos01gt0  11652  sin02gt0  11653  sin4lt0  11656  cos12dec  11657  egt2lt3  11669  odd2np1lem  11755  odd2np1  11756  ltoddhalfle  11776  halfleoddlt  11777  opoe  11778  omoe  11779  opeo  11780  omeo  11781  nno  11789  nn0o  11790  flodddiv4  11817  6gcd4e2  11870  3lcm2e6woprm  11954  6lcm4e12  11955  sqrt2irrlem  12026  oddpwdclemodd  12037  coscn  13062  sinhalfpilem  13083  cospi  13092  ef2pi  13097  ef2kpi  13098  efper  13099  sinperlem  13100  sin2kpi  13103  cos2kpi  13104  sin2pim  13105  cos2pim  13106  ptolemy  13116  sincosq3sgn  13120  sincosq4sgn  13121  sinq12gt0  13122  cosq23lt0  13125  coseq00topi  13127  tangtx  13130  sincos4thpi  13132  sincos6thpi  13134  sincos3rdpi  13135  pigt3  13136  abssinper  13138  coskpi  13140  cosq34lt1  13142  logsqrt  13214  2logb9irrALT  13262  ex-fl  13272  ex-ceil  13273  ex-exp  13274  ex-fac  13275