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

Theorem 2cn 11051
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 11050 . 2 2 ∈ ℝ
21recni 10012 1 2 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  cc 9894  2c2 11030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-i2m1 9964  ax-1ne0 9965  ax-rrecex 9968  ax-cnre 9969
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-iota 5820  df-fv 5865  df-ov 6618  df-2 11039
This theorem is referenced by:  2ex  11052  2cnd  11053  2m1e1  11095  3m1e2  11097  2p2e4  11104  times2  11106  2div2e1  11110  1p2e3  11112  3p3e6  11121  4p3e7  11123  5p3e8  11126  6p3e9  11130  7p3e10OLD  11133  2t1e2  11136  2t2e4  11137  3t3e9  11140  2t0e0  11143  4d2e2  11144  2cnne0  11202  halfcn  11207  1mhlfehlf  11211  8th4div3  11212  halfpm6th  11213  2mulicn  11215  2muline0  11216  halfcl  11217  half0  11219  2halves  11220  halfaddsub  11225  div4p1lem1div2  11247  3halfnz  11416  zneo  11420  nneo  11421  zeo  11423  7p3e10  11563  4t4e16  11593  6t3e18  11602  7t7e49  11613  8t5e40  11617  8t5e40OLD  11618  9t9e81  11630  decbin0  11642  decbin2  11643  halfthird  11645  fztpval  12360  fz0tp  12397  fz0to4untppr  12399  fzo0to3tp  12511  fzo1to4tp  12513  expubnd  12877  sq2  12916  sq4e2t8  12918  cu2  12919  subsq2  12929  binom2sub  12937  binom3  12941  zesq  12943  fac2  13022  fac3  13023  faclbnd2  13034  faclbnd4lem1  13036  faclbnd4lem3  13038  faclbnd4lem4  13039  faclbnd5  13041  bcn2  13062  4bc2eq6  13072  swrd2lsw  13645  crre  13804  addcj  13838  imval2  13841  sqrlem7  13939  absmax  14019  rddif  14030  sqreulem  14049  amgm2  14059  abs3lemi  14099  iseraltlem2  14363  ackbijnn  14504  climcndslem1  14525  climcndslem2  14526  arisum  14536  arisum2  14537  geo2sum2  14549  geo2lim  14550  geoihalfsum  14558  bpoly2  14732  bpoly3  14733  bpoly4  14734  fsumcube  14735  efcllem  14752  ege2le3  14764  efgt0  14777  tanval2  14807  tanval3  14808  efi4p  14811  efival  14826  sinadd  14838  cosadd  14839  sinmul  14846  cos2tsin  14853  ef01bndlem  14858  cos01bnd  14860  cos1bnd  14861  cos2bnd  14862  cos01gt0  14865  sin02gt0  14866  sin4lt0  14869  znnenlem  14884  sqr2irrlem  14921  odd2np1lem  15007  odd2np1  15008  opoe  15030  omoe  15031  opeo  15032  omeo  15033  nno  15041  nn0o  15042  flodddiv4  15080  bits0  15093  bitsfzolem  15099  0bits  15104  bitsinv1  15107  sadcadd  15123  smumullem  15157  6gcd4e2  15198  3lcm2e6woprm  15271  6lcm4e12  15272  pythagtriplem1  15464  pythagtriplem12  15474  pythagtriplem14  15476  pythagtriplem15  15477  pythagtriplem16  15478  pythagtriplem17  15479  iserodd  15483  prmreclem5  15567  prmreclem6  15568  4sqlem11  15602  4sqlem12  15603  prmo2  15687  prmo3  15688  dec5dvds  15711  dec2nprm  15714  decexp2  15722  2exp6  15738  2exp8  15739  2exp16  15740  7prm  15760  11prm  15765  13prm  15766  37prm  15771  43prm  15772  83prm  15773  139prm  15774  163prm  15775  317prm  15776  631prm  15777  1259lem1  15781  1259lem2  15782  1259lem3  15783  1259lem4  15784  1259lem5  15785  1259prm  15786  2503lem1  15787  2503lem2  15788  2503lem3  15789  4001lem1  15791  4001lem2  15792  4001lem3  15793  4001lem4  15794  4001prm  15795  psgnunilem2  17855  efgtlen  18079  efgredleme  18096  frgpnabllem1  18216  lt6abl  18236  htpycc  22719  pcoval2  22756  pcocn  22757  pcohtpylem  22759  pcopt  22762  pcopt2  22763  pcoass  22764  pcorevlem  22766  csbren  23122  minveclem2  23137  ovolunlem1a  23204  ovolunlem1  23205  vitalilem4  23320  mbfi1fseqlem5  23426  dvmptre  23672  dvsincos  23682  aaliou3lem2  24036  aaliou3lem3  24037  aaliou3lem8  24038  coscn  24137  sinhalfpilem  24153  cospi  24162  ef2pi  24167  ef2kpi  24168  efper  24169  sinperlem  24170  sin2kpi  24173  cos2kpi  24174  sin2pim  24175  cos2pim  24176  sinhalfpip  24182  sinhalfpim  24183  coshalfpip  24184  coshalfpim  24185  sincosq3sgn  24190  sincosq4sgn  24191  tangtx  24195  sinq12gt0  24197  sincosq1eq  24202  sincos4thpi  24203  sincos6thpi  24205  sincos3rdpi  24206  pige3  24207  abssinper  24208  coskpi  24210  sineq0  24211  coseq1  24212  efeq1  24213  efif1olem4  24229  eflogeq  24286  tanarg  24303  cxpsqrtlem  24382  cxpsqrt  24383  logsqrt  24384  root1eq1  24430  cxpeq  24432  ang180lem2  24474  ang180lem3  24475  quad2  24500  1cubrlem  24502  1cubr  24503  dcubic2  24505  dcubic1  24506  dcubic  24507  mcubic  24508  cubic2  24509  cubic  24510  dquartlem1  24512  dquartlem2  24513  dquart  24514  quart1lem  24516  quart1  24517  quartlem1  24518  quartlem2  24519  quartlem3  24520  quart  24522  sinasin  24550  asinsin  24553  atancj  24571  efiatan  24573  efiatan2  24578  2efiatan  24579  tanatan  24580  atantan  24584  atanbndlem  24586  atans2  24592  dvatan  24596  atantayl2  24599  leibpilem1  24601  leibpilem2  24602  log2cnv  24605  log2tlbnd  24606  log2ublem2  24608  log2ublem3  24609  log2ub  24610  birthday  24615  zetacvg  24675  basellem1  24741  basellem3  24743  basellem8  24748  basellem9  24749  cht3  24833  1sgm2ppw  24859  ppiub  24863  chtublem  24870  chtub  24871  perfect1  24887  perfectlem1  24888  perfectlem2  24889  perfect  24890  bcmax  24937  bcp1ctr  24938  bclbnd  24939  bpos1lem  24941  bpos1  24942  bposlem1  24943  bposlem2  24944  bposlem4  24946  bposlem5  24947  bposlem6  24948  bposlem8  24950  bposlem9  24951  lgsdir2lem2  24985  gausslemma2dlem6  25031  lgsquadlem1  25039  lgsquadlem2  25040  lgsquad2lem2  25044  m1lgs  25047  2lgslem3a  25055  2lgslem3b  25056  2lgslem3c  25057  2lgslem3d  25058  2lgsoddprmlem2  25068  2lgsoddprmlem3c  25071  2lgsoddprmlem3d  25072  rplogsumlem1  25107  dchrisum0fno1  25134  dchrisum0lem1  25139  dchrisum0lem2  25141  logdivsum  25156  mulog2sumlem3  25159  log2sumbnd  25167  selberglem1  25168  selberglem2  25169  selberg2  25174  selberg4lem1  25183  selberg3r  25192  pntpbnd1a  25208  pntpbnd2  25210  pntibndlem2  25214  pntlemk  25229  ax5seglem7  25749  axlowdimlem13  25768  elwspths2spth  26763  clwlkclwwlklem2a4  26799  numclwwlkovf2ex  27109  ex-fl  27192  ex-ceil  27193  ex-exp  27195  ex-fac  27196  ex-abs  27200  ex-ind-dvds  27206  ipidsq  27453  cncph  27562  ip0i  27568  ip1ilem  27569  ipdirilem  27572  minvecolem2  27619  hvsubcan2i  27809  norm-ii-i  27882  norm3lem  27894  normpar2i  27901  polid2i  27902  hhph  27923  mayete3i  28475  nmcexi  28773  opsqrlem6  28892  addltmulALT  29193  omssubadd  30185  oddpwdc  30239  fib5  30290  ballotlem2  30373  ballotth  30422  itgexpif  30493  problem4  31323  problem5  31324  quad3  31325  cnndvlem1  32223  sin2h  33070  cos2h  33071  tan2h  33072  poimirlem29  33109  mblfinlem1  33117  mblfinlem2  33118  mblfinlem3  33119  itg2addnclem3  33134  dvasin  33167  areacirc  33176  heiborlem6  33286  rmxluc  37020  rmyluc  37021  jm2.17a  37046  jm2.18  37074  jm2.23  37082  jm3.1lem1  37103  proot1ex  37299  areaquad  37322  lhe4.4ex1a  38049  sineq0ALT  38695  coskpi2  39412  cosnegpi  39413  cosknegpi  39415  stoweidlem26  39580  wallispilem4  39622  wallispi  39624  wallispi2lem1  39625  stirlinglem8  39635  dirkerper  39650  dirkertrigeqlem3  39654  dirkertrigeq  39655  dirkeritg  39656  dirkercncflem1  39657  dirkercncflem2  39658  fourierdlem57  39717  fourierdlem58  39718  fourierdlem62  39722  fourierdlem76  39736  fourierdlem103  39763  fourierdlem104  39764  sqwvfourb  39783  fourierswlem  39784  fmtnoge3  40771  fmtnorec1  40778  fmtno0  40781  fmtno1  40782  fmtnorec3  40789  fmtnorec4  40790  fmtno5lem2  40795  fmtno5lem4  40797  257prm  40802  fmtnoprmfac2lem1  40807  fmtno4prmfac  40813  fmtno5faclem2  40821  fmtno5faclem3  40822  fmtno5fac  40823  2exp5  40836  139prmALT  40840  31prm  40841  2exp7  40843  127prm  40844  2exp11  40846  mod42tp1mod8  40848  lighneallem2  40852  lighneallem3  40853  lighneallem4a  40854  3exp4mod41  40862  41prothprmlem1  40863  41prothprmlem2  40864  41prothprm  40865  bits0ALTV  40919  0evenALTV  40928  6even  40949  8even  40951  perfectALTVlem1  40955  perfectALTVlem2  40956  perfectALTV  40957  nnsum3primes4  40995  bgoldbtbndlem1  41012  0nodd  41128  0even  41249  2even  41251  2zrngamgm  41257  2t6m3t4e0  41444  linevalexample  41502  zlmodzxzequap  41606  pw2m1lepw2m1  41628  nnlog2ge0lt1  41682  logbpw2m1  41683  nnpw2blen  41696  nnpw2pmod  41699  blen1  41700  blen2  41701  blennnt2  41705  nnolog2flm1  41706  0dig2nn0e  41728  0dig2nn0o  41729  nn0sumshdiglemA  41735  nn0sumshdiglemB  41736  nn0sumshdiglem1  41737  nn0sumshdiglem2  41738  sinhpcosh  41804
  Copyright terms: Public domain W3C validator