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

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

Proof of Theorem 2cn
StepHypRef Expression
1 2re 10844 . 2 2 ∈ ℝ
21recni 9806 1 2 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1938  cc 9688  2c2 10824
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-resscn 9747  ax-1cn 9748  ax-icn 9749  ax-addcl 9750  ax-addrcl 9751  ax-mulcl 9752  ax-mulrcl 9753  ax-i2m1 9758  ax-1ne0 9759  ax-rrecex 9762  ax-cnre 9763
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-iota 5653  df-fv 5697  df-ov 6428  df-2 10833
This theorem is referenced by:  2ex  10846  2cnd  10847  2m1e1  10889  3m1e2  10891  2p2e4  10898  times2  10900  2div2e1  10904  1p2e3  10906  3p3e6  10915  4p3e7  10917  5p3e8  10920  6p3e9  10924  7p3e10OLD  10927  2t1e2  10930  2t2e4  10931  3t3e9  10934  2t0e0  10937  4d2e2  10938  2cnne0  10996  halfcn  11001  1mhlfehlf  11005  8th4div3  11006  halfpm6th  11007  2mulicn  11009  2muline0  11010  halfcl  11011  half0  11013  2halves  11014  halfaddsub  11019  div4p1lem1div2  11041  3halfnz  11195  zneo  11199  nneo  11200  zeo  11202  7p3e10  11342  4t4e16  11372  6t3e18  11381  7t7e49  11392  8t5e40  11396  8t5e40OLD  11397  9t9e81  11409  decbin0  11421  decbin2  11422  halfthird  11424  fztpval  12139  fz0tp  12176  fz0to4untppr  12178  fzo0to3tp  12288  fzo1to4tp  12290  expubnd  12650  sq2  12689  sq4e2t8  12691  cu2  12692  subsq2  12702  binom2sub  12710  binom3  12714  zesq  12716  fac2  12795  fac3  12796  faclbnd2  12807  faclbnd4lem1  12809  faclbnd4lem3  12811  faclbnd4lem4  12812  faclbnd5  12814  bcn2  12835  4bc2eq6  12845  swrd2lsw  13400  crre  13559  addcj  13593  imval2  13596  sqrlem7  13694  absmax  13774  rddif  13785  sqreulem  13804  amgm2  13814  abs3lemi  13854  iseraltlem2  14128  ackbijnn  14266  climcndslem1  14287  climcndslem2  14288  arisum  14298  arisum2  14299  geo2sum2  14311  geo2lim  14312  geoihalfsum  14320  bpoly2  14494  bpoly3  14495  bpoly4  14496  fsumcube  14497  efcllem  14514  ege2le3  14526  efgt0  14539  tanval2  14569  tanval3  14570  efi4p  14573  efival  14588  sinadd  14600  cosadd  14601  sinmul  14608  cos2tsin  14615  ef01bndlem  14620  cos01bnd  14622  cos1bnd  14623  cos2bnd  14624  cos01gt0  14627  sin02gt0  14628  sin4lt0  14631  znnenlem  14646  sqr2irrlem  14683  odd2np1lem  14769  odd2np1  14770  opoe  14792  omoe  14793  opeo  14794  omeo  14795  nno  14803  nn0o  14804  flodddiv4  14845  bits0  14858  bitsfzolem  14864  bitsfzolemOLD  14865  0bits  14870  bitsinv1  14873  sadcadd  14889  smumullem  14923  6gcd4e2  14964  3lcm2e6woprm  15040  6lcm4e12  15041  pythagtriplem1  15241  pythagtriplem12  15251  pythagtriplem14  15253  pythagtriplem15  15254  pythagtriplem16  15255  pythagtriplem17  15256  iserodd  15260  prmreclem5  15344  prmreclem6  15345  4sqlem11  15379  4sqlem12  15380  prmo2  15464  prmo3  15465  dec5dvds  15488  dec2nprm  15491  decexp2  15499  2exp6  15515  2exp8  15516  2exp16  15517  7prm  15537  11prm  15542  13prm  15543  37prm  15548  43prm  15549  83prm  15550  139prm  15551  163prm  15552  317prm  15553  631prm  15554  1259lem1  15558  1259lem2  15559  1259lem3  15560  1259lem4  15561  1259lem5  15562  1259prm  15563  2503lem1  15564  2503lem2  15565  2503lem3  15566  4001lem1  15568  4001lem2  15569  4001lem3  15570  4001lem4  15571  4001prm  15572  psgnunilem2  17628  efgtlen  17868  efgredleme  17885  frgpnabllem1  18004  lt6abl  18024  htpycc  22511  pcoval2  22548  pcocn  22549  pcohtpylem  22551  pcopt  22554  pcopt2  22555  pcoass  22556  pcorevlem  22558  csbren  22854  minveclem2  22869  minveclem2OLD  22881  ovolunlem1a  22947  ovolunlem1  22948  vitalilem4  23062  mbfi1fseqlem5  23168  dvmptre  23414  dvsincos  23424  aaliou3lem2  23790  aaliou3lem3  23791  aaliou3lem8  23792  coscn  23891  sinhalfpilem  23907  cospi  23916  ef2pi  23921  ef2kpi  23922  efper  23923  sinperlem  23924  sin2kpi  23927  cos2kpi  23928  sin2pim  23929  cos2pim  23930  sinhalfpip  23936  sinhalfpim  23937  coshalfpip  23938  coshalfpim  23939  sincosq3sgn  23944  sincosq4sgn  23945  tangtx  23949  sinq12gt0  23951  sincosq1eq  23956  sincos4thpi  23957  sincos6thpi  23959  sincos3rdpi  23960  pige3  23961  abssinper  23962  coskpi  23964  sineq0  23965  coseq1  23966  efeq1  23967  efif1olem4  23983  eflogeq  24040  tanarg  24057  cxpsqrtlem  24136  cxpsqrt  24137  logsqrt  24138  root1eq1  24184  cxpeq  24186  ang180lem2  24228  ang180lem3  24229  quad2  24254  1cubrlem  24256  1cubr  24257  dcubic2  24259  dcubic1  24260  dcubic  24261  mcubic  24262  cubic2  24263  cubic  24264  dquartlem1  24266  dquartlem2  24267  dquart  24268  quart1lem  24270  quart1  24271  quartlem1  24272  quartlem2  24273  quartlem3  24274  quart  24276  sinasin  24304  asinsin  24307  atancj  24325  efiatan  24327  efiatan2  24332  2efiatan  24333  tanatan  24334  atantan  24338  atanbndlem  24340  atans2  24346  dvatan  24350  atantayl2  24353  leibpilem1  24355  leibpilem2  24356  log2cnv  24359  log2tlbnd  24360  log2ublem2  24362  log2ublem3  24363  log2ub  24364  birthday  24369  zetacvg  24429  basellem1  24497  basellem3  24499  basellem8  24504  basellem9  24505  cht3  24589  1sgm2ppw  24615  ppiub  24619  chtublem  24626  chtub  24627  perfect1  24643  perfectlem1  24644  perfectlem2  24645  perfect  24646  bcmax  24693  bcp1ctr  24694  bclbnd  24695  bpos1lem  24697  bpos1  24698  bposlem1  24699  bposlem2  24700  bposlem4  24702  bposlem5  24703  bposlem6  24704  bposlem8  24706  bposlem9  24707  lgsdir2lem2  24741  gausslemma2dlem6  24787  lgsquadlem1  24795  lgsquadlem2  24796  lgsquad2lem2  24800  m1lgs  24803  2lgslem3a  24811  2lgslem3b  24812  2lgslem3c  24813  2lgslem3d  24814  2lgsoddprmlem2  24824  2lgsoddprmlem3c  24827  2lgsoddprmlem3d  24828  rplogsumlem1  24863  dchrisum0fno1  24890  dchrisum0lem1  24895  dchrisum0lem2  24897  logdivsum  24912  mulog2sumlem3  24915  log2sumbnd  24923  selberglem1  24924  selberglem2  24925  selberg2  24930  selberg4lem1  24939  selberg3r  24948  pntpbnd1a  24964  pntpbnd2  24966  pntibndlem2  24970  pntlemk  24985  ax5seglem7  25506  axlowdimlem13  25525  wlkdvspthlem  25876  clwlkisclwwlklem2a4  26051  numclwwlkovf2ex  26352  ex-fl  26435  ex-ceil  26436  ex-exp  26438  ex-fac  26439  ex-abs  26443  ex-ind-dvds  26449  ipidsq  26726  cncph  26837  ip0i  26843  ip1ilem  26844  ipdirilem  26847  minvecolem2  26894  minvecolem2OLD  26904  hvsubcan2i  27094  norm-ii-i  27167  norm3lem  27179  normpar2i  27186  polid2i  27187  hhph  27208  mayete3i  27760  nmcexi  28058  opsqrlem6  28177  addltmulALT  28478  omssubadd  29492  omssubaddOLD  29496  oddpwdc  29551  fib5  29602  ballotlem2  29685  ballotth  29734  ballotthOLD  29772  problem4  30660  problem5  30661  quad3  30662  cnndvlem1  31533  sin2h  32444  cos2h  32445  tan2h  32446  poimirlem29  32483  mblfinlem1  32491  mblfinlem2  32492  mblfinlem3  32493  itg2addnclem3  32508  dvasin  32541  areacirc  32550  heiborlem6  32660  rmxluc  36394  rmyluc  36395  jm2.17a  36420  jm2.18  36448  jm2.23  36456  jm3.1lem1  36477  proot1ex  36680  areaquad  36703  lhe4.4ex1a  37432  sineq0ALT  38077  coskpi2  38636  cosnegpi  38637  cosknegpi  38639  stoweidlem26  38809  wallispilem4  38851  wallispi  38853  wallispi2lem1  38854  stirlinglem8  38864  dirkerper  38879  dirkertrigeqlem3  38883  dirkertrigeq  38884  dirkeritg  38885  dirkercncflem1  38886  dirkercncflem2  38887  fourierdlem57  38948  fourierdlem58  38949  fourierdlem62  38953  fourierdlem76  38967  fourierdlem103  38994  fourierdlem104  38995  sqwvfourb  39014  fourierswlem  39015  fmtnoge3  39875  fmtnorec1  39882  fmtno0  39885  fmtno1  39886  fmtnorec3  39893  fmtnorec4  39894  fmtno5lem2  39899  fmtno5lem4  39901  257prm  39906  fmtnoprmfac2lem1  39911  fmtno4prmfac  39917  fmtno5faclem2  39925  fmtno5faclem3  39926  fmtno5fac  39927  2exp5  39940  139prmALT  39944  31prm  39945  2exp7  39947  127prm  39948  2exp11  39950  mod42tp1mod8  39952  lighneallem2  39956  lighneallem3  39957  lighneallem4a  39958  3exp4mod41  39966  41prothprmlem1  39967  41prothprmlem2  39968  41prothprm  39969  bits0ALTV  40023  0evenALTV  40032  6even  40053  8even  40055  perfectALTVlem1  40059  perfectALTVlem2  40060  perfectALTV  40061  nnsum3primes4  40099  bgoldbtbndlem1  40116  elwspths2spth  41263  clwlkclwwlklem2a4  41298  av-numclwwlkovf2ex  41609  0nodd  41692  0even  41813  2even  41815  2zrngamgm  41821  2t6m3t4e0  42011  linevalexample  42070  zlmodzxzequap  42174  pw2m1lepw2m1  42196  nnlog2ge0lt1  42250  logbpw2m1  42251  nnpw2blen  42264  nnpw2pmod  42267  blen1  42268  blen2  42269  blennnt2  42273  nnolog2flm1  42274  0dig2nn0e  42296  0dig2nn0o  42297  nn0sumshdiglemA  42303  nn0sumshdiglemB  42304  nn0sumshdiglem1  42305  nn0sumshdiglem2  42306  sinhpcosh  42333
  Copyright terms: Public domain W3C validator