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

Theorem 2cn 10070
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 10069 . 2  |-  2  e.  RR
21recni 9102 1  |-  2  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   CCcc 8988   2c2 10049
This theorem is referenced by:  2m1e1  10095  3m1e2  10096  3m1e2OLD  10097  2p2e4  10098  times2  10100  3p3e6  10112  4p3e7  10114  5p3e8  10117  6p3e9  10121  7p3e10  10124  2t2e4  10127  3t3e9  10129  4d2e2  10132  1mhlfehlf  10190  8th4div3  10191  halfpm6th  10192  halfcl  10193  half0  10195  2halves  10196  halfaddsub  10201  zneo  10352  nneo  10353  zeo  10355  zeo2  10356  4t4e16  10455  6t3e18  10460  7t7e49  10469  8t5e40  10473  9t9e81  10484  decbin0  10485  decbin2  10486  fz0tp  11103  fztpval  11107  fzo0to3tp  11185  flhalf  11231  expubnd  11440  sq2  11477  cu2  11479  subsq2  11489  binom2sub  11498  binom3  11500  zesq  11502  expmulnbnd  11511  discr  11516  fac2  11572  fac3  11573  faclbnd2  11582  faclbnd4lem1  11584  faclbnd4lem3  11586  faclbnd4lem4  11587  faclbnd5  11589  bcn2  11610  crre  11919  addcj  11953  imval2  11956  sqrlem7  12054  absmax  12133  rddif  12144  sqreulem  12163  amgm2  12173  abs3lemi  12213  iseraltlem2  12476  iseralt  12478  ackbijnn  12607  climcndslem1  12629  climcndslem2  12630  arisum  12639  arisum2  12640  trirecip  12642  geo2sum  12650  geo2sum2  12651  geo2lim  12652  geoihalfsum  12659  efcllem  12680  ege2le3  12692  efgt0  12704  sinf  12725  tanval2  12734  tanval3  12735  efi4p  12738  sinneg  12747  efival  12753  sinhval  12755  tanhlt1  12761  sinadd  12765  cosadd  12766  sinmul  12773  cosmul  12774  cos2tsin  12780  ef01bndlem  12785  sin01bnd  12786  cos01bnd  12787  cos1bnd  12788  cos2bnd  12789  cos01gt0  12792  sin02gt0  12793  sin4lt0  12796  znnenlem  12811  rpnnen2lem3  12816  rpnnen2lem11  12824  sqr2irrlem  12847  sqr2irr  12848  odd2np1lem  12907  odd2np1  12908  oddm1even  12909  oddp1even  12910  bits0  12940  bitsp1o  12945  bitsfzolem  12946  bitsfzo  12947  bitsmod  12948  0bits  12951  bitsinv1lem  12953  bitsinv1  12954  sadadd2lem2  12962  sadcadd  12970  bitsuz  12986  bitsshft  12987  smumullem  13004  prmdiv  13174  opoe  13185  omoe  13186  opeo  13187  omeo  13188  pythagtriplem1  13190  pythagtriplem4  13193  pythagtriplem12  13200  pythagtriplem14  13202  pythagtriplem15  13203  pythagtriplem16  13204  pythagtriplem17  13205  iserodd  13209  prmreclem5  13288  prmreclem6  13289  4sqlem7  13312  4sqlem10  13315  4sqlem11  13323  4sqlem12  13324  4sqlem19  13331  dec5dvds  13400  dec2nprm  13403  decexp2  13411  2exp6  13422  2exp8  13423  2exp16  13424  2expltfac  13426  prmlem1a  13429  7prm  13433  11prm  13437  13prm  13438  prmlem2  13442  37prm  13443  43prm  13444  83prm  13445  139prm  13446  163prm  13447  317prm  13448  631prm  13449  1259lem1  13450  1259lem2  13451  1259lem3  13452  1259lem4  13453  1259lem5  13454  1259prm  13455  2503lem1  13456  2503lem2  13457  2503lem3  13458  4001lem1  13460  4001lem2  13461  4001lem3  13462  4001lem4  13463  4001prm  13464  efgtlen  15358  efgredlemg  15374  efgredleme  15375  frgpnabllem1  15484  lt6abl  15504  metnrmlem3  18891  iihalf1cn  18957  iihalf2cn  18959  htpycc  19005  pco0  19039  pco1  19040  pcoval2  19041  pcocn  19042  pcohtpylem  19044  pcopt  19047  pcopt2  19048  pcoass  19049  pcorevlem  19051  minveclem2  19327  ovolunlem1a  19392  ovolunlem1  19393  uniioombllem5  19479  uniioombl  19481  dyaddisjlem  19487  vitalilem4  19503  mbfi1fseqlem5  19611  mbfi1fseqlem6  19612  dvmptre  19855  dvmptim  19856  dvsincos  19865  lhop1  19898  aaliou3lem2  20260  aaliou3lem3  20261  aaliou3lem8  20262  sincn  20360  coscn  20361  pilem2  20368  sinhalfpilem  20374  cospi  20380  sin2pi  20383  cos2pi  20384  ef2pi  20385  ef2kpi  20386  efper  20387  sinperlem  20388  sin2kpi  20391  cos2kpi  20392  sin2pim  20393  cos2pim  20394  sinhalfpip  20400  sinhalfpim  20401  coshalfpip  20402  coshalfpim  20403  ptolemy  20404  sincosq3sgn  20408  sincosq4sgn  20409  tangtx  20413  sinq12gt0  20415  sincosq1eq  20420  sincos4thpi  20421  sincos6thpi  20423  sincos3rdpi  20424  pige3  20425  abssinper  20426  coskpi  20428  sineq0  20429  coseq1  20430  efeq1  20431  efif1olem4  20447  eflogeq  20496  cosargd  20503  tanarg  20514  cxpsqrlem  20593  cxpsqr  20594  logsqr  20595  dvsqr  20628  root1id  20638  root1eq1  20639  cxpeq  20641  ang180lem2  20652  ang180lem3  20653  pythag  20659  ssscongptld  20666  chordthmlem  20673  chordthmlem2  20674  chordthmlem4  20676  quad2  20679  1cubrlem  20681  1cubr  20682  dcubic1lem  20683  dcubic2  20684  dcubic1  20685  dcubic  20686  mcubic  20687  cubic2  20688  cubic  20689  dquartlem1  20691  dquartlem2  20692  dquart  20693  quart1lem  20695  quart1  20696  quartlem1  20697  quartlem2  20698  quartlem3  20699  quartlem4  20700  quart  20701  sinasin  20729  asinsin  20732  cosasin  20744  atancj  20750  efiatan  20752  efiatan2  20757  2efiatan  20758  tanatan  20759  cosatan  20761  atantan  20763  atanbndlem  20765  atan1  20768  atans2  20771  dvatan  20775  atantayl  20777  atantayl2  20778  atantayl3  20779  leibpilem1  20780  leibpilem2  20781  log2cnv  20784  log2tlbnd  20785  log2ublem2  20787  log2ublem3  20788  log2ub  20789  birthday  20793  cxp2limlem  20814  divsqrsumlem  20818  ftalem2  20856  basellem1  20863  basellem2  20864  basellem3  20865  basellem8  20870  basellem9  20871  cht3  20956  1sgm2ppw  20984  ppiub  20988  chtublem  20995  chtub  20996  logfaclbnd  21006  perfect1  21012  perfectlem1  21013  perfectlem2  21014  perfect  21015  bcmax  21062  bcp1ctr  21063  bclbnd  21064  bpos1lem  21066  bpos1  21067  bposlem1  21068  bposlem2  21069  bposlem4  21071  bposlem5  21072  bposlem6  21073  bposlem8  21075  bposlem9  21076  lgslem1  21080  lgsdir2lem2  21108  lgsqrlem2  21126  lgseisenlem1  21133  lgseisenlem2  21134  lgseisenlem3  21135  lgseisenlem4  21136  lgsquadlem1  21138  lgsquadlem2  21139  lgsquad2lem1  21142  lgsquad2lem2  21143  m1lgs  21146  chebbnd1lem1  21163  chebbnd1lem3  21165  chto1ub  21170  rplogsumlem1  21178  dchrisumlem2  21184  dchrisum0flblem2  21203  dchrisum0fno1  21205  dchrisum0lem1b  21209  dchrisum0lem1  21210  dchrisum0lem2  21212  logdivsum  21227  mulog2sumlem2  21229  mulog2sumlem3  21230  vmalogdivsum2  21232  log2sumbnd  21238  selberglem1  21239  selberglem2  21240  selberg2  21245  chpdifbndlem1  21247  selberg3lem1  21251  selberg3  21253  selberg4lem1  21254  selberg4  21255  selberg3r  21263  selberg4r  21264  selberg34r  21265  pntrlog2bndlem3  21273  pntrlog2bndlem4  21274  pntrlog2bndlem5  21275  pntrlog2bndlem6  21277  pntpbnd1a  21279  pntpbnd2  21281  pntibndlem2  21285  pntlemg  21292  pntlemh  21293  pntlemk  21300  pntlemo  21301  ostth2lem1  21312  usgraexvlem  21414  wlkdvspthlem  21607  eupath  21703  konigsberg  21709  1kp2ke3k  21754  ex-fl  21755  ipidsq  22209  cncph  22320  ip0i  22326  ip1ilem  22327  ipdirilem  22330  minvecolem2  22377  hvsubcan2i  22566  norm-ii-i  22639  norm3lem  22651  normpar2i  22658  polid2i  22659  hhph  22680  mayete3i  23230  mayete3iOLD  23231  nmcexi  23529  opsqrlem6  23648  cdj3lem1  23937  addltmulALT  23949  sqsscirc1  24306  dya2icoseg  24627  dya2iocucvr  24634  ballotlem2  24746  ballotth  24795  zetacvg  24799  lgamgulmlem4  24816  lgamucov  24822  subfacp1lem1  24865  subfacp1lem5  24870  4bc2eq6  25204  halfthird  25205  ax5seglem7  25874  axlowdimlem13  25893  bpolydiflem  26100  bpoly2  26103  bpoly3  26104  bpoly4  26105  fsumcube  26106  mblfinlem1  26243  mblfinlem2  26244  mblfinlem3  26245  itg2addnclem  26256  itg2addnclem3  26258  dvreasin  26290  dvreacos  26291  areacirclem1  26292  areacirclem3  26294  areacirc  26297  csbrn  26456  trirn  26457  isbnd2  26492  heiborlem6  26525  rabren3dioph  26876  rmxluc  26999  rmyluc  27000  rmyluc2  27001  rmydbl  27003  jm2.17a  27025  jm2.18  27059  jm2.22  27066  jm2.23  27067  jm2.25  27070  jm2.27c  27078  jm3.1lem1  27088  jm3.1lem2  27089  psgnunilem2  27395  proot1ex  27497  lhe4.4ex1a  27523  refsum2cnlem1  27684  m1expeven  27701  itgsinexp  27725  stoweidlem1  27726  stoweidlem14  27739  stoweidlem24  27749  stoweidlem26  27751  stoweidlem62  27787  wallispilem4  27793  wallispilem5  27794  wallispi  27795  wallispi2lem1  27796  wallispi2lem2  27797  wallispi2  27798  stirlinglem1  27799  stirlinglem3  27801  stirlinglem4  27802  stirlinglem5  27803  stirlinglem6  27804  stirlinglem7  27805  stirlinglem8  27806  stirlinglem10  27808  stirlinglem11  27809  stirlinglem13  27811  stirlinglem14  27812  stirlinglem15  27813  2txmodxeq0  28162  sinhpcosh  28483  sineq0ALT  29049
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-i2m1 9058  ax-1ne0 9059  ax-rrecex 9062  ax-cnre 9063
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-iota 5418  df-fv 5462  df-ov 6084  df-2 10058
  Copyright terms: Public domain W3C validator