Theorem nnzd 9441

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

Syntax hints:   → wi 4   ∈ wcel 2164  ℕcn 8984  ℤcz 9320

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4148  ax-pow 4204  ax-pr 4239  ax-un 4465  ax-setind 4570  ax-cnex 7965  ax-resscn 7966  ax-1cn 7967  ax-1re 7968  ax-icn 7969  ax-addcl 7970  ax-addrcl 7971  ax-mulcl 7972  ax-addcom 7974  ax-addass 7976  ax-distr 7978  ax-i2m1 7979  ax-0lt1 7980  ax-0id 7982  ax-rnegex 7983  ax-cnre 7985  ax-pre-ltirr 7986  ax-pre-ltwlin 7987  ax-pre-lttrn 7988  ax-pre-ltadd 7990

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-reu 2479  df-rab 2481  df-v 2762  df-sbc 2987  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-pw 3604  df-sn 3625  df-pr 3626  df-op 3628  df-uni 3837  df-int 3872  df-br 4031  df-opab 4092  df-id 4325  df-xp 4666  df-rel 4667  df-cnv 4668  df-co 4669  df-dm 4670  df-iota 5216  df-fun 5257  df-fv 5263  df-riota 5874  df-ov 5922  df-oprab 5923  df-mpo 5924  df-pnf 8058  df-mnf 8059  df-xr 8060  df-ltxr 8061  df-le 8062  df-sub 8194  df-neg 8195  df-inn 8985  df-n0 9244  df-z 9321

This theorem is referenced by:  qapne  9707  qtri3or  10313  exbtwnzlemstep  10319  modifeq2int  10460  modsumfzodifsn  10470  addmodlteq  10472  expnnval  10616  expnegap0  10621  expaddzaplem  10656  expmulzap  10659  facndiv  10813  bcval  10823  bcval5  10837  bcpasc  10840  caucvgre  11128  cvg1nlemcau  11131  cvg1nlemres  11132  resqrexlemdecn  11159  resqrexlemnmsq  11164  resqrexlemnm  11165  resqrexlemcvg  11166  resqrexlemoverl  11168  sumeq2  11505  nnf1o  11522  summodclem3  11526  summodclem2a  11527  summodclem2  11528  summodc  11529  zsumdc  11530  fsum3  11533  fisumss  11538  fsum3cvg3  11542  fsumcl2lem  11544  fsumadd  11552  sumsnf  11555  fsummulc2  11594  bcxmas  11635  geo2lim  11662  cvgratnnlembern  11669  cvgratnnlemseq  11672  cvgratnnlemabsle  11673  cvgratnnlemsumlt  11674  cvgratnnlemfm  11675  cvgratnnlemrate  11676  cvgratz  11678  mertenslemub  11680  mertenslemi1  11681  mertenslem2  11682  prodeq2  11703  prodmodclem3  11721  prodmodclem2a  11722  prodmodclem2  11723  fprodseq  11729  fprodssdc  11736  fprodmul  11737  prodsnf  11738  eftcl  11800  eftlub  11836  eirraplem  11923  dvdsle  11989  fzm1ndvds  12001  dvdsfac  12005  dvdsmod  12007  divalglemeunn  12065  gcddvds  12103  gcdnncl  12107  gcd1  12127  dvdsgcdidd  12134  bezoutlemnewy  12136  bezoutlemstep  12137  mulgcd  12156  gcdmultiplez  12161  rplpwr  12167  rppwr  12168  sqgcd  12169  dvdssq  12171  uzwodc  12177  lcmneg  12215  lcmgcdlem  12218  ncoprmgcdne1b  12230  rpdvds  12240  congr  12241  cncongr1  12244  cncongr2  12245  prmz  12252  prmind2  12261  divgcdodd  12284  isprm6  12288  prmexpb  12292  prmfac1  12293  rpexp  12294  sqrt2irrlem  12302  pw2dvdslemn  12306  pw2dvdseulemle  12308  oddpwdclemxy  12310  oddpwdclemodd  12313  sqpweven  12316  2sqpwodd  12317  sqrt2irraplemnn  12320  numdensq  12343  phivalfi  12353  hashdvds  12362  phiprmpw  12363  crth  12365  phimullem  12366  eulerthlem1  12368  eulerthlemfi  12369  eulerthlemrprm  12370  eulerthlema  12371  eulerthlemh  12372  eulerthlemth  12373  eulerth  12374  prmdivdiv  12378  hashgcdlem  12379  hashgcdeq  12380  phisum  12381  odzdvds  12386  powm2modprm  12393  pythagtriplem2  12407  pythagtriplem4  12409  pythagtriplem6  12411  pythagtriplem7  12412  pythagtriplem11  12415  pythagtriplem13  12417  pythagtriplem16  12420  pythagtriplem19  12423  pythagtrip  12424  pclemub  12428  pcprendvds2  12432  pcpre1  12433  pcpremul  12434  pceulem  12435  pcqmul  12444  pcdvdsb  12461  pcidlem  12464  pcdvdstr  12468  pcgcd1  12469  pc2dvds  12471  pcprmpw2  12474  pcaddlem  12480  pcadd  12481  pcmpt  12484  pcmpt2  12485  pcmptdvds  12486  pcprod  12487  pcfac  12491  pcbc  12492  qexpz  12493  oddprmdvds  12495  prmpwdvds  12496  pockthlem  12497  pockthg  12498  infpnlem2  12501  1arithlem4  12507  1arith  12508  4sqlem5  12523  4sqlem6  12524  4sqlem8  12526  4sqlem9  12527  4sqlem10  12528  4sqlemafi  12536  4sqlemffi  12537  4sqleminfi  12538  4sqlem11  12542  4sqlem12  12543  4sqlem14  12545  4sqlem16  12547  4sqlem17  12548  oddennn  12552  exmidunben  12586  nninfdclemcl  12608  nninfdclemp1  12610  nninfdclemlt  12611  unbendc  12614  strleund  12724  gsumwsubmcl  13071  gsumwmhm  13073  mulgneg  13213  mulgnndir  13224  znrrg  14159  logbgcd1irraplemexp  15141  logbgcd1irraplemap  15142  lgsfvalg  15162  lgsfcl2  15163  lgsmod  15183  lgsdir  15192  lgsdilem2  15193  lgsne0  15195  gausslemma2dlem0c  15208  gausslemma2dlem0d  15209  gausslemma2dlem0h  15213  gausslemma2dlem0i  15214  gausslemma2dlem1  15218  gausslemma2dlem2  15219  gausslemma2dlem3  15220  gausslemma2dlem4  15221  gausslemma2dlem5a  15222  gausslemma2dlem5  15223  gausslemma2dlem6  15224  gausslemma2dlem7  15225  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgseisen  15231  lgsquadlemsfi  15232  lgsquadlem1  15234  lgsquadlem2  15235  lgsquadlem3  15236  lgsquad2lem1  15238  lgsquad2lem2  15239  lgsquad2  15240  lgsquad3  15241  m1lgs  15242  2lgslem1  15248  2lgslem2  15249  2sqlem3  15274  2sqlem4  15275  2sqlem8  15280  2sqlem9  15281  cvgcmp2nlemabs  15592  trilpolemclim  15596  trilpolemisumle  15598  trilpolemeq1  15600  trilpolemlt1  15601  nconstwlpolemgt0  15624