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

Theorem 2cn 10030
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 10029 . 2  |-  2  e.  RR
21recni 9062 1  |-  2  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   CCcc 8948   2c2 10009
This theorem is referenced by:  2m1e1  10055  3m1e2  10056  3m1e2OLD  10057  2p2e4  10058  times2  10060  3p3e6  10072  4p3e7  10074  5p3e8  10077  6p3e9  10081  7p3e10  10084  2t2e4  10087  3t3e9  10089  4d2e2  10092  1mhlfehlf  10150  8th4div3  10151  halfpm6th  10152  halfcl  10153  half0  10155  2halves  10156  halfaddsub  10161  zneo  10312  nneo  10313  zeo  10315  zeo2  10316  4t4e16  10415  6t3e18  10420  7t7e49  10429  8t5e40  10433  9t9e81  10444  decbin0  10445  decbin2  10446  fz0tp  11063  fztpval  11067  fzo0to3tp  11144  flhalf  11190  expubnd  11399  sq2  11436  cu2  11438  subsq2  11448  binom2sub  11457  binom3  11459  zesq  11461  expmulnbnd  11470  discr  11475  fac2  11531  fac3  11532  faclbnd2  11541  faclbnd4lem1  11543  faclbnd4lem3  11545  faclbnd4lem4  11546  faclbnd5  11548  bcn2  11569  crre  11878  addcj  11912  imval2  11915  sqrlem7  12013  absmax  12092  rddif  12103  sqreulem  12122  amgm2  12132  abs3lemi  12172  iseraltlem2  12435  iseralt  12437  ackbijnn  12566  climcndslem1  12588  climcndslem2  12589  arisum  12598  arisum2  12599  trirecip  12601  geo2sum  12609  geo2sum2  12610  geo2lim  12611  geoihalfsum  12618  efcllem  12639  ege2le3  12651  efgt0  12663  sinf  12684  tanval2  12693  tanval3  12694  efi4p  12697  sinneg  12706  efival  12712  sinhval  12714  tanhlt1  12720  sinadd  12724  cosadd  12725  sinmul  12732  cosmul  12733  cos2tsin  12739  ef01bndlem  12744  sin01bnd  12745  cos01bnd  12746  cos1bnd  12747  cos2bnd  12748  cos01gt0  12751  sin02gt0  12752  sin4lt0  12755  znnenlem  12770  rpnnen2lem3  12775  rpnnen2lem11  12783  sqr2irrlem  12806  sqr2irr  12807  odd2np1lem  12866  odd2np1  12867  oddm1even  12868  oddp1even  12869  bits0  12899  bitsp1o  12904  bitsfzolem  12905  bitsfzo  12906  bitsmod  12907  0bits  12910  bitsinv1lem  12912  bitsinv1  12913  sadadd2lem2  12921  sadcadd  12929  bitsuz  12945  bitsshft  12946  smumullem  12963  prmdiv  13133  opoe  13144  omoe  13145  opeo  13146  omeo  13147  pythagtriplem1  13149  pythagtriplem4  13152  pythagtriplem12  13159  pythagtriplem14  13161  pythagtriplem15  13162  pythagtriplem16  13163  pythagtriplem17  13164  iserodd  13168  prmreclem5  13247  prmreclem6  13248  4sqlem7  13271  4sqlem10  13274  4sqlem11  13282  4sqlem12  13283  4sqlem19  13290  dec5dvds  13359  dec2nprm  13362  decexp2  13370  2exp6  13381  2exp8  13382  2exp16  13383  2expltfac  13385  prmlem1a  13388  7prm  13392  11prm  13396  13prm  13397  prmlem2  13401  37prm  13402  43prm  13403  83prm  13404  139prm  13405  163prm  13406  317prm  13407  631prm  13408  1259lem1  13409  1259lem2  13410  1259lem3  13411  1259lem4  13412  1259lem5  13413  1259prm  13414  2503lem1  13415  2503lem2  13416  2503lem3  13417  4001lem1  13419  4001lem2  13420  4001lem3  13421  4001lem4  13422  4001prm  13423  efgtlen  15317  efgredlemg  15333  efgredleme  15334  frgpnabllem1  15443  lt6abl  15463  metnrmlem3  18848  iihalf1cn  18914  iihalf2cn  18916  htpycc  18962  pco0  18996  pco1  18997  pcoval2  18998  pcocn  18999  pcohtpylem  19001  pcopt  19004  pcopt2  19005  pcoass  19006  pcorevlem  19008  minveclem2  19284  ovolunlem1a  19349  ovolunlem1  19350  uniioombllem5  19436  uniioombl  19438  dyaddisjlem  19444  vitalilem4  19460  mbfi1fseqlem5  19568  mbfi1fseqlem6  19569  dvmptre  19812  dvmptim  19813  dvsincos  19822  lhop1  19855  aaliou3lem2  20217  aaliou3lem3  20218  aaliou3lem8  20219  sincn  20317  coscn  20318  pilem2  20325  sinhalfpilem  20331  cospi  20337  sin2pi  20340  cos2pi  20341  ef2pi  20342  ef2kpi  20343  efper  20344  sinperlem  20345  sin2kpi  20348  cos2kpi  20349  sin2pim  20350  cos2pim  20351  sinhalfpip  20357  sinhalfpim  20358  coshalfpip  20359  coshalfpim  20360  ptolemy  20361  sincosq3sgn  20365  sincosq4sgn  20366  tangtx  20370  sinq12gt0  20372  sincosq1eq  20377  sincos4thpi  20378  sincos6thpi  20380  sincos3rdpi  20381  pige3  20382  abssinper  20383  coskpi  20385  sineq0  20386  coseq1  20387  efeq1  20388  efif1olem4  20404  eflogeq  20453  cosargd  20460  tanarg  20471  cxpsqrlem  20550  cxpsqr  20551  logsqr  20552  dvsqr  20585  root1id  20595  root1eq1  20596  cxpeq  20598  ang180lem2  20609  ang180lem3  20610  pythag  20616  ssscongptld  20623  chordthmlem  20630  chordthmlem2  20631  chordthmlem4  20633  quad2  20636  1cubrlem  20638  1cubr  20639  dcubic1lem  20640  dcubic2  20641  dcubic1  20642  dcubic  20643  mcubic  20644  cubic2  20645  cubic  20646  dquartlem1  20648  dquartlem2  20649  dquart  20650  quart1lem  20652  quart1  20653  quartlem1  20654  quartlem2  20655  quartlem3  20656  quartlem4  20657  quart  20658  sinasin  20686  asinsin  20689  cosasin  20701  atancj  20707  efiatan  20709  efiatan2  20714  2efiatan  20715  tanatan  20716  cosatan  20718  atantan  20720  atanbndlem  20722  atan1  20725  atans2  20728  dvatan  20732  atantayl  20734  atantayl2  20735  atantayl3  20736  leibpilem1  20737  leibpilem2  20738  log2cnv  20741  log2tlbnd  20742  log2ublem2  20744  log2ublem3  20745  log2ub  20746  birthday  20750  cxp2limlem  20771  divsqrsumlem  20775  ftalem2  20813  basellem1  20820  basellem2  20821  basellem3  20822  basellem8  20827  basellem9  20828  cht3  20913  1sgm2ppw  20941  ppiub  20945  chtublem  20952  chtub  20953  logfaclbnd  20963  perfect1  20969  perfectlem1  20970  perfectlem2  20971  perfect  20972  bcmax  21019  bcp1ctr  21020  bclbnd  21021  bpos1lem  21023  bpos1  21024  bposlem1  21025  bposlem2  21026  bposlem4  21028  bposlem5  21029  bposlem6  21030  bposlem8  21032  bposlem9  21033  lgslem1  21037  lgsdir2lem2  21065  lgsqrlem2  21083  lgseisenlem1  21090  lgseisenlem2  21091  lgseisenlem3  21092  lgseisenlem4  21093  lgsquadlem1  21095  lgsquadlem2  21096  lgsquad2lem1  21099  lgsquad2lem2  21100  m1lgs  21103  chebbnd1lem1  21120  chebbnd1lem3  21122  chto1ub  21127  rplogsumlem1  21135  dchrisumlem2  21141  dchrisum0flblem2  21160  dchrisum0fno1  21162  dchrisum0lem1b  21166  dchrisum0lem1  21167  dchrisum0lem2  21169  logdivsum  21184  mulog2sumlem2  21186  mulog2sumlem3  21187  vmalogdivsum2  21189  log2sumbnd  21195  selberglem1  21196  selberglem2  21197  selberg2  21202  chpdifbndlem1  21204  selberg3lem1  21208  selberg3  21210  selberg4lem1  21211  selberg4  21212  selberg3r  21220  selberg4r  21221  selberg34r  21222  pntrlog2bndlem3  21230  pntrlog2bndlem4  21231  pntrlog2bndlem5  21232  pntrlog2bndlem6  21234  pntpbnd1a  21236  pntpbnd2  21238  pntibndlem2  21242  pntlemg  21249  pntlemh  21250  pntlemk  21257  pntlemo  21258  ostth2lem1  21269  usgraexvlem  21371  wlkdvspthlem  21564  eupath  21660  konigsberg  21666  1kp2ke3k  21711  ex-fl  21712  ipidsq  22166  cncph  22277  ip0i  22283  ip1ilem  22284  ipdirilem  22287  minvecolem2  22334  hvsubcan2i  22523  norm-ii-i  22596  norm3lem  22608  normpar2i  22615  polid2i  22616  hhph  22637  mayete3i  23187  mayete3iOLD  23188  nmcexi  23486  opsqrlem6  23605  cdj3lem1  23894  addltmulALT  23906  sqsscirc1  24263  dya2icoseg  24584  dya2iocucvr  24591  ballotlem2  24703  ballotth  24752  zetacvg  24756  lgamgulmlem4  24773  lgamucov  24779  subfacp1lem1  24822  subfacp1lem5  24827  4bc2eq6  25161  halfthird  25162  ax5seglem7  25782  axlowdimlem13  25801  bpolydiflem  26008  bpoly2  26011  bpoly3  26012  bpoly4  26013  fsumcube  26014  mblfinlem  26147  mblfinlem2  26148  itg2addnclem  26159  itg2addnclem3  26161  dvreasin  26183  dvreacos  26184  areacirclem2  26185  areacirclem3  26186  areacirclem1  26188  areacirc  26191  csbrn  26350  trirn  26351  isbnd2  26386  heiborlem6  26419  rabren3dioph  26770  rmxluc  26893  rmyluc  26894  rmyluc2  26895  rmydbl  26897  jm2.17a  26919  jm2.18  26953  jm2.22  26960  jm2.23  26961  jm2.25  26964  jm2.27c  26972  jm3.1lem1  26982  jm3.1lem2  26983  psgnunilem2  27290  proot1ex  27392  lhe4.4ex1a  27418  refsum2cnlem1  27579  m1expeven  27596  itgsinexp  27620  stoweidlem1  27621  stoweidlem14  27634  stoweidlem24  27644  stoweidlem26  27646  stoweidlem62  27682  wallispilem4  27688  wallispilem5  27689  wallispi  27690  wallispi2lem1  27691  wallispi2lem2  27692  wallispi2  27693  stirlinglem1  27694  stirlinglem3  27696  stirlinglem4  27697  stirlinglem5  27698  stirlinglem6  27699  stirlinglem7  27700  stirlinglem8  27701  stirlinglem10  27703  stirlinglem11  27704  stirlinglem13  27706  stirlinglem14  27707  stirlinglem15  27708  sinhpcosh  28201
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-resscn 9007  ax-1cn 9008  ax-icn 9009  ax-addcl 9010  ax-addrcl 9011  ax-mulcl 9012  ax-mulrcl 9013  ax-i2m1 9018  ax-1ne0 9019  ax-rrecex 9022  ax-cnre 9023
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 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-op 3787  df-uni 3980  df-br 4177  df-iota 5381  df-fv 5425  df-ov 6047  df-2 10018
  Copyright terms: Public domain W3C validator