Theorem nnzd 9601

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℕcn 9143  ℤcz 9479

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-br 4089  df-opab 4151  df-id 4390  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-iota 5286  df-fun 5328  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-n0 9403  df-z 9480

This theorem is referenced by:  qapne  9873  qtri3or  10501  exbtwnzlemstep  10508  modifeq2int  10649  modsumfzodifsn  10659  addmodlteq  10661  expnnval  10805  expnegap0  10810  expaddzaplem  10845  expmulzap  10848  facndiv  11002  bcval  11012  bcval5  11026  bcpasc  11029  caucvgre  11546  cvg1nlemcau  11549  cvg1nlemres  11550  resqrexlemdecn  11577  resqrexlemnmsq  11582  resqrexlemnm  11583  resqrexlemcvg  11584  resqrexlemoverl  11586  sumeq2  11924  nnf1o  11942  summodclem3  11946  summodclem2a  11947  summodclem2  11948  summodc  11949  zsumdc  11950  fsum3  11953  fisumss  11958  fsum3cvg3  11962  fsumcl2lem  11964  fsumadd  11972  sumsnf  11975  fsummulc2  12014  bcxmas  12055  geo2lim  12082  cvgratnnlembern  12089  cvgratnnlemseq  12092  cvgratnnlemabsle  12093  cvgratnnlemsumlt  12094  cvgratnnlemfm  12095  cvgratnnlemrate  12096  cvgratz  12098  mertenslemub  12100  mertenslemi1  12101  mertenslem2  12102  prodeq2  12123  prodmodclem3  12141  prodmodclem2a  12142  prodmodclem2  12143  fprodseq  12149  fprodssdc  12156  fprodmul  12157  prodsnf  12158  eftcl  12220  eftlub  12256  eirraplem  12343  dvdsle  12410  fzm1ndvds  12422  dvdsfac  12426  dvdsmod  12428  divalglemeunn  12487  bitsfzolem  12520  bitsmod  12522  bitsfi  12523  bitscmp  12524  bitsinv1  12528  gcddvds  12539  gcdnncl  12543  gcd1  12563  dvdsgcdidd  12570  bezoutlemnewy  12572  bezoutlemstep  12573  mulgcd  12592  gcdmultiplez  12597  rplpwr  12603  rppwr  12604  sqgcd  12605  dvdssq  12607  uzwodc  12613  lcmneg  12651  lcmgcdlem  12654  ncoprmgcdne1b  12666  rpdvds  12676  congr  12677  cncongr1  12680  cncongr2  12681  prmz  12688  prmind2  12697  divgcdodd  12720  isprm6  12724  prmexpb  12728  prmfac1  12729  rpexp  12730  sqrt2irrlem  12738  pw2dvdslemn  12742  pw2dvdseulemle  12744  oddpwdclemxy  12746  oddpwdclemodd  12749  sqpweven  12752  2sqpwodd  12753  sqrt2irraplemnn  12756  numdensq  12779  phivalfi  12789  hashdvds  12798  phiprmpw  12799  crth  12801  phimullem  12802  eulerthlem1  12804  eulerthlemfi  12805  eulerthlemrprm  12806  eulerthlema  12807  eulerthlemh  12808  eulerthlemth  12809  eulerth  12810  prmdivdiv  12814  hashgcdlem  12815  hashgcdeq  12817  phisum  12818  odzdvds  12823  powm2modprm  12830  pythagtriplem2  12844  pythagtriplem4  12846  pythagtriplem6  12848  pythagtriplem7  12849  pythagtriplem11  12852  pythagtriplem13  12854  pythagtriplem16  12857  pythagtriplem19  12860  pythagtrip  12861  pclemub  12865  pcprendvds2  12869  pcpre1  12870  pcpremul  12871  pceulem  12872  pcqmul  12881  pcdvdsb  12898  pcidlem  12901  pcdvdstr  12905  pcgcd1  12906  pc2dvds  12908  pcprmpw2  12911  pcaddlem  12917  pcadd  12918  pcmpt  12921  pcmpt2  12922  pcmptdvds  12923  pcprod  12924  pcfac  12928  pcbc  12929  qexpz  12930  oddprmdvds  12932  prmpwdvds  12933  pockthlem  12934  pockthg  12935  infpnlem2  12938  1arithlem4  12944  1arith  12945  4sqlem5  12960  4sqlem6  12961  4sqlem8  12963  4sqlem9  12964  4sqlem10  12965  4sqlemafi  12973  4sqlemffi  12974  4sqleminfi  12975  4sqlem11  12979  4sqlem12  12980  4sqlem14  12982  4sqlem16  12984  4sqlem17  12985  oddennn  13018  exmidunben  13052  nninfdclemcl  13074  nninfdclemp1  13076  nninfdclemlt  13077  unbendc  13080  bassetsnn  13144  strleund  13191  gsumwsubmcl  13584  gsumwmhm  13586  mulgneg  13732  mulgnndir  13743  znrrg  14680  logbgcd1irraplemexp  15698  logbgcd1irraplemap  15699  sgmnncl  15718  dvdsppwf1o  15719  mpodvdsmulf1o  15720  mersenne  15727  perfect1  15728  perfectlem1  15729  perfectlem2  15730  perfect  15731  lgsfvalg  15740  lgsfcl2  15741  lgsmod  15761  lgsdir  15770  lgsdilem2  15771  lgsne0  15773  gausslemma2dlem0c  15786  gausslemma2dlem0d  15787  gausslemma2dlem0h  15791  gausslemma2dlem0i  15792  gausslemma2dlem1  15796  gausslemma2dlem2  15797  gausslemma2dlem3  15798  gausslemma2dlem4  15799  gausslemma2dlem5a  15800  gausslemma2dlem5  15801  gausslemma2dlem6  15802  gausslemma2dlem7  15803  gausslemma2d  15804  lgseisenlem1  15805  lgseisenlem2  15806  lgseisenlem3  15807  lgseisenlem4  15808  lgseisen  15809  lgsquadlemsfi  15810  lgsquadlem1  15812  lgsquadlem2  15813  lgsquadlem3  15814  lgsquad2lem1  15816  lgsquad2lem2  15817  lgsquad2  15818  lgsquad3  15819  m1lgs  15820  2lgslem1  15826  2lgslem2  15827  2sqlem3  15852  2sqlem4  15853  2sqlem8  15858  2sqlem9  15859  cvgcmp2nlemabs  16662  trilpolemclim  16666  trilpolemisumle  16668  trilpolemeq1  16670  trilpolemlt1  16671  nconstwlpolemgt0  16695