Theorem nnzd 9303

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

Syntax hints:   → wi 4   ∈ wcel 2135  ℕcn 8848  ℤcz 9182

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-setind 4508  ax-cnex 7835  ax-resscn 7836  ax-1cn 7837  ax-1re 7838  ax-icn 7839  ax-addcl 7840  ax-addrcl 7841  ax-mulcl 7842  ax-addcom 7844  ax-addass 7846  ax-distr 7848  ax-i2m1 7849  ax-0lt1 7850  ax-0id 7852  ax-rnegex 7853  ax-cnre 7855  ax-pre-ltirr 7856  ax-pre-ltwlin 7857  ax-pre-lttrn 7858  ax-pre-ltadd 7860

This theorem depends on definitions:  df-bi 116  df-3or 968  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-reu 2449  df-rab 2451  df-v 2723  df-sbc 2947  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-int 3819  df-br 3977  df-opab 4038  df-id 4265  df-xp 4604  df-rel 4605  df-cnv 4606  df-co 4607  df-dm 4608  df-iota 5147  df-fun 5184  df-fv 5190  df-riota 5792  df-ov 5839  df-oprab 5840  df-mpo 5841  df-pnf 7926  df-mnf 7927  df-xr 7928  df-ltxr 7929  df-le 7930  df-sub 8062  df-neg 8063  df-inn 8849  df-n0 9106  df-z 9183

This theorem is referenced by:  qapne  9568  qtri3or  10168  exbtwnzlemstep  10173  modifeq2int  10311  modsumfzodifsn  10321  addmodlteq  10323  expnnval  10448  expnegap0  10453  expaddzaplem  10488  expmulzap  10491  facndiv  10641  bcval  10651  bcval5  10665  bcpasc  10668  caucvgre  10909  cvg1nlemcau  10912  cvg1nlemres  10913  resqrexlemdecn  10940  resqrexlemnmsq  10945  resqrexlemnm  10946  resqrexlemcvg  10947  resqrexlemoverl  10949  sumeq2  11286  nnf1o  11303  summodclem3  11307  summodclem2a  11308  summodclem2  11309  summodc  11310  zsumdc  11311  fsum3  11314  fisumss  11319  fsum3cvg3  11323  fsumcl2lem  11325  fsumadd  11333  sumsnf  11336  fsummulc2  11375  bcxmas  11416  geo2lim  11443  cvgratnnlembern  11450  cvgratnnlemseq  11453  cvgratnnlemabsle  11454  cvgratnnlemsumlt  11455  cvgratnnlemfm  11456  cvgratnnlemrate  11457  cvgratz  11459  mertenslemub  11461  mertenslemi1  11462  mertenslem2  11463  prodeq2  11484  prodmodclem3  11502  prodmodclem2a  11503  prodmodclem2  11504  fprodseq  11510  fprodssdc  11517  fprodmul  11518  prodsnf  11519  eftcl  11581  eftlub  11617  eirraplem  11703  dvdsle  11767  fzm1ndvds  11779  dvdsfac  11783  dvdsmod  11785  divalglemeunn  11843  gcddvds  11881  gcdnncl  11885  gcd1  11905  dvdsgcdidd  11912  bezoutlemnewy  11914  bezoutlemstep  11915  mulgcd  11934  gcdmultiplez  11939  rplpwr  11945  rppwr  11946  sqgcd  11947  dvdssq  11949  lcmneg  11985  lcmgcdlem  11988  ncoprmgcdne1b  12000  rpdvds  12010  congr  12011  cncongr1  12014  cncongr2  12015  prmz  12022  prmind2  12031  divgcdodd  12052  isprm6  12056  prmexpb  12060  prmfac1  12061  rpexp  12062  sqrt2irrlem  12070  pw2dvdslemn  12074  pw2dvdseulemle  12076  oddpwdclemxy  12078  oddpwdclemodd  12081  sqpweven  12084  2sqpwodd  12085  sqrt2irraplemnn  12088  numdensq  12111  phivalfi  12121  hashdvds  12130  phiprmpw  12131  crth  12133  phimullem  12134  eulerthlem1  12136  eulerthlemfi  12137  eulerthlemrprm  12138  eulerthlema  12139  eulerthlemh  12140  eulerthlemth  12141  eulerth  12142  prmdivdiv  12146  hashgcdlem  12147  hashgcdeq  12148  phisum  12149  odzdvds  12154  powm2modprm  12161  pythagtriplem2  12175  pythagtriplem4  12177  pythagtriplem6  12179  pythagtriplem7  12180  pythagtriplem11  12183  pythagtriplem13  12185  pythagtriplem16  12188  pythagtriplem19  12191  pythagtrip  12192  pclemub  12196  pcprendvds2  12200  pcpre1  12201  pcpremul  12202  pceulem  12203  pcqmul  12212  pcdvdsb  12228  pcidlem  12231  pcdvdstr  12235  pcgcd1  12236  pc2dvds  12238  pcprmpw2  12241  pcaddlem  12247  pcadd  12248  pcmpt  12250  pcmpt2  12251  pcmptdvds  12252  pcprod  12253  pcfac  12257  pcbc  12258  qexpz  12259  oddprmdvds  12261  oddennn  12262  exmidunben  12296  nninfdclemcl  12320  nninfdclemp1  12322  nninfdclemlt  12323  unbendc  12326  strleund  12419  logbgcd1irraplemexp  13427  logbgcd1irraplemap  13428  cvgcmp2nlemabs  13745  trilpolemclim  13749  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  nconstwlpolemgt0  13776