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

Theorem 2cn 9749
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 9748 . 2  |-  2  e.  RR
21recni 8782 1  |-  2  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   CCcc 8668   2c2 9728
This theorem is referenced by:  2p2e4  9774  times2  9776  3p3e6  9788  4p3e7  9790  5p3e8  9793  6p3e9  9797  7p3e10  9800  2t2e4  9803  3t3e9  9805  4d2e2  9808  1mhlfehlf  9866  8th4div3  9867  halfpm6th  9868  halfcl  9869  half0  9871  2halves  9872  halfaddsub  9877  addltmul  9879  zneo  10026  nneo  10027  zeo  10029  zeo2  10030  4t4e16  10129  6t3e18  10134  7t7e49  10143  8t5e40  10147  9t9e81  10158  decbin0  10159  decbin2  10160  fztpval  10776  flhalf  10885  expubnd  11093  sq2  11130  cu2  11132  subsq2  11142  binom2sub  11151  binom3  11153  zesq  11155  expmulnbnd  11164  discr  11169  fac2  11225  fac3  11226  faclbnd2  11235  faclbnd4lem1  11237  faclbnd4lem3  11239  faclbnd4lem4  11240  faclbnd5  11242  bcn2  11262  crre  11529  addcj  11563  imval2  11566  sqrlem7  11664  absmax  11743  rddif  11754  sqreulem  11773  amgm2  11783  abs3lemi  11823  iseraltlem2  12085  iseralt  12087  ackbijnn  12216  climcndslem1  12235  climcndslem2  12236  arisum  12245  arisum2  12246  trirecip  12248  geo2sum  12256  geo2sum2  12257  geo2lim  12258  geoihalfsum  12265  efcllem  12286  ege2le3  12298  efgt0  12310  sinf  12331  tanval2  12340  tanval3  12341  efi4p  12344  sinneg  12353  efival  12359  sinhval  12361  tanhlt1  12367  sinadd  12371  cosadd  12372  sinmul  12379  cosmul  12380  cos2tsin  12386  ef01bndlem  12391  sin01bnd  12392  cos01bnd  12393  cos1bnd  12394  cos2bnd  12395  cos01gt0  12398  sin02gt0  12399  sin4lt0  12402  znnenlem  12417  rpnnen2lem3  12422  rpnnen2lem11  12430  sqr2irrlem  12453  sqr2irr  12454  odd2np1lem  12513  odd2np1  12514  oddm1even  12515  oddp1even  12516  bits0  12546  bitsp1o  12551  bitsfzolem  12552  bitsfzo  12553  bitsmod  12554  0bits  12557  bitsinv1lem  12559  bitsinv1  12560  sadadd2lem2  12568  sadcadd  12576  bitsuz  12592  bitsshft  12593  smumullem  12610  3prm  12702  prmdiv  12780  opoe  12791  omoe  12792  opeo  12793  omeo  12794  pythagtriplem1  12796  pythagtriplem4  12799  pythagtriplem12  12806  pythagtriplem14  12808  pythagtriplem15  12809  pythagtriplem16  12810  pythagtriplem17  12811  iserodd  12815  prmreclem5  12894  prmreclem6  12895  4sqlem7  12918  4sqlem10  12921  4sqlem11  12929  4sqlem12  12930  4sqlem19  12937  dec5dvds  13006  dec2nprm  13009  decexp2  13017  2exp6  13028  2exp8  13029  2exp16  13030  2expltfac  13032  prmlem1a  13035  7prm  13039  11prm  13043  13prm  13044  prmlem2  13048  37prm  13049  43prm  13050  83prm  13051  139prm  13052  163prm  13053  317prm  13054  631prm  13055  1259lem1  13056  1259lem2  13057  1259lem3  13058  1259lem4  13059  1259lem5  13060  1259prm  13061  2503lem1  13062  2503lem2  13063  2503lem3  13064  4001lem1  13066  4001lem2  13067  4001lem3  13068  4001lem4  13069  4001prm  13070  efgtlen  14962  efgredlemg  14978  efgredleme  14979  frgpnabllem1  15088  lt6abl  15108  metnrmlem3  18292  iihalf1cn  18357  iihalf2cn  18359  htpycc  18405  pco0  18439  pco1  18440  pcoval2  18441  pcocn  18442  pcohtpylem  18444  pcopt  18447  pcopt2  18448  pcoass  18449  pcorevlem  18451  minveclem2  18717  ovolunlem1a  18782  ovolunlem1  18783  uniioombllem5  18869  uniioombl  18871  dyaddisjlem  18877  vitalilem4  18893  mbfi1fseqlem5  19001  mbfi1fseqlem6  19002  dvmptre  19245  dvmptim  19246  dvsincos  19255  lhop1  19288  aaliou3lem2  19650  aaliou3lem3  19651  aaliou3lem8  19652  sincn  19747  coscn  19748  pilem2  19755  sinhalfpilem  19761  cospi  19767  sin2pi  19770  cos2pi  19771  ef2pi  19772  ef2kpi  19773  efper  19774  sinperlem  19775  sin2kpi  19778  cos2kpi  19779  sin2pim  19780  cos2pim  19781  sinhalfpip  19787  sinhalfpim  19788  coshalfpip  19789  coshalfpim  19790  ptolemy  19791  sincosq3sgn  19795  sincosq4sgn  19796  tangtx  19800  sinq12gt0  19802  sincosq1eq  19807  sincos4thpi  19808  sincos6thpi  19810  sincos3rdpi  19811  pige3  19812  abssinper  19813  coskpi  19815  sineq0  19816  coseq1  19817  efeq1  19818  efif1olem4  19834  eflogeq  19882  cosargd  19889  tanarg  19897  cxpsqrlem  19976  cxpsqr  19977  logsqr  19978  dvsqr  20011  root1id  20021  root1eq1  20022  cxpeq  20024  ang180lem2  20035  ang180lem3  20036  pythag  20042  ssscongptld  20049  chordthmlem  20056  chordthmlem2  20057  chordthmlem4  20059  quad2  20062  1cubrlem  20064  1cubr  20065  dcubic1lem  20066  dcubic2  20067  dcubic1  20068  dcubic  20069  mcubic  20070  cubic2  20071  cubic  20072  dquartlem1  20074  dquartlem2  20075  dquart  20076  quart1lem  20078  quart1  20079  quartlem1  20080  quartlem2  20081  quartlem3  20082  quartlem4  20083  quart  20084  sinasin  20112  asinsin  20115  cosasin  20127  atancj  20133  efiatan  20135  efiatan2  20140  2efiatan  20141  tanatan  20142  cosatan  20144  atantan  20146  atanbndlem  20148  atan1  20151  atans2  20154  dvatan  20158  atantayl  20160  atantayl2  20161  atantayl3  20162  leibpilem1  20163  leibpilem2  20164  log2cnv  20167  log2tlbnd  20168  log2ublem2  20170  log2ublem3  20171  log2ub  20172  birthday  20176  cxp2limlem  20197  divsqrsumlem  20201  ftalem2  20238  basellem1  20245  basellem2  20246  basellem3  20247  basellem8  20252  basellem9  20253  ppiprm  20316  ppinprm  20317  chtprm  20318  chtnprm  20319  cht3  20338  1sgm2ppw  20366  ppiub  20370  chtublem  20377  chtub  20378  logfaclbnd  20388  perfect1  20394  perfectlem1  20395  perfectlem2  20396  perfect  20397  bcmax  20444  bcp1ctr  20445  bclbnd  20446  bpos1lem  20448  bpos1  20449  bposlem1  20450  bposlem2  20451  bposlem4  20453  bposlem5  20454  bposlem6  20455  bposlem8  20457  bposlem9  20458  lgslem1  20462  lgslem4  20465  lgsdir2lem2  20490  lgsqrlem2  20508  lgseisenlem1  20515  lgseisenlem2  20516  lgseisenlem3  20517  lgseisenlem4  20518  lgsquadlem1  20520  lgsquadlem2  20521  lgsquad2lem1  20524  lgsquad2lem2  20525  m1lgs  20528  chebbnd1lem1  20545  chebbnd1lem3  20547  chto1ub  20552  rplogsumlem1  20560  dchrisumlem2  20566  dchrisum0flblem2  20585  dchrisum0fno1  20587  dchrisum0lem1b  20591  dchrisum0lem1  20592  dchrisum0lem2  20594  logdivsum  20609  mulog2sumlem2  20611  mulog2sumlem3  20612  vmalogdivsum2  20614  log2sumbnd  20620  selberglem1  20621  selberglem2  20622  selberg2  20627  chpdifbndlem1  20629  selberg3lem1  20633  selberg3  20635  selberg4lem1  20636  selberg4  20637  selberg3r  20645  selberg4r  20646  selberg34r  20647  pntrlog2bndlem3  20655  pntrlog2bndlem4  20656  pntrlog2bndlem5  20657  pntrlog2bndlem6  20659  pntpbnd1a  20661  pntpbnd2  20663  pntibndlem2  20667  pntlemg  20674  pntlemh  20675  pntlemk  20682  pntlemo  20683  ostth2lem1  20694  1kp2ke3k  20741  ex-fl  20742  ipidsq  21211  cncph  21322  ip0i  21328  ip1ilem  21329  ipdirilem  21332  minvecolem2  21379  hvsubcan2i  21568  norm-ii-i  21641  norm3lem  21653  normpar2i  21660  polid2i  21661  hhph  21682  mayete3i  22250  mayete3iOLD  22251  nmcexi  22531  opsqrlem6  22650  cdj3lem1  22939  addltmulALT  22951  ballotlem2  22973  ballotth  23022  zetacvg  23026  subfacp1lem1  23047  subfacp1lem5  23052  eupath  23242  konigsberg  23248  4bc2eq6  23435  halfthird  23436  ax5seglem7  23903  axlowdimlem13  23922  axlowdimlem16  23925  axlowdim  23929  bpolydiflem  24129  bpoly2  24132  bpoly3  24133  bpoly4  24134  fsumcube  24135  3timesi  24510  2eq3m1  24511  cntrset  24934  mslb1  24939  2wsms  24940  csbrn  25794  trirn  25795  isbnd2  25839  heiborlem6  25872  rabren3dioph  26230  rmxluc  26353  rmyluc  26354  rmyluc2  26355  rmydbl  26357  jm2.17a  26379  jm2.18  26413  jm2.22  26420  jm2.23  26421  jm2.25  26424  jm2.27c  26432  jm3.1lem1  26442  jm3.1lem2  26443  psgnunilem2  26750  proot1ex  26852  lhe4.4ex1a  26878  refsum2cnlem1  27041  stoweidlem1  27050  stoweidlem13  27062  stoweidlem14  27063  stoweidlem24  27073  stoweidlem26  27075  stoweidlem62  27111  sinhpcosh  27222  2m1e1  27274
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 8727  ax-1cn 8728  ax-icn 8729  ax-addcl 8730  ax-addrcl 8731  ax-mulcl 8732  ax-mulrcl 8733  ax-i2m1 8738  ax-1ne0 8739  ax-rrecex 8742  ax-cnre 8743
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 2520  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-xp 4640  df-cnv 4642  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fv 4654  df-ov 5760  df-2 9737
  Copyright terms: Public domain W3C validator