Theorem nnzd 9579

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

Syntax hints:   → wi 4   ∈ wcel 2200  ℕcn 9121  ℤcz 9457

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8101  ax-resscn 8102  ax-1cn 8103  ax-1re 8104  ax-icn 8105  ax-addcl 8106  ax-addrcl 8107  ax-mulcl 8108  ax-addcom 8110  ax-addass 8112  ax-distr 8114  ax-i2m1 8115  ax-0lt1 8116  ax-0id 8118  ax-rnegex 8119  ax-cnre 8121  ax-pre-ltirr 8122  ax-pre-ltwlin 8123  ax-pre-lttrn 8124  ax-pre-ltadd 8126

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326  df-riota 5960  df-ov 6010  df-oprab 6011  df-mpo 6012  df-pnf 8194  df-mnf 8195  df-xr 8196  df-ltxr 8197  df-le 8198  df-sub 8330  df-neg 8331  df-inn 9122  df-n0 9381  df-z 9458

This theorem is referenced by:  qapne  9846  qtri3or  10472  exbtwnzlemstep  10479  modifeq2int  10620  modsumfzodifsn  10630  addmodlteq  10632  expnnval  10776  expnegap0  10781  expaddzaplem  10816  expmulzap  10819  facndiv  10973  bcval  10983  bcval5  10997  bcpasc  11000  caucvgre  11507  cvg1nlemcau  11510  cvg1nlemres  11511  resqrexlemdecn  11538  resqrexlemnmsq  11543  resqrexlemnm  11544  resqrexlemcvg  11545  resqrexlemoverl  11547  sumeq2  11885  nnf1o  11902  summodclem3  11906  summodclem2a  11907  summodclem2  11908  summodc  11909  zsumdc  11910  fsum3  11913  fisumss  11918  fsum3cvg3  11922  fsumcl2lem  11924  fsumadd  11932  sumsnf  11935  fsummulc2  11974  bcxmas  12015  geo2lim  12042  cvgratnnlembern  12049  cvgratnnlemseq  12052  cvgratnnlemabsle  12053  cvgratnnlemsumlt  12054  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratz  12058  mertenslemub  12060  mertenslemi1  12061  mertenslem2  12062  prodeq2  12083  prodmodclem3  12101  prodmodclem2a  12102  prodmodclem2  12103  fprodseq  12109  fprodssdc  12116  fprodmul  12117  prodsnf  12118  eftcl  12180  eftlub  12216  eirraplem  12303  dvdsle  12370  fzm1ndvds  12382  dvdsfac  12386  dvdsmod  12388  divalglemeunn  12447  bitsfzolem  12480  bitsmod  12482  bitsfi  12483  bitscmp  12484  bitsinv1  12488  gcddvds  12499  gcdnncl  12503  gcd1  12523  dvdsgcdidd  12530  bezoutlemnewy  12532  bezoutlemstep  12533  mulgcd  12552  gcdmultiplez  12557  rplpwr  12563  rppwr  12564  sqgcd  12565  dvdssq  12567  uzwodc  12573  lcmneg  12611  lcmgcdlem  12614  ncoprmgcdne1b  12626  rpdvds  12636  congr  12637  cncongr1  12640  cncongr2  12641  prmz  12648  prmind2  12657  divgcdodd  12680  isprm6  12684  prmexpb  12688  prmfac1  12689  rpexp  12690  sqrt2irrlem  12698  pw2dvdslemn  12702  pw2dvdseulemle  12704  oddpwdclemxy  12706  oddpwdclemodd  12709  sqpweven  12712  2sqpwodd  12713  sqrt2irraplemnn  12716  numdensq  12739  phivalfi  12749  hashdvds  12758  phiprmpw  12759  crth  12761  phimullem  12762  eulerthlem1  12764  eulerthlemfi  12765  eulerthlemrprm  12766  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  eulerth  12770  prmdivdiv  12774  hashgcdlem  12775  hashgcdeq  12777  phisum  12778  odzdvds  12783  powm2modprm  12790  pythagtriplem2  12804  pythagtriplem4  12806  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem11  12812  pythagtriplem13  12814  pythagtriplem16  12817  pythagtriplem19  12820  pythagtrip  12821  pclemub  12825  pcprendvds2  12829  pcpre1  12830  pcpremul  12831  pceulem  12832  pcqmul  12841  pcdvdsb  12858  pcidlem  12861  pcdvdstr  12865  pcgcd1  12866  pc2dvds  12868  pcprmpw2  12871  pcaddlem  12877  pcadd  12878  pcmpt  12881  pcmpt2  12882  pcmptdvds  12883  pcprod  12884  pcfac  12888  pcbc  12889  qexpz  12890  oddprmdvds  12892  prmpwdvds  12893  pockthlem  12894  pockthg  12895  infpnlem2  12898  1arithlem4  12904  1arith  12905  4sqlem5  12920  4sqlem6  12921  4sqlem8  12923  4sqlem9  12924  4sqlem10  12925  4sqlemafi  12933  4sqlemffi  12934  4sqleminfi  12935  4sqlem11  12939  4sqlem12  12940  4sqlem14  12942  4sqlem16  12944  4sqlem17  12945  oddennn  12978  exmidunben  13012  nninfdclemcl  13034  nninfdclemp1  13036  nninfdclemlt  13037  unbendc  13040  bassetsnn  13104  strleund  13151  gsumwsubmcl  13544  gsumwmhm  13546  mulgneg  13692  mulgnndir  13703  znrrg  14639  logbgcd1irraplemexp  15657  logbgcd1irraplemap  15658  sgmnncl  15677  dvdsppwf1o  15678  mpodvdsmulf1o  15679  mersenne  15686  perfect1  15687  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgsfvalg  15699  lgsfcl2  15700  lgsmod  15720  lgsdir  15729  lgsdilem2  15730  lgsne0  15732  gausslemma2dlem0c  15745  gausslemma2dlem0d  15746  gausslemma2dlem0h  15750  gausslemma2dlem0i  15751  gausslemma2dlem1  15755  gausslemma2dlem2  15756  gausslemma2dlem3  15757  gausslemma2dlem4  15758  gausslemma2dlem5a  15759  gausslemma2dlem5  15760  gausslemma2dlem6  15761  gausslemma2dlem7  15762  gausslemma2d  15763  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgseisen  15768  lgsquadlemsfi  15769  lgsquadlem1  15771  lgsquadlem2  15772  lgsquadlem3  15773  lgsquad2lem1  15775  lgsquad2lem2  15776  lgsquad2  15777  lgsquad3  15778  m1lgs  15779  2lgslem1  15785  2lgslem2  15786  2sqlem3  15811  2sqlem4  15812  2sqlem8  15817  2sqlem9  15818  cvgcmp2nlemabs  16460  trilpolemclim  16464  trilpolemisumle  16466  trilpolemeq1  16468  trilpolemlt1  16469  nconstwlpolemgt0  16492