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

Theorem 2cn 10938
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 10937 . 2 2 ∈ ℝ
21recni 9908 1 2 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  cc 9790  2c2 10917
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-i2m1 9860  ax-1ne0 9861  ax-rrecex 9864  ax-cnre 9865
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 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-iota 5754  df-fv 5798  df-ov 6530  df-2 10926
This theorem is referenced by:  2ex  10939  2cnd  10940  2m1e1  10982  3m1e2  10984  2p2e4  10991  times2  10993  2div2e1  10997  1p2e3  10999  3p3e6  11008  4p3e7  11010  5p3e8  11013  6p3e9  11017  7p3e10OLD  11020  2t1e2  11023  2t2e4  11024  3t3e9  11027  2t0e0  11030  4d2e2  11031  2cnne0  11089  halfcn  11094  1mhlfehlf  11098  8th4div3  11099  halfpm6th  11100  2mulicn  11102  2muline0  11103  halfcl  11104  half0  11106  2halves  11107  halfaddsub  11112  div4p1lem1div2  11134  3halfnz  11288  zneo  11292  nneo  11293  zeo  11295  7p3e10  11435  4t4e16  11465  6t3e18  11474  7t7e49  11485  8t5e40  11489  8t5e40OLD  11490  9t9e81  11502  decbin0  11514  decbin2  11515  halfthird  11517  fztpval  12227  fz0tp  12264  fz0to4untppr  12266  fzo0to3tp  12376  fzo1to4tp  12378  expubnd  12738  sq2  12777  sq4e2t8  12779  cu2  12780  subsq2  12790  binom2sub  12798  binom3  12802  zesq  12804  fac2  12883  fac3  12884  faclbnd2  12895  faclbnd4lem1  12897  faclbnd4lem3  12899  faclbnd4lem4  12900  faclbnd5  12902  bcn2  12923  4bc2eq6  12933  swrd2lsw  13489  crre  13648  addcj  13682  imval2  13685  sqrlem7  13783  absmax  13863  rddif  13874  sqreulem  13893  amgm2  13903  abs3lemi  13943  iseraltlem2  14207  ackbijnn  14345  climcndslem1  14366  climcndslem2  14367  arisum  14377  arisum2  14378  geo2sum2  14390  geo2lim  14391  geoihalfsum  14399  bpoly2  14573  bpoly3  14574  bpoly4  14575  fsumcube  14576  efcllem  14593  ege2le3  14605  efgt0  14618  tanval2  14648  tanval3  14649  efi4p  14652  efival  14667  sinadd  14679  cosadd  14680  sinmul  14687  cos2tsin  14694  ef01bndlem  14699  cos01bnd  14701  cos1bnd  14702  cos2bnd  14703  cos01gt0  14706  sin02gt0  14707  sin4lt0  14710  znnenlem  14725  sqr2irrlem  14762  odd2np1lem  14848  odd2np1  14849  opoe  14871  omoe  14872  opeo  14873  omeo  14874  nno  14882  nn0o  14883  flodddiv4  14921  bits0  14934  bitsfzolem  14940  0bits  14945  bitsinv1  14948  sadcadd  14964  smumullem  14998  6gcd4e2  15039  3lcm2e6woprm  15112  6lcm4e12  15113  pythagtriplem1  15305  pythagtriplem12  15315  pythagtriplem14  15317  pythagtriplem15  15318  pythagtriplem16  15319  pythagtriplem17  15320  iserodd  15324  prmreclem5  15408  prmreclem6  15409  4sqlem11  15443  4sqlem12  15444  prmo2  15528  prmo3  15529  dec5dvds  15552  dec2nprm  15555  decexp2  15563  2exp6  15579  2exp8  15580  2exp16  15581  7prm  15601  11prm  15606  13prm  15607  37prm  15612  43prm  15613  83prm  15614  139prm  15615  163prm  15616  317prm  15617  631prm  15618  1259lem1  15622  1259lem2  15623  1259lem3  15624  1259lem4  15625  1259lem5  15626  1259prm  15627  2503lem1  15628  2503lem2  15629  2503lem3  15630  4001lem1  15632  4001lem2  15633  4001lem3  15634  4001lem4  15635  4001prm  15636  psgnunilem2  17684  efgtlen  17908  efgredleme  17925  frgpnabllem1  18045  lt6abl  18065  htpycc  22518  pcoval2  22555  pcocn  22556  pcohtpylem  22558  pcopt  22561  pcopt2  22562  pcoass  22563  pcorevlem  22565  csbren  22907  minveclem2  22922  ovolunlem1a  22988  ovolunlem1  22989  vitalilem4  23103  mbfi1fseqlem5  23209  dvmptre  23455  dvsincos  23465  aaliou3lem2  23819  aaliou3lem3  23820  aaliou3lem8  23821  coscn  23920  sinhalfpilem  23936  cospi  23945  ef2pi  23950  ef2kpi  23951  efper  23952  sinperlem  23953  sin2kpi  23956  cos2kpi  23957  sin2pim  23958  cos2pim  23959  sinhalfpip  23965  sinhalfpim  23966  coshalfpip  23967  coshalfpim  23968  sincosq3sgn  23973  sincosq4sgn  23974  tangtx  23978  sinq12gt0  23980  sincosq1eq  23985  sincos4thpi  23986  sincos6thpi  23988  sincos3rdpi  23989  pige3  23990  abssinper  23991  coskpi  23993  sineq0  23994  coseq1  23995  efeq1  23996  efif1olem4  24012  eflogeq  24069  tanarg  24086  cxpsqrtlem  24165  cxpsqrt  24166  logsqrt  24167  root1eq1  24213  cxpeq  24215  ang180lem2  24257  ang180lem3  24258  quad2  24283  1cubrlem  24285  1cubr  24286  dcubic2  24288  dcubic1  24289  dcubic  24290  mcubic  24291  cubic2  24292  cubic  24293  dquartlem1  24295  dquartlem2  24296  dquart  24297  quart1lem  24299  quart1  24300  quartlem1  24301  quartlem2  24302  quartlem3  24303  quart  24305  sinasin  24333  asinsin  24336  atancj  24354  efiatan  24356  efiatan2  24361  2efiatan  24362  tanatan  24363  atantan  24367  atanbndlem  24369  atans2  24375  dvatan  24379  atantayl2  24382  leibpilem1  24384  leibpilem2  24385  log2cnv  24388  log2tlbnd  24389  log2ublem2  24391  log2ublem3  24392  log2ub  24393  birthday  24398  zetacvg  24458  basellem1  24524  basellem3  24526  basellem8  24531  basellem9  24532  cht3  24616  1sgm2ppw  24642  ppiub  24646  chtublem  24653  chtub  24654  perfect1  24670  perfectlem1  24671  perfectlem2  24672  perfect  24673  bcmax  24720  bcp1ctr  24721  bclbnd  24722  bpos1lem  24724  bpos1  24725  bposlem1  24726  bposlem2  24727  bposlem4  24729  bposlem5  24730  bposlem6  24731  bposlem8  24733  bposlem9  24734  lgsdir2lem2  24768  gausslemma2dlem6  24814  lgsquadlem1  24822  lgsquadlem2  24823  lgsquad2lem2  24827  m1lgs  24830  2lgslem3a  24838  2lgslem3b  24839  2lgslem3c  24840  2lgslem3d  24841  2lgsoddprmlem2  24851  2lgsoddprmlem3c  24854  2lgsoddprmlem3d  24855  rplogsumlem1  24890  dchrisum0fno1  24917  dchrisum0lem1  24922  dchrisum0lem2  24924  logdivsum  24939  mulog2sumlem3  24942  log2sumbnd  24950  selberglem1  24951  selberglem2  24952  selberg2  24957  selberg4lem1  24966  selberg3r  24975  pntpbnd1a  24991  pntpbnd2  24993  pntibndlem2  24997  pntlemk  25012  ax5seglem7  25533  axlowdimlem13  25552  wlkdvspthlem  25903  clwlkisclwwlklem2a4  26078  numclwwlkovf2ex  26379  ex-fl  26462  ex-ceil  26463  ex-exp  26465  ex-fac  26466  ex-abs  26470  ex-ind-dvds  26476  ipidsq  26753  cncph  26864  ip0i  26870  ip1ilem  26871  ipdirilem  26874  minvecolem2  26921  hvsubcan2i  27111  norm-ii-i  27184  norm3lem  27196  normpar2i  27203  polid2i  27204  hhph  27225  mayete3i  27777  nmcexi  28075  opsqrlem6  28194  addltmulALT  28495  omssubadd  29495  oddpwdc  29549  fib5  29600  ballotlem2  29683  ballotth  29732  problem4  30622  problem5  30623  quad3  30624  cnndvlem1  31504  sin2h  32372  cos2h  32373  tan2h  32374  poimirlem29  32411  mblfinlem1  32419  mblfinlem2  32420  mblfinlem3  32421  itg2addnclem3  32436  dvasin  32469  areacirc  32478  heiborlem6  32588  rmxluc  36322  rmyluc  36323  jm2.17a  36348  jm2.18  36376  jm2.23  36384  jm3.1lem1  36405  proot1ex  36601  areaquad  36624  lhe4.4ex1a  37353  sineq0ALT  37998  coskpi2  38553  cosnegpi  38554  cosknegpi  38556  stoweidlem26  38723  wallispilem4  38765  wallispi  38767  wallispi2lem1  38768  stirlinglem8  38778  dirkerper  38793  dirkertrigeqlem3  38797  dirkertrigeq  38798  dirkeritg  38799  dirkercncflem1  38800  dirkercncflem2  38801  fourierdlem57  38860  fourierdlem58  38861  fourierdlem62  38865  fourierdlem76  38879  fourierdlem103  38906  fourierdlem104  38907  sqwvfourb  38926  fourierswlem  38927  fmtnoge3  39785  fmtnorec1  39792  fmtno0  39795  fmtno1  39796  fmtnorec3  39803  fmtnorec4  39804  fmtno5lem2  39809  fmtno5lem4  39811  257prm  39816  fmtnoprmfac2lem1  39821  fmtno4prmfac  39827  fmtno5faclem2  39835  fmtno5faclem3  39836  fmtno5fac  39837  2exp5  39850  139prmALT  39854  31prm  39855  2exp7  39857  127prm  39858  2exp11  39860  mod42tp1mod8  39862  lighneallem2  39866  lighneallem3  39867  lighneallem4a  39868  3exp4mod41  39876  41prothprmlem1  39877  41prothprmlem2  39878  41prothprm  39879  bits0ALTV  39933  0evenALTV  39942  6even  39963  8even  39965  perfectALTVlem1  39969  perfectALTVlem2  39970  perfectALTV  39971  nnsum3primes4  40009  bgoldbtbndlem1  40026  elwspths2spth  41173  clwlkclwwlklem2a4  41208  av-numclwwlkovf2ex  41519  0nodd  41602  0even  41723  2even  41725  2zrngamgm  41731  2t6m3t4e0  41921  linevalexample  41980  zlmodzxzequap  42084  pw2m1lepw2m1  42106  nnlog2ge0lt1  42160  logbpw2m1  42161  nnpw2blen  42174  nnpw2pmod  42177  blen1  42178  blen2  42179  blennnt2  42183  nnolog2flm1  42184  0dig2nn0e  42206  0dig2nn0o  42207  nn0sumshdiglemA  42213  nn0sumshdiglemB  42214  nn0sumshdiglem1  42215  nn0sumshdiglem2  42216  sinhpcosh  42243
  Copyright terms: Public domain W3C validator