Theorem 2cn 10379

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 10378	. 2 |- 2 e. RR
2	1	recni 9385	1 |- 2 e. CC

Syntax hints:   e. wcel 1755   CCcc 9267   2c2 10358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-resscn 9326  ax-1cn 9327  ax-icn 9328  ax-addcl 9329  ax-addrcl 9330  ax-mulcl 9331  ax-mulrcl 9332  ax-i2m1 9337  ax-1ne0 9338  ax-rrecex 9341  ax-cnre 9342

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-2 10367

This theorem is referenced by:  2ex  10380  2cnd  10381  2m1e1  10423  3m1e2  10425  2p2e4  10426  times2  10428  2div2e1  10431  1p2e3  10433  3p3e6  10442  4p3e7  10444  5p3e8  10447  6p3e9  10451  7p3e10  10454  2t1e2  10457  2t2e4  10458  3t3e9  10461  2t0e0  10464  4d2e2  10465  2cnne0  10523  halfcn  10528  1mhlfehlf  10531  8th4div3  10532  halfpm6th  10533  2mulicn  10535  2muline0  10536  halfcl  10537  half0  10539  2halves  10540  halfaddsub  10545  zneo  10711  nneo  10712  zeo  10714  4t4e16  10815  6t3e18  10820  7t7e49  10829  8t5e40  10833  9t9e81  10844  decbin0  10845  decbin2  10846  fz0tp  11497  fztpval  11501  fzo0to3tp  11598  expubnd  11907  sq2  11945  cu2  11947  subsq2  11957  binom2sub  11966  binom3  11968  zesq  11970  fac2  12040  fac3  12041  faclbnd2  12050  faclbnd4lem1  12052  faclbnd4lem3  12054  faclbnd4lem4  12055  faclbnd5  12057  bcn2  12078  swrd2lsw  12535  crre  12586  addcj  12620  imval2  12623  sqrlem7  12721  absmax  12800  rddif  12811  sqreulem  12830  amgm2  12840  abs3lemi  12880  iseraltlem2  13143  ackbijnn  13273  climcndslem1  13294  climcndslem2  13295  arisum  13304  arisum2  13305  geo2sum2  13316  geo2lim  13317  geoihalfsum  13324  efcllem  13345  ege2le3  13357  efgt0  13369  tanval2  13399  tanval3  13400  efi4p  13403  efival  13418  sinadd  13430  cosadd  13431  sinmul  13438  cos2tsin  13445  ef01bndlem  13450  cos01bnd  13452  cos1bnd  13453  cos2bnd  13454  cos01gt0  13457  sin02gt0  13458  sin4lt0  13461  znnenlem  13476  sqr2irrlem  13512  odd2np1lem  13573  odd2np1  13574  bits0  13606  bitsfzolem  13612  0bits  13617  bitsinv1  13620  sadcadd  13636  smumullem  13670  opoe  13860  omoe  13861  opeo  13862  omeo  13863  pythagtriplem1  13865  pythagtriplem12  13875  pythagtriplem14  13877  pythagtriplem15  13878  pythagtriplem16  13879  pythagtriplem17  13880  iserodd  13884  prmreclem5  13963  prmreclem6  13964  4sqlem11  13998  4sqlem12  13999  dec5dvds  14075  dec2nprm  14078  decexp2  14086  2exp6  14097  2exp8  14098  2exp16  14099  7prm  14120  11prm  14124  13prm  14125  37prm  14130  43prm  14131  83prm  14132  139prm  14133  163prm  14134  317prm  14135  631prm  14136  1259lem1  14137  1259lem2  14138  1259lem3  14139  1259lem4  14140  1259lem5  14141  1259prm  14142  2503lem1  14143  2503lem2  14144  2503lem3  14145  4001lem1  14147  4001lem2  14148  4001lem3  14149  4001lem4  14150  4001prm  14151  psgnunilem2  15980  efgtlen  16202  efgredleme  16219  frgpnabllem1  16330  lt6abl  16350  htpycc  20393  pcoval2  20429  pcocn  20430  pcohtpylem  20432  pcopt  20435  pcopt2  20436  pcoass  20437  pcorevlem  20439  csbren  20739  minveclem2  20754  ovolunlem1a  20820  ovolunlem1  20821  vitalilem4  20932  mbfi1fseqlem5  21038  dvmptre  21284  dvsincos  21294  aaliou3lem2  21693  aaliou3lem3  21694  aaliou3lem8  21695  coscn  21794  sinhalfpilem  21809  cospi  21818  ef2pi  21823  ef2kpi  21824  efper  21825  sinperlem  21826  sin2kpi  21829  cos2kpi  21830  sin2pim  21831  cos2pim  21832  sinhalfpip  21838  sinhalfpim  21839  coshalfpip  21840  coshalfpim  21841  sincosq3sgn  21846  sincosq4sgn  21847  tangtx  21851  sinq12gt0  21853  sincosq1eq  21858  sincos4thpi  21859  sincos6thpi  21861  sincos3rdpi  21862  pige3  21863  abssinper  21864  coskpi  21866  sineq0  21867  coseq1  21868  efeq1  21869  efif1olem4  21885  eflogeq  21934  tanarg  21952  cxpsqrlem  22031  cxpsqr  22032  logsqr  22033  root1eq1  22077  cxpeq  22079  ang180lem2  22090  ang180lem3  22091  quad2  22118  1cubrlem  22120  1cubr  22121  dcubic2  22123  dcubic1  22124  dcubic  22125  mcubic  22126  cubic2  22127  cubic  22128  dquartlem1  22130  dquartlem2  22131  dquart  22132  quart1lem  22134  quart1  22135  quartlem1  22136  quartlem2  22137  quartlem3  22138  quart  22140  sinasin  22168  asinsin  22171  atancj  22189  efiatan  22191  efiatan2  22196  2efiatan  22197  tanatan  22198  atantan  22202  atanbndlem  22204  atans2  22210  dvatan  22214  atantayl2  22217  leibpilem1  22219  leibpilem2  22220  log2cnv  22223  log2tlbnd  22224  log2ublem2  22226  log2ublem3  22227  log2ub  22228  birthday  22232  basellem1  22302  basellem3  22304  basellem8  22309  basellem9  22310  cht3  22395  1sgm2ppw  22423  ppiub  22427  chtublem  22434  chtub  22435  perfect1  22451  perfectlem1  22452  perfectlem2  22453  perfect  22454  bcmax  22501  bcp1ctr  22502  bclbnd  22503  bpos1lem  22505  bpos1  22506  bposlem1  22507  bposlem2  22508  bposlem4  22510  bposlem5  22511  bposlem6  22512  bposlem8  22514  bposlem9  22515  lgsdir2lem2  22547  lgsquadlem1  22577  lgsquadlem2  22578  lgsquad2lem2  22582  m1lgs  22585  rplogsumlem1  22617  dchrisum0fno1  22644  dchrisum0lem1  22649  dchrisum0lem2  22651  logdivsum  22666  mulog2sumlem3  22669  log2sumbnd  22677  selberglem1  22678  selberglem2  22679  selberg2  22684  selberg4lem1  22693  selberg3r  22702  pntpbnd1a  22718  pntpbnd2  22720  pntibndlem2  22724  pntlemk  22739  ax5seglem7  23003  axlowdimlem13  23022  usgraexvlem  23135  wlkdvspthlem  23328  ex-fl  23476  ipidsq  23930  cncph  24041  ip0i  24047  ip1ilem  24048  ipdirilem  24051  minvecolem2  24098  hvsubcan2i  24288  norm-ii-i  24361  norm3lem  24373  normpar2i  24380  polid2i  24381  hhph  24402  mayete3i  24953  mayete3iOLD  24954  nmcexi  25252  opsqrlem6  25371  addltmulALT  25672  oddpwdc  26584  fib5  26635  ballotlem2  26718  ballotth  26767  zetacvg  26848  problem4  27148  problem5  27149  4bc2eq6  27237  halfthird  27238  bpoly2  28046  bpoly3  28047  bpoly4  28048  fsumcube  28049  sin2h  28263  cos2h  28264  tan2h  28265  mblfinlem1  28269  mblfinlem2  28270  mblfinlem3  28271  itg2addnclem3  28286  dvasin  28321  areacirc  28330  heiborlem6  28556  rmxluc  29119  rmyluc  29120  jm2.17a  29145  jm2.18  29179  jm2.23  29187  jm3.1lem1  29208  proot1ex  29411  areaquad  29434  lhe4.4ex1a  29445  stoweidlem26  29664  wallispilem4  29706  wallispi  29708  wallispi2lem1  29709  wallispi2lem2  29710  wallispi2  29711  stirlinglem8  29719  stirlinglem11  29722  clwlkisclwwlklem2a4  30289  numclwwlkovf2ex  30522  2t6m3t4e0  30581  linevalexample  30635  zlmodzxzequap  30747  sinhpcosh  30781  sineq0ALT  31372