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

Theorem nnzd 10338
Description: A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)
Hypothesis
Ref Expression
nnzd.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnzd  |-  ( ph  ->  A  e.  ZZ )

Proof of Theorem nnzd
StepHypRef Expression
1 nnzd.1 . . 3  |-  ( ph  ->  A  e.  NN )
21nnnn0d 10238 . 2  |-  ( ph  ->  A  e.  NN0 )
32nn0zd 10337 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1721   NNcn 9964   ZZcz 10246
This theorem is referenced by:  expaddzlem  11386  expmulz  11389  expmulnbnd  11474  facndiv  11542  bcval5  11572  bcpasc  11575  hashf1  11669  isercolllem1  12421  isercolllem2  12422  o1fsum  12555  bcxmas  12578  climcndslem2  12593  climcnds  12594  mertenslem1  12624  eftlub  12673  eirrlem  12766  rpnnen2lem7  12783  rpnnen2lem9  12785  rpnnen2lem11  12787  sqr2irrlem  12810  dvdsfac  12867  dvdsmod  12869  bitsfzolem  12909  bitsmod  12911  bitsfi  12912  bitscmp  12913  bitsinv1  12917  sadadd3  12936  sadaddlem  12941  bitsuz  12949  bitsshft  12950  gcd1  12995  bezoutlem3  13003  bezoutlem4  13004  mulgcd  13009  gcdmultiplez  13014  rplpwr  13019  rppwr  13020  sqgcd  13021  dvdssq  13023  prmz  13046  prmind2  13053  isprm6  13072  prmexpb  13080  prmfac1  13081  divgcdodd  13082  rpexp  13083  rpdvds  13087  numdensq  13109  hashdvds  13127  phiprmpw  13128  crt  13130  phimullem  13131  eulerthlem1  13133  eulerthlem2  13134  prmdivdiv  13139  odzdvds  13144  pythagtriplem4  13156  pythagtriplem6  13158  pythagtriplem7  13159  pythagtriplem11  13162  pythagtriplem13  13164  pythagtriplem19  13170  pclem  13175  pcprendvds2  13178  pcpre1  13179  pcpremul  13180  pceulem  13182  pcqmul  13190  pcdvdsb  13205  pcidlem  13208  pcdvdstr  13212  pcgcd1  13213  pc2dvds  13215  pcprmpw2  13218  pcaddlem  13220  pcadd  13221  pcmpt2  13225  pcmptdvds  13226  pcfac  13231  pcbc  13232  qexpz  13233  prmpwdvds  13235  pockthlem  13236  pockthg  13237  prmreclem2  13248  prmreclem3  13249  prmreclem4  13250  prmreclem5  13251  prmreclem6  13252  4sqlem5  13273  4sqlem8  13276  4sqlem9  13277  4sqlem10  13278  4sqlem12  13287  4sqlem14  13289  4sqlem16  13291  4sqlem17  13292  vdwlem1  13312  vdwlem2  13313  vdwlem3  13314  vdwlem6  13317  vdwlem9  13320  vdwlem10  13321  vdwnnlem3  13328  gsumwsubmcl  14747  gsumccat  14750  gsumwmhm  14753  mulgneg  14871  mulgnndir  14875  odlem2  15140  mndodconglem  15142  odmod  15147  gexlem2  15179  gexcl3  15184  gexcl2  15186  sylow1lem1  15195  sylow1lem3  15197  sylow1lem5  15199  pgpfi  15202  fislw  15222  sylow3lem4  15227  gexexlem  15430  ablfacrplem  15586  ablfacrp  15587  ablfacrp2  15588  ablfac1lem  15589  ablfac1b  15591  ablfac1eu  15594  pgpfac1lem3a  15597  ablfaclem3  15608  caublcls  19222  ovolicc2lem4  19377  iundisj2  19404  volsup  19411  uniioombllem3  19438  mbfi1fseqlem3  19570  mbfi1fseqlem4  19571  elqaalem2  20198  aalioulem1  20210  aalioulem4  20213  aalioulem5  20214  aalioulem6  20215  aaliou  20216  aaliou3lem1  20220  aaliou3lem2  20221  aaliou3lem3  20222  aaliou3lem8  20223  aaliou3lem5  20225  aaliou3lem6  20226  aaliou3lem7  20227  taylthlem2  20251  cxpeq  20602  amgmlem  20789  wilthlem2  20813  wilth  20815  ftalem5  20820  basellem2  20825  basellem3  20826  basellem4  20827  basellem5  20828  muval1  20877  dvdssqf  20882  sgmnncl  20891  efchtdvds  20903  mumullem2  20924  mumul  20925  sqff1o  20926  fsumdvdsdiaglem  20929  dvdsppwf1o  20932  dvdsflf1o  20933  muinv  20939  dvdsmulf1o  20940  chtublem  20956  fsumvma2  20959  vmasum  20961  chpchtsum  20964  logfacubnd  20966  mersenne  20972  perfect1  20973  perfectlem1  20974  perfectlem2  20975  perfect  20976  dchrelbas4  20988  dchrfi  21000  bcmono  21022  bcp1ctr  21024  bclbnd  21025  bposlem1  21029  bposlem3  21031  bposlem5  21033  bposlem6  21034  bposlem9  21037  lgsmod  21066  lgsdir  21075  lgsdilem2  21076  lgsne0  21078  lgsqrlem2  21087  lgsqr  21091  lgseisenlem1  21094  lgseisenlem2  21095  lgseisenlem3  21096  lgseisenlem4  21097  lgsquadlem1  21099  lgsquadlem2  21100  lgsquadlem3  21101  lgsquad2lem1  21103  lgsquad2lem2  21104  lgsquad2  21105  m1lgs  21107  2sqlem3  21111  2sqlem4  21112  2sqlem8  21117  chebbnd1lem1  21124  rplogsumlem2  21140  rpvmasumlem  21142  dchrisumlem1  21144  dchrisumlem2  21145  dchrisumlem3  21146  dchrisum0fmul  21161  dchrisum0ff  21162  dchrisum0flblem1  21163  dchrisum0flblem2  21164  dchrisum0flb  21165  dchrisum0  21175  pntrsumbnd2  21222  pntrlog2bndlem1  21232  pntrlog2bndlem6  21238  pntpbnd2  21242  pntlemg  21253  pntlemj  21258  pntlemf  21260  ostth2lem2  21289  ostth2lem3  21290  ostth3  21293  minvecolem4  22343  iundisj2f  23991  ssnnssfz  24109  iundisj2fi  24114  numdenneg  24121  ltesubnnd  24123  isarchi2  24216  qqhval2  24327  qqhf  24331  qqhghm  24333  qqhrhm  24334  qqhnm  24335  qqhre  24347  esumcvg  24437  meascnbl  24534  ballotlemfp1  24710  ballotlemfc0  24711  ballotlemfcc  24712  ballotlemimin  24724  ballotlemic  24725  ballotlem1c  24726  lgamgulmlem4  24777  lgamcvg2  24800  subfaclim  24835  cvmliftlem7  24939  sinccvglem  25070  fprodser  25236  faclimlem2  25319  faclim2  25323  bpolydiflem  26012  mblfinlem  26151  seqpo  26349  incsequz  26350  incsequz2  26351  irrapxlem3  26785  irrapxlem5  26787  pellexlem5  26794  pellexlem6  26795  pellex  26796  pell1234qrmulcl  26816  jm2.23  26965  jm2.20nn  26966  jm2.26lem3  26970  jm2.27a  26974  jm2.27b  26975  jm2.27c  26976  jm3.1lem1  26986  jm3.1lem3  26988  psgnunilem4  27296  hashgcdlem  27392  fmuldfeq  27588  stoweidlem1  27625  stoweidlem3  27627  stoweidlem11  27635  stoweidlem20  27644  stoweidlem26  27650  stoweidlem34  27658  stoweidlem51  27675  stirlinglem4  27701  stirlinglem5  27702  stirlinglem8  27705
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030  ax-pre-mulgt0 9031
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-riota 6516  df-recs 6600  df-rdg 6635  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-pnf 9086  df-mnf 9087  df-xr 9088  df-ltxr 9089  df-le 9090  df-sub 9257  df-neg 9258  df-nn 9965  df-n0 10186  df-z 10247
  Copyright terms: Public domain W3C validator