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

Theorem 2cn 11294
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 11293 . 2 2 ∈ ℝ
21recni 10255 1 2 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2145  cc 10137  2c2 11273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-resscn 10196  ax-1cn 10197  ax-icn 10198  ax-addcl 10199  ax-addrcl 10200  ax-mulcl 10201  ax-mulrcl 10202  ax-i2m1 10207  ax-1ne0 10208  ax-rrecex 10211  ax-cnre 10212
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-iota 5995  df-fv 6040  df-ov 6797  df-2 11282
This theorem is referenced by:  2ex  11295  2cnd  11296  2m1e1  11338  3m1e2  11340  2p2e4  11347  times2  11349  2div2e1  11353  1p2e3  11355  3p3e6  11364  4p3e7  11366  5p3e8  11369  6p3e9  11373  7p3e10OLD  11376  2t1e2  11379  2t2e4  11380  3t3e9  11383  2t0e0  11386  4d2e2  11387  2cnne0  11445  halfcn  11450  1mhlfehlf  11454  8th4div3  11455  halfpm6th  11456  2mulicn  11458  2muline0  11459  halfcl  11460  half0  11462  2halves  11463  halfaddsub  11468  div4p1lem1div2  11490  3halfnz  11659  zneo  11663  nneo  11664  zeo  11666  7p3e10  11805  4t4e16  11835  6t3e18  11844  7t7e49  11855  8t5e40  11859  8t5e40OLD  11860  9t9e81  11872  decbin0  11884  decbin2  11885  halfthird  11887  fztpval  12610  fz0tp  12649  fz0to4untppr  12651  fzo0to3tp  12763  fzo1to4tp  12765  expubnd  13129  sq2  13168  sq4e2t8  13170  cu2  13171  subsq2  13181  binom2sub  13189  binom3  13193  zesq  13195  fac2  13271  fac3  13272  faclbnd2  13283  faclbnd4lem1  13285  faclbnd4lem3  13287  faclbnd4lem4  13288  faclbnd5  13290  bcn2  13311  4bc2eq6  13321  swrd2lsw  13906  crre  14063  addcj  14097  imval2  14100  sqrlem7  14198  absmax  14278  rddif  14289  sqreulem  14308  amgm2  14318  abs3lemi  14358  iseraltlem2  14622  ackbijnn  14768  climcndslem1  14789  climcndslem2  14790  arisum  14800  arisum2  14801  geo2sum2  14813  geo2lim  14814  geoihalfsum  14822  bpoly2  14995  bpoly3  14996  bpoly4  14997  fsumcube  14998  efcllem  15015  ege2le3  15027  efgt0  15040  tanval2  15070  tanval3  15071  efi4p  15074  efival  15089  sinadd  15101  cosadd  15102  sinmul  15109  cos2tsin  15116  ef01bndlem  15121  cos01bnd  15123  cos1bnd  15124  cos2bnd  15125  cos01gt0  15128  sin02gt0  15129  sin4lt0  15132  znnenlem  15147  sqrt2irrlemOLD  15185  odd2np1lem  15273  odd2np1  15274  opoe  15296  omoe  15297  opeo  15298  omeo  15299  nno  15307  nn0o  15308  flodddiv4  15346  bits0  15359  bitsfzolem  15365  0bits  15370  bitsinv1  15373  sadcadd  15389  smumullem  15423  6gcd4e2  15464  3lcm2e6woprm  15537  6lcm4e12  15538  pythagtriplem1  15729  pythagtriplem12  15739  pythagtriplem14  15741  pythagtriplem15  15742  pythagtriplem16  15743  pythagtriplem17  15744  iserodd  15748  prmreclem5  15832  prmreclem6  15833  4sqlem11  15867  4sqlem12  15868  prmo2  15952  prmo3  15953  dec5dvds  15976  dec2nprm  15979  decexp2  15987  2exp6  16003  2exp8  16004  2exp16  16005  7prm  16025  11prm  16030  13prm  16031  37prm  16036  43prm  16037  83prm  16038  139prm  16039  163prm  16040  317prm  16041  631prm  16042  1259lem1  16046  1259lem2  16047  1259lem3  16048  1259lem4  16049  1259lem5  16050  1259prm  16051  2503lem1  16052  2503lem2  16053  2503lem3  16054  4001lem1  16056  4001lem2  16057  4001lem3  16058  4001lem4  16059  4001prm  16060  psgnunilem2  18123  efgtlen  18347  efgredleme  18364  frgpnabllem1  18484  lt6abl  18504  htpycc  23000  pcoval2  23036  pcocn  23037  pcohtpylem  23039  pcopt  23042  pcopt2  23043  pcoass  23044  pcorevlem  23046  csbren  23402  minveclem2  23417  ovolunlem1a  23485  ovolunlem1  23486  vitalilem4  23600  mbfi1fseqlem5  23707  dvmptre  23953  dvsincos  23965  aaliou3lem2  24319  aaliou3lem3  24320  aaliou3lem8  24321  coscn  24420  sinhalfpilem  24437  cospi  24446  ef2pi  24451  ef2kpi  24452  efper  24453  sinperlem  24454  sin2kpi  24457  cos2kpi  24458  sin2pim  24459  cos2pim  24460  sinhalfpip  24466  sinhalfpim  24467  coshalfpip  24468  coshalfpim  24469  sincosq3sgn  24474  sincosq4sgn  24475  tangtx  24479  sinq12gt0  24481  sincosq1eq  24486  sincos4thpi  24487  sincos6thpi  24489  sincos3rdpi  24490  pige3  24491  abssinper  24492  coskpi  24494  sineq0  24495  coseq1  24496  efeq1  24497  efif1olem4  24513  eflogeq  24570  tanarg  24587  cxpsqrtlem  24670  cxpsqrt  24671  logsqrt  24672  root1eq1  24718  cxpeq  24720  ang180lem2  24762  ang180lem3  24763  quad2  24788  1cubrlem  24790  1cubr  24791  dcubic2  24793  dcubic1  24794  dcubic  24795  mcubic  24796  cubic2  24797  cubic  24798  dquartlem1  24800  dquartlem2  24801  dquart  24802  quart1lem  24804  quart1  24805  quartlem1  24806  quartlem2  24807  quartlem3  24808  quart  24810  sinasin  24838  asinsin  24841  atancj  24859  efiatan  24861  efiatan2  24866  2efiatan  24867  tanatan  24868  atantan  24872  atanbndlem  24874  atans2  24880  dvatan  24884  atantayl2  24887  leibpilem1  24889  leibpilem2  24890  log2cnv  24893  log2tlbnd  24894  log2ublem2  24896  log2ublem3  24897  log2ub  24898  birthday  24903  zetacvg  24963  basellem1  25029  basellem3  25031  basellem8  25036  basellem9  25037  cht3  25121  1sgm2ppw  25147  ppiub  25151  chtublem  25158  chtub  25159  perfect1  25175  perfectlem1  25176  perfectlem2  25177  perfect  25178  bcmax  25225  bcp1ctr  25226  bclbnd  25227  bpos1lem  25229  bpos1  25230  bposlem1  25231  bposlem2  25232  bposlem4  25234  bposlem5  25235  bposlem6  25236  bposlem8  25238  bposlem9  25239  lgsdir2lem2  25273  gausslemma2dlem6  25319  lgsquadlem1  25327  lgsquadlem2  25328  lgsquad2lem2  25332  m1lgs  25335  2lgslem3a  25343  2lgslem3b  25344  2lgslem3c  25345  2lgslem3d  25346  2lgsoddprmlem2  25356  2lgsoddprmlem3c  25359  2lgsoddprmlem3d  25360  rplogsumlem1  25395  dchrisum0fno1  25422  dchrisum0lem1  25427  dchrisum0lem2  25429  logdivsum  25444  mulog2sumlem3  25447  log2sumbnd  25455  selberglem1  25456  selberglem2  25457  selberg2  25462  selberg4lem1  25471  selberg3r  25480  pntpbnd1a  25496  pntpbnd2  25498  pntibndlem2  25502  pntlemk  25517  ax5seglem7  26037  axlowdimlem13  26056  elwspths2spth  27117  clwlkclwwlklem2a4  27148  clwwlknonex2  27286  2clwwlk2  27533  numclwlk1lem1  27561  ex-fl  27647  ex-ceil  27648  ex-exp  27650  ex-fac  27651  ex-abs  27655  ex-ind-dvds  27661  ipidsq  27906  cncph  28015  ip0i  28021  ip1ilem  28022  ipdirilem  28025  minvecolem2  28072  hvsubcan2i  28262  norm-ii-i  28335  norm3lem  28347  normpar2i  28354  polid2i  28355  hhph  28376  mayete3i  28928  nmcexi  29226  opsqrlem6  29345  addltmulALT  29646  omssubadd  30703  oddpwdc  30757  fib5  30808  ballotlem2  30891  ballotth  30940  efmul2picn  31015  itgexpif  31025  vtscl  31057  circlemeth  31059  hgt750lemd  31067  logdivsqrle  31069  hgt750lem  31070  hgt750lem2  31071  problem4  31901  problem5  31902  quad3  31903  cnndvlem1  32866  sin2h  33733  cos2h  33734  tan2h  33735  poimirlem29  33772  mblfinlem1  33780  mblfinlem2  33781  mblfinlem3  33782  itg2addnclem3  33796  dvasin  33829  areacirc  33838  heiborlem6  33948  rmxluc  38028  rmyluc  38029  jm2.17a  38054  jm2.18  38082  jm2.23  38090  jm3.1lem1  38111  proot1ex  38306  areaquad  38329  lhe4.4ex1a  39055  sineq0ALT  39696  coskpi2  40596  cosnegpi  40597  cosknegpi  40599  stoweidlem26  40761  wallispilem4  40803  wallispi  40805  wallispi2lem1  40806  stirlinglem8  40816  dirkerper  40831  dirkertrigeqlem3  40835  dirkertrigeq  40836  dirkeritg  40837  dirkercncflem1  40838  dirkercncflem2  40839  fourierdlem57  40898  fourierdlem58  40899  fourierdlem62  40903  fourierdlem76  40917  fourierdlem103  40944  fourierdlem104  40945  sqwvfourb  40964  fourierswlem  40965  fmtnoge3  41971  fmtnorec1  41978  fmtno0  41981  fmtno1  41982  fmtnorec3  41989  fmtnorec4  41990  fmtno5lem2  41995  fmtno5lem4  41997  257prm  42002  fmtnoprmfac2lem1  42007  fmtno4prmfac  42013  fmtno5faclem2  42021  fmtno5faclem3  42022  fmtno5fac  42023  2exp5  42036  139prmALT  42040  31prm  42041  2exp7  42043  127prm  42044  2exp11  42046  mod42tp1mod8  42048  lighneallem2  42052  lighneallem3  42053  lighneallem4a  42054  3exp4mod41  42062  41prothprmlem1  42063  41prothprmlem2  42064  41prothprm  42065  bits0ALTV  42119  0evenALTV  42128  6even  42149  8even  42151  perfectALTVlem1  42159  perfectALTVlem2  42160  perfectALTV  42161  mogoldbb  42202  nnsum3primes4  42205  bgoldbtbndlem1  42222  0nodd  42339  0even  42460  2even  42462  2zrngamgm  42468  2t6m3t4e0  42655  linevalexample  42713  zlmodzxzequap  42817  pw2m1lepw2m1  42839  nnlog2ge0lt1  42889  logbpw2m1  42890  nnpw2blen  42903  nnpw2pmod  42906  blen1  42907  blen2  42908  blennnt2  42912  nnolog2flm1  42913  0dig2nn0e  42935  0dig2nn0o  42936  nn0sumshdiglemA  42942  nn0sumshdiglemB  42943  nn0sumshdiglem1  42944  nn0sumshdiglem2  42945  sinhpcosh  43013
  Copyright terms: Public domain W3C validator