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

Theorem 2cn 9696
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 9695 . 2  |-  2  e.  RR
21recni 8729 1  |-  2  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   CCcc 8615   2c2 9675
This theorem is referenced by:  2p2e4  9721  times2  9723  3p3e6  9735  4p3e7  9737  5p3e8  9740  6p3e9  9744  7p3e10  9747  2t2e4  9750  3t3e9  9752  4d2e2  9755  1mhlfehlf  9813  8th4div3  9814  halfpm6th  9815  halfcl  9816  half0  9818  2halves  9819  halfaddsub  9824  addltmul  9826  zneo  9973  nneo  9974  zeo  9976  zeo2  9977  4t4e16  10076  6t3e18  10081  7t7e49  10090  8t5e40  10094  9t9e81  10105  decbin0  10106  decbin2  10107  fztpval  10723  flhalf  10832  expubnd  11040  sq2  11077  cu2  11079  subsq2  11089  binom2sub  11098  binom3  11100  zesq  11102  expmulnbnd  11111  discr  11116  fac2  11172  fac3  11173  faclbnd2  11182  faclbnd4lem1  11184  faclbnd4lem3  11186  faclbnd4lem4  11187  faclbnd5  11189  bcn2  11209  crre  11476  addcj  11510  imval2  11513  sqrlem7  11611  absmax  11690  rddif  11701  sqreulem  11720  amgm2  11730  abs3lemi  11770  iseraltlem2  12032  iseralt  12034  ackbijnn  12163  climcndslem1  12182  climcndslem2  12183  arisum  12192  arisum2  12193  trirecip  12195  geo2sum  12203  geo2sum2  12204  geo2lim  12205  geoihalfsum  12212  efcllem  12233  ege2le3  12245  efgt0  12257  sinf  12278  tanval2  12287  tanval3  12288  efi4p  12291  sinneg  12300  efival  12306  sinhval  12308  tanhlt1  12314  sinadd  12318  cosadd  12319  sinmul  12326  cosmul  12327  cos2tsin  12333  ef01bndlem  12338  sin01bnd  12339  cos01bnd  12340  cos1bnd  12341  cos2bnd  12342  cos01gt0  12345  sin02gt0  12346  sin4lt0  12349  znnenlem  12364  rpnnen2lem3  12369  rpnnen2lem11  12377  sqr2irrlem  12400  sqr2irr  12401  odd2np1lem  12460  odd2np1  12461  oddm1even  12462  oddp1even  12463  bits0  12493  bitsp1o  12498  bitsfzolem  12499  bitsfzo  12500  bitsmod  12501  0bits  12504  bitsinv1lem  12506  bitsinv1  12507  sadadd2lem2  12515  sadcadd  12523  bitsuz  12539  bitsshft  12540  smumullem  12557  3prm  12649  prmdiv  12727  opoe  12738  omoe  12739  opeo  12740  omeo  12741  pythagtriplem1  12743  pythagtriplem4  12746  pythagtriplem12  12753  pythagtriplem14  12755  pythagtriplem15  12756  pythagtriplem16  12757  pythagtriplem17  12758  iserodd  12762  prmreclem5  12841  prmreclem6  12842  4sqlem7  12865  4sqlem10  12868  4sqlem11  12876  4sqlem12  12877  4sqlem19  12884  dec5dvds  12953  dec2nprm  12956  decexp2  12964  2exp6  12975  2exp8  12976  2exp16  12977  2expltfac  12979  prmlem1a  12982  7prm  12986  11prm  12990  13prm  12991  prmlem2  12995  37prm  12996  43prm  12997  83prm  12998  139prm  12999  163prm  13000  317prm  13001  631prm  13002  1259lem1  13003  1259lem2  13004  1259lem3  13005  1259lem4  13006  1259lem5  13007  1259prm  13008  2503lem1  13009  2503lem2  13010  2503lem3  13011  4001lem1  13013  4001lem2  13014  4001lem3  13015  4001lem4  13016  4001prm  13017  efgtlen  14870  efgredlemg  14886  efgredleme  14887  frgpnabllem1  14996  lt6abl  15016  metnrmlem3  18197  iihalf1cn  18262  iihalf2cn  18264  htpycc  18310  pco0  18344  pco1  18345  pcoval2  18346  pcocn  18347  pcohtpylem  18349  pcopt  18352  pcopt2  18353  pcoass  18354  pcorevlem  18356  minveclem2  18622  ovolunlem1a  18687  ovolunlem1  18688  uniioombllem5  18774  uniioombl  18776  dyaddisjlem  18782  vitalilem4  18798  mbfi1fseqlem5  18906  mbfi1fseqlem6  18907  dvmptre  19150  dvmptim  19151  dvsincos  19160  lhop1  19193  aaliou3lem2  19555  aaliou3lem3  19556  aaliou3lem8  19557  sincn  19652  coscn  19653  pilem2  19660  sinhalfpilem  19666  cospi  19672  sin2pi  19675  cos2pi  19676  ef2pi  19677  ef2kpi  19678  efper  19679  sinperlem  19680  sin2kpi  19683  cos2kpi  19684  sin2pim  19685  cos2pim  19686  sinhalfpip  19692  sinhalfpim  19693  coshalfpip  19694  coshalfpim  19695  ptolemy  19696  sincosq3sgn  19700  sincosq4sgn  19701  tangtx  19705  sinq12gt0  19707  sincosq1eq  19712  sincos4thpi  19713  sincos6thpi  19715  sincos3rdpi  19716  pige3  19717  abssinper  19718  coskpi  19720  sineq0  19721  coseq1  19722  efeq1  19723  efif1olem4  19739  eflogeq  19787  cosargd  19794  tanarg  19802  ang180lem2  19852  ang180lem3  19853  pythag  19859  ssscongptld  19866  chordthmlem  19873  chordthmlem2  19874  chordthmlem4  19876  cxpsqrlem  19917  cxpsqr  19918  logsqr  19919  dvsqr  19952  root1id  19962  root1eq1  19963  cxpeq  19965  quad2  19967  1cubrlem  19969  1cubr  19970  dcubic1lem  19971  dcubic2  19972  dcubic1  19973  dcubic  19974  mcubic  19975  cubic2  19976  cubic  19977  dquartlem1  19979  dquartlem2  19980  dquart  19981  quart1lem  19983  quart1  19984  quartlem1  19985  quartlem2  19986  quartlem3  19987  quartlem4  19988  quart  19989  sinasin  20017  asinsin  20020  cosasin  20032  atancj  20038  efiatan  20040  efiatan2  20045  2efiatan  20046  tanatan  20047  cosatan  20049  atantan  20051  atanbndlem  20053  atan1  20056  atans2  20059  dvatan  20063  atantayl  20065  atantayl2  20066  atantayl3  20067  leibpilem1  20068  leibpilem2  20069  log2cnv  20072  log2tlbnd  20073  log2ublem2  20075  log2ublem3  20076  log2ub  20077  birthday  20081  cxp2limlem  20102  divsqrsumlem  20106  ftalem2  20143  basellem1  20150  basellem2  20151  basellem3  20152  basellem8  20157  basellem9  20158  ppiprm  20221  ppinprm  20222  chtprm  20223  chtnprm  20224  cht3  20243  1sgm2ppw  20271  ppiub  20275  chtublem  20282  chtub  20283  logfaclbnd  20293  perfect1  20299  perfectlem1  20300  perfectlem2  20301  perfect  20302  bcmax  20349  bcp1ctr  20350  bclbnd  20351  bpos1lem  20353  bpos1  20354  bposlem1  20355  bposlem2  20356  bposlem4  20358  bposlem5  20359  bposlem6  20360  bposlem8  20362  bposlem9  20363  lgslem1  20367  lgslem4  20370  lgsdir2lem2  20395  lgsqrlem2  20413  lgseisenlem1  20420  lgseisenlem2  20421  lgseisenlem3  20422  lgseisenlem4  20423  lgsquadlem1  20425  lgsquadlem2  20426  lgsquad2lem1  20429  lgsquad2lem2  20430  m1lgs  20433  chebbnd1lem1  20450  chebbnd1lem3  20452  chto1ub  20457  rplogsumlem1  20465  dchrisumlem2  20471  dchrisum0flblem2  20490  dchrisum0fno1  20492  dchrisum0lem1b  20496  dchrisum0lem1  20497  dchrisum0lem2  20499  logdivsum  20514  mulog2sumlem2  20516  mulog2sumlem3  20517  vmalogdivsum2  20519  log2sumbnd  20525  selberglem1  20526  selberglem2  20527  selberg2  20532  chpdifbndlem1  20534  selberg3lem1  20538  selberg3  20540  selberg4lem1  20541  selberg4  20542  selberg3r  20550  selberg4r  20551  selberg34r  20552  pntrlog2bndlem3  20560  pntrlog2bndlem4  20561  pntrlog2bndlem5  20562  pntrlog2bndlem6  20564  pntpbnd1a  20566  pntpbnd2  20568  pntibndlem2  20572  pntlemg  20579  pntlemh  20580  pntlemk  20587  pntlemo  20588  ostth2lem1  20599  1kp2ke3k  20646  ex-fl  20647  ipidsq  21116  cncph  21227  ip0i  21233  ip1ilem  21234  ipdirilem  21237  minvecolem2  21284  hvsubcan2i  21473  norm-ii-i  21546  norm3lem  21558  normpar2i  21565  polid2i  21566  hhph  21587  mayete3i  22155  mayete3iOLD  22156  nmcexi  22436  opsqrlem6  22555  cdj3lem1  22844  addltmulALT  22856  zetacvg  22860  subfacp1lem1  22881  subfacp1lem5  22886  eupath  23076  konigsberg  23082  4bc2eq6  23269  halfthird  23270  ax5seglem7  23737  axlowdimlem13  23756  axlowdimlem16  23759  axlowdim  23763  bpolydiflem  23963  bpoly2  23966  bpoly3  23967  bpoly4  23968  fsumcube  23969  3timesi  24344  2eq3m1  24345  cntrset  24768  mslb1  24773  2wsms  24774  csbrn  25628  trirn  25629  isbnd2  25673  heiborlem6  25706  rabren3dioph  26064  rmxluc  26187  rmyluc  26188  rmyluc2  26189  rmydbl  26191  jm2.17a  26213  jm2.18  26247  jm2.22  26254  jm2.23  26255  jm2.25  26258  jm2.27c  26266  jm3.1lem1  26276  jm3.1lem2  26277  psgnunilem2  26584  proot1ex  26686  lhe4.4ex1a  26712  sinhpcosh  26899  2m1e1  26951
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 1926  ax-ext 2234  ax-resscn 8674  ax-1cn 8675  ax-icn 8676  ax-addcl 8677  ax-addrcl 8678  ax-mulcl 8679  ax-mulrcl 8680  ax-i2m1 8685  ax-1ne0 8686  ax-rrecex 8689  ax-cnre 8690
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-ral 2513  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-xp 4594  df-cnv 4596  df-dm 4598  df-rn 4599  df-res 4600  df-ima 4601  df-fv 4608  df-ov 5713  df-2 9684
  Copyright terms: Public domain W3C validator