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

Theorem nn0cnd 10879
Description: A nonnegative integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nn0red.1
Assertion
Ref Expression
nn0cnd

Proof of Theorem nn0cnd
StepHypRef Expression
1 nn0red.1 . . 3
21nn0red 10878 . 2
32recnd 9643 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818   cc 9511   cn0 10820
This theorem is referenced by:  quoremnn0ALT  11984  expaddzlem  12209  expaddz  12210  expmulz  12212  facdiv  12365  faclbnd4lem3  12373  bcp1n  12394  bcn2m1  12402  bcn2p1  12403  hashgadd  12445  hashdom  12447  hashun3  12452  hashssdif  12475  hashxplem  12491  hashmap  12493  hashbclem  12501  hashf1lem2  12505  hashf1  12506  ccatcl  12593  ccatval3  12597  ccatlid  12603  ccatrid  12604  ccatass  12605  ccatrn  12606  lswccat0lsw  12608  wrdlenccats1lenm1  12627  ccats1val2  12631  ccatws1lenrev  12635  ccatw2s1p1  12640  swrdid  12652  addlenswrd  12662  swrdtrcfvl  12675  swrdccat2  12683  ccatopth2  12696  cats1un  12701  swrdccat3b  12721  spllen  12730  splfv2a  12732  revccat  12740  cshwlen  12770  cshwidxmod  12774  repswcshw  12780  2cshwid  12782  cshweqdif2  12787  isercoll2  13491  iseraltlem3  13506  binomlem  13641  bcxmas  13647  incexclem  13648  incexc  13649  incexc2  13650  climcndslem1  13661  climcndslem2  13662  arisum  13671  arisum2  13672  geomulcvg  13685  mertens  13695  effsumlt  13846  dvdsexp  14042  divalgmod  14064  bitsinv1lem  14091  sadcp1  14105  sadcaddlem  14107  sadadd2lem  14109  sadadd3  14111  sadaddlem  14116  sadasslem  14120  smupp1  14130  smumullem  14142  mulgcd  14184  absmulgcd  14185  mulgcdr  14186  gcddiv  14187  mulgcddvds  14245  qredeu  14248  odzdvds  14322  powm2modprm  14328  coprimeprodsq  14333  pceulem  14369  pczpre  14371  pcqmul  14377  pcaddlem  14407  pcmpt  14411  pcmpt2  14412  sumhash  14415  mul4sq  14472  4sqlem12  14474  vdwapun  14492  vdwlem2  14500  vdwlem3  14501  vdwlem6  14504  vdwlem8  14506  vdwlem9  14507  ramub1lem2  14545  ramcl  14547  mulgnn0dir  16165  mulgnn0ass  16171  lagsubg2  16262  psgnunilem2  16520  odmodnn0  16564  odmulg  16578  odmulgeq  16579  odinv  16583  sylow1lem1  16618  sylow2a  16639  sylow2blem3  16642  sylow3lem3  16649  sylow3lem4  16650  efginvrel2  16745  efgsval2  16751  efgsp1  16755  efgredlemg  16760  efgredleme  16761  efgcpbllemb  16773  odadd2  16855  odadd  16856  torsubg  16860  frgpnabllem1  16877  pgpfaclem1  17132  srgbinomlem3  17193  srgbinomlem4  17194  mplcoe5  18131  mplcoe2OLD  18133  coe1tmmul2  18317  coe1tmmul2fv  18319  coe1pwmulfv  18321  nn0srg  18486  mbfi1fseqlem3  22124  dvn2bss  22333  tdeglem4  22458  tdeglem2  22459  mdegmullem  22478  coe1mul3  22500  ply1divex  22537  fta1glem1  22566  plyaddlem1  22610  plymullem1  22611  coeeulem  22621  coemulc  22652  dgrmulc  22668  dgrcolem2  22671  dgrco  22672  dvply1  22680  dvply2g  22681  plydivlem4  22692  fta1lem  22703  vieta1lem1  22706  aareccl  22722  aaliou3lem8  22741  taylply2  22763  dvtaylp  22765  dvntaylp  22766  dvntaylp0  22767  dvradcnv  22816  pserdvlem2  22823  advlogexp  23036  cxpeq  23131  atantayl3  23270  birthdaylem2  23282  harmonicbnd4  23340  wilthlem2  23343  basellem2  23355  basellem3  23356  basellem5  23358  0sgm  23418  sgmppw  23472  chtublem  23486  chpval2  23493  sumdchr2  23545  bcp1ctr  23554  lgslem1  23571  lgseisenlem2  23625  lgseisenlem3  23626  lgsquadlem1  23629  lgsquadlem2  23630  lgsquad2lem2  23634  m1lgs  23637  2sqlem8  23647  dchrisumlem1  23674  dchrisum0flblem2  23694  rpvmasum2  23697  mulogsumlem  23716  selberg2lem  23735  pntrsumo1  23750  pntrlog2bndlem4  23765  cusgrasizeinds  24476  wlklniswwlkn2  24700  wwlknred  24723  wwlknext  24724  wwlknextbi  24725  wwlknredwwlkn  24726  wwlkextproplem2  24742  clwlkisclwwlk  24789  vdgrfiun  24902  nbhashuvtx1  24915  eupath2lem3  24979  frghash2spot  25063  usgreghash2spotv  25066  frgregordn0  25070  numclwwlk3  25109  ex-ind-dvds  25170  divnumden2  27609  2sqmod  27636  omndmul2  27702  omndmul3  27703  archiabllem1a  27735  oddpwdc  28293  eulerpartlemsv2  28297  eulerpartlems  28299  eulerpartlemsv3  28300  eulerpartlemv  28303  eulerpartlemb  28307  iwrdsplit  28326  ballotlemgun  28463  ccatmulgnn0dir  28496  ofcccat  28498  signsplypnf  28507  signslema  28519  signstfvn  28526  signstfveq0  28534  signsvtp  28540  signsvtn  28541  signlem0  28544  signshf  28545  dmgmaddnn0  28569  lgamucov  28580  subfacp1lem6  28629  subfacval2  28631  subfaclim  28632  cvmliftlem7  28736  elmrsubrn  28880  relexpadd  29061  rtrclreclem.trans  29069  risefacval2  29132  fallfacval2  29133  fallfacval3  29134  risefallfac  29146  risefacp1  29151  fallfacp1  29152  fallfacfwd  29158  binomfallfaclem1  29161  binomfallfaclem2  29162  binomrisefac  29164  faclimlem1  29168  faclim2  29173  bpolycl  29814  bpolysum  29815  bpolydiflem  29816  fsumkthpow  29818  bpoly4  29821  rmxyneg  30856  rmxyadd  30857  rmyp1  30869  rmxm1  30870  rmym1  30871  rmxluc  30872  rmyluc  30873  rmxdbl  30875  rmydbl  30876  jm2.18  30930  jm2.19lem1  30931  jm2.19lem2  30932  jm2.22  30937  jm2.23  30938  jm2.25  30941  jm2.27c  30949  rmxdiophlem  30957  expdioph  30965  hbtlem4  31075  itgpowd  31182  radcnvrat  31195  lcmgcd  31213  lcmid  31215  nzprmdif  31224  bcc0  31245  bccp1k  31246  bccbc  31250  binomcxplemnn0  31254  binomcxplemrat  31255  binomcxplemfrat  31256  binomcxplemnotnn0  31261  fzisoeu  31500  mccllem  31605  dvxpaek  31737  dvnxpaek  31739  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  stoweidlem24  31806  stirlinglem3  31858  stirlinglem7  31862  fourierdlem36  31925  fourierdlem47  31936  etransclem23  32040  etransclem32  32049  etransclem48  32065  fz0addcom  32333  altgsumbc  32941  altgsumbcALT  32942  aacllem  33216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-i2m1 9581  ax-1ne0 9582  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-om 6701  df-recs 7061  df-rdg 7095  df-nn 10562  df-n0 10821
  Copyright terms: Public domain W3C validator