Theorem nnzd 9373

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

Syntax hints:   → wi 4   ∈ wcel 2148  ℕcn 8918  ℤcz 9252

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 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-cnex 7901  ax-resscn 7902  ax-1cn 7903  ax-1re 7904  ax-icn 7905  ax-addcl 7906  ax-addrcl 7907  ax-mulcl 7908  ax-addcom 7910  ax-addass 7912  ax-distr 7914  ax-i2m1 7915  ax-0lt1 7916  ax-0id 7918  ax-rnegex 7919  ax-cnre 7921  ax-pre-ltirr 7922  ax-pre-ltwlin 7923  ax-pre-lttrn 7924  ax-pre-ltadd 7926

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 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4004  df-opab 4065  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-iota 5178  df-fun 5218  df-fv 5224  df-riota 5830  df-ov 5877  df-oprab 5878  df-mpo 5879  df-pnf 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997  df-sub 8129  df-neg 8130  df-inn 8919  df-n0 9176  df-z 9253

This theorem is referenced by:  qapne  9638  qtri3or  10242  exbtwnzlemstep  10247  modifeq2int  10385  modsumfzodifsn  10395  addmodlteq  10397  expnnval  10522  expnegap0  10527  expaddzaplem  10562  expmulzap  10565  facndiv  10718  bcval  10728  bcval5  10742  bcpasc  10745  caucvgre  10989  cvg1nlemcau  10992  cvg1nlemres  10993  resqrexlemdecn  11020  resqrexlemnmsq  11025  resqrexlemnm  11026  resqrexlemcvg  11027  resqrexlemoverl  11029  sumeq2  11366  nnf1o  11383  summodclem3  11387  summodclem2a  11388  summodclem2  11389  summodc  11390  zsumdc  11391  fsum3  11394  fisumss  11399  fsum3cvg3  11403  fsumcl2lem  11405  fsumadd  11413  sumsnf  11416  fsummulc2  11455  bcxmas  11496  geo2lim  11523  cvgratnnlembern  11530  cvgratnnlemseq  11533  cvgratnnlemabsle  11534  cvgratnnlemsumlt  11535  cvgratnnlemfm  11536  cvgratnnlemrate  11537  cvgratz  11539  mertenslemub  11541  mertenslemi1  11542  mertenslem2  11543  prodeq2  11564  prodmodclem3  11582  prodmodclem2a  11583  prodmodclem2  11584  fprodseq  11590  fprodssdc  11597  fprodmul  11598  prodsnf  11599  eftcl  11661  eftlub  11697  eirraplem  11783  dvdsle  11849  fzm1ndvds  11861  dvdsfac  11865  dvdsmod  11867  divalglemeunn  11925  gcddvds  11963  gcdnncl  11967  gcd1  11987  dvdsgcdidd  11994  bezoutlemnewy  11996  bezoutlemstep  11997  mulgcd  12016  gcdmultiplez  12021  rplpwr  12027  rppwr  12028  sqgcd  12029  dvdssq  12031  uzwodc  12037  lcmneg  12073  lcmgcdlem  12076  ncoprmgcdne1b  12088  rpdvds  12098  congr  12099  cncongr1  12102  cncongr2  12103  prmz  12110  prmind2  12119  divgcdodd  12142  isprm6  12146  prmexpb  12150  prmfac1  12151  rpexp  12152  sqrt2irrlem  12160  pw2dvdslemn  12164  pw2dvdseulemle  12166  oddpwdclemxy  12168  oddpwdclemodd  12171  sqpweven  12174  2sqpwodd  12175  sqrt2irraplemnn  12178  numdensq  12201  phivalfi  12211  hashdvds  12220  phiprmpw  12221  crth  12223  phimullem  12224  eulerthlem1  12226  eulerthlemfi  12227  eulerthlemrprm  12228  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  eulerth  12232  prmdivdiv  12236  hashgcdlem  12237  hashgcdeq  12238  phisum  12239  odzdvds  12244  powm2modprm  12251  pythagtriplem2  12265  pythagtriplem4  12267  pythagtriplem6  12269  pythagtriplem7  12270  pythagtriplem11  12273  pythagtriplem13  12275  pythagtriplem16  12278  pythagtriplem19  12281  pythagtrip  12282  pclemub  12286  pcprendvds2  12290  pcpre1  12291  pcpremul  12292  pceulem  12293  pcqmul  12302  pcdvdsb  12318  pcidlem  12321  pcdvdstr  12325  pcgcd1  12326  pc2dvds  12328  pcprmpw2  12331  pcaddlem  12337  pcadd  12338  pcmpt  12340  pcmpt2  12341  pcmptdvds  12342  pcprod  12343  pcfac  12347  pcbc  12348  qexpz  12349  oddprmdvds  12351  prmpwdvds  12352  pockthlem  12353  pockthg  12354  infpnlem2  12357  1arithlem4  12363  1arith  12364  4sqlem5  12379  4sqlem6  12380  4sqlem8  12382  4sqlem9  12383  4sqlem10  12384  oddennn  12392  exmidunben  12426  nninfdclemcl  12448  nninfdclemp1  12450  nninfdclemlt  12451  unbendc  12454  strleund  12561  mulgneg  13000  mulgnndir  13010  logbgcd1irraplemexp  14356  logbgcd1irraplemap  14357  lgsfvalg  14376  lgsfcl2  14377  lgsmod  14397  lgsdir  14406  lgsdilem2  14407  lgsne0  14409  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2sqlem3  14434  2sqlem4  14435  2sqlem8  14440  2sqlem9  14441  cvgcmp2nlemabs  14750  trilpolemclim  14754  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  nconstwlpolemgt0  14781