Theorem nnzd 9447

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

Syntax hints:   → wi 4   ∈ wcel 2167  ℕcn 8990  ℤcz 9326

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4151  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-cnex 7970  ax-resscn 7971  ax-1cn 7972  ax-1re 7973  ax-icn 7974  ax-addcl 7975  ax-addrcl 7976  ax-mulcl 7977  ax-addcom 7979  ax-addass 7981  ax-distr 7983  ax-i2m1 7984  ax-0lt1 7985  ax-0id 7987  ax-rnegex 7988  ax-cnre 7990  ax-pre-ltirr 7991  ax-pre-ltwlin 7992  ax-pre-lttrn 7993  ax-pre-ltadd 7995

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-br 4034  df-opab 4095  df-id 4328  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-iota 5219  df-fun 5260  df-fv 5266  df-riota 5877  df-ov 5925  df-oprab 5926  df-mpo 5927  df-pnf 8063  df-mnf 8064  df-xr 8065  df-ltxr 8066  df-le 8067  df-sub 8199  df-neg 8200  df-inn 8991  df-n0 9250  df-z 9327

This theorem is referenced by:  qapne  9713  qtri3or  10330  exbtwnzlemstep  10337  modifeq2int  10478  modsumfzodifsn  10488  addmodlteq  10490  expnnval  10634  expnegap0  10639  expaddzaplem  10674  expmulzap  10677  facndiv  10831  bcval  10841  bcval5  10855  bcpasc  10858  caucvgre  11146  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemdecn  11177  resqrexlemnmsq  11182  resqrexlemnm  11183  resqrexlemcvg  11184  resqrexlemoverl  11186  sumeq2  11524  nnf1o  11541  summodclem3  11545  summodclem2a  11546  summodclem2  11547  summodc  11548  zsumdc  11549  fsum3  11552  fisumss  11557  fsum3cvg3  11561  fsumcl2lem  11563  fsumadd  11571  sumsnf  11574  fsummulc2  11613  bcxmas  11654  geo2lim  11681  cvgratnnlembern  11688  cvgratnnlemseq  11691  cvgratnnlemabsle  11692  cvgratnnlemsumlt  11693  cvgratnnlemfm  11694  cvgratnnlemrate  11695  cvgratz  11697  mertenslemub  11699  mertenslemi1  11700  mertenslem2  11701  prodeq2  11722  prodmodclem3  11740  prodmodclem2a  11741  prodmodclem2  11742  fprodseq  11748  fprodssdc  11755  fprodmul  11756  prodsnf  11757  eftcl  11819  eftlub  11855  eirraplem  11942  dvdsle  12009  fzm1ndvds  12021  dvdsfac  12025  dvdsmod  12027  divalglemeunn  12086  bitsfzolem  12118  gcddvds  12130  gcdnncl  12134  gcd1  12154  dvdsgcdidd  12161  bezoutlemnewy  12163  bezoutlemstep  12164  mulgcd  12183  gcdmultiplez  12188  rplpwr  12194  rppwr  12195  sqgcd  12196  dvdssq  12198  uzwodc  12204  lcmneg  12242  lcmgcdlem  12245  ncoprmgcdne1b  12257  rpdvds  12267  congr  12268  cncongr1  12271  cncongr2  12272  prmz  12279  prmind2  12288  divgcdodd  12311  isprm6  12315  prmexpb  12319  prmfac1  12320  rpexp  12321  sqrt2irrlem  12329  pw2dvdslemn  12333  pw2dvdseulemle  12335  oddpwdclemxy  12337  oddpwdclemodd  12340  sqpweven  12343  2sqpwodd  12344  sqrt2irraplemnn  12347  numdensq  12370  phivalfi  12380  hashdvds  12389  phiprmpw  12390  crth  12392  phimullem  12393  eulerthlem1  12395  eulerthlemfi  12396  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  eulerth  12401  prmdivdiv  12405  hashgcdlem  12406  hashgcdeq  12408  phisum  12409  odzdvds  12414  powm2modprm  12421  pythagtriplem2  12435  pythagtriplem4  12437  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem11  12443  pythagtriplem13  12445  pythagtriplem16  12448  pythagtriplem19  12451  pythagtrip  12452  pclemub  12456  pcprendvds2  12460  pcpre1  12461  pcpremul  12462  pceulem  12463  pcqmul  12472  pcdvdsb  12489  pcidlem  12492  pcdvdstr  12496  pcgcd1  12497  pc2dvds  12499  pcprmpw2  12502  pcaddlem  12508  pcadd  12509  pcmpt  12512  pcmpt2  12513  pcmptdvds  12514  pcprod  12515  pcfac  12519  pcbc  12520  qexpz  12521  oddprmdvds  12523  prmpwdvds  12524  pockthlem  12525  pockthg  12526  infpnlem2  12529  1arithlem4  12535  1arith  12536  4sqlem5  12551  4sqlem6  12552  4sqlem8  12554  4sqlem9  12555  4sqlem10  12556  4sqlemafi  12564  4sqlemffi  12565  4sqleminfi  12566  4sqlem11  12570  4sqlem12  12571  4sqlem14  12573  4sqlem16  12575  4sqlem17  12576  oddennn  12609  exmidunben  12643  nninfdclemcl  12665  nninfdclemp1  12667  nninfdclemlt  12668  unbendc  12671  strleund  12781  gsumwsubmcl  13128  gsumwmhm  13130  mulgneg  13270  mulgnndir  13281  znrrg  14216  logbgcd1irraplemexp  15204  logbgcd1irraplemap  15205  sgmnncl  15224  dvdsppwf1o  15225  mpodvdsmulf1o  15226  mersenne  15233  perfect1  15234  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgsfvalg  15246  lgsfcl2  15247  lgsmod  15267  lgsdir  15276  lgsdilem2  15277  lgsne0  15279  gausslemma2dlem0c  15292  gausslemma2dlem0d  15293  gausslemma2dlem0h  15297  gausslemma2dlem0i  15298  gausslemma2dlem1  15302  gausslemma2dlem2  15303  gausslemma2dlem3  15304  gausslemma2dlem4  15305  gausslemma2dlem5a  15306  gausslemma2dlem5  15307  gausslemma2dlem6  15308  gausslemma2dlem7  15309  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgseisen  15315  lgsquadlemsfi  15316  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem1  15322  lgsquad2lem2  15323  lgsquad2  15324  lgsquad3  15325  m1lgs  15326  2lgslem1  15332  2lgslem2  15333  2sqlem3  15358  2sqlem4  15359  2sqlem8  15364  2sqlem9  15365  cvgcmp2nlemabs  15676  trilpolemclim  15680  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  nconstwlpolemgt0  15708