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

Theorem 2cn 9832
Description: The number 2 is a complex number. (Contributed by NM, 30-Jul-2004.)
Assertion
Ref Expression
2cn  |-  2  e.  CC

Proof of Theorem 2cn
StepHypRef Expression
1 2re 9831 . 2  |-  2  e.  RR
21recni 8865 1  |-  2  e.  CC
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   CCcc 8751   2c2 9811
This theorem is referenced by:  2m1e1  9857  2p2e4  9858  times2  9860  3p3e6  9872  4p3e7  9874  5p3e8  9877  6p3e9  9881  7p3e10  9884  2t2e4  9887  3t3e9  9889  4d2e2  9892  1mhlfehlf  9950  8th4div3  9951  halfpm6th  9952  halfcl  9953  half0  9955  2halves  9956  halfaddsub  9961  addltmul  9963  zneo  10110  nneo  10111  zeo  10113  zeo2  10114  4t4e16  10213  6t3e18  10218  7t7e49  10227  8t5e40  10231  9t9e81  10242  decbin0  10243  decbin2  10244  fztpval  10861  flhalf  10970  expubnd  11178  sq2  11215  cu2  11217  subsq2  11227  binom2sub  11236  binom3  11238  zesq  11240  expmulnbnd  11249  discr  11254  fac2  11310  fac3  11311  faclbnd2  11320  faclbnd4lem1  11322  faclbnd4lem3  11324  faclbnd4lem4  11325  faclbnd5  11327  bcn2  11347  crre  11615  addcj  11649  imval2  11652  sqrlem7  11750  absmax  11829  rddif  11840  sqreulem  11859  amgm2  11869  abs3lemi  11909  iseraltlem2  12171  iseralt  12173  ackbijnn  12302  climcndslem1  12324  climcndslem2  12325  arisum  12334  arisum2  12335  trirecip  12337  geo2sum  12345  geo2sum2  12346  geo2lim  12347  geoihalfsum  12354  efcllem  12375  ege2le3  12387  efgt0  12399  sinf  12420  tanval2  12429  tanval3  12430  efi4p  12433  sinneg  12442  efival  12448  sinhval  12450  tanhlt1  12456  sinadd  12460  cosadd  12461  sinmul  12468  cosmul  12469  cos2tsin  12475  ef01bndlem  12480  sin01bnd  12481  cos01bnd  12482  cos1bnd  12483  cos2bnd  12484  cos01gt0  12487  sin02gt0  12488  sin4lt0  12491  znnenlem  12506  rpnnen2lem3  12511  rpnnen2lem11  12519  sqr2irrlem  12542  sqr2irr  12543  odd2np1lem  12602  odd2np1  12603  oddm1even  12604  oddp1even  12605  bits0  12635  bitsp1o  12640  bitsfzolem  12641  bitsfzo  12642  bitsmod  12643  0bits  12646  bitsinv1lem  12648  bitsinv1  12649  sadadd2lem2  12657  sadcadd  12665  bitsuz  12681  bitsshft  12682  smumullem  12699  3prm  12791  prmdiv  12869  opoe  12880  omoe  12881  opeo  12882  omeo  12883  pythagtriplem1  12885  pythagtriplem4  12888  pythagtriplem12  12895  pythagtriplem14  12897  pythagtriplem15  12898  pythagtriplem16  12899  pythagtriplem17  12900  iserodd  12904  prmreclem5  12983  prmreclem6  12984  4sqlem7  13007  4sqlem10  13010  4sqlem11  13018  4sqlem12  13019  4sqlem19  13026  dec5dvds  13095  dec2nprm  13098  decexp2  13106  2exp6  13117  2exp8  13118  2exp16  13119  2expltfac  13121  prmlem1a  13124  7prm  13128  11prm  13132  13prm  13133  prmlem2  13137  37prm  13138  43prm  13139  83prm  13140  139prm  13141  163prm  13142  317prm  13143  631prm  13144  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem1  13151  2503lem2  13152  2503lem3  13153  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  efgtlen  15051  efgredlemg  15067  efgredleme  15068  frgpnabllem1  15177  lt6abl  15197  metnrmlem3  18381  iihalf1cn  18446  iihalf2cn  18448  htpycc  18494  pco0  18528  pco1  18529  pcoval2  18530  pcocn  18531  pcohtpylem  18533  pcopt  18536  pcopt2  18537  pcoass  18538  pcorevlem  18540  minveclem2  18806  ovolunlem1a  18871  ovolunlem1  18872  uniioombllem5  18958  uniioombl  18960  dyaddisjlem  18966  vitalilem4  18982  mbfi1fseqlem5  19090  mbfi1fseqlem6  19091  dvmptre  19334  dvmptim  19335  dvsincos  19344  lhop1  19377  aaliou3lem2  19739  aaliou3lem3  19740  aaliou3lem8  19741  sincn  19836  coscn  19837  pilem2  19844  sinhalfpilem  19850  cospi  19856  sin2pi  19859  cos2pi  19860  ef2pi  19861  ef2kpi  19862  efper  19863  sinperlem  19864  sin2kpi  19867  cos2kpi  19868  sin2pim  19869  cos2pim  19870  sinhalfpip  19876  sinhalfpim  19877  coshalfpip  19878  coshalfpim  19879  ptolemy  19880  sincosq3sgn  19884  sincosq4sgn  19885  tangtx  19889  sinq12gt0  19891  sincosq1eq  19896  sincos4thpi  19897  sincos6thpi  19899  sincos3rdpi  19900  pige3  19901  abssinper  19902  coskpi  19904  sineq0  19905  coseq1  19906  efeq1  19907  efif1olem4  19923  eflogeq  19971  cosargd  19978  tanarg  19986  cxpsqrlem  20065  cxpsqr  20066  logsqr  20067  dvsqr  20100  root1id  20110  root1eq1  20111  cxpeq  20113  ang180lem2  20124  ang180lem3  20125  pythag  20131  ssscongptld  20138  chordthmlem  20145  chordthmlem2  20146  chordthmlem4  20148  quad2  20151  1cubrlem  20153  1cubr  20154  dcubic1lem  20155  dcubic2  20156  dcubic1  20157  dcubic  20158  mcubic  20159  cubic2  20160  cubic  20161  dquartlem1  20163  dquartlem2  20164  dquart  20165  quart1lem  20167  quart1  20168  quartlem1  20169  quartlem2  20170  quartlem3  20171  quartlem4  20172  quart  20173  sinasin  20201  asinsin  20204  cosasin  20216  atancj  20222  efiatan  20224  efiatan2  20229  2efiatan  20230  tanatan  20231  cosatan  20233  atantan  20235  atanbndlem  20237  atan1  20240  atans2  20243  dvatan  20247  atantayl  20249  atantayl2  20250  atantayl3  20251  leibpilem1  20252  leibpilem2  20253  log2cnv  20256  log2tlbnd  20257  log2ublem2  20259  log2ublem3  20260  log2ub  20261  birthday  20265  cxp2limlem  20286  divsqrsumlem  20290  ftalem2  20327  basellem1  20334  basellem2  20335  basellem3  20336  basellem8  20341  basellem9  20342  ppiprm  20405  ppinprm  20406  chtprm  20407  chtnprm  20408  cht3  20427  1sgm2ppw  20455  ppiub  20459  chtublem  20466  chtub  20467  logfaclbnd  20477  perfect1  20483  perfectlem1  20484  perfectlem2  20485  perfect  20486  bcmax  20533  bcp1ctr  20534  bclbnd  20535  bpos1lem  20537  bpos1  20538  bposlem1  20539  bposlem2  20540  bposlem4  20542  bposlem5  20543  bposlem6  20544  bposlem8  20546  bposlem9  20547  lgslem1  20551  lgslem4  20554  lgsdir2lem2  20579  lgsqrlem2  20597  lgseisenlem1  20604  lgseisenlem2  20605  lgseisenlem3  20606  lgseisenlem4  20607  lgsquadlem1  20609  lgsquadlem2  20610  lgsquad2lem1  20613  lgsquad2lem2  20614  m1lgs  20617  chebbnd1lem1  20634  chebbnd1lem3  20636  chto1ub  20641  rplogsumlem1  20649  dchrisumlem2  20655  dchrisum0flblem2  20674  dchrisum0fno1  20676  dchrisum0lem1b  20680  dchrisum0lem1  20681  dchrisum0lem2  20683  logdivsum  20698  mulog2sumlem2  20700  mulog2sumlem3  20701  vmalogdivsum2  20703  log2sumbnd  20709  selberglem1  20710  selberglem2  20711  selberg2  20716  chpdifbndlem1  20718  selberg3lem1  20722  selberg3  20724  selberg4lem1  20725  selberg4  20726  selberg3r  20734  selberg4r  20735  selberg34r  20736  pntrlog2bndlem3  20744  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  pntpbnd1a  20750  pntpbnd2  20752  pntibndlem2  20756  pntlemg  20763  pntlemh  20764  pntlemk  20771  pntlemo  20772  ostth2lem1  20783  1kp2ke3k  20849  ex-fl  20850  ipidsq  21302  cncph  21413  ip0i  21419  ip1ilem  21420  ipdirilem  21423  minvecolem2  21470  hvsubcan2i  21659  norm-ii-i  21732  norm3lem  21744  normpar2i  21751  polid2i  21752  hhph  21773  mayete3i  22323  mayete3iOLD  22324  nmcexi  22622  opsqrlem6  22741  cdj3lem1  23030  addltmulALT  23042  ballotlem2  23063  ballotth  23112  sqsscirc1  23307  dya2iocress  23592  dya2iocseg  23594  coinflippvt  23700  zetacvg  23704  subfacp1lem1  23725  subfacp1lem5  23730  eupath  23920  konigsberg  23926  4bc2eq6  24114  halfthird  24115  ax5seglem7  24635  axlowdimlem13  24654  axlowdimlem16  24657  axlowdim  24661  bpolydiflem  24861  bpoly2  24864  bpoly3  24865  bpoly4  24866  fsumcube  24867  itg2addnclem  25003  itg2addnc  25005  dvreasin  25026  dvreacos  25027  areacirclem2  25028  areacirclem3  25029  areacirclem1  25031  areacirc  25034  3timesi  25281  2eq3m1  25282  cntrset  25705  mslb1  25710  2wsms  25711  csbrn  26565  trirn  26566  isbnd2  26610  heiborlem6  26643  rabren3dioph  27001  rmxluc  27124  rmyluc  27125  rmyluc2  27126  rmydbl  27128  jm2.17a  27150  jm2.18  27184  jm2.22  27191  jm2.23  27192  jm2.25  27195  jm2.27c  27203  jm3.1lem1  27213  jm3.1lem2  27214  psgnunilem2  27521  proot1ex  27623  lhe4.4ex1a  27649  refsum2cnlem1  27811  m1expeven  27828  itgsinexp  27852  stoweidlem1  27853  stoweidlem13  27865  stoweidlem14  27866  stoweidlem24  27876  stoweidlem26  27878  stoweidlem62  27914  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2lem2  27924  wallispi2  27925  stirlinglem1  27926  stirlinglem3  27928  stirlinglem4  27929  stirlinglem5  27930  stirlinglem6  27931  stirlinglem7  27932  stirlinglem8  27933  stirlinglem10  27935  stirlinglem11  27936  stirlinglem13  27938  stirlinglem14  27939  stirlinglem15  27940  fzo0to3tp  28210  usgraexvlem  28261  wlkntrllem3  28347  wlkdvspthlem  28365  sinhpcosh  28464
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-resscn 8810  ax-1cn 8811  ax-icn 8812  ax-addcl 8813  ax-addrcl 8814  ax-mulcl 8815  ax-mulrcl 8816  ax-i2m1 8821  ax-1ne0 8822  ax-rrecex 8825  ax-cnre 8826
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-2 9820
  Copyright terms: Public domain W3C validator