Theorem nnzd 9476

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

Syntax hints:   → wi 4   ∈ wcel 2175  ℕcn 9018  ℤcz 9354

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-13 2177  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-pow 4217  ax-pr 4252  ax-un 4478  ax-setind 4583  ax-cnex 7998  ax-resscn 7999  ax-1cn 8000  ax-1re 8001  ax-icn 8002  ax-addcl 8003  ax-addrcl 8004  ax-mulcl 8005  ax-addcom 8007  ax-addass 8009  ax-distr 8011  ax-i2m1 8012  ax-0lt1 8013  ax-0id 8015  ax-rnegex 8016  ax-cnre 8018  ax-pre-ltirr 8019  ax-pre-ltwlin 8020  ax-pre-lttrn 8021  ax-pre-ltadd 8023

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1375  df-fal 1378  df-nf 1483  df-sb 1785  df-eu 2056  df-mo 2057  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-ne 2376  df-nel 2471  df-ral 2488  df-rex 2489  df-reu 2490  df-rab 2492  df-v 2773  df-sbc 2998  df-dif 3167  df-un 3169  df-in 3171  df-ss 3178  df-pw 3617  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-int 3885  df-br 4044  df-opab 4105  df-id 4338  df-xp 4679  df-rel 4680  df-cnv 4681  df-co 4682  df-dm 4683  df-iota 5229  df-fun 5270  df-fv 5276  df-riota 5889  df-ov 5937  df-oprab 5938  df-mpo 5939  df-pnf 8091  df-mnf 8092  df-xr 8093  df-ltxr 8094  df-le 8095  df-sub 8227  df-neg 8228  df-inn 9019  df-n0 9278  df-z 9355

This theorem is referenced by:  qapne  9742  qtri3or  10364  exbtwnzlemstep  10371  modifeq2int  10512  modsumfzodifsn  10522  addmodlteq  10524  expnnval  10668  expnegap0  10673  expaddzaplem  10708  expmulzap  10711  facndiv  10865  bcval  10875  bcval5  10889  bcpasc  10892  caucvgre  11211  cvg1nlemcau  11214  cvg1nlemres  11215  resqrexlemdecn  11242  resqrexlemnmsq  11247  resqrexlemnm  11248  resqrexlemcvg  11249  resqrexlemoverl  11251  sumeq2  11589  nnf1o  11606  summodclem3  11610  summodclem2a  11611  summodclem2  11612  summodc  11613  zsumdc  11614  fsum3  11617  fisumss  11622  fsum3cvg3  11626  fsumcl2lem  11628  fsumadd  11636  sumsnf  11639  fsummulc2  11678  bcxmas  11719  geo2lim  11746  cvgratnnlembern  11753  cvgratnnlemseq  11756  cvgratnnlemabsle  11757  cvgratnnlemsumlt  11758  cvgratnnlemfm  11759  cvgratnnlemrate  11760  cvgratz  11762  mertenslemub  11764  mertenslemi1  11765  mertenslem2  11766  prodeq2  11787  prodmodclem3  11805  prodmodclem2a  11806  prodmodclem2  11807  fprodseq  11813  fprodssdc  11820  fprodmul  11821  prodsnf  11822  eftcl  11884  eftlub  11920  eirraplem  12007  dvdsle  12074  fzm1ndvds  12086  dvdsfac  12090  dvdsmod  12092  divalglemeunn  12151  bitsfzolem  12184  bitsmod  12186  bitsfi  12187  bitscmp  12188  bitsinv1  12192  gcddvds  12203  gcdnncl  12207  gcd1  12227  dvdsgcdidd  12234  bezoutlemnewy  12236  bezoutlemstep  12237  mulgcd  12256  gcdmultiplez  12261  rplpwr  12267  rppwr  12268  sqgcd  12269  dvdssq  12271  uzwodc  12277  lcmneg  12315  lcmgcdlem  12318  ncoprmgcdne1b  12330  rpdvds  12340  congr  12341  cncongr1  12344  cncongr2  12345  prmz  12352  prmind2  12361  divgcdodd  12384  isprm6  12388  prmexpb  12392  prmfac1  12393  rpexp  12394  sqrt2irrlem  12402  pw2dvdslemn  12406  pw2dvdseulemle  12408  oddpwdclemxy  12410  oddpwdclemodd  12413  sqpweven  12416  2sqpwodd  12417  sqrt2irraplemnn  12420  numdensq  12443  phivalfi  12453  hashdvds  12462  phiprmpw  12463  crth  12465  phimullem  12466  eulerthlem1  12468  eulerthlemfi  12469  eulerthlemrprm  12470  eulerthlema  12471  eulerthlemh  12472  eulerthlemth  12473  eulerth  12474  prmdivdiv  12478  hashgcdlem  12479  hashgcdeq  12481  phisum  12482  odzdvds  12487  powm2modprm  12494  pythagtriplem2  12508  pythagtriplem4  12510  pythagtriplem6  12512  pythagtriplem7  12513  pythagtriplem11  12516  pythagtriplem13  12518  pythagtriplem16  12521  pythagtriplem19  12524  pythagtrip  12525  pclemub  12529  pcprendvds2  12533  pcpre1  12534  pcpremul  12535  pceulem  12536  pcqmul  12545  pcdvdsb  12562  pcidlem  12565  pcdvdstr  12569  pcgcd1  12570  pc2dvds  12572  pcprmpw2  12575  pcaddlem  12581  pcadd  12582  pcmpt  12585  pcmpt2  12586  pcmptdvds  12587  pcprod  12588  pcfac  12592  pcbc  12593  qexpz  12594  oddprmdvds  12596  prmpwdvds  12597  pockthlem  12598  pockthg  12599  infpnlem2  12602  1arithlem4  12608  1arith  12609  4sqlem5  12624  4sqlem6  12625  4sqlem8  12627  4sqlem9  12628  4sqlem10  12629  4sqlemafi  12637  4sqlemffi  12638  4sqleminfi  12639  4sqlem11  12643  4sqlem12  12644  4sqlem14  12646  4sqlem16  12648  4sqlem17  12649  oddennn  12682  exmidunben  12716  nninfdclemcl  12738  nninfdclemp1  12740  nninfdclemlt  12741  unbendc  12744  strleund  12854  gsumwsubmcl  13246  gsumwmhm  13248  mulgneg  13394  mulgnndir  13405  znrrg  14340  logbgcd1irraplemexp  15358  logbgcd1irraplemap  15359  sgmnncl  15378  dvdsppwf1o  15379  mpodvdsmulf1o  15380  mersenne  15387  perfect1  15388  perfectlem1  15389  perfectlem2  15390  perfect  15391  lgsfvalg  15400  lgsfcl2  15401  lgsmod  15421  lgsdir  15430  lgsdilem2  15431  lgsne0  15433  gausslemma2dlem0c  15446  gausslemma2dlem0d  15447  gausslemma2dlem0h  15451  gausslemma2dlem0i  15452  gausslemma2dlem1  15456  gausslemma2dlem2  15457  gausslemma2dlem3  15458  gausslemma2dlem4  15459  gausslemma2dlem5a  15460  gausslemma2dlem5  15461  gausslemma2dlem6  15462  gausslemma2dlem7  15463  gausslemma2d  15464  lgseisenlem1  15465  lgseisenlem2  15466  lgseisenlem3  15467  lgseisenlem4  15468  lgseisen  15469  lgsquadlemsfi  15470  lgsquadlem1  15472  lgsquadlem2  15473  lgsquadlem3  15474  lgsquad2lem1  15476  lgsquad2lem2  15477  lgsquad2  15478  lgsquad3  15479  m1lgs  15480  2lgslem1  15486  2lgslem2  15487  2sqlem3  15512  2sqlem4  15513  2sqlem8  15518  2sqlem9  15519  cvgcmp2nlemabs  15835  trilpolemclim  15839  trilpolemisumle  15841  trilpolemeq1  15843  trilpolemlt1  15844  nconstwlpolemgt0  15867