Theorem 2cn 10647

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 10646	. 2 |- 2 e. RR
2	1	recni 9638	1 |- 2 e. CC

Syntax hints:   e. wcel 1842   CCcc 9520   2c2 10626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-resscn 9579  ax-1cn 9580  ax-icn 9581  ax-addcl 9582  ax-addrcl 9583  ax-mulcl 9584  ax-mulrcl 9585  ax-i2m1 9590  ax-1ne0 9591  ax-rrecex 9594  ax-cnre 9595

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2759  df-rex 2760  df-rab 2763  df-v 3061  df-dif 3417  df-un 3419  df-in 3421  df-ss 3428  df-nul 3739  df-if 3886  df-sn 3973  df-pr 3975  df-op 3979  df-uni 4192  df-br 4396  df-iota 5533  df-fv 5577  df-ov 6281  df-2 10635

This theorem is referenced by:  2ex  10648  2cnd  10649  2m1e1  10691  3m1e2  10693  2p2e4  10694  times2  10696  2div2e1  10699  1p2e3  10701  3p3e6  10710  4p3e7  10712  5p3e8  10715  6p3e9  10719  7p3e10  10722  2t1e2  10725  2t2e4  10726  3t3e9  10729  2t0e0  10732  4d2e2  10733  2cnne0  10791  halfcn  10796  1mhlfehlf  10799  8th4div3  10800  halfpm6th  10801  2mulicn  10803  2muline0  10804  halfcl  10805  half0  10807  2halves  10808  halfaddsub  10813  zneo  10986  nneo  10987  zeo  10989  4t4e16  11092  6t3e18  11097  7t7e49  11106  8t5e40  11110  9t9e81  11121  decbin0  11122  decbin2  11123  halfthird  11125  fztpval  11796  fz0tp  11832  fzo0to3tp  11937  expubnd  12271  sq2  12309  cu2  12311  subsq2  12321  binom2sub  12329  binom3  12331  zesq  12333  fac2  12403  fac3  12404  faclbnd2  12413  faclbnd4lem1  12415  faclbnd4lem3  12417  faclbnd4lem4  12418  faclbnd5  12420  bcn2  12441  4bc2eq6  12451  swrd2lsw  12946  crre  13096  addcj  13130  imval2  13133  sqrlem7  13231  absmax  13311  rddif  13322  sqreulem  13341  amgm2  13351  abs3lemi  13391  iseraltlem2  13654  ackbijnn  13791  climcndslem1  13812  climcndslem2  13813  arisum  13823  arisum2  13824  geo2sum2  13835  geo2lim  13836  geoihalfsum  13843  bpoly2  14002  bpoly3  14003  bpoly4  14004  fsumcube  14005  efcllem  14022  ege2le3  14034  efgt0  14047  tanval2  14077  tanval3  14078  efi4p  14081  efival  14096  sinadd  14108  cosadd  14109  sinmul  14116  cos2tsin  14123  ef01bndlem  14128  cos01bnd  14130  cos1bnd  14131  cos2bnd  14132  cos01gt0  14135  sin02gt0  14136  sin4lt0  14139  znnenlem  14154  sqr2irrlem  14190  odd2np1lem  14254  odd2np1  14255  bits0  14287  bitsfzolem  14293  0bits  14298  bitsinv1  14301  sadcadd  14317  smumullem  14351  opoe  14544  omoe  14545  opeo  14546  omeo  14547  pythagtriplem1  14549  pythagtriplem12  14559  pythagtriplem14  14561  pythagtriplem15  14562  pythagtriplem16  14563  pythagtriplem17  14564  iserodd  14568  prmreclem5  14647  prmreclem6  14648  4sqlem11  14682  4sqlem12  14683  dec5dvds  14759  dec2nprm  14762  decexp2  14770  2exp6  14781  2exp6OLD  14782  2exp8  14783  2exp16  14784  7prm  14805  11prm  14809  13prm  14810  37prm  14815  43prm  14816  83prm  14817  139prm  14818  163prm  14819  317prm  14820  631prm  14821  1259lem1  14822  1259lem2  14823  1259lem3  14824  1259lem4  14825  1259lem5  14826  1259prm  14827  2503lem1  14828  2503lem2  14829  2503lem3  14830  4001lem1  14832  4001lem2  14833  4001lem3  14834  4001lem4  14835  4001prm  14836  psgnunilem2  16844  efgtlen  17068  efgredleme  17085  frgpnabllem1  17201  lt6abl  17221  htpycc  21772  pcoval2  21808  pcocn  21809  pcohtpylem  21811  pcopt  21814  pcopt2  21815  pcoass  21816  pcorevlem  21818  csbren  22118  minveclem2  22133  ovolunlem1a  22199  ovolunlem1  22200  vitalilem4  22312  mbfi1fseqlem5  22418  dvmptre  22664  dvsincos  22674  aaliou3lem2  23031  aaliou3lem3  23032  aaliou3lem8  23033  coscn  23132  sinhalfpilem  23148  cospi  23157  ef2pi  23162  ef2kpi  23163  efper  23164  sinperlem  23165  sin2kpi  23168  cos2kpi  23169  sin2pim  23170  cos2pim  23171  sinhalfpip  23177  sinhalfpim  23178  coshalfpip  23179  coshalfpim  23180  sincosq3sgn  23185  sincosq4sgn  23186  tangtx  23190  sinq12gt0  23192  sincosq1eq  23197  sincos4thpi  23198  sincos6thpi  23200  sincos3rdpi  23201  pige3  23202  abssinper  23203  coskpi  23205  sineq0  23206  coseq1  23207  efeq1  23208  efif1olem4  23224  eflogeq  23281  tanarg  23298  cxpsqrtlem  23377  cxpsqrt  23378  logsqrt  23379  root1eq1  23425  cxpeq  23427  ang180lem2  23469  ang180lem3  23470  quad2  23495  1cubrlem  23497  1cubr  23498  dcubic2  23500  dcubic1  23501  dcubic  23502  mcubic  23503  cubic2  23504  cubic  23505  dquartlem1  23507  dquartlem2  23508  dquart  23509  quart1lem  23511  quart1  23512  quartlem1  23513  quartlem2  23514  quartlem3  23515  quart  23517  sinasin  23545  asinsin  23548  atancj  23566  efiatan  23568  efiatan2  23573  2efiatan  23574  tanatan  23575  atantan  23579  atanbndlem  23581  atans2  23587  dvatan  23591  atantayl2  23594  leibpilem1  23596  leibpilem2  23597  log2cnv  23600  log2tlbnd  23601  log2ublem2  23603  log2ublem3  23604  log2ub  23605  birthday  23610  zetacvg  23670  basellem1  23735  basellem3  23737  basellem8  23742  basellem9  23743  cht3  23828  1sgm2ppw  23856  ppiub  23860  chtublem  23867  chtub  23868  perfect1  23884  perfectlem1  23885  perfectlem2  23886  perfect  23887  bcmax  23934  bcp1ctr  23935  bclbnd  23936  bpos1lem  23938  bpos1  23939  bposlem1  23940  bposlem2  23941  bposlem4  23943  bposlem5  23944  bposlem6  23945  bposlem8  23947  bposlem9  23948  lgsdir2lem2  23980  lgsquadlem1  24010  lgsquadlem2  24011  lgsquad2lem2  24015  m1lgs  24018  rplogsumlem1  24050  dchrisum0fno1  24077  dchrisum0lem1  24082  dchrisum0lem2  24084  logdivsum  24099  mulog2sumlem3  24102  log2sumbnd  24110  selberglem1  24111  selberglem2  24112  selberg2  24117  selberg4lem1  24126  selberg3r  24135  pntpbnd1a  24151  pntpbnd2  24153  pntibndlem2  24157  pntlemk  24172  ax5seglem7  24655  axlowdimlem13  24674  usgraexvlem  24812  wlkdvspthlem  25026  clwlkisclwwlklem2a4  25201  numclwwlkovf2ex  25503  ex-fl  25585  ex-ind-dvds  25587  ipidsq  26037  cncph  26148  ip0i  26154  ip1ilem  26155  ipdirilem  26158  minvecolem2  26205  hvsubcan2i  26395  norm-ii-i  26468  norm3lem  26480  normpar2i  26487  polid2i  26488  hhph  26509  mayete3i  27060  nmcexi  27358  opsqrlem6  27477  addltmulALT  27778  omssubadd  28748  oddpwdc  28799  fib5  28850  ballotlem2  28933  ballotth  28982  problem4  29874  problem5  29875  quad3  29876  sin2h  31417  cos2h  31418  tan2h  31419  mblfinlem1  31423  mblfinlem2  31424  mblfinlem3  31425  itg2addnclem3  31441  dvasin  31474  areacirc  31483  heiborlem6  31594  rmxluc  35233  rmyluc  35234  jm2.17a  35259  jm2.18  35292  jm2.23  35300  jm3.1lem1  35321  proot1ex  35525  areaquad  35548  lhe4.4ex1a  36082  sineq0ALT  36768  coskpi2  37034  cosnegpi  37035  cosknegpi  37037  stoweidlem26  37176  wallispilem4  37218  wallispi  37220  wallispi2lem1  37221  stirlinglem8  37231  dirkerper  37246  dirkertrigeqlem3  37250  dirkertrigeq  37251  dirkeritg  37252  dirkercncflem1  37253  dirkercncflem2  37254  fourierdlem57  37314  fourierdlem58  37315  fourierdlem62  37319  fourierdlem76  37333  fourierdlem103  37360  fourierdlem104  37361  sqwvfourb  37380  fourierswlem  37381  bits0ALTV  37761  0evenALTV  37770  6even  37791  8even  37793  perfectALTVlem1  37796  perfectALTVlem2  37797  perfectALTV  37798  nnsum3primes4  37836  bgoldbtbndlem1  37853  3exp4mod41  37862  41prothprmlem1  37863  41prothprmlem2  37864  41prothprm  37865  0nodd  38127  0even  38248  2even  38250  2zrngamgm  38256  2t6m3t4e0  38448  linevalexample  38507  zlmodzxzequap  38611  3halfnz  38637  pw2m1lepw2m1  38638  nno  38648  nn0o  38649  nnlog2ge0lt1  38697  logbpw2m1  38698  nnpw2blen  38711  nnpw2pmod  38714  blen1  38715  blen2  38716  blennnt2  38720  nnolog2flm1  38721  0dig2nn0e  38743  0dig2nn0o  38744  nn0sumshdiglemA  38750  nn0sumshdiglemB  38751  nn0sumshdiglem1  38752  nn0sumshdiglem2  38753  sinhpcosh  38780