Theorem nnzd 11766

Description: A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nnzd.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnzd	⊢ (𝜑 → 𝐴 ∈ ℤ)

Proof of Theorem nnzd

Step	Hyp	Ref	Expression
1		nnzd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2	1	nnnn0d 11636	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	2	nn0zd 11765	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2157  ℕcn 11314  ℤcz 11662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7188  ax-resscn 10287  ax-1cn 10288  ax-icn 10289  ax-addcl 10290  ax-addrcl 10291  ax-mulcl 10292  ax-mulrcl 10293  ax-mulcom 10294  ax-addass 10295  ax-mulass 10296  ax-distr 10297  ax-i2m1 10298  ax-1ne0 10299  ax-1rid 10300  ax-rnegex 10301  ax-rrecex 10302  ax-cnre 10303  ax-pre-lttri 10304  ax-pre-lttrn 10305  ax-pre-ltadd 10306  ax-pre-mulgt0 10307

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-iun 4725  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5906  df-ord 5952  df-on 5953  df-lim 5954  df-suc 5955  df-iota 6073  df-fun 6112  df-fn 6113  df-f 6114  df-f1 6115  df-fo 6116  df-f1o 6117  df-fv 6118  df-riota 6844  df-ov 6886  df-oprab 6887  df-mpt2 6888  df-om 7305  df-wrecs 7651  df-recs 7713  df-rdg 7751  df-er 7988  df-en 8202  df-dom 8203  df-sdom 8204  df-pnf 10370  df-mnf 10371  df-xr 10372  df-ltxr 10373  df-le 10374  df-sub 10562  df-neg 10563  df-nn 11315  df-n0 11579  df-z 11663

This theorem is referenced by:  expaddzlem  13145  expmulz  13148  expmulnbnd  13238  facndiv  13314  bcval5  13344  bcpasc  13347  hashf1  13477  isercolllem1  14637  isercolllem2  14638  o1fsum  14786  bcxmas  14808  climcndslem2  14823  climcnds  14824  mertenslem1  14856  fprodser  14919  bpolydiflem  15024  eftlub  15078  eirrlem  15171  rpnnen2lem7  15188  rpnnen2lem9  15190  rpnnen2lem11  15192  sqrt2irrlem  15216  sqrt2irrlemOLD  15217  dvdsfac  15290  dvdsmod  15292  oddpwp1fsum  15354  bitsfzolem  15394  bitsmod  15396  bitsfi  15397  bitscmp  15398  bitsinv1  15402  sadadd3  15421  sadaddlem  15426  bitsuz  15434  bitsshft  15435  gcdnncl  15467  gcd1  15487  bezoutlem3  15496  bezoutlem4  15497  mulgcd  15503  gcdmultiplez  15508  rplpwr  15514  rppwr  15515  sqgcd  15516  dvdssq  15518  lcmneg  15554  lcmgcdlem  15557  rpdvds  15611  coprmprod  15612  coprmproddvdslem  15613  congr  15615  cncongr1  15618  cncongr2  15619  prmz  15626  prmind2  15635  divgcdodd  15658  isprm6  15662  prmexpb  15666  prmfac1  15667  rpexp  15668  numdensq  15698  hashdvds  15716  phiprmpw  15717  crth  15719  phimullem  15720  eulerthlem1  15722  eulerthlem2  15723  prmdivdiv  15728  hashgcdlem  15729  odzdvds  15736  pythagtriplem4  15760  pythagtriplem6  15762  pythagtriplem7  15763  pythagtriplem11  15766  pythagtriplem13  15768  pythagtriplem19  15774  pclem  15779  pcprendvds2  15782  pcpre1  15783  pcpremul  15784  pceulem  15786  pcqmul  15794  pcdvdsb  15809  pcidlem  15812  pcdvdstr  15816  pcgcd1  15817  pc2dvds  15819  pcprmpw2  15822  pcaddlem  15828  pcadd  15829  pcmpt2  15833  pcmptdvds  15834  pcfac  15839  pcbc  15840  qexpz  15841  oddprmdvds  15843  prmpwdvds  15844  pockthlem  15845  pockthg  15846  prmreclem2  15857  prmreclem3  15858  prmreclem4  15859  prmreclem5  15860  prmreclem6  15861  4sqlem5  15882  4sqlem8  15885  4sqlem9  15886  4sqlem10  15887  4sqlem12  15896  4sqlem14  15898  4sqlem16  15900  4sqlem17  15901  vdwlem1  15921  vdwlem2  15922  vdwlem3  15923  vdwlem6  15926  vdwlem9  15929  vdwlem10  15930  vdwnnlem3  15937  prmdvdsprmop  15983  prmolelcmf  15988  prmgaplem1  15989  prmgaplem7  15997  prmgaplem8  15998  gsumwsubmcl  17599  gsumccat  17602  gsumwmhm  17606  mulgneg  17783  mulgnndir  17792  psgnunilem4  18137  odlem2  18178  mndodconglem  18180  odmod  18185  gexlem2  18217  gexcl3  18222  gexcl2  18224  sylow1lem1  18233  sylow1lem3  18235  sylow1lem5  18237  pgpfi  18240  fislw  18260  sylow3lem4  18265  gexexlem  18475  ablfacrplem  18685  ablfacrp  18686  ablfacrp2  18687  ablfac1lem  18688  ablfac1b  18690  ablfac1eu  18693  pgpfac1lem3a  18696  ablfaclem3  18707  znrrg  20140  cayhamlem1  20904  caublcls  23340  ovolicc2lem4  23523  iundisj2  23552  volsup  23559  uniioombllem3  23588  mbfi1fseqlem3  23720  mbfi1fseqlem4  23721  elqaalem2  24311  aalioulem1  24323  aalioulem4  24326  aalioulem5  24327  aalioulem6  24328  aaliou  24329  aaliou3lem1  24333  aaliou3lem2  24334  aaliou3lem3  24335  aaliou3lem8  24336  aaliou3lem5  24338  aaliou3lem6  24339  aaliou3lem7  24340  taylthlem2  24364  cxpeq  24734  amgmlem  24952  lgamgulmlem4  24994  lgamcvg2  25017  wilthlem2  25031  wilth  25033  wilthimp  25034  ftalem5  25039  basellem2  25044  basellem3  25045  basellem4  25046  basellem5  25047  muval1  25095  dvdssqf  25100  sgmnncl  25109  efchtdvds  25121  mumullem2  25142  mumul  25143  sqff1o  25144  fsumdvdsdiaglem  25145  dvdsppwf1o  25148  dvdsflf1o  25149  muinv  25155  dvdsmulf1o  25156  chtublem  25172  fsumvma2  25175  vmasum  25177  chpchtsum  25180  logfacubnd  25182  mersenne  25188  perfect1  25189  perfectlem1  25190  perfectlem2  25191  perfect  25192  dchrelbas4  25204  dchrfi  25216  bcmono  25238  bcp1ctr  25240  bclbnd  25241  bposlem1  25245  bposlem3  25247  bposlem5  25249  bposlem6  25250  bposlem9  25253  lgsmod  25284  lgsdir  25293  lgsdilem2  25294  lgsne0  25296  lgsqrlem2  25308  lgsqr  25312  lgsqrmodndvds  25314  gausslemma2dlem0c  25319  gausslemma2dlem0h  25324  gausslemma2dlem0i  25325  gausslemma2dlem2  25328  gausslemma2dlem6  25333  gausslemma2dlem7  25334  gausslemma2d  25335  lgseisenlem1  25336  lgseisenlem2  25337  lgseisenlem3  25338  lgseisenlem4  25339  lgsquadlem1  25341  lgsquadlem2  25342  lgsquadlem3  25343  lgsquad2lem1  25345  lgsquad2lem2  25346  lgsquad2  25347  m1lgs  25349  2lgslem2  25356  2sqlem3  25381  2sqlem4  25382  2sqlem8  25387  chebbnd1lem1  25394  rplogsumlem2  25410  rpvmasumlem  25412  dchrisumlem1  25414  dchrisumlem2  25415  dchrisumlem3  25416  dchrisum0fmul  25431  dchrisum0ff  25432  dchrisum0flblem1  25433  dchrisum0flblem2  25434  dchrisum0flb  25435  dchrisum0  25445  pntrsumbnd2  25492  pntrlog2bndlem1  25502  pntrlog2bndlem6  25508  pntpbnd2  25512  pntlemg  25523  pntlemj  25528  pntlemf  25530  ostth2lem2  25559  ostth2lem3  25560  ostth3  25563  numclwlk2lem2f1o  27581  minvecolem4  28086  iundisj2f  29750  ssnnssfz  29898  iundisj2fi  29905  f1ocnt  29908  numdenneg  29912  ltesubnnd  29917  isarchi3  30088  archiabllem1b  30093  psgnfzto1stlem  30197  smatrcl  30209  1smat1  30217  submateqlem1  30220  submateqlem2  30221  lmatfvlem  30228  qqhval2  30373  qqhf  30377  qqhghm  30379  qqhrhm  30380  qqhnm  30381  qqhre  30411  esumcvg  30495  meascnbl  30629  omssubadd  30709  oddpwdc  30763  ballotlemfp1  30900  ballotlemfc0  30901  ballotlemfcc  30902  ballotlemimin  30914  ballotlemic  30915  ballotlem1c  30916  hgt750lemc  31072  hgt750lemd  31073  hgt750lemb  31081  hgt750leme  31083  subfaclim  31514  cvmliftlem7  31617  sinccvglem  31909  bcprod  31967  bccolsum  31968  faclimlem2  31973  faclim2  31977  poimirlem1  33741  poimirlem2  33742  poimirlem3  33743  poimirlem4  33744  poimirlem6  33746  poimirlem8  33748  poimirlem9  33749  poimirlem10  33750  poimirlem11  33751  poimirlem13  33753  poimirlem14  33754  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem18  33758  poimirlem19  33759  poimirlem20  33760  poimirlem21  33761  poimirlem22  33762  poimirlem23  33763  poimirlem24  33764  poimirlem26  33766  poimirlem27  33767  poimirlem28  33768  poimirlem31  33771  mblfinlem2  33778  seqpo  33872  incsequz  33873  incsequz2  33874  irrapxlem3  37907  irrapxlem5  37909  pellexlem5  37916  pellexlem6  37917  pellex  37918  pell1234qrmulcl  37938  jm2.23  38081  jm2.20nn  38082  jm2.26lem3  38086  jm2.27a  38090  jm2.27b  38091  jm2.27c  38092  jm3.1lem1  38102  jm3.1lem3  38104  inductionexd  38970  nznngen  39032  hashnzfz2  39037  fmuldfeq  40312  divcnvg  40356  stoweidlem1  40714  stoweidlem3  40716  stoweidlem11  40724  stoweidlem20  40733  stoweidlem26  40739  stoweidlem34  40747  stoweidlem51  40764  stirlinglem4  40790  stirlinglem5  40791  stirlinglem8  40794  dirkerper  40809  dirkertrigeqlem2  40812  dirkertrigeqlem3  40813  dirkercncflem2  40817  fourierdlem11  40831  fourierdlem14  40834  fourierdlem20  40840  fourierdlem25  40845  fourierdlem37  40857  fourierdlem41  40861  fourierdlem48  40867  fourierdlem49  40868  fourierdlem54  40873  fourierdlem64  40883  fourierdlem73  40892  fourierdlem79  40898  fourierdlem92  40911  fourierdlem93  40912  fourierdlem111  40930  sqwvfourb  40942  etransclem3  40950  etransclem7  40954  etransclem10  40957  etransclem15  40962  etransclem24  40971  etransclem25  40972  etransclem26  40973  etransclem27  40974  etransclem28  40975  etransclem35  40982  etransclem37  40984  etransclem38  40985  etransclem41  40988  etransclem44  40991  etransclem45  40992  etransclem48  40995  ovnsubaddlem1  41283  vonioolem1  41393  iccpartgtprec  41948  iccpartipre  41949  fmtnoodd  42037  goldbachthlem2  42050  goldbachth  42051  odz2prm2pw  42067  fmtnoprmfac1lem  42068  fmtnoprmfac2lem1  42070  fmtnoprmfac2  42071  fmtnofac2lem  42072  2pwp1prm  42095  lighneallem1  42114  lighneallem4  42119  proththdlem  42122  proththd  42123  divgcdoddALTV  42185  perfectALTVlem1  42222  perfectALTVlem2  42223  perfectALTV  42224  gbowge7  42243  pw2m1lepw2m1  42895  nnolog2flm1  42969  dignn0fr  42980  dignn0flhalflem1  42994