Theorem nnzd 9320

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℕcn 8865  ℤcz 9199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-cnex 7852  ax-resscn 7853  ax-1cn 7854  ax-1re 7855  ax-icn 7856  ax-addcl 7857  ax-addrcl 7858  ax-mulcl 7859  ax-addcom 7861  ax-addass 7863  ax-distr 7865  ax-i2m1 7866  ax-0lt1 7867  ax-0id 7869  ax-rnegex 7870  ax-cnre 7872  ax-pre-ltirr 7873  ax-pre-ltwlin 7874  ax-pre-lttrn 7875  ax-pre-ltadd 7877

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-br 3988  df-opab 4049  df-id 4276  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-iota 5158  df-fun 5198  df-fv 5204  df-riota 5806  df-ov 5853  df-oprab 5854  df-mpo 5855  df-pnf 7943  df-mnf 7944  df-xr 7945  df-ltxr 7946  df-le 7947  df-sub 8079  df-neg 8080  df-inn 8866  df-n0 9123  df-z 9200

This theorem is referenced by:  qapne  9585  qtri3or  10186  exbtwnzlemstep  10191  modifeq2int  10329  modsumfzodifsn  10339  addmodlteq  10341  expnnval  10466  expnegap0  10471  expaddzaplem  10506  expmulzap  10509  facndiv  10660  bcval  10670  bcval5  10684  bcpasc  10687  caucvgre  10932  cvg1nlemcau  10935  cvg1nlemres  10936  resqrexlemdecn  10963  resqrexlemnmsq  10968  resqrexlemnm  10969  resqrexlemcvg  10970  resqrexlemoverl  10972  sumeq2  11309  nnf1o  11326  summodclem3  11330  summodclem2a  11331  summodclem2  11332  summodc  11333  zsumdc  11334  fsum3  11337  fisumss  11342  fsum3cvg3  11346  fsumcl2lem  11348  fsumadd  11356  sumsnf  11359  fsummulc2  11398  bcxmas  11439  geo2lim  11466  cvgratnnlembern  11473  cvgratnnlemseq  11476  cvgratnnlemabsle  11477  cvgratnnlemsumlt  11478  cvgratnnlemfm  11479  cvgratnnlemrate  11480  cvgratz  11482  mertenslemub  11484  mertenslemi1  11485  mertenslem2  11486  prodeq2  11507  prodmodclem3  11525  prodmodclem2a  11526  prodmodclem2  11527  fprodseq  11533  fprodssdc  11540  fprodmul  11541  prodsnf  11542  eftcl  11604  eftlub  11640  eirraplem  11726  dvdsle  11791  fzm1ndvds  11803  dvdsfac  11807  dvdsmod  11809  divalglemeunn  11867  gcddvds  11905  gcdnncl  11909  gcd1  11929  dvdsgcdidd  11936  bezoutlemnewy  11938  bezoutlemstep  11939  mulgcd  11958  gcdmultiplez  11963  rplpwr  11969  rppwr  11970  sqgcd  11971  dvdssq  11973  uzwodc  11979  lcmneg  12015  lcmgcdlem  12018  ncoprmgcdne1b  12030  rpdvds  12040  congr  12041  cncongr1  12044  cncongr2  12045  prmz  12052  prmind2  12061  divgcdodd  12084  isprm6  12088  prmexpb  12092  prmfac1  12093  rpexp  12094  sqrt2irrlem  12102  pw2dvdslemn  12106  pw2dvdseulemle  12108  oddpwdclemxy  12110  oddpwdclemodd  12113  sqpweven  12116  2sqpwodd  12117  sqrt2irraplemnn  12120  numdensq  12143  phivalfi  12153  hashdvds  12162  phiprmpw  12163  crth  12165  phimullem  12166  eulerthlem1  12168  eulerthlemfi  12169  eulerthlemrprm  12170  eulerthlema  12171  eulerthlemh  12172  eulerthlemth  12173  eulerth  12174  prmdivdiv  12178  hashgcdlem  12179  hashgcdeq  12180  phisum  12181  odzdvds  12186  powm2modprm  12193  pythagtriplem2  12207  pythagtriplem4  12209  pythagtriplem6  12211  pythagtriplem7  12212  pythagtriplem11  12215  pythagtriplem13  12217  pythagtriplem16  12220  pythagtriplem19  12223  pythagtrip  12224  pclemub  12228  pcprendvds2  12232  pcpre1  12233  pcpremul  12234  pceulem  12235  pcqmul  12244  pcdvdsb  12260  pcidlem  12263  pcdvdstr  12267  pcgcd1  12268  pc2dvds  12270  pcprmpw2  12273  pcaddlem  12279  pcadd  12280  pcmpt  12282  pcmpt2  12283  pcmptdvds  12284  pcprod  12285  pcfac  12289  pcbc  12290  qexpz  12291  oddprmdvds  12293  prmpwdvds  12294  pockthlem  12295  pockthg  12296  infpnlem2  12299  1arithlem4  12305  1arith  12306  4sqlem5  12321  4sqlem6  12322  4sqlem8  12324  4sqlem9  12325  4sqlem10  12326  oddennn  12334  exmidunben  12368  nninfdclemcl  12390  nninfdclemp1  12392  nninfdclemlt  12393  unbendc  12396  strleund  12493  logbgcd1irraplemexp  13639  logbgcd1irraplemap  13640  lgsfvalg  13659  lgsfcl2  13660  lgsmod  13680  lgsdir  13689  lgsdilem2  13690  lgsne0  13692  2sqlem3  13706  2sqlem4  13707  2sqlem8  13712  2sqlem9  13713  cvgcmp2nlemabs  14024  trilpolemclim  14028  trilpolemisumle  14030  trilpolemeq1  14032  trilpolemlt1  14033  nconstwlpolemgt0  14055