Theorem 2cn 8924

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 8923	. 2 |- 2 e. RR
2	1	recni 7907	1 |- 2 e. CC

Syntax hints:   e. wcel 2136   CCcc 7747   2c2 8904

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 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147  ax-resscn 7841  ax-1re 7843  ax-addrcl 7846

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3121  df-ss 3128  df-2 8912

This theorem is referenced by:  2ex  8925  2cnd  8926  2m1e1  8971  3m1e2  8973  2p2e4  8980  times2  8982  2div2e1  8985  1p2e3  8987  3p3e6  8995  4p3e7  8997  5p3e8  9000  6p3e9  9003  2t1e2  9006  2t2e4  9007  3t3e9  9010  2t0e0  9012  4d2e2  9013  2cnne0  9062  1mhlfehlf  9071  8th4div3  9072  halfpm6th  9073  2mulicn  9075  2muliap0  9077  halfcl  9079  half0  9081  2halves  9082  halfaddsub  9087  div4p1lem1div2  9106  3halfnz  9284  zneo  9288  nneoor  9289  zeo  9292  7p3e10  9392  4t4e16  9416  6t3e18  9422  7t7e49  9431  8t5e40  9435  9t9e81  9446  decbin0  9457  decbin2  9458  halfthird  9460  fztpval  10014  fz0tp  10053  fz0to4untppr  10055  fzo0to3tp  10150  2tnp1ge0ge0  10232  expubnd  10508  sq2  10546  sq4e2t8  10548  cu2  10549  subsq2  10558  binom2sub  10564  binom3  10568  zesq  10569  fac2  10640  fac3  10641  faclbnd2  10651  bcn2  10673  4bc2eq6  10683  crre  10795  addcj  10829  imval2  10832  resqrexlemover  10948  resqrexlemcalc1  10952  resqrexlemnm  10956  resqrexlemcvg  10957  amgm2  11056  arisum  11435  arisum2  11436  geo2sum2  11452  geo2lim  11453  geoihalfsum  11459  efcllemp  11595  ege2le3  11608  tanval2ap  11650  tanval3ap  11651  efi4p  11654  efival  11669  sinadd  11673  cosadd  11674  sinmul  11681  cosmul  11682  cos2tsin  11688  ef01bndlem  11693  sin01bnd  11694  cos01bnd  11695  cos1bnd  11696  cos2bnd  11697  cos01gt0  11699  sin02gt0  11700  sin4lt0  11703  cos12dec  11704  egt2lt3  11716  odd2np1lem  11805  odd2np1  11806  ltoddhalfle  11826  halfleoddlt  11827  opoe  11828  omoe  11829  opeo  11830  omeo  11831  nno  11839  nn0o  11840  flodddiv4  11867  6gcd4e2  11924  3lcm2e6woprm  12014  6lcm4e12  12015  sqrt2irrlem  12089  oddpwdclemodd  12100  pythagtriplem1  12193  pythagtriplem12  12203  pythagtriplem14  12205  coscn  13291  sinhalfpilem  13312  cospi  13321  ef2pi  13326  ef2kpi  13327  efper  13328  sinperlem  13329  sin2kpi  13332  cos2kpi  13333  sin2pim  13334  cos2pim  13335  ptolemy  13345  sincosq3sgn  13349  sincosq4sgn  13350  sinq12gt0  13351  cosq23lt0  13354  coseq00topi  13356  tangtx  13359  sincos4thpi  13361  sincos6thpi  13363  sincos3rdpi  13364  pigt3  13365  abssinper  13367  coskpi  13369  cosq34lt1  13371  logsqrt  13443  2logb9irrALT  13492  lgsdir2lem2  13530  ex-fl  13566  ex-ceil  13567  ex-exp  13568  ex-fac  13569