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

Theorem nnzd 10205
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 10107 . 2  |-  ( ph  ->  A  e.  NN0 )
32nn0zd 10204 1  |-  ( ph  ->  A  e.  ZZ )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1710   NNcn 9833   ZZcz 10113
This theorem is referenced by:  expaddzlem  11235  expmulz  11238  expmulnbnd  11323  facndiv  11391  bcval5  11420  bcpasc  11423  hashf1  11485  isercolllem1  12228  isercolllem2  12229  o1fsum  12362  bcxmas  12385  climcndslem2  12400  climcnds  12401  mertenslem1  12431  eftlub  12480  eirrlem  12573  rpnnen2lem7  12590  rpnnen2lem9  12592  rpnnen2lem11  12594  sqr2irrlem  12617  dvdsfac  12674  dvdsmod  12676  bitsfzolem  12716  bitsmod  12718  bitsfi  12719  bitscmp  12720  bitsinv1  12724  sadadd3  12743  sadaddlem  12748  bitsuz  12756  bitsshft  12757  gcd1  12802  bezoutlem3  12810  bezoutlem4  12811  mulgcd  12816  gcdmultiplez  12821  rplpwr  12826  rppwr  12827  sqgcd  12828  dvdssq  12830  prmz  12853  prmind2  12860  isprm6  12879  prmexpb  12887  prmfac1  12888  divgcdodd  12889  rpexp  12890  rpdvds  12894  numdensq  12916  hashdvds  12934  phiprmpw  12935  crt  12937  phimullem  12938  eulerthlem1  12940  eulerthlem2  12941  prmdivdiv  12946  odzdvds  12951  pythagtriplem4  12963  pythagtriplem6  12965  pythagtriplem7  12966  pythagtriplem11  12969  pythagtriplem13  12971  pythagtriplem19  12977  pclem  12982  pcprendvds2  12985  pcpre1  12986  pcpremul  12987  pceulem  12989  pcqmul  12997  pcdvdsb  13012  pcidlem  13015  pcdvdstr  13019  pcgcd1  13020  pc2dvds  13022  pcprmpw2  13025  pcaddlem  13027  pcadd  13028  pcmpt2  13032  pcmptdvds  13033  pcfac  13038  pcbc  13039  qexpz  13040  prmpwdvds  13042  pockthlem  13043  pockthg  13044  prmreclem2  13055  prmreclem3  13056  prmreclem4  13057  prmreclem5  13058  prmreclem6  13059  4sqlem5  13080  4sqlem8  13083  4sqlem9  13084  4sqlem10  13085  4sqlem12  13094  4sqlem14  13096  4sqlem16  13098  4sqlem17  13099  vdwlem1  13119  vdwlem2  13120  vdwlem3  13121  vdwlem6  13124  vdwlem9  13127  vdwlem10  13128  vdwnnlem3  13135  gsumwsubmcl  14554  gsumccat  14557  gsumwmhm  14560  mulgneg  14678  mulgnndir  14682  odlem2  14947  mndodconglem  14949  odmod  14954  gexlem2  14986  gexcl3  14991  gexcl2  14993  sylow1lem1  15002  sylow1lem3  15004  sylow1lem5  15006  pgpfi  15009  fislw  15029  sylow3lem4  15034  gexexlem  15237  ablfacrplem  15393  ablfacrp  15394  ablfacrp2  15395  ablfac1lem  15396  ablfac1b  15398  ablfac1eu  15401  pgpfac1lem3a  15404  ablfaclem3  15415  caublcls  18832  ovolicc2lem4  18977  iundisj2  19004  volsup  19011  uniioombllem3  19038  mbfi1fseqlem3  19170  mbfi1fseqlem4  19171  elqaalem2  19798  aalioulem1  19810  aalioulem4  19813  aalioulem5  19814  aalioulem6  19815  aaliou  19816  aaliou3lem1  19820  aaliou3lem2  19821  aaliou3lem3  19822  aaliou3lem8  19823  aaliou3lem5  19825  aaliou3lem6  19826  aaliou3lem7  19827  taylthlem2  19851  cxpeq  20202  amgmlem  20389  wilthlem2  20413  wilth  20415  ftalem5  20420  basellem2  20425  basellem3  20426  basellem4  20427  basellem5  20428  muval1  20477  dvdssqf  20482  sgmnncl  20491  efchtdvds  20503  mumullem2  20524  mumul  20525  sqff1o  20526  fsumdvdsdiaglem  20529  dvdsppwf1o  20532  dvdsflf1o  20533  muinv  20539  dvdsmulf1o  20540  chtublem  20556  fsumvma2  20559  vmasum  20561  chpchtsum  20564  logfacubnd  20566  mersenne  20572  perfect1  20573  perfectlem1  20574  perfectlem2  20575  perfect  20576  dchrelbas4  20588  dchrfi  20600  bcmono  20622  bcp1ctr  20624  bclbnd  20625  bposlem1  20629  bposlem3  20631  bposlem5  20633  bposlem6  20634  bposlem9  20637  lgsmod  20666  lgsdir  20675  lgsdilem2  20676  lgsne0  20678  lgsqrlem2  20687  lgsqr  20691  lgseisenlem1  20694  lgseisenlem2  20695  lgseisenlem3  20696  lgseisenlem4  20697  lgsquadlem1  20699  lgsquadlem2  20700  lgsquadlem3  20701  lgsquad2lem1  20703  lgsquad2lem2  20704  lgsquad2  20705  m1lgs  20707  2sqlem3  20711  2sqlem4  20712  2sqlem8  20717  chebbnd1lem1  20724  rplogsumlem2  20740  rpvmasumlem  20742  dchrisumlem1  20744  dchrisumlem2  20745  dchrisumlem3  20746  dchrisum0fmul  20761  dchrisum0ff  20762  dchrisum0flblem1  20763  dchrisum0flblem2  20764  dchrisum0flb  20765  dchrisum0  20775  pntrsumbnd2  20822  pntrlog2bndlem1  20832  pntrlog2bndlem6  20838  pntpbnd2  20842  pntlemg  20853  pntlemj  20858  pntlemf  20860  ostth2lem2  20889  ostth2lem3  20890  ostth3  20893  minvecolem4  21567  iundisj2f  23225  ssnnssfz  23347  iundisj2fi  23354  numdenneg  23364  ltesubnnd  23366  qqhval2  23639  qqhf  23643  qqhghm  23645  qqhrhm  23646  qqhnm  23647  qqhre  23653  esumcvg  23742  meascnbl  23837  ballotlemfp1  23998  ballotlemfc0  23999  ballotlemfcc  24000  ballotlemimin  24012  ballotlemic  24013  ballotlem1c  24014  ballotlemsgt1  24017  lgamgulmlem4  24065  lgamcvg2  24088  subfaclim  24123  cvmliftlem7  24226  sinccvglem  24409  fprodser  24576  faclimlem2  24655  faclim2  24659  bpolydiflem  25348  seqpo  25781  incsequz  25782  incsequz2  25783  irrapxlem3  26232  irrapxlem5  26234  pellexlem5  26241  pellexlem6  26242  pellex  26243  pell1234qrmulcl  26263  jm2.23  26412  jm2.20nn  26413  jm2.26lem3  26417  jm2.27a  26421  jm2.27b  26422  jm2.27c  26423  jm3.1lem1  26433  jm3.1lem3  26435  psgnunilem4  26743  hashgcdlem  26839  stirlinglem5  27150  stirlinglem8  27153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-resscn 8881  ax-1cn 8882  ax-icn 8883  ax-addcl 8884  ax-addrcl 8885  ax-mulcl 8886  ax-mulrcl 8887  ax-mulcom 8888  ax-addass 8889  ax-mulass 8890  ax-distr 8891  ax-i2m1 8892  ax-1ne0 8893  ax-1rid 8894  ax-rnegex 8895  ax-rrecex 8896  ax-cnre 8897  ax-pre-lttri 8898  ax-pre-lttrn 8899  ax-pre-ltadd 8900  ax-pre-mulgt0 8901
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-nel 2524  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-iun 3986  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-ov 5945  df-oprab 5946  df-mpt2 5947  df-riota 6388  df-recs 6472  df-rdg 6507  df-er 6744  df-en 6949  df-dom 6950  df-sdom 6951  df-pnf 8956  df-mnf 8957  df-xr 8958  df-ltxr 8959  df-le 8960  df-sub 9126  df-neg 9127  df-nn 9834  df-n0 10055  df-z 10114
  Copyright terms: Public domain W3C validator