Theorem nnzd 9376

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℕcn 8921  ℤcz 9255

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7904  ax-resscn 7905  ax-1cn 7906  ax-1re 7907  ax-icn 7908  ax-addcl 7909  ax-addrcl 7910  ax-mulcl 7911  ax-addcom 7913  ax-addass 7915  ax-distr 7917  ax-i2m1 7918  ax-0lt1 7919  ax-0id 7921  ax-rnegex 7922  ax-cnre 7924  ax-pre-ltirr 7925  ax-pre-ltwlin 7926  ax-pre-lttrn 7927  ax-pre-ltadd 7929

This theorem depends on definitions:  df-bi 117  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2741  df-sbc 2965  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-br 4006  df-opab 4067  df-id 4295  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-iota 5180  df-fun 5220  df-fv 5226  df-riota 5833  df-ov 5880  df-oprab 5881  df-mpo 5882  df-pnf 7996  df-mnf 7997  df-xr 7998  df-ltxr 7999  df-le 8000  df-sub 8132  df-neg 8133  df-inn 8922  df-n0 9179  df-z 9256

This theorem is referenced by:  qapne  9641  qtri3or  10245  exbtwnzlemstep  10250  modifeq2int  10388  modsumfzodifsn  10398  addmodlteq  10400  expnnval  10525  expnegap0  10530  expaddzaplem  10565  expmulzap  10568  facndiv  10721  bcval  10731  bcval5  10745  bcpasc  10748  caucvgre  10992  cvg1nlemcau  10995  cvg1nlemres  10996  resqrexlemdecn  11023  resqrexlemnmsq  11028  resqrexlemnm  11029  resqrexlemcvg  11030  resqrexlemoverl  11032  sumeq2  11369  nnf1o  11386  summodclem3  11390  summodclem2a  11391  summodclem2  11392  summodc  11393  zsumdc  11394  fsum3  11397  fisumss  11402  fsum3cvg3  11406  fsumcl2lem  11408  fsumadd  11416  sumsnf  11419  fsummulc2  11458  bcxmas  11499  geo2lim  11526  cvgratnnlembern  11533  cvgratnnlemseq  11536  cvgratnnlemabsle  11537  cvgratnnlemsumlt  11538  cvgratnnlemfm  11539  cvgratnnlemrate  11540  cvgratz  11542  mertenslemub  11544  mertenslemi1  11545  mertenslem2  11546  prodeq2  11567  prodmodclem3  11585  prodmodclem2a  11586  prodmodclem2  11587  fprodseq  11593  fprodssdc  11600  fprodmul  11601  prodsnf  11602  eftcl  11664  eftlub  11700  eirraplem  11786  dvdsle  11852  fzm1ndvds  11864  dvdsfac  11868  dvdsmod  11870  divalglemeunn  11928  gcddvds  11966  gcdnncl  11970  gcd1  11990  dvdsgcdidd  11997  bezoutlemnewy  11999  bezoutlemstep  12000  mulgcd  12019  gcdmultiplez  12024  rplpwr  12030  rppwr  12031  sqgcd  12032  dvdssq  12034  uzwodc  12040  lcmneg  12076  lcmgcdlem  12079  ncoprmgcdne1b  12091  rpdvds  12101  congr  12102  cncongr1  12105  cncongr2  12106  prmz  12113  prmind2  12122  divgcdodd  12145  isprm6  12149  prmexpb  12153  prmfac1  12154  rpexp  12155  sqrt2irrlem  12163  pw2dvdslemn  12167  pw2dvdseulemle  12169  oddpwdclemxy  12171  oddpwdclemodd  12174  sqpweven  12177  2sqpwodd  12178  sqrt2irraplemnn  12181  numdensq  12204  phivalfi  12214  hashdvds  12223  phiprmpw  12224  crth  12226  phimullem  12227  eulerthlem1  12229  eulerthlemfi  12230  eulerthlemrprm  12231  eulerthlema  12232  eulerthlemh  12233  eulerthlemth  12234  eulerth  12235  prmdivdiv  12239  hashgcdlem  12240  hashgcdeq  12241  phisum  12242  odzdvds  12247  powm2modprm  12254  pythagtriplem2  12268  pythagtriplem4  12270  pythagtriplem6  12272  pythagtriplem7  12273  pythagtriplem11  12276  pythagtriplem13  12278  pythagtriplem16  12281  pythagtriplem19  12284  pythagtrip  12285  pclemub  12289  pcprendvds2  12293  pcpre1  12294  pcpremul  12295  pceulem  12296  pcqmul  12305  pcdvdsb  12321  pcidlem  12324  pcdvdstr  12328  pcgcd1  12329  pc2dvds  12331  pcprmpw2  12334  pcaddlem  12340  pcadd  12341  pcmpt  12343  pcmpt2  12344  pcmptdvds  12345  pcprod  12346  pcfac  12350  pcbc  12351  qexpz  12352  oddprmdvds  12354  prmpwdvds  12355  pockthlem  12356  pockthg  12357  infpnlem2  12360  1arithlem4  12366  1arith  12367  4sqlem5  12382  4sqlem6  12383  4sqlem8  12385  4sqlem9  12386  4sqlem10  12387  oddennn  12395  exmidunben  12429  nninfdclemcl  12451  nninfdclemp1  12453  nninfdclemlt  12454  unbendc  12457  strleund  12564  mulgneg  13006  mulgnndir  13017  logbgcd1irraplemexp  14471  logbgcd1irraplemap  14472  lgsfvalg  14491  lgsfcl2  14492  lgsmod  14512  lgsdir  14521  lgsdilem2  14522  lgsne0  14524  lgseisenlem1  14535  lgseisenlem2  14536  m1lgs  14537  2sqlem3  14549  2sqlem4  14550  2sqlem8  14555  2sqlem9  14556  cvgcmp2nlemabs  14865  trilpolemclim  14869  trilpolemisumle  14871  trilpolemeq1  14873  trilpolemlt1  14874  nconstwlpolemgt0  14897