Theorem 2cn 9325

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 9324	. 2 |- 2 e. RR
2	1	recni 8302	1 |- 2 e. CC

Syntax hints:   e. wcel 2205   CCcc 8141   2c2 9305

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-resscn 8235  ax-1re 8237  ax-addrcl 8240

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227  df-2 9313

This theorem is referenced by:  2ex  9326  2cnd  9327  2m1e1  9372  3m1e2  9374  2p2e4  9381  times2  9383  2div2e1  9387  1p2e3  9389  3p3e6  9397  4p3e7  9399  5p3e8  9402  6p3e9  9405  2t1e2  9408  2t2e4  9409  3t3e9  9412  2t0e0  9414  4d2e2  9415  2cnne0  9464  1mhlfehlf  9473  8th4div3  9474  halfpm6th  9475  2mulicn  9477  2muliap0  9479  halfcl  9481  half0  9483  2halves  9484  halfaddsub  9489  div4p1lem1div2  9509  3halfnz  9693  zneo  9697  nneoor  9698  zeo  9701  7p3e10  9801  4t4e16  9825  6t3e18  9831  7t7e49  9840  8t5e40  9844  9t9e81  9855  decbin0  9866  decbin2  9867  halfthird  9869  fztpval  10439  fz0tp  10478  fz0to4untppr  10480  fzo0to3tp  10586  2tnp1ge0ge0  10685  fldiv4lem1div2  10691  expubnd  10982  sq2  11021  sq4e2t8  11023  cu2  11024  subsq2  11033  binom2sub  11039  binom3  11043  zesq  11045  fac2  11118  fac3  11119  faclbnd2  11129  bcn2  11151  4bc2eq6  11162  crre  11567  addcj  11601  imval2  11604  resqrexlemover  11720  resqrexlemcalc1  11724  resqrexlemnm  11728  resqrexlemcvg  11729  amgm2  11828  arisum  12209  arisum2  12210  geo2sum2  12226  geo2lim  12227  geoihalfsum  12233  efcllemp  12369  ege2le3  12382  tanval2ap  12424  tanval3ap  12425  efi4p  12428  efival  12443  sinadd  12447  cosadd  12448  sinmul  12455  cosmul  12456  cos2tsin  12462  ef01bndlem  12467  sin01bnd  12468  cos01bnd  12469  cos1bnd  12470  cos2bnd  12471  cos01gt0  12474  sin02gt0  12475  sin4lt0  12478  cos12dec  12479  egt2lt3  12491  odd2np1lem  12583  odd2np1  12584  ltoddhalfle  12604  halfleoddlt  12605  opoe  12606  omoe  12607  opeo  12608  omeo  12609  nno  12617  nn0o  12618  flodddiv4  12647  bits0  12659  bitsfzolem  12665  0bits  12670  bitsinv1  12673  6gcd4e2  12716  3lcm2e6woprm  12808  6lcm4e12  12809  sqrt2irrlem  12883  oddpwdclemodd  12894  pythagtriplem1  12988  pythagtriplem12  12998  pythagtriplem14  13000  4sqlem11  13124  4sqlem12  13125  dec5dvds  13135  dec2nprm  13138  2exp5  13155  2exp6  13156  2exp7  13157  2exp8  13158  2exp11  13159  2exp16  13160  ballotfilem2  13172  ballotfilemth  13225  maxcncf  15606  mincncf  15607  coscn  15761  sinhalfpilem  15782  cospi  15791  ef2pi  15796  ef2kpi  15797  efper  15798  sinperlem  15799  sin2kpi  15802  cos2kpi  15803  sin2pim  15804  cos2pim  15805  ptolemy  15815  sincosq3sgn  15819  sincosq4sgn  15820  sinq12gt0  15821  cosq23lt0  15824  coseq00topi  15826  tangtx  15829  sincos4thpi  15831  sincos6thpi  15833  sincos3rdpi  15834  pigt3  15835  abssinper  15837  coskpi  15839  cosq34lt1  15841  logsqrt  15914  2logb9irrALT  15965  1sgm2ppw  15989  perfect1  15992  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgsdir2lem2  16028  gausslemma2dlem6  16066  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem2  16081  m1lgs  16084  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgsoddprmlem2  16105  2lgsoddprmlem3c  16108  2lgsoddprmlem3d  16109  clwwlknonex2  16560  ex-fl  16619  ex-ceil  16620  ex-exp  16621  ex-fac  16622