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

Theorem 2cn 11129
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 11128 . 2 2 ∈ ℝ
21recni 10090 1 2 ∈ ℂ
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  cc 9972  2c2 11108
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-i2m1 10042  ax-1ne0 10043  ax-rrecex 10046  ax-cnre 10047
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-2 11117
This theorem is referenced by:  2ex  11130  2cnd  11131  2m1e1  11173  3m1e2  11175  2p2e4  11182  times2  11184  2div2e1  11188  1p2e3  11190  3p3e6  11199  4p3e7  11201  5p3e8  11204  6p3e9  11208  7p3e10OLD  11211  2t1e2  11214  2t2e4  11215  3t3e9  11218  2t0e0  11221  4d2e2  11222  2cnne0  11280  halfcn  11285  1mhlfehlf  11289  8th4div3  11290  halfpm6th  11291  2mulicn  11293  2muline0  11294  halfcl  11295  half0  11297  2halves  11298  halfaddsub  11303  div4p1lem1div2  11325  3halfnz  11494  zneo  11498  nneo  11499  zeo  11501  7p3e10  11641  4t4e16  11671  6t3e18  11680  7t7e49  11691  8t5e40  11695  8t5e40OLD  11696  9t9e81  11708  decbin0  11720  decbin2  11721  halfthird  11723  fztpval  12440  fz0tp  12479  fz0to4untppr  12481  fzo0to3tp  12594  fzo1to4tp  12596  expubnd  12961  sq2  13000  sq4e2t8  13002  cu2  13003  subsq2  13013  binom2sub  13021  binom3  13025  zesq  13027  fac2  13106  fac3  13107  faclbnd2  13118  faclbnd4lem1  13120  faclbnd4lem3  13122  faclbnd4lem4  13123  faclbnd5  13125  bcn2  13146  4bc2eq6  13156  swrd2lsw  13741  crre  13898  addcj  13932  imval2  13935  sqrlem7  14033  absmax  14113  rddif  14124  sqreulem  14143  amgm2  14153  abs3lemi  14193  iseraltlem2  14457  ackbijnn  14604  climcndslem1  14625  climcndslem2  14626  arisum  14636  arisum2  14637  geo2sum2  14649  geo2lim  14650  geoihalfsum  14658  bpoly2  14832  bpoly3  14833  bpoly4  14834  fsumcube  14835  efcllem  14852  ege2le3  14864  efgt0  14877  tanval2  14907  tanval3  14908  efi4p  14911  efival  14926  sinadd  14938  cosadd  14939  sinmul  14946  cos2tsin  14953  ef01bndlem  14958  cos01bnd  14960  cos1bnd  14961  cos2bnd  14962  cos01gt0  14965  sin02gt0  14966  sin4lt0  14969  znnenlem  14984  sqrt2irrlemOLD  15022  odd2np1lem  15111  odd2np1  15112  opoe  15134  omoe  15135  opeo  15136  omeo  15137  nno  15145  nn0o  15146  flodddiv4  15184  bits0  15197  bitsfzolem  15203  0bits  15208  bitsinv1  15211  sadcadd  15227  smumullem  15261  6gcd4e2  15302  3lcm2e6woprm  15375  6lcm4e12  15376  pythagtriplem1  15568  pythagtriplem12  15578  pythagtriplem14  15580  pythagtriplem15  15581  pythagtriplem16  15582  pythagtriplem17  15583  iserodd  15587  prmreclem5  15671  prmreclem6  15672  4sqlem11  15706  4sqlem12  15707  prmo2  15791  prmo3  15792  dec5dvds  15815  dec2nprm  15818  decexp2  15826  2exp6  15842  2exp8  15843  2exp16  15844  7prm  15864  11prm  15869  13prm  15870  37prm  15875  43prm  15876  83prm  15877  139prm  15878  163prm  15879  317prm  15880  631prm  15881  1259lem1  15885  1259lem2  15886  1259lem3  15887  1259lem4  15888  1259lem5  15889  1259prm  15890  2503lem1  15891  2503lem2  15892  2503lem3  15893  4001lem1  15895  4001lem2  15896  4001lem3  15897  4001lem4  15898  4001prm  15899  psgnunilem2  17961  efgtlen  18185  efgredleme  18202  frgpnabllem1  18322  lt6abl  18342  htpycc  22826  pcoval2  22862  pcocn  22863  pcohtpylem  22865  pcopt  22868  pcopt2  22869  pcoass  22870  pcorevlem  22872  csbren  23228  minveclem2  23243  ovolunlem1a  23310  ovolunlem1  23311  vitalilem4  23425  mbfi1fseqlem5  23531  dvmptre  23777  dvsincos  23789  aaliou3lem2  24143  aaliou3lem3  24144  aaliou3lem8  24145  coscn  24244  sinhalfpilem  24260  cospi  24269  ef2pi  24274  ef2kpi  24275  efper  24276  sinperlem  24277  sin2kpi  24280  cos2kpi  24281  sin2pim  24282  cos2pim  24283  sinhalfpip  24289  sinhalfpim  24290  coshalfpip  24291  coshalfpim  24292  sincosq3sgn  24297  sincosq4sgn  24298  tangtx  24302  sinq12gt0  24304  sincosq1eq  24309  sincos4thpi  24310  sincos6thpi  24312  sincos3rdpi  24313  pige3  24314  abssinper  24315  coskpi  24317  sineq0  24318  coseq1  24319  efeq1  24320  efif1olem4  24336  eflogeq  24393  tanarg  24410  cxpsqrtlem  24493  cxpsqrt  24494  logsqrt  24495  root1eq1  24541  cxpeq  24543  ang180lem2  24585  ang180lem3  24586  quad2  24611  1cubrlem  24613  1cubr  24614  dcubic2  24616  dcubic1  24617  dcubic  24618  mcubic  24619  cubic2  24620  cubic  24621  dquartlem1  24623  dquartlem2  24624  dquart  24625  quart1lem  24627  quart1  24628  quartlem1  24629  quartlem2  24630  quartlem3  24631  quart  24633  sinasin  24661  asinsin  24664  atancj  24682  efiatan  24684  efiatan2  24689  2efiatan  24690  tanatan  24691  atantan  24695  atanbndlem  24697  atans2  24703  dvatan  24707  atantayl2  24710  leibpilem1  24712  leibpilem2  24713  log2cnv  24716  log2tlbnd  24717  log2ublem2  24719  log2ublem3  24720  log2ub  24721  birthday  24726  zetacvg  24786  basellem1  24852  basellem3  24854  basellem8  24859  basellem9  24860  cht3  24944  1sgm2ppw  24970  ppiub  24974  chtublem  24981  chtub  24982  perfect1  24998  perfectlem1  24999  perfectlem2  25000  perfect  25001  bcmax  25048  bcp1ctr  25049  bclbnd  25050  bpos1lem  25052  bpos1  25053  bposlem1  25054  bposlem2  25055  bposlem4  25057  bposlem5  25058  bposlem6  25059  bposlem8  25061  bposlem9  25062  lgsdir2lem2  25096  gausslemma2dlem6  25142  lgsquadlem1  25150  lgsquadlem2  25151  lgsquad2lem2  25155  m1lgs  25158  2lgslem3a  25166  2lgslem3b  25167  2lgslem3c  25168  2lgslem3d  25169  2lgsoddprmlem2  25179  2lgsoddprmlem3c  25182  2lgsoddprmlem3d  25183  rplogsumlem1  25218  dchrisum0fno1  25245  dchrisum0lem1  25250  dchrisum0lem2  25252  logdivsum  25267  mulog2sumlem3  25270  log2sumbnd  25278  selberglem1  25279  selberglem2  25280  selberg2  25285  selberg4lem1  25294  selberg3r  25303  pntpbnd1a  25319  pntpbnd2  25321  pntibndlem2  25325  pntlemk  25340  ax5seglem7  25860  axlowdimlem13  25879  elwspths2spth  26934  clwlkclwwlklem2a4  26963  clwwlknonex2  27084  2clwwlk2  27336  ex-fl  27434  ex-ceil  27435  ex-exp  27437  ex-fac  27438  ex-abs  27442  ex-ind-dvds  27448  ipidsq  27693  cncph  27802  ip0i  27808  ip1ilem  27809  ipdirilem  27812  minvecolem2  27859  hvsubcan2i  28049  norm-ii-i  28122  norm3lem  28134  normpar2i  28141  polid2i  28142  hhph  28163  mayete3i  28715  nmcexi  29013  opsqrlem6  29132  addltmulALT  29433  omssubadd  30490  oddpwdc  30544  fib5  30595  ballotlem2  30678  ballotth  30727  efmul2picn  30802  itgexpif  30812  vtscl  30844  circlemeth  30846  hgt750lemd  30854  logdivsqrle  30856  hgt750lem  30857  hgt750lem2  30858  problem4  31688  problem5  31689  quad3  31690  cnndvlem1  32653  sin2h  33529  cos2h  33530  tan2h  33531  poimirlem29  33568  mblfinlem1  33576  mblfinlem2  33577  mblfinlem3  33578  itg2addnclem3  33593  dvasin  33626  areacirc  33635  heiborlem6  33745  rmxluc  37818  rmyluc  37819  jm2.17a  37844  jm2.18  37872  jm2.23  37880  jm3.1lem1  37901  proot1ex  38096  areaquad  38119  lhe4.4ex1a  38845  sineq0ALT  39487  coskpi2  40395  cosnegpi  40396  cosknegpi  40398  stoweidlem26  40561  wallispilem4  40603  wallispi  40605  wallispi2lem1  40606  stirlinglem8  40616  dirkerper  40631  dirkertrigeqlem3  40635  dirkertrigeq  40636  dirkeritg  40637  dirkercncflem1  40638  dirkercncflem2  40639  fourierdlem57  40698  fourierdlem58  40699  fourierdlem62  40703  fourierdlem76  40717  fourierdlem103  40744  fourierdlem104  40745  sqwvfourb  40764  fourierswlem  40765  fmtnoge3  41767  fmtnorec1  41774  fmtno0  41777  fmtno1  41778  fmtnorec3  41785  fmtnorec4  41786  fmtno5lem2  41791  fmtno5lem4  41793  257prm  41798  fmtnoprmfac2lem1  41803  fmtno4prmfac  41809  fmtno5faclem2  41817  fmtno5faclem3  41818  fmtno5fac  41819  2exp5  41832  139prmALT  41836  31prm  41837  2exp7  41839  127prm  41840  2exp11  41842  mod42tp1mod8  41844  lighneallem2  41848  lighneallem3  41849  lighneallem4a  41850  3exp4mod41  41858  41prothprmlem1  41859  41prothprmlem2  41860  41prothprm  41861  bits0ALTV  41915  0evenALTV  41924  6even  41945  8even  41947  perfectALTVlem1  41955  perfectALTVlem2  41956  perfectALTV  41957  mogoldbb  41998  nnsum3primes4  42001  bgoldbtbndlem1  42018  0nodd  42135  0even  42256  2even  42258  2zrngamgm  42264  2t6m3t4e0  42451  linevalexample  42509  zlmodzxzequap  42613  pw2m1lepw2m1  42635  nnlog2ge0lt1  42685  logbpw2m1  42686  nnpw2blen  42699  nnpw2pmod  42702  blen1  42703  blen2  42704  blennnt2  42708  nnolog2flm1  42709  0dig2nn0e  42731  0dig2nn0o  42732  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739  nn0sumshdiglem1  42740  nn0sumshdiglem2  42741  sinhpcosh  42809
  Copyright terms: Public domain W3C validator