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

Theorem 2cn 9811
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 9810 . 2  |-  2  e.  RR
21recni 8844 1  |-  2  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1685   CCcc 8730   2c2 9790
This theorem is referenced by:  2m1e1  9836  2p2e4  9837  times2  9839  3p3e6  9851  4p3e7  9853  5p3e8  9856  6p3e9  9860  7p3e10  9863  2t2e4  9866  3t3e9  9868  4d2e2  9871  1mhlfehlf  9929  8th4div3  9930  halfpm6th  9931  halfcl  9932  half0  9934  2halves  9935  halfaddsub  9940  addltmul  9942  zneo  10089  nneo  10090  zeo  10092  zeo2  10093  4t4e16  10192  6t3e18  10197  7t7e49  10206  8t5e40  10210  9t9e81  10221  decbin0  10222  decbin2  10223  fztpval  10839  flhalf  10948  expubnd  11156  sq2  11193  cu2  11195  subsq2  11205  binom2sub  11214  binom3  11216  zesq  11218  expmulnbnd  11227  discr  11232  fac2  11288  fac3  11289  faclbnd2  11298  faclbnd4lem1  11300  faclbnd4lem3  11302  faclbnd4lem4  11303  faclbnd5  11305  bcn2  11325  crre  11593  addcj  11627  imval2  11630  sqrlem7  11728  absmax  11807  rddif  11818  sqreulem  11837  amgm2  11847  abs3lemi  11887  iseraltlem2  12149  iseralt  12151  ackbijnn  12280  climcndslem1  12302  climcndslem2  12303  arisum  12312  arisum2  12313  trirecip  12315  geo2sum  12323  geo2sum2  12324  geo2lim  12325  geoihalfsum  12332  efcllem  12353  ege2le3  12365  efgt0  12377  sinf  12398  tanval2  12407  tanval3  12408  efi4p  12411  sinneg  12420  efival  12426  sinhval  12428  tanhlt1  12434  sinadd  12438  cosadd  12439  sinmul  12446  cosmul  12447  cos2tsin  12453  ef01bndlem  12458  sin01bnd  12459  cos01bnd  12460  cos1bnd  12461  cos2bnd  12462  cos01gt0  12465  sin02gt0  12466  sin4lt0  12469  znnenlem  12484  rpnnen2lem3  12489  rpnnen2lem11  12497  sqr2irrlem  12520  sqr2irr  12521  odd2np1lem  12580  odd2np1  12581  oddm1even  12582  oddp1even  12583  bits0  12613  bitsp1o  12618  bitsfzolem  12619  bitsfzo  12620  bitsmod  12621  0bits  12624  bitsinv1lem  12626  bitsinv1  12627  sadadd2lem2  12635  sadcadd  12643  bitsuz  12659  bitsshft  12660  smumullem  12677  3prm  12769  prmdiv  12847  opoe  12858  omoe  12859  opeo  12860  omeo  12861  pythagtriplem1  12863  pythagtriplem4  12866  pythagtriplem12  12873  pythagtriplem14  12875  pythagtriplem15  12876  pythagtriplem16  12877  pythagtriplem17  12878  iserodd  12882  prmreclem5  12961  prmreclem6  12962  4sqlem7  12985  4sqlem10  12988  4sqlem11  12996  4sqlem12  12997  4sqlem19  13004  dec5dvds  13073  dec2nprm  13076  decexp2  13084  2exp6  13095  2exp8  13096  2exp16  13097  2expltfac  13099  prmlem1a  13102  7prm  13106  11prm  13110  13prm  13111  prmlem2  13115  37prm  13116  43prm  13117  83prm  13118  139prm  13119  163prm  13120  317prm  13121  631prm  13122  1259lem1  13123  1259lem2  13124  1259lem3  13125  1259lem4  13126  1259lem5  13127  1259prm  13128  2503lem1  13129  2503lem2  13130  2503lem3  13131  4001lem1  13133  4001lem2  13134  4001lem3  13135  4001lem4  13136  4001prm  13137  efgtlen  15029  efgredlemg  15045  efgredleme  15046  frgpnabllem1  15155  lt6abl  15175  metnrmlem3  18359  iihalf1cn  18424  iihalf2cn  18426  htpycc  18472  pco0  18506  pco1  18507  pcoval2  18508  pcocn  18509  pcohtpylem  18511  pcopt  18514  pcopt2  18515  pcoass  18516  pcorevlem  18518  minveclem2  18784  ovolunlem1a  18849  ovolunlem1  18850  uniioombllem5  18936  uniioombl  18938  dyaddisjlem  18944  vitalilem4  18960  mbfi1fseqlem5  19068  mbfi1fseqlem6  19069  dvmptre  19312  dvmptim  19313  dvsincos  19322  lhop1  19355  aaliou3lem2  19717  aaliou3lem3  19718  aaliou3lem8  19719  sincn  19814  coscn  19815  pilem2  19822  sinhalfpilem  19828  cospi  19834  sin2pi  19837  cos2pi  19838  ef2pi  19839  ef2kpi  19840  efper  19841  sinperlem  19842  sin2kpi  19845  cos2kpi  19846  sin2pim  19847  cos2pim  19848  sinhalfpip  19854  sinhalfpim  19855  coshalfpip  19856  coshalfpim  19857  ptolemy  19858  sincosq3sgn  19862  sincosq4sgn  19863  tangtx  19867  sinq12gt0  19869  sincosq1eq  19874  sincos4thpi  19875  sincos6thpi  19877  sincos3rdpi  19878  pige3  19879  abssinper  19880  coskpi  19882  sineq0  19883  coseq1  19884  efeq1  19885  efif1olem4  19901  eflogeq  19949  cosargd  19956  tanarg  19964  cxpsqrlem  20043  cxpsqr  20044  logsqr  20045  dvsqr  20078  root1id  20088  root1eq1  20089  cxpeq  20091  ang180lem2  20102  ang180lem3  20103  pythag  20109  ssscongptld  20116  chordthmlem  20123  chordthmlem2  20124  chordthmlem4  20126  quad2  20129  1cubrlem  20131  1cubr  20132  dcubic1lem  20133  dcubic2  20134  dcubic1  20135  dcubic  20136  mcubic  20137  cubic2  20138  cubic  20139  dquartlem1  20141  dquartlem2  20142  dquart  20143  quart1lem  20145  quart1  20146  quartlem1  20147  quartlem2  20148  quartlem3  20149  quartlem4  20150  quart  20151  sinasin  20179  asinsin  20182  cosasin  20194  atancj  20200  efiatan  20202  efiatan2  20207  2efiatan  20208  tanatan  20209  cosatan  20211  atantan  20213  atanbndlem  20215  atan1  20218  atans2  20221  dvatan  20225  atantayl  20227  atantayl2  20228  atantayl3  20229  leibpilem1  20230  leibpilem2  20231  log2cnv  20234  log2tlbnd  20235  log2ublem2  20237  log2ublem3  20238  log2ub  20239  birthday  20243  cxp2limlem  20264  divsqrsumlem  20268  ftalem2  20305  basellem1  20312  basellem2  20313  basellem3  20314  basellem8  20319  basellem9  20320  ppiprm  20383  ppinprm  20384  chtprm  20385  chtnprm  20386  cht3  20405  1sgm2ppw  20433  ppiub  20437  chtublem  20444  chtub  20445  logfaclbnd  20455  perfect1  20461  perfectlem1  20462  perfectlem2  20463  perfect  20464  bcmax  20511  bcp1ctr  20512  bclbnd  20513  bpos1lem  20515  bpos1  20516  bposlem1  20517  bposlem2  20518  bposlem4  20520  bposlem5  20521  bposlem6  20522  bposlem8  20524  bposlem9  20525  lgslem1  20529  lgslem4  20532  lgsdir2lem2  20557  lgsqrlem2  20575  lgseisenlem1  20582  lgseisenlem2  20583  lgseisenlem3  20584  lgseisenlem4  20585  lgsquadlem1  20587  lgsquadlem2  20588  lgsquad2lem1  20591  lgsquad2lem2  20592  m1lgs  20595  chebbnd1lem1  20612  chebbnd1lem3  20614  chto1ub  20619  rplogsumlem1  20627  dchrisumlem2  20633  dchrisum0flblem2  20652  dchrisum0fno1  20654  dchrisum0lem1b  20658  dchrisum0lem1  20659  dchrisum0lem2  20661  logdivsum  20676  mulog2sumlem2  20678  mulog2sumlem3  20679  vmalogdivsum2  20681  log2sumbnd  20687  selberglem1  20688  selberglem2  20689  selberg2  20694  chpdifbndlem1  20696  selberg3lem1  20700  selberg3  20702  selberg4lem1  20703  selberg4  20704  selberg3r  20712  selberg4r  20713  selberg34r  20714  pntrlog2bndlem3  20722  pntrlog2bndlem4  20723  pntrlog2bndlem5  20724  pntrlog2bndlem6  20726  pntpbnd1a  20728  pntpbnd2  20730  pntibndlem2  20734  pntlemg  20741  pntlemh  20742  pntlemk  20749  pntlemo  20750  ostth2lem1  20761  1kp2ke3k  20808  ex-fl  20809  ipidsq  21278  cncph  21389  ip0i  21395  ip1ilem  21396  ipdirilem  21399  minvecolem2  21446  hvsubcan2i  21635  norm-ii-i  21708  norm3lem  21720  normpar2i  21727  polid2i  21728  hhph  21749  mayete3i  22299  mayete3iOLD  22300  nmcexi  22598  opsqrlem6  22717  cdj3lem1  23006  addltmulALT  23018  ballotlem2  23040  ballotth  23089  zetacvg  23093  subfacp1lem1  23114  subfacp1lem5  23119  eupath  23309  konigsberg  23315  4bc2eq6  23502  halfthird  23503  ax5seglem7  23970  axlowdimlem13  23989  axlowdimlem16  23992  axlowdim  23996  bpolydiflem  24196  bpoly2  24199  bpoly3  24200  bpoly4  24201  fsumcube  24202  3timesi  24577  2eq3m1  24578  cntrset  25001  mslb1  25006  2wsms  25007  csbrn  25861  trirn  25862  isbnd2  25906  heiborlem6  25939  rabren3dioph  26297  rmxluc  26420  rmyluc  26421  rmyluc2  26422  rmydbl  26424  jm2.17a  26446  jm2.18  26480  jm2.22  26487  jm2.23  26488  jm2.25  26491  jm2.27c  26499  jm3.1lem1  26509  jm3.1lem2  26510  psgnunilem2  26817  proot1ex  26919  lhe4.4ex1a  26945  refsum2cnlem1  27107  m1expeven  27124  itgsinexp  27148  stoweidlem1  27149  stoweidlem13  27161  stoweidlem14  27162  stoweidlem24  27172  stoweidlem26  27174  stoweidlem62  27210  wallispilem4  27216  wallispilem5  27217  wallispi  27218  wallispi2lem1  27219  wallispi2lem2  27220  wallispi2  27221  stirlinglem1  27222  stirlinglem3  27224  stirlinglem4  27225  stirlinglem5  27226  stirlinglem6  27227  stirlinglem7  27228  stirlinglem8  27229  stirlinglem10  27231  stirlinglem11  27232  stirlinglem13  27234  stirlinglem14  27235  stirlinglem15  27236  sinhpcosh  27470
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-resscn 8789  ax-1cn 8790  ax-icn 8791  ax-addcl 8792  ax-addrcl 8793  ax-mulcl 8794  ax-mulrcl 8795  ax-i2m1 8800  ax-1ne0 8801  ax-rrecex 8804  ax-cnre 8805
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-xp 4694  df-cnv 4696  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fv 5229  df-ov 5822  df-2 9799
  Copyright terms: Public domain W3C validator