Theorem nnzd 9645

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℕcn 9185  ℤcz 9523

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641  ax-cnex 8166  ax-resscn 8167  ax-1cn 8168  ax-1re 8169  ax-icn 8170  ax-addcl 8171  ax-addrcl 8172  ax-mulcl 8173  ax-addcom 8175  ax-addass 8177  ax-distr 8179  ax-i2m1 8180  ax-0lt1 8181  ax-0id 8183  ax-rnegex 8184  ax-cnre 8186  ax-pre-ltirr 8187  ax-pre-ltwlin 8188  ax-pre-lttrn 8189  ax-pre-ltadd 8191

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-nel 2499  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fv 5341  df-riota 5981  df-ov 6031  df-oprab 6032  df-mpo 6033  df-pnf 8258  df-mnf 8259  df-xr 8260  df-ltxr 8261  df-le 8262  df-sub 8394  df-neg 8395  df-inn 9186  df-n0 9445  df-z 9524

This theorem is referenced by:  qapne  9917  qtri3or  10546  exbtwnzlemstep  10553  modifeq2int  10694  modsumfzodifsn  10704  addmodlteq  10706  expnnval  10850  expnegap0  10855  expaddzaplem  10890  expmulzap  10893  facndiv  11047  bcval  11057  bcval5  11071  bcpasc  11074  caucvgre  11604  cvg1nlemcau  11607  cvg1nlemres  11608  resqrexlemdecn  11635  resqrexlemnmsq  11640  resqrexlemnm  11641  resqrexlemcvg  11642  resqrexlemoverl  11644  sumeq2  11982  nnf1o  12000  summodclem3  12004  summodclem2a  12005  summodclem2  12006  summodc  12007  zsumdc  12008  fsum3  12011  fisumss  12016  fsum3cvg3  12020  fsumcl2lem  12022  fsumadd  12030  sumsnf  12033  fsummulc2  12072  bcxmas  12113  geo2lim  12140  cvgratnnlembern  12147  cvgratnnlemseq  12150  cvgratnnlemabsle  12151  cvgratnnlemsumlt  12152  cvgratnnlemfm  12153  cvgratnnlemrate  12154  cvgratz  12156  mertenslemub  12158  mertenslemi1  12159  mertenslem2  12160  prodeq2  12181  prodmodclem3  12199  prodmodclem2a  12200  prodmodclem2  12201  fprodseq  12207  fprodssdc  12214  fprodmul  12215  prodsnf  12216  eftcl  12278  eftlub  12314  eirraplem  12401  dvdsle  12468  fzm1ndvds  12480  dvdsfac  12484  dvdsmod  12486  divalglemeunn  12545  bitsfzolem  12578  bitsmod  12580  bitsfi  12581  bitscmp  12582  bitsinv1  12586  gcddvds  12597  gcdnncl  12601  gcd1  12621  dvdsgcdidd  12628  bezoutlemnewy  12630  bezoutlemstep  12631  mulgcd  12650  gcdmultiplez  12655  rplpwr  12661  rppwr  12662  sqgcd  12663  dvdssq  12665  uzwodc  12671  lcmneg  12709  lcmgcdlem  12712  ncoprmgcdne1b  12724  rpdvds  12734  congr  12735  cncongr1  12738  cncongr2  12739  prmz  12746  prmind2  12755  divgcdodd  12778  isprm6  12782  prmexpb  12786  prmfac1  12787  rpexp  12788  sqrt2irrlem  12796  pw2dvdslemn  12800  pw2dvdseulemle  12802  oddpwdclemxy  12804  oddpwdclemodd  12807  sqpweven  12810  2sqpwodd  12811  sqrt2irraplemnn  12814  numdensq  12837  phivalfi  12847  hashdvds  12856  phiprmpw  12857  crth  12859  phimullem  12860  eulerthlem1  12862  eulerthlemfi  12863  eulerthlemrprm  12864  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  eulerth  12868  prmdivdiv  12872  hashgcdlem  12873  hashgcdeq  12875  phisum  12876  odzdvds  12881  powm2modprm  12888  pythagtriplem2  12902  pythagtriplem4  12904  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem11  12910  pythagtriplem13  12912  pythagtriplem16  12915  pythagtriplem19  12918  pythagtrip  12919  pclemub  12923  pcprendvds2  12927  pcpre1  12928  pcpremul  12929  pceulem  12930  pcqmul  12939  pcdvdsb  12956  pcidlem  12959  pcdvdstr  12963  pcgcd1  12964  pc2dvds  12966  pcprmpw2  12969  pcaddlem  12975  pcadd  12976  pcmpt  12979  pcmpt2  12980  pcmptdvds  12981  pcprod  12982  pcfac  12986  pcbc  12987  qexpz  12988  oddprmdvds  12990  prmpwdvds  12991  pockthlem  12992  pockthg  12993  infpnlem2  12996  1arithlem4  13002  1arith  13003  4sqlem5  13018  4sqlem6  13019  4sqlem8  13021  4sqlem9  13022  4sqlem10  13023  4sqlemafi  13031  4sqlemffi  13032  4sqleminfi  13033  4sqlem11  13037  4sqlem12  13038  4sqlem14  13040  4sqlem16  13042  4sqlem17  13043  oddennn  13076  exmidunben  13110  nninfdclemcl  13132  nninfdclemp1  13134  nninfdclemlt  13135  unbendc  13138  bassetsnn  13202  strleund  13249  gsumwsubmcl  13642  gsumwmhm  13644  mulgneg  13790  mulgnndir  13801  znrrg  14739  logbgcd1irraplemexp  15762  logbgcd1irraplemap  15763  sgmnncl  15785  dvdsppwf1o  15786  mpodvdsmulf1o  15787  mersenne  15794  perfect1  15795  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgsfvalg  15807  lgsfcl2  15808  lgsmod  15828  lgsdir  15837  lgsdilem2  15838  lgsne0  15840  gausslemma2dlem0c  15853  gausslemma2dlem0d  15854  gausslemma2dlem0h  15858  gausslemma2dlem0i  15859  gausslemma2dlem1  15863  gausslemma2dlem2  15864  gausslemma2dlem3  15865  gausslemma2dlem4  15866  gausslemma2dlem5a  15867  gausslemma2dlem5  15868  gausslemma2dlem6  15869  gausslemma2dlem7  15870  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgseisen  15876  lgsquadlemsfi  15877  lgsquadlem1  15879  lgsquadlem2  15880  lgsquadlem3  15881  lgsquad2lem1  15883  lgsquad2lem2  15884  lgsquad2  15885  lgsquad3  15886  m1lgs  15887  2lgslem1  15893  2lgslem2  15894  2sqlem3  15919  2sqlem4  15920  2sqlem8  15925  2sqlem9  15926  cvgcmp2nlemabs  16747  trilpolemclim  16751  trilpolemisumle  16753  trilpolemeq1  16755  trilpolemlt1  16756  nconstwlpolemgt0  16780