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

Theorem 2cn 9770
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 9769 . 2  |-  2  e.  RR
21recni 8803 1  |-  2  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   CCcc 8689   2c2 9749
This theorem is referenced by:  2p2e4  9795  times2  9797  3p3e6  9809  4p3e7  9811  5p3e8  9814  6p3e9  9818  7p3e10  9821  2t2e4  9824  3t3e9  9826  4d2e2  9829  1mhlfehlf  9887  8th4div3  9888  halfpm6th  9889  halfcl  9890  half0  9892  2halves  9893  halfaddsub  9898  addltmul  9900  zneo  10047  nneo  10048  zeo  10050  zeo2  10051  4t4e16  10150  6t3e18  10155  7t7e49  10164  8t5e40  10168  9t9e81  10179  decbin0  10180  decbin2  10181  fztpval  10797  flhalf  10906  expubnd  11114  sq2  11151  cu2  11153  subsq2  11163  binom2sub  11172  binom3  11174  zesq  11176  expmulnbnd  11185  discr  11190  fac2  11246  fac3  11247  faclbnd2  11256  faclbnd4lem1  11258  faclbnd4lem3  11260  faclbnd4lem4  11261  faclbnd5  11263  bcn2  11283  crre  11550  addcj  11584  imval2  11587  sqrlem7  11685  absmax  11764  rddif  11775  sqreulem  11794  amgm2  11804  abs3lemi  11844  iseraltlem2  12106  iseralt  12108  ackbijnn  12237  climcndslem1  12256  climcndslem2  12257  arisum  12266  arisum2  12267  trirecip  12269  geo2sum  12277  geo2sum2  12278  geo2lim  12279  geoihalfsum  12286  efcllem  12307  ege2le3  12319  efgt0  12331  sinf  12352  tanval2  12361  tanval3  12362  efi4p  12365  sinneg  12374  efival  12380  sinhval  12382  tanhlt1  12388  sinadd  12392  cosadd  12393  sinmul  12400  cosmul  12401  cos2tsin  12407  ef01bndlem  12412  sin01bnd  12413  cos01bnd  12414  cos1bnd  12415  cos2bnd  12416  cos01gt0  12419  sin02gt0  12420  sin4lt0  12423  znnenlem  12438  rpnnen2lem3  12443  rpnnen2lem11  12451  sqr2irrlem  12474  sqr2irr  12475  odd2np1lem  12534  odd2np1  12535  oddm1even  12536  oddp1even  12537  bits0  12567  bitsp1o  12572  bitsfzolem  12573  bitsfzo  12574  bitsmod  12575  0bits  12578  bitsinv1lem  12580  bitsinv1  12581  sadadd2lem2  12589  sadcadd  12597  bitsuz  12613  bitsshft  12614  smumullem  12631  3prm  12723  prmdiv  12801  opoe  12812  omoe  12813  opeo  12814  omeo  12815  pythagtriplem1  12817  pythagtriplem4  12820  pythagtriplem12  12827  pythagtriplem14  12829  pythagtriplem15  12830  pythagtriplem16  12831  pythagtriplem17  12832  iserodd  12836  prmreclem5  12915  prmreclem6  12916  4sqlem7  12939  4sqlem10  12942  4sqlem11  12950  4sqlem12  12951  4sqlem19  12958  dec5dvds  13027  dec2nprm  13030  decexp2  13038  2exp6  13049  2exp8  13050  2exp16  13051  2expltfac  13053  prmlem1a  13056  7prm  13060  11prm  13064  13prm  13065  prmlem2  13069  37prm  13070  43prm  13071  83prm  13072  139prm  13073  163prm  13074  317prm  13075  631prm  13076  1259lem1  13077  1259lem2  13078  1259lem3  13079  1259lem4  13080  1259lem5  13081  1259prm  13082  2503lem1  13083  2503lem2  13084  2503lem3  13085  4001lem1  13087  4001lem2  13088  4001lem3  13089  4001lem4  13090  4001prm  13091  efgtlen  14983  efgredlemg  14999  efgredleme  15000  frgpnabllem1  15109  lt6abl  15129  metnrmlem3  18313  iihalf1cn  18378  iihalf2cn  18380  htpycc  18426  pco0  18460  pco1  18461  pcoval2  18462  pcocn  18463  pcohtpylem  18465  pcopt  18468  pcopt2  18469  pcoass  18470  pcorevlem  18472  minveclem2  18738  ovolunlem1a  18803  ovolunlem1  18804  uniioombllem5  18890  uniioombl  18892  dyaddisjlem  18898  vitalilem4  18914  mbfi1fseqlem5  19022  mbfi1fseqlem6  19023  dvmptre  19266  dvmptim  19267  dvsincos  19276  lhop1  19309  aaliou3lem2  19671  aaliou3lem3  19672  aaliou3lem8  19673  sincn  19768  coscn  19769  pilem2  19776  sinhalfpilem  19782  cospi  19788  sin2pi  19791  cos2pi  19792  ef2pi  19793  ef2kpi  19794  efper  19795  sinperlem  19796  sin2kpi  19799  cos2kpi  19800  sin2pim  19801  cos2pim  19802  sinhalfpip  19808  sinhalfpim  19809  coshalfpip  19810  coshalfpim  19811  ptolemy  19812  sincosq3sgn  19816  sincosq4sgn  19817  tangtx  19821  sinq12gt0  19823  sincosq1eq  19828  sincos4thpi  19829  sincos6thpi  19831  sincos3rdpi  19832  pige3  19833  abssinper  19834  coskpi  19836  sineq0  19837  coseq1  19838  efeq1  19839  efif1olem4  19855  eflogeq  19903  cosargd  19910  tanarg  19918  cxpsqrlem  19997  cxpsqr  19998  logsqr  19999  dvsqr  20032  root1id  20042  root1eq1  20043  cxpeq  20045  ang180lem2  20056  ang180lem3  20057  pythag  20063  ssscongptld  20070  chordthmlem  20077  chordthmlem2  20078  chordthmlem4  20080  quad2  20083  1cubrlem  20085  1cubr  20086  dcubic1lem  20087  dcubic2  20088  dcubic1  20089  dcubic  20090  mcubic  20091  cubic2  20092  cubic  20093  dquartlem1  20095  dquartlem2  20096  dquart  20097  quart1lem  20099  quart1  20100  quartlem1  20101  quartlem2  20102  quartlem3  20103  quartlem4  20104  quart  20105  sinasin  20133  asinsin  20136  cosasin  20148  atancj  20154  efiatan  20156  efiatan2  20161  2efiatan  20162  tanatan  20163  cosatan  20165  atantan  20167  atanbndlem  20169  atan1  20172  atans2  20175  dvatan  20179  atantayl  20181  atantayl2  20182  atantayl3  20183  leibpilem1  20184  leibpilem2  20185  log2cnv  20188  log2tlbnd  20189  log2ublem2  20191  log2ublem3  20192  log2ub  20193  birthday  20197  cxp2limlem  20218  divsqrsumlem  20222  ftalem2  20259  basellem1  20266  basellem2  20267  basellem3  20268  basellem8  20273  basellem9  20274  ppiprm  20337  ppinprm  20338  chtprm  20339  chtnprm  20340  cht3  20359  1sgm2ppw  20387  ppiub  20391  chtublem  20398  chtub  20399  logfaclbnd  20409  perfect1  20415  perfectlem1  20416  perfectlem2  20417  perfect  20418  bcmax  20465  bcp1ctr  20466  bclbnd  20467  bpos1lem  20469  bpos1  20470  bposlem1  20471  bposlem2  20472  bposlem4  20474  bposlem5  20475  bposlem6  20476  bposlem8  20478  bposlem9  20479  lgslem1  20483  lgslem4  20486  lgsdir2lem2  20511  lgsqrlem2  20529  lgseisenlem1  20536  lgseisenlem2  20537  lgseisenlem3  20538  lgseisenlem4  20539  lgsquadlem1  20541  lgsquadlem2  20542  lgsquad2lem1  20545  lgsquad2lem2  20546  m1lgs  20549  chebbnd1lem1  20566  chebbnd1lem3  20568  chto1ub  20573  rplogsumlem1  20581  dchrisumlem2  20587  dchrisum0flblem2  20606  dchrisum0fno1  20608  dchrisum0lem1b  20612  dchrisum0lem1  20613  dchrisum0lem2  20615  logdivsum  20630  mulog2sumlem2  20632  mulog2sumlem3  20633  vmalogdivsum2  20635  log2sumbnd  20641  selberglem1  20642  selberglem2  20643  selberg2  20648  chpdifbndlem1  20650  selberg3lem1  20654  selberg3  20656  selberg4lem1  20657  selberg4  20658  selberg3r  20666  selberg4r  20667  selberg34r  20668  pntrlog2bndlem3  20676  pntrlog2bndlem4  20677  pntrlog2bndlem5  20678  pntrlog2bndlem6  20680  pntpbnd1a  20682  pntpbnd2  20684  pntibndlem2  20688  pntlemg  20695  pntlemh  20696  pntlemk  20703  pntlemo  20704  ostth2lem1  20715  1kp2ke3k  20762  ex-fl  20763  ipidsq  21232  cncph  21343  ip0i  21349  ip1ilem  21350  ipdirilem  21353  minvecolem2  21400  hvsubcan2i  21589  norm-ii-i  21662  norm3lem  21674  normpar2i  21681  polid2i  21682  hhph  21703  mayete3i  22271  mayete3iOLD  22272  nmcexi  22552  opsqrlem6  22671  cdj3lem1  22960  addltmulALT  22972  ballotlem2  22994  ballotth  23043  zetacvg  23047  subfacp1lem1  23068  subfacp1lem5  23073  eupath  23263  konigsberg  23269  4bc2eq6  23456  halfthird  23457  ax5seglem7  23924  axlowdimlem13  23943  axlowdimlem16  23946  axlowdim  23950  bpolydiflem  24150  bpoly2  24153  bpoly3  24154  bpoly4  24155  fsumcube  24156  3timesi  24531  2eq3m1  24532  cntrset  24955  mslb1  24960  2wsms  24961  csbrn  25815  trirn  25816  isbnd2  25860  heiborlem6  25893  rabren3dioph  26251  rmxluc  26374  rmyluc  26375  rmyluc2  26376  rmydbl  26378  jm2.17a  26400  jm2.18  26434  jm2.22  26441  jm2.23  26442  jm2.25  26445  jm2.27c  26453  jm3.1lem1  26463  jm3.1lem2  26464  psgnunilem2  26771  proot1ex  26873  lhe4.4ex1a  26899  refsum2cnlem1  27062  stoweidlem1  27071  stoweidlem13  27083  stoweidlem14  27084  stoweidlem24  27094  stoweidlem26  27096  stoweidlem62  27132  sinhpcosh  27243  2m1e1  27295
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-resscn 8748  ax-1cn 8749  ax-icn 8750  ax-addcl 8751  ax-addrcl 8752  ax-mulcl 8753  ax-mulrcl 8754  ax-i2m1 8759  ax-1ne0 8760  ax-rrecex 8763  ax-cnre 8764
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-xp 4661  df-cnv 4663  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fv 4675  df-ov 5781  df-2 9758
  Copyright terms: Public domain W3C validator