Theorem nnzd 9699

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 9553	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	2	nn0zd 9698	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2203  ℕcn 9237  ℤcz 9577

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-pow 4287  ax-pr 4322  ax-un 4554  ax-setind 4659  ax-cnex 8218  ax-resscn 8219  ax-1cn 8220  ax-1re 8221  ax-icn 8222  ax-addcl 8223  ax-addrcl 8224  ax-mulcl 8225  ax-addcom 8227  ax-addass 8229  ax-distr 8231  ax-i2m1 8232  ax-0lt1 8233  ax-0id 8235  ax-rnegex 8236  ax-cnre 8238  ax-pre-ltirr 8239  ax-pre-ltwlin 8240  ax-pre-lttrn 8241  ax-pre-ltadd 8243

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2815  df-sbc 3043  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-pw 3671  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-int 3950  df-br 4110  df-opab 4172  df-id 4414  df-xp 4755  df-rel 4756  df-cnv 4757  df-co 4758  df-dm 4759  df-iota 5312  df-fun 5354  df-fv 5360  df-riota 6003  df-ov 6053  df-oprab 6054  df-mpo 6055  df-pnf 8310  df-mnf 8311  df-xr 8312  df-ltxr 8313  df-le 8314  df-sub 8446  df-neg 8447  df-inn 9238  df-n0 9497  df-z 9578

This theorem is referenced by:  qapne  9971  qtri3or  10600  exbtwnzlemstep  10607  modifeq2int  10748  modsumfzodifsn  10758  addmodlteq  10760  expnnval  10904  expnegap0  10909  expaddzaplem  10944  expmulzap  10947  facndiv  11101  bcval  11111  bcval5  11125  bcpasc  11128  caucvgre  11666  cvg1nlemcau  11669  cvg1nlemres  11670  resqrexlemdecn  11697  resqrexlemnmsq  11702  resqrexlemnm  11703  resqrexlemcvg  11704  resqrexlemoverl  11706  sumeq2  12044  nnf1o  12062  summodclem3  12066  summodclem2a  12067  summodclem2  12068  summodc  12069  zsumdc  12070  fsum3  12073  fisumss  12078  fsum3cvg3  12082  fsumcl2lem  12084  fsumadd  12092  sumsnf  12095  fsummulc2  12134  bcxmas  12175  geo2lim  12202  cvgratnnlembern  12209  cvgratnnlemseq  12212  cvgratnnlemabsle  12213  cvgratnnlemsumlt  12214  cvgratnnlemfm  12215  cvgratnnlemrate  12216  cvgratz  12218  mertenslemub  12220  mertenslemi1  12221  mertenslem2  12222  prodeq2  12243  prodmodclem3  12261  prodmodclem2a  12262  prodmodclem2  12263  fprodseq  12269  fprodssdc  12276  fprodmul  12277  prodsnf  12278  eftcl  12340  eftlub  12376  eirraplem  12463  dvdsle  12530  fzm1ndvds  12542  dvdsfac  12546  dvdsmod  12548  divalglemeunn  12607  bitsfzolem  12640  bitsmod  12642  bitsfi  12643  bitscmp  12644  bitsinv1  12648  gcddvds  12659  gcdnncl  12663  gcd1  12683  dvdsgcdidd  12690  bezoutlemnewy  12692  bezoutlemstep  12693  mulgcd  12712  gcdmultiplez  12717  rplpwr  12723  rppwr  12724  sqgcd  12725  dvdssq  12727  uzwodc  12733  lcmneg  12771  lcmgcdlem  12774  ncoprmgcdne1b  12786  rpdvds  12796  congr  12797  cncongr1  12800  cncongr2  12801  prmz  12808  prmind2  12817  divgcdodd  12840  isprm6  12844  prmexpb  12848  prmfac1  12849  rpexp  12850  sqrt2irrlem  12858  pw2dvdslemn  12862  pw2dvdseulemle  12864  oddpwdclemxy  12866  oddpwdclemodd  12869  sqpweven  12872  2sqpwodd  12873  sqrt2irraplemnn  12876  numdensq  12899  phivalfi  12909  hashdvds  12918  phiprmpw  12919  crth  12921  phimullem  12922  eulerthlem1  12924  eulerthlemfi  12925  eulerthlemrprm  12926  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  eulerth  12930  prmdivdiv  12934  hashgcdlem  12935  hashgcdeq  12937  phisum  12938  odzdvds  12943  powm2modprm  12950  pythagtriplem2  12964  pythagtriplem4  12966  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem11  12972  pythagtriplem13  12974  pythagtriplem16  12977  pythagtriplem19  12980  pythagtrip  12981  pclemub  12985  pcprendvds2  12989  pcpre1  12990  pcpremul  12991  pceulem  12992  pcqmul  13001  pcdvdsb  13018  pcidlem  13021  pcdvdstr  13025  pcgcd1  13026  pc2dvds  13028  pcprmpw2  13031  pcaddlem  13037  pcadd  13038  pcmpt  13041  pcmpt2  13042  pcmptdvds  13043  pcprod  13044  pcfac  13048  pcbc  13049  qexpz  13050  oddprmdvds  13052  prmpwdvds  13053  pockthlem  13054  pockthg  13055  infpnlem2  13058  1arithlem4  13064  1arith  13065  4sqlem5  13080  4sqlem6  13081  4sqlem8  13083  4sqlem9  13084  4sqlem10  13085  4sqlemafi  13093  4sqlemffi  13094  4sqleminfi  13095  4sqlem11  13099  4sqlem12  13100  4sqlem14  13102  4sqlem16  13104  4sqlem17  13105  oddennn  13143  exmidunben  13177  nninfdclemcl  13199  nninfdclemp1  13201  nninfdclemlt  13202  unbendc  13205  bassetsnn  13269  strleund  13316  gsumwsubmcl  13709  gsumwmhm  13711  mulgneg  13857  mulgnndir  13868  znrrg  14808  logbgcd1irraplemexp  15833  logbgcd1irraplemap  15834  sgmnncl  15856  dvdsppwf1o  15857  mpodvdsmulf1o  15858  mersenne  15865  perfect1  15866  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgsfvalg  15878  lgsfcl2  15879  lgsmod  15899  lgsdir  15908  lgsdilem2  15909  lgsne0  15911  gausslemma2dlem0c  15924  gausslemma2dlem0d  15925  gausslemma2dlem0h  15929  gausslemma2dlem0i  15930  gausslemma2dlem1  15934  gausslemma2dlem2  15935  gausslemma2dlem3  15936  gausslemma2dlem4  15937  gausslemma2dlem5a  15938  gausslemma2dlem5  15939  gausslemma2dlem6  15940  gausslemma2dlem7  15941  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgseisen  15947  lgsquadlemsfi  15948  lgsquadlem1  15950  lgsquadlem2  15951  lgsquadlem3  15952  lgsquad2lem1  15954  lgsquad2lem2  15955  lgsquad2  15956  lgsquad3  15957  m1lgs  15958  2lgslem1  15964  2lgslem2  15965  2sqlem3  15990  2sqlem4  15991  2sqlem8  15996  2sqlem9  15997  cvgcmp2nlemabs  16816  trilpolemclim  16820  trilpolemisumle  16822  trilpolemeq1  16824  trilpolemlt1  16825  nconstwlpolemgt0  16850