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

Theorem 2cn 10769
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 10768 . 2 2 ∈ ℝ
21recni 9740 1 2 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1937  cc 9622  2c2 10748
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-resscn 9681  ax-1cn 9682  ax-icn 9683  ax-addcl 9684  ax-addrcl 9685  ax-mulcl 9686  ax-mulrcl 9687  ax-i2m1 9692  ax-1ne0 9693  ax-rrecex 9696  ax-cnre 9697
This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-iota 5597  df-fv 5641  df-ov 6366  df-2 10757
This theorem is referenced by:  2ex  10770  2cnd  10771  2m1e1  10813  3m1e2  10815  2p2e4  10817  times2  10819  2div2e1  10822  1p2e3  10824  3p3e6  10833  4p3e7  10835  5p3e8  10838  6p3e9  10842  7p3e10  10845  2t1e2  10848  2t2e4  10849  3t3e9  10852  2t0e0  10855  4d2e2  10856  2cnne0  10914  halfcn  10919  1mhlfehlf  10922  8th4div3  10923  halfpm6th  10924  2mulicn  10926  2muline0  10927  halfcl  10928  half0  10930  2halves  10931  halfaddsub  10936  zneo  11108  nneo  11109  zeo  11111  4t4e16  11214  6t3e18  11219  7t7e49  11228  8t5e40  11232  9t9e81  11243  decbin0  11244  decbin2  11245  halfthird  11247  fztpval  11955  fz0tp  11992  fzo0to3tp  12103  expubnd  12447  sq2  12485  cu2  12487  subsq2  12497  binom2sub  12505  binom3  12507  zesq  12509  fac2  12579  fac3  12580  faclbnd2  12590  faclbnd4lem1  12592  faclbnd4lem3  12594  faclbnd4lem4  12595  faclbnd5  12597  bcn2  12618  4bc2eq6  12628  swrd2lsw  13181  crre  13337  addcj  13371  imval2  13374  sqrlem7  13472  absmax  13552  rddif  13563  sqreulem  13582  amgm2  13592  abs3lemi  13632  iseraltlem2  13909  ackbijnn  14046  climcndslem1  14067  climcndslem2  14068  arisum  14078  arisum2  14079  geo2sum2  14090  geo2lim  14091  geoihalfsum  14098  bpoly2  14270  bpoly3  14271  bpoly4  14272  fsumcube  14273  efcllem  14292  ege2le3  14304  efgt0  14317  tanval2  14347  tanval3  14348  efi4p  14351  efival  14366  sinadd  14378  cosadd  14379  sinmul  14386  cos2tsin  14393  ef01bndlem  14398  cos01bnd  14400  cos1bnd  14401  cos2bnd  14402  cos01gt0  14405  sin02gt0  14406  sin4lt0  14409  znnenlem  14424  sqr2irrlem  14460  odd2np1lem  14525  odd2np1  14526  bits0  14563  bitsfzolem  14569  bitsfzolemOLD  14570  0bits  14575  bitsinv1  14578  sadcadd  14594  smumullem  14628  6gcd4e2  14664  3lcm2e6woprm  14742  6lcm4e12  14743  opoe  14923  omoe  14924  opeo  14925  omeo  14926  pythagtriplem1  14928  pythagtriplem12  14938  pythagtriplem14  14940  pythagtriplem15  14941  pythagtriplem16  14942  pythagtriplem17  14943  iserodd  14947  prmreclem5  15026  prmreclem6  15027  4sqlem11  15061  4sqlem12  15062  prmo2  15160  prmo3  15161  dec5dvds  15198  dec2nprm  15201  decexp2  15209  2exp6  15220  2exp8  15221  2exp16  15222  7prm  15243  11prm  15247  13prm  15248  37prm  15253  43prm  15254  83prm  15255  139prm  15256  163prm  15257  317prm  15258  631prm  15259  1259lem1  15263  1259lem2  15264  1259lem3  15265  1259lem4  15266  1259lem5  15267  1259prm  15268  2503lem1  15269  2503lem2  15270  2503lem3  15271  4001lem1  15273  4001lem2  15274  4001lem3  15275  4001lem4  15276  4001prm  15277  psgnunilem2  17297  efgtlen  17537  efgredleme  17554  frgpnabllem1  17670  lt6abl  17690  htpycc  22169  pcoval2  22206  pcocn  22207  pcohtpylem  22209  pcopt  22212  pcopt2  22213  pcoass  22214  pcorevlem  22216  csbren  22512  minveclem2  22527  minveclem2OLD  22539  ovolunlem1a  22608  ovolunlem1  22609  vitalilem4  22730  mbfi1fseqlem5  22838  dvmptre  23084  dvsincos  23094  aaliou3lem2  23460  aaliou3lem3  23461  aaliou3lem8  23462  coscn  23561  sinhalfpilem  23579  cospi  23588  ef2pi  23593  ef2kpi  23594  efper  23595  sinperlem  23596  sin2kpi  23599  cos2kpi  23600  sin2pim  23601  cos2pim  23602  sinhalfpip  23608  sinhalfpim  23609  coshalfpip  23610  coshalfpim  23611  sincosq3sgn  23616  sincosq4sgn  23617  tangtx  23621  sinq12gt0  23623  sincosq1eq  23628  sincos4thpi  23629  sincos6thpi  23631  sincos3rdpi  23632  pige3  23633  abssinper  23634  coskpi  23636  sineq0  23637  coseq1  23638  efeq1  23639  efif1olem4  23655  eflogeq  23712  tanarg  23729  cxpsqrtlem  23808  cxpsqrt  23809  logsqrt  23810  root1eq1  23856  cxpeq  23858  ang180lem2  23900  ang180lem3  23901  quad2  23926  1cubrlem  23928  1cubr  23929  dcubic2  23931  dcubic1  23932  dcubic  23933  mcubic  23934  cubic2  23935  cubic  23936  dquartlem1  23938  dquartlem2  23939  dquart  23940  quart1lem  23942  quart1  23943  quartlem1  23944  quartlem2  23945  quartlem3  23946  quart  23948  sinasin  23976  asinsin  23979  atancj  23997  efiatan  23999  efiatan2  24004  2efiatan  24005  tanatan  24006  atantan  24010  atanbndlem  24012  atans2  24018  dvatan  24022  atantayl2  24025  leibpilem1  24027  leibpilem2  24028  log2cnv  24031  log2tlbnd  24032  log2ublem2  24034  log2ublem3  24035  log2ub  24036  birthday  24041  zetacvg  24101  basellem1  24168  basellem3  24170  basellem8  24175  basellem9  24176  cht3  24261  1sgm2ppw  24289  ppiub  24293  chtublem  24300  chtub  24301  perfect1  24317  perfectlem1  24318  perfectlem2  24319  perfect  24320  bcmax  24367  bcp1ctr  24368  bclbnd  24369  bpos1lem  24371  bpos1  24372  bposlem1  24373  bposlem2  24374  bposlem4  24376  bposlem5  24377  bposlem6  24378  bposlem8  24380  bposlem9  24381  lgsdir2lem2  24413  lgsquadlem1  24443  lgsquadlem2  24444  lgsquad2lem2  24448  m1lgs  24451  rplogsumlem1  24483  dchrisum0fno1  24510  dchrisum0lem1  24515  dchrisum0lem2  24517  logdivsum  24532  mulog2sumlem3  24535  log2sumbnd  24543  selberglem1  24544  selberglem2  24545  selberg2  24550  selberg4lem1  24559  selberg3r  24568  pntpbnd1a  24584  pntpbnd2  24586  pntibndlem2  24590  pntlemk  24605  ax5seglem7  25126  axlowdimlem13  25145  usgraexmplvtxlem  25283  wlkdvspthlem  25498  clwlkisclwwlklem2a4  25673  numclwwlkovf2ex  25974  ex-fl  26057  ex-ind-dvds  26060  ipidsq  26512  cncph  26623  ip0i  26629  ip1ilem  26630  ipdirilem  26633  minvecolem2  26680  minvecolem2OLD  26690  hvsubcan2i  26880  norm-ii-i  26953  norm3lem  26965  normpar2i  26972  polid2i  26973  hhph  26994  mayete3i  27544  nmcexi  27842  opsqrlem6  27961  addltmulALT  28262  omssubadd  29282  omssubaddOLD  29286  oddpwdc  29341  fib5  29392  ballotlem2  29475  ballotth  29524  ballotthOLD  29562  problem4  30452  problem5  30453  quad3  30454  sin2h  32168  cos2h  32169  tan2h  32170  poimirlem29  32207  mblfinlem1  32215  mblfinlem2  32216  mblfinlem3  32217  itg2addnclem3  32233  dvasin  32266  areacirc  32275  heiborlem6  32385  rmxluc  36024  rmyluc  36025  jm2.17a  36050  jm2.18  36083  jm2.23  36091  jm3.1lem1  36112  proot1ex  36318  areaquad  36341  lhe4.4ex1a  37035  sineq0ALT  37682  coskpi2  38150  cosnegpi  38151  cosknegpi  38153  stoweidlem26  38322  wallispilem4  38366  wallispi  38368  wallispi2lem1  38369  stirlinglem8  38379  dirkerper  38394  dirkertrigeqlem3  38398  dirkertrigeq  38399  dirkeritg  38400  dirkercncflem1  38401  dirkercncflem2  38402  fourierdlem57  38463  fourierdlem58  38464  fourierdlem62  38468  fourierdlem76  38482  fourierdlem103  38509  fourierdlem104  38510  sqwvfourb  38529  fourierswlem  38530  bits0ALTV  39328  0evenALTV  39337  6even  39358  8even  39360  perfectALTVlem1  39363  perfectALTVlem2  39364  perfectALTV  39365  nnsum3primes4  39403  bgoldbtbndlem1  39420  3exp4mod41  39436  41prothprmlem1  39437  41prothprmlem2  39438  41prothprm  39439  elwspths2spth  40571  clwlkclwwlklem2a4  40606  av-numclwwlkovf2ex  40917  0nodd  41000  0even  41121  2even  41123  2zrngamgm  41129  2t6m3t4e0  41319  linevalexample  41378  zlmodzxzequap  41482  3halfnz  41506  pw2m1lepw2m1  41507  nno  41517  nn0o  41518  nnlog2ge0lt1  41566  logbpw2m1  41567  nnpw2blen  41580  nnpw2pmod  41583  blen1  41584  blen2  41585  blennnt2  41589  nnolog2flm1  41590  0dig2nn0e  41612  0dig2nn0o  41613  nn0sumshdiglemA  41619  nn0sumshdiglemB  41620  nn0sumshdiglem1  41621  nn0sumshdiglem2  41622  sinhpcosh  41649
  Copyright terms: Public domain W3C validator