MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2cn Unicode version

Theorem 2cn 10003
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
StepHypRef Expression
1 2re 10002 . 2  |-  2  e.  RR
21recni 9036 1  |-  2  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   CCcc 8922   2c2 9982
This theorem is referenced by:  2m1e1  10028  3m1e2  10029  3m1e2OLD  10030  2p2e4  10031  times2  10033  3p3e6  10045  4p3e7  10047  5p3e8  10050  6p3e9  10054  7p3e10  10057  2t2e4  10060  3t3e9  10062  4d2e2  10065  1mhlfehlf  10123  8th4div3  10124  halfpm6th  10125  halfcl  10126  half0  10128  2halves  10129  halfaddsub  10134  zneo  10285  nneo  10286  zeo  10288  zeo2  10289  4t4e16  10388  6t3e18  10393  7t7e49  10402  8t5e40  10406  9t9e81  10417  decbin0  10418  decbin2  10419  fztpval  11039  fzo0to3tp  11113  flhalf  11159  expubnd  11368  sq2  11405  cu2  11407  subsq2  11417  binom2sub  11426  binom3  11428  zesq  11430  expmulnbnd  11439  discr  11444  fac2  11500  fac3  11501  faclbnd2  11510  faclbnd4lem1  11512  faclbnd4lem3  11514  faclbnd4lem4  11515  faclbnd5  11517  bcn2  11538  crre  11847  addcj  11881  imval2  11884  sqrlem7  11982  absmax  12061  rddif  12072  sqreulem  12091  amgm2  12101  abs3lemi  12141  iseraltlem2  12404  iseralt  12406  ackbijnn  12535  climcndslem1  12557  climcndslem2  12558  arisum  12567  arisum2  12568  trirecip  12570  geo2sum  12578  geo2sum2  12579  geo2lim  12580  geoihalfsum  12587  efcllem  12608  ege2le3  12620  efgt0  12632  sinf  12653  tanval2  12662  tanval3  12663  efi4p  12666  sinneg  12675  efival  12681  sinhval  12683  tanhlt1  12689  sinadd  12693  cosadd  12694  sinmul  12701  cosmul  12702  cos2tsin  12708  ef01bndlem  12713  sin01bnd  12714  cos01bnd  12715  cos1bnd  12716  cos2bnd  12717  cos01gt0  12720  sin02gt0  12721  sin4lt0  12724  znnenlem  12739  rpnnen2lem3  12744  rpnnen2lem11  12752  sqr2irrlem  12775  sqr2irr  12776  odd2np1lem  12835  odd2np1  12836  oddm1even  12837  oddp1even  12838  bits0  12868  bitsp1o  12873  bitsfzolem  12874  bitsfzo  12875  bitsmod  12876  0bits  12879  bitsinv1lem  12881  bitsinv1  12882  sadadd2lem2  12890  sadcadd  12898  bitsuz  12914  bitsshft  12915  smumullem  12932  prmdiv  13102  opoe  13113  omoe  13114  opeo  13115  omeo  13116  pythagtriplem1  13118  pythagtriplem4  13121  pythagtriplem12  13128  pythagtriplem14  13130  pythagtriplem15  13131  pythagtriplem16  13132  pythagtriplem17  13133  iserodd  13137  prmreclem5  13216  prmreclem6  13217  4sqlem7  13240  4sqlem10  13243  4sqlem11  13251  4sqlem12  13252  4sqlem19  13259  dec5dvds  13328  dec2nprm  13331  decexp2  13339  2exp6  13350  2exp8  13351  2exp16  13352  2expltfac  13354  prmlem1a  13357  7prm  13361  11prm  13365  13prm  13366  prmlem2  13370  37prm  13371  43prm  13372  83prm  13373  139prm  13374  163prm  13375  317prm  13376  631prm  13377  1259lem1  13378  1259lem2  13379  1259lem3  13380  1259lem4  13381  1259lem5  13382  1259prm  13383  2503lem1  13384  2503lem2  13385  2503lem3  13386  4001lem1  13388  4001lem2  13389  4001lem3  13390  4001lem4  13391  4001prm  13392  efgtlen  15286  efgredlemg  15302  efgredleme  15303  frgpnabllem1  15412  lt6abl  15432  metnrmlem3  18763  iihalf1cn  18829  iihalf2cn  18831  htpycc  18877  pco0  18911  pco1  18912  pcoval2  18913  pcocn  18914  pcohtpylem  18916  pcopt  18919  pcopt2  18920  pcoass  18921  pcorevlem  18923  minveclem2  19195  ovolunlem1a  19260  ovolunlem1  19261  uniioombllem5  19347  uniioombl  19349  dyaddisjlem  19355  vitalilem4  19371  mbfi1fseqlem5  19479  mbfi1fseqlem6  19480  dvmptre  19723  dvmptim  19724  dvsincos  19733  lhop1  19766  aaliou3lem2  20128  aaliou3lem3  20129  aaliou3lem8  20130  sincn  20228  coscn  20229  pilem2  20236  sinhalfpilem  20242  cospi  20248  sin2pi  20251  cos2pi  20252  ef2pi  20253  ef2kpi  20254  efper  20255  sinperlem  20256  sin2kpi  20259  cos2kpi  20260  sin2pim  20261  cos2pim  20262  sinhalfpip  20268  sinhalfpim  20269  coshalfpip  20270  coshalfpim  20271  ptolemy  20272  sincosq3sgn  20276  sincosq4sgn  20277  tangtx  20281  sinq12gt0  20283  sincosq1eq  20288  sincos4thpi  20289  sincos6thpi  20291  sincos3rdpi  20292  pige3  20293  abssinper  20294  coskpi  20296  sineq0  20297  coseq1  20298  efeq1  20299  efif1olem4  20315  eflogeq  20364  cosargd  20371  tanarg  20382  cxpsqrlem  20461  cxpsqr  20462  logsqr  20463  dvsqr  20496  root1id  20506  root1eq1  20507  cxpeq  20509  ang180lem2  20520  ang180lem3  20521  pythag  20527  ssscongptld  20534  chordthmlem  20541  chordthmlem2  20542  chordthmlem4  20544  quad2  20547  1cubrlem  20549  1cubr  20550  dcubic1lem  20551  dcubic2  20552  dcubic1  20553  dcubic  20554  mcubic  20555  cubic2  20556  cubic  20557  dquartlem1  20559  dquartlem2  20560  dquart  20561  quart1lem  20563  quart1  20564  quartlem1  20565  quartlem2  20566  quartlem3  20567  quartlem4  20568  quart  20569  sinasin  20597  asinsin  20600  cosasin  20612  atancj  20618  efiatan  20620  efiatan2  20625  2efiatan  20626  tanatan  20627  cosatan  20629  atantan  20631  atanbndlem  20633  atan1  20636  atans2  20639  dvatan  20643  atantayl  20645  atantayl2  20646  atantayl3  20647  leibpilem1  20648  leibpilem2  20649  log2cnv  20652  log2tlbnd  20653  log2ublem2  20655  log2ublem3  20656  log2ub  20657  birthday  20661  cxp2limlem  20682  divsqrsumlem  20686  ftalem2  20724  basellem1  20731  basellem2  20732  basellem3  20733  basellem8  20738  basellem9  20739  cht3  20824  1sgm2ppw  20852  ppiub  20856  chtublem  20863  chtub  20864  logfaclbnd  20874  perfect1  20880  perfectlem1  20881  perfectlem2  20882  perfect  20883  bcmax  20930  bcp1ctr  20931  bclbnd  20932  bpos1lem  20934  bpos1  20935  bposlem1  20936  bposlem2  20937  bposlem4  20939  bposlem5  20940  bposlem6  20941  bposlem8  20943  bposlem9  20944  lgslem1  20948  lgsdir2lem2  20976  lgsqrlem2  20994  lgseisenlem1  21001  lgseisenlem2  21002  lgseisenlem3  21003  lgseisenlem4  21004  lgsquadlem1  21006  lgsquadlem2  21007  lgsquad2lem1  21010  lgsquad2lem2  21011  m1lgs  21014  chebbnd1lem1  21031  chebbnd1lem3  21033  chto1ub  21038  rplogsumlem1  21046  dchrisumlem2  21052  dchrisum0flblem2  21071  dchrisum0fno1  21073  dchrisum0lem1b  21077  dchrisum0lem1  21078  dchrisum0lem2  21080  logdivsum  21095  mulog2sumlem2  21097  mulog2sumlem3  21098  vmalogdivsum2  21100  log2sumbnd  21106  selberglem1  21107  selberglem2  21108  selberg2  21113  chpdifbndlem1  21115  selberg3lem1  21119  selberg3  21121  selberg4lem1  21122  selberg4  21123  selberg3r  21131  selberg4r  21132  selberg34r  21133  pntrlog2bndlem3  21141  pntrlog2bndlem4  21142  pntrlog2bndlem5  21143  pntrlog2bndlem6  21145  pntpbnd1a  21147  pntpbnd2  21149  pntibndlem2  21153  pntlemg  21160  pntlemh  21161  pntlemk  21168  pntlemo  21169  ostth2lem1  21180  usgraexvlem  21281  wlkntrllem3  21416  wlkdvspthlem  21456  eupath  21552  konigsberg  21558  1kp2ke3k  21603  ex-fl  21604  ipidsq  22058  cncph  22169  ip0i  22175  ip1ilem  22176  ipdirilem  22179  minvecolem2  22226  hvsubcan2i  22415  norm-ii-i  22488  norm3lem  22500  normpar2i  22507  polid2i  22508  hhph  22529  mayete3i  23079  mayete3iOLD  23080  nmcexi  23378  opsqrlem6  23497  cdj3lem1  23786  addltmulALT  23798  sqsscirc1  24111  dya2icoseg  24422  dya2iocucvr  24429  ballotlem2  24526  ballotth  24575  zetacvg  24579  lgamgulmlem4  24596  lgamucov  24602  subfacp1lem1  24645  subfacp1lem5  24650  4bc2eq6  24984  halfthird  24985  ax5seglem7  25589  axlowdimlem13  25608  bpolydiflem  25815  bpoly2  25818  bpoly3  25819  bpoly4  25820  fsumcube  25821  itg2addnclem  25958  itg2addnc  25960  dvreasin  25981  dvreacos  25982  areacirclem2  25983  areacirclem3  25984  areacirclem1  25986  areacirc  25989  csbrn  26148  trirn  26149  isbnd2  26184  heiborlem6  26217  rabren3dioph  26568  rmxluc  26691  rmyluc  26692  rmyluc2  26693  rmydbl  26695  jm2.17a  26717  jm2.18  26751  jm2.22  26758  jm2.23  26759  jm2.25  26762  jm2.27c  26770  jm3.1lem1  26780  jm3.1lem2  26781  psgnunilem2  27088  proot1ex  27190  lhe4.4ex1a  27216  refsum2cnlem1  27377  m1expeven  27394  itgsinexp  27418  stoweidlem1  27419  stoweidlem14  27432  stoweidlem24  27442  stoweidlem26  27444  stoweidlem62  27480  wallispilem4  27486  wallispilem5  27487  wallispi  27488  wallispi2lem1  27489  wallispi2lem2  27490  wallispi2  27491  stirlinglem1  27492  stirlinglem3  27494  stirlinglem4  27495  stirlinglem5  27496  stirlinglem6  27497  stirlinglem7  27498  stirlinglem8  27499  stirlinglem10  27501  stirlinglem11  27502  stirlinglem13  27504  stirlinglem14  27505  stirlinglem15  27506  sinhpcosh  27830
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-resscn 8981  ax-1cn 8982  ax-icn 8983  ax-addcl 8984  ax-addrcl 8985  ax-mulcl 8986  ax-mulrcl 8987  ax-i2m1 8992  ax-1ne0 8993  ax-rrecex 8996  ax-cnre 8997
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-rab 2659  df-v 2902  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-nul 3573  df-if 3684  df-sn 3764  df-pr 3765  df-op 3767  df-uni 3959  df-br 4155  df-iota 5359  df-fv 5403  df-ov 6024  df-2 9991
  Copyright terms: Public domain W3C validator