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

Theorem 2cn 10631
Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
Assertion
Ref Expression
2cn

Proof of Theorem 2cn
StepHypRef Expression
1 2re 10630 . 2
21recni 9629 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1818   cc 9511  2c2 10610
This theorem is referenced by:  2ex  10632  2cnd  10633  2m1e1  10675  3m1e2  10677  2p2e4  10678  times2  10680  2div2e1  10683  1p2e3  10685  3p3e6  10694  4p3e7  10696  5p3e8  10699  6p3e9  10703  7p3e10  10706  2t1e2  10709  2t2e4  10710  3t3e9  10713  2t0e0  10716  4d2e2  10717  2cnne0  10775  halfcn  10780  1mhlfehlf  10783  8th4div3  10784  halfpm6th  10785  2mulicn  10787  2muline0  10788  halfcl  10789  half0  10791  2halves  10792  halfaddsub  10797  zneo  10970  nneo  10971  zeo  10973  4t4e16  11077  6t3e18  11082  7t7e49  11091  8t5e40  11095  9t9e81  11106  decbin0  11107  decbin2  11108  fztpval  11770  fz0tp  11806  fzo0to3tp  11900  expubnd  12226  sq2  12264  cu2  12266  subsq2  12276  binom2sub  12285  binom3  12287  zesq  12289  fac2  12359  fac3  12360  faclbnd2  12369  faclbnd4lem1  12371  faclbnd4lem3  12373  faclbnd4lem4  12374  faclbnd5  12376  bcn2  12397  swrd2lsw  12890  crre  12947  addcj  12981  imval2  12984  sqrlem7  13082  absmax  13162  rddif  13173  sqreulem  13192  amgm2  13202  abs3lemi  13242  iseraltlem2  13505  ackbijnn  13640  climcndslem1  13661  climcndslem2  13662  arisum  13671  arisum2  13672  geo2sum2  13683  geo2lim  13684  geoihalfsum  13691  efcllem  13813  ege2le3  13825  efgt0  13838  tanval2  13868  tanval3  13869  efi4p  13872  efival  13887  sinadd  13899  cosadd  13900  sinmul  13907  cos2tsin  13914  ef01bndlem  13919  cos01bnd  13921  cos1bnd  13922  cos2bnd  13923  cos01gt0  13926  sin02gt0  13927  sin4lt0  13930  znnenlem  13945  sqr2irrlem  13981  odd2np1lem  14045  odd2np1  14046  bits0  14078  bitsfzolem  14084  0bits  14089  bitsinv1  14092  sadcadd  14108  smumullem  14142  opoe  14335  omoe  14336  opeo  14337  omeo  14338  pythagtriplem1  14340  pythagtriplem12  14350  pythagtriplem14  14352  pythagtriplem15  14353  pythagtriplem16  14354  pythagtriplem17  14355  iserodd  14359  prmreclem5  14438  prmreclem6  14439  4sqlem11  14473  4sqlem12  14474  dec5dvds  14550  dec2nprm  14553  decexp2  14561  2exp6  14572  2exp6OLD  14573  2exp8  14574  2exp16  14575  7prm  14596  11prm  14600  13prm  14601  37prm  14606  43prm  14607  83prm  14608  139prm  14609  163prm  14610  317prm  14611  631prm  14612  1259lem1  14613  1259lem2  14614  1259lem3  14615  1259lem4  14616  1259lem5  14617  1259prm  14618  2503lem1  14619  2503lem2  14620  2503lem3  14621  4001lem1  14623  4001lem2  14624  4001lem3  14625  4001lem4  14626  4001prm  14627  psgnunilem2  16520  efgtlen  16744  efgredleme  16761  frgpnabllem1  16877  lt6abl  16897  htpycc  21480  pcoval2  21516  pcocn  21517  pcohtpylem  21519  pcopt  21522  pcopt2  21523  pcoass  21524  pcorevlem  21526  csbren  21826  minveclem2  21841  ovolunlem1a  21907  ovolunlem1  21908  vitalilem4  22020  mbfi1fseqlem5  22126  dvmptre  22372  dvsincos  22382  aaliou3lem2  22739  aaliou3lem3  22740  aaliou3lem8  22741  coscn  22840  sinhalfpilem  22856  cospi  22865  ef2pi  22870  ef2kpi  22871  efper  22872  sinperlem  22873  sin2kpi  22876  cos2kpi  22877  sin2pim  22878  cos2pim  22879  sinhalfpip  22885  sinhalfpim  22886  coshalfpip  22887  coshalfpim  22888  sincosq3sgn  22893  sincosq4sgn  22894  tangtx  22898  sinq12gt0  22900  sincosq1eq  22905  sincos4thpi  22906  sincos6thpi  22908  sincos3rdpi  22909  pige3  22910  abssinper  22911  coskpi  22913  sineq0  22914  coseq1  22915  efeq1  22916  efif1olem4  22932  eflogeq  22986  tanarg  23004  cxpsqrtlem  23083  cxpsqrt  23084  logsqrt  23085  root1eq1  23129  cxpeq  23131  ang180lem2  23142  ang180lem3  23143  quad2  23170  1cubrlem  23172  1cubr  23173  dcubic2  23175  dcubic1  23176  dcubic  23177  mcubic  23178  cubic2  23179  cubic  23180  dquartlem1  23182  dquartlem2  23183  dquart  23184  quart1lem  23186  quart1  23187  quartlem1  23188  quartlem2  23189  quartlem3  23190  quart  23192  sinasin  23220  asinsin  23223  atancj  23241  efiatan  23243  efiatan2  23248  2efiatan  23249  tanatan  23250  atantan  23254  atanbndlem  23256  atans2  23262  dvatan  23266  atantayl2  23269  leibpilem1  23271  leibpilem2  23272  log2cnv  23275  log2tlbnd  23276  log2ublem2  23278  log2ublem3  23279  log2ub  23280  birthday  23284  basellem1  23354  basellem3  23356  basellem8  23361  basellem9  23362  cht3  23447  1sgm2ppw  23475  ppiub  23479  chtublem  23486  chtub  23487  perfect1  23503  perfectlem1  23504  perfectlem2  23505  perfect  23506  bcmax  23553  bcp1ctr  23554  bclbnd  23555  bpos1lem  23557  bpos1  23558  bposlem1  23559  bposlem2  23560  bposlem4  23562  bposlem5  23563  bposlem6  23564  bposlem8  23566  bposlem9  23567  lgsdir2lem2  23599  lgsquadlem1  23629  lgsquadlem2  23630  lgsquad2lem2  23634  m1lgs  23637  rplogsumlem1  23669  dchrisum0fno1  23696  dchrisum0lem1  23701  dchrisum0lem2  23703  logdivsum  23718  mulog2sumlem3  23721  log2sumbnd  23729  selberglem1  23730  selberglem2  23731  selberg2  23736  selberg4lem1  23745  selberg3r  23754  pntpbnd1a  23770  pntpbnd2  23772  pntibndlem2  23776  pntlemk  23791  ax5seglem7  24238  axlowdimlem13  24257  usgraexvlem  24395  wlkdvspthlem  24609  clwlkisclwwlklem2a4  24784  numclwwlkovf2ex  25086  ex-fl  25168  ex-ind-dvds  25170  ipidsq  25623  cncph  25734  ip0i  25740  ip1ilem  25741  ipdirilem  25744  minvecolem2  25791  hvsubcan2i  25981  norm-ii-i  26054  norm3lem  26066  normpar2i  26073  polid2i  26074  hhph  26095  mayete3i  26646  mayete3iOLD  26647  nmcexi  26945  opsqrlem6  27064  addltmulALT  27365  oddpwdc  28293  fib5  28344  ballotlem2  28427  ballotth  28476  zetacvg  28557  problem4  29022  problem5  29023  quad3  29024  4bc2eq6  29112  halfthird  29113  bpoly2  29819  bpoly3  29820  bpoly4  29821  fsumcube  29822  sin2h  30045  cos2h  30046  tan2h  30047  mblfinlem1  30051  mblfinlem2  30052  mblfinlem3  30053  itg2addnclem3  30068  dvasin  30103  areacirc  30112  heiborlem6  30312  rmxluc  30872  rmyluc  30873  jm2.17a  30898  jm2.18  30930  jm2.23  30938  jm3.1lem1  30959  proot1ex  31161  areaquad  31184  lhe4.4ex1a  31234  coskpi2  31666  cosnegpi  31667  cosknegpi  31669  stoweidlem26  31808  wallispilem4  31850  wallispi  31852  wallispi2lem1  31853  stirlinglem8  31863  dirkerper  31878  dirkertrigeqlem3  31882  dirkertrigeq  31883  dirkeritg  31884  dirkercncflem1  31885  dirkercncflem2  31886  fourierdlem57  31946  fourierdlem58  31947  fourierdlem62  31951  fourierdlem76  31965  fourierdlem103  31992  fourierdlem104  31993  sqwvfourb  32012  fourierswlem  32013  0nodd  32498  0even  32737  2even  32739  2zrngamgm  32745  2t6m3t4e0  32937  linevalexample  32996  zlmodzxzequap  33100  sinhpcosh  33134  sineq0ALT  33737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299  df-2 10619
  Copyright terms: Public domain W3C validator