Theorem nn0zd 12614

Description: A nonnegative integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nn0zd.1	⊢ (𝜑 → 𝐴 ∈ ℕ0)

Assertion

Ref	Expression
nn0zd	⊢ (𝜑 → 𝐴 ∈ ℤ)

Proof of Theorem nn0zd

Step	Hyp	Ref	Expression
1		nn0ssz 12611	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3978	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2099  ℕ₀cn0 12502  ℤcz 12588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5299  ax-nul 5306  ax-pr 5429  ax-un 7740  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-i2m1 11206  ax-1ne0 11207  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3374  df-rab 3430  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6305  df-ord 6372  df-on 6373  df-lim 6374  df-suc 6375  df-iota 6500  df-fun 6550  df-fn 6551  df-f 6552  df-f1 6553  df-fo 6554  df-f1o 6555  df-fv 6556  df-ov 7423  df-om 7871  df-2nd 7994  df-frecs 8286  df-wrecs 8317  df-recs 8391  df-rdg 8430  df-neg 11477  df-nn 12243  df-n0 12503  df-z 12589

This theorem is referenced by:  nnzd  12615  eluzmn  12859  difelfznle  13647  zmodfz  13890  expnegz  14093  expaddzlem  14102  expaddz  14103  expmulz  14105  faclbnd  14281  bcpasc  14312  hashf1  14450  fz1isolem  14454  hashge2el2dif  14473  hashtpg  14478  wrdffz  14517  ffz0iswrd  14523  wrdsymb0  14531  wrdlenge1n0  14532  ccatcl  14556  ccatval3  14561  ccatsymb  14564  ccatval21sw  14567  ccatass  14570  ccatrn  14571  lswccatn0lsw  14573  ccats1val2  14609  swrdnd  14636  swrdccat2  14651  pfxtrcfv0  14676  pfxtrcfvl  14679  pfxccat1  14684  swrdccatin2  14711  pfxccatin12  14715  pfxccatpfx2  14719  pfxccat3a  14720  splfv2a  14738  splval2  14739  revcl  14743  revccat  14748  revrev  14749  cshwmodn  14777  cshwsublen  14778  cshwn  14779  cshwidxmod  14785  2cshwid  14796  3cshw  14800  cshweqdif2  14801  revco  14817  ccatco  14818  ccat2s1fvwALT  14938  ofccat  14948  zabscl  15292  absrdbnd  15320  iseraltlem3  15662  fsum0diaglem  15754  modfsummods  15771  binomlem  15807  binom1p  15809  incexc2  15816  climcndslem1  15827  geoser  15845  pwm1geoser  15847  geolim2  15849  mertenslem1  15862  mertenslem2  15863  mertens  15864  binomfallfaclem2  16016  binomrisefac  16018  fallfacval4  16019  bpolydiflem  16030  ruclem10  16215  sumodd  16364  divalglem9  16377  divalgmod  16382  bitsfzolem  16408  bitsfzo  16409  bitsmod  16410  bitsfi  16411  bitsinv1lem  16415  sadcaddlem  16431  sadadd3  16435  sadaddlem  16440  sadadd  16441  sadasslem  16444  sadass  16445  sadeq  16446  bitsres  16447  bitsuz  16448  bitsshft  16449  smuval2  16456  smupvallem  16457  smupval  16462  smueqlem  16464  smumullem  16466  smumul  16467  gcdcllem1  16473  zeqzmulgcd  16484  gcd0id  16493  gcdneg  16496  modgcd  16507  gcdmultipled  16509  bezoutlem4  16517  dvdsgcdb  16520  gcdass  16522  mulgcd  16523  gcdzeq  16527  dvdsmulgcd  16530  bezoutr  16538  bezoutr1  16539  nn0seqcvgd  16540  algfx  16550  eucalginv  16554  eucalg  16557  gcddvdslcm  16572  lcmneg  16573  lcmgcdlem  16576  lcmdvds  16578  lcmgcdeq  16582  lcmdvdsb  16583  lcmass  16584  lcmftp  16606  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  lcmfunsnlem2  16610  lcmfdvdsb  16613  lcmfun  16615  lcmfass  16616  mulgcddvds  16625  rpmulgcd2  16626  qredeu  16628  divgcdcoprm0  16635  sqnprm  16672  prmdvdsbc  16697  divnumden  16719  powm2modprm  16771  coprimeprodsq  16776  iserodd  16803  pclem  16806  pcpre1  16810  pcpremul  16811  pcqcl  16824  pcdvdsb  16837  pcidlem  16840  pc2dvds  16847  pcprmpw2  16850  dvdsprmpweqle  16854  pcadd  16857  pcfac  16867  pcbc  16868  pockthlem  16873  prmreclem2  16885  prmreclem3  16886  mul4sqlem  16921  4sqlem11  16923  4sqlem12  16924  4sqlem14  16926  vdwapun  16942  prmgaplcmlem1  17019  lagsubg  19149  psgnuni  19453  psgnran  19469  odmodnn0  19494  mndodconglem  19495  mndodcong  19496  odm1inv  19507  odmulg2  19509  odmulg  19510  odmulgeq  19511  odbezout  19512  odinv  19515  odf1  19516  gexod  19540  gexdvds3  19544  sylow1lem1  19552  sylow1lem3  19554  pgpfi  19559  pgpssslw  19568  sylow2alem2  19572  sylow2blem3  19576  fislw  19579  sylow3lem4  19584  sylow3lem6  19586  efginvrel2  19681  efgredlemf  19695  efgredlemd  19698  efgredlemc  19699  efgredlem  19701  efgcpbllemb  19709  odadd1  19802  odadd2  19803  gexexlem  19806  gexex  19807  torsubg  19808  lt6abl  19849  gsummulg  19896  ablfacrplem  20021  ablfacrp  20022  ablfacrp2  20023  ablfac1b  20026  ablfac1c  20027  ablfac1eulem  20028  ablfac1eu  20029  pgpfac1lem2  20031  pgpfaclem1  20037  ablfaclem3  20043  srgbinomlem3  20167  srgbinomlem4  20168  chrid  21454  znunit  21496  freshmansdream  21507  psgnghm  21511  asclmulg  21834  psrbaglefi  21864  psrbaglefiOLD  21865  psdvsca  22087  psdmul  22089  chfacfscmulfsupp  22760  chfacfpmmulfsupp  22764  cpmadugsumlemF  22777  dyadss  25522  dyaddisjlem  25523  ply1divex  26071  ply1termlem  26136  plyeq0lem  26143  plyaddlem1  26146  plymullem1  26147  coeeulem  26157  coeidlem  26170  coeeq2  26175  coemulhi  26187  dvply1  26217  dvply2g  26218  dvply2gOLD  26219  plydivex  26231  elqaalem2  26254  aareccl  26260  aannenlem1  26262  aalioulem1  26266  taylplem1  26296  taylplem2  26297  taylpfval  26298  dvtaylp  26304  taylthlem2  26308  taylthlem2OLD  26309  dvradcnv  26356  abelthlem7  26374  cxpeq  26691  birthdaylem2  26883  ftalem1  27004  basellem3  27014  isppw2  27046  isnsqf  27066  mule1  27079  ppinncl  27105  musum  27122  chtublem  27143  pclogsum  27147  vmasum  27148  dchrabs  27192  bcmax  27210  bposlem1  27216  bposlem6  27221  lgsval2lem  27239  lgsmod  27255  lgsne0  27267  gausslemma2dlem0h  27295  gausslemma2dlem0i  27296  gausslemma2dlem2  27299  gausslemma2dlem6  27304  gausslemma2d  27306  lgseisenlem1  27307  lgseisenlem2  27308  lgseisenlem3  27309  lgseisenlem4  27310  lgsquadlem1  27312  m1lgs  27320  2lgslem1a  27323  2lgslem3a  27328  2lgslem3b  27329  2lgslem3c  27330  2lgslem3d  27331  2lgslem3d1  27335  2lgsoddprmlem2  27341  2sqlem8  27358  2sqcoprm  27367  2sqmod  27368  chebbnd1lem1  27401  dchrisumlem1  27421  dchrisum0flblem1  27440  selberg2lem  27482  ostth2lem2  27566  ostth2lem3  27567  finsumvtxdg2sstep  29362  finsumvtxdgeven  29365  vtxdgoddnumeven  29366  redwlklem  29484  wlkdlem1  29495  pthdlem1  29579  crctcshwlkn0lem4  29623  wwlksnredwwlkn0  29706  wwlksnextproplem2  29720  clwwlkccatlem  29798  clwlkclwwlkfo  29818  clwwlkwwlksb  29863  clwwlkndivn  29889  eupth2lem3lem3  30039  eupth2lem3lem4  30040  eupth2lem3  30045  eupth2lems  30047  numclwwlk5  30197  numclwwlk6  30199  ex-ind-dvds  30270  nndiffz1  32554  ccatf1  32672  pfxlsw2ccat  32673  wrdt2ind  32674  cycpmfv1  32834  cycpmco2lem2  32848  cycpmco2lem3  32849  cycpmco2lem4  32850  cycpmco2lem5  32851  cycpmco2lem6  32852  cycpmco2  32854  cycpmrn  32864  cyc3genpm  32873  cycpmconjslem2  32876  cyc3conja  32878  archirng  32896  archirngz  32897  archiabllem1a  32899  elrspunidl  33144  ply1degltel  33261  ply1degltdimlem  33316  algextdeglem8  33392  madjusmdetlem4  33431  qqhval2lem  33582  oddpwdc  33974  eulerpartlems  33980  eulerpartlemb  33988  sseqfv1  34009  sseqfn  34010  sseqmw  34011  sseqf  34012  sseqfv2  34014  sseqp1  34015  ccatmulgnn0dir  34174  signsplypnf  34182  signsply0  34183  signslema  34194  signstfvn  34201  signstfvp  34203  signstfvc  34206  fsum2dsub  34239  reprinfz1  34254  reprfi2  34255  hashrepr  34257  reprdifc  34259  breprexplema  34262  breprexplemc  34264  circlemeth  34272  circlevma  34274  circlemethhgt  34275  hgt750lema  34289  tgoldbachgtde  34292  lpadlem3  34310  revpfxsfxrev  34725  revwlk  34734  subfacval3  34799  bcprod  35332  bccolsum  35333  fwddifnp1  35761  knoppndvlem6  35992  knoppndvlem7  35993  knoppndvlem10  35996  knoppndvlem14  36000  knoppndvlem15  36001  knoppndvlem16  36002  knoppndvlem17  36003  knoppndvlem19  36005  knoppndvlem21  36007  dfgcd3  36803  poimirlem3  37096  poimirlem4  37097  poimirlem6  37099  poimirlem13  37106  poimirlem14  37107  poimirlem17  37110  poimirlem21  37114  poimirlem22  37115  poimirlem23  37116  poimirlem26  37119  poimirlem27  37120  poimirlem31  37124  geomcau  37232  bccl2d  41462  lcmineqlem12  41511  lcmineqlem17  41516  dvrelogpow2b  41539  aks4d1p1p2  41541  aks4d1p1p4  41542  aks4d1p1p6  41544  aks4d1p1p7  41545  aks4d1p1p5  41546  aks4d1p1  41547  aks4d1p3  41549  aks4d1p6  41552  aks4d1p8d2  41556  aks4d1p8d3  41557  aks4d1p8  41558  primrootscoprmpow  41570  primrootlekpowne0  41576  aks6d1c1  41587  aks6d1c2p2  41590  aks6d1c2lem4  41598  aks6d1c2  41601  aks6d1c5lem3  41608  aks6d1c5lem2  41609  2np3bcnp1  41616  sticksstones5  41622  sticksstones6  41623  sticksstones7  41624  sticksstones10  41627  sticksstones11  41628  sticksstones12a  41629  sticksstones12  41630  sticksstones22  41640  aks6d1c6lem3  41644  bcled  41650  bcle2d  41651  aks6d1c7lem1  41652  aks6d1c7lem2  41653  prodsplit  41692  frlmvscadiccat  41746  sumcubes  41873  gcdle1d  41890  gcdle2d  41891  fltdiv  42060  flt4lem4  42073  fltnltalem  42086  eldioph2lem1  42180  pellexlem5  42253  congrep  42394  jm2.18  42409  jm2.19lem1  42410  jm2.19lem2  42411  jm2.19  42414  jm2.22  42416  jm2.23  42417  jm2.20nn  42418  jm2.25  42420  jm2.26a  42421  jm2.26lem3  42422  jm2.26  42423  jm2.27a  42426  jm2.27b  42427  jm2.27c  42428  jm3.1  42441  expdiophlem1  42442  hbtlem5  42552  radcnvrat  43751  nzin  43755  bccbc  43782  binomcxplemnn0  43786  binomcxplemnotnn0  43793  fprodexp  44982  mccllem  44985  ioodvbdlimc1lem2  45320  ioodvbdlimc2lem  45322  dvnxpaek  45330  dvnmul  45331  dvnprodlem1  45334  dvnprodlem2  45335  wallispilem1  45453  wallispilem5  45457  stirlinglem3  45464  stirlinglem5  45466  stirlinglem7  45468  stirlinglem8  45469  fourierdlem102  45596  fourierdlem114  45608  sqwvfoura  45616  elaa2lem  45621  etransclem10  45632  etransclem20  45642  etransclem21  45643  etransclem22  45644  etransclem23  45645  etransclem24  45646  etransclem27  45649  etransclem28  45650  etransclem35  45657  etransclem38  45660  etransclem44  45666  etransclem45  45667  etransclem46  45668  sge0ad2en  45819  fsummmodsnunz  46715  fmtnoge3  46870  fmtnof1  46875  fmtnorec1  46877  sqrtpwpw2p  46878  fmtnodvds  46884  goldbachthlem2  46886  fmtnoprmfac2lem1  46906  lighneallem3  46947  lighneallem4b  46949  lighneallem4  46950  ssnn0ssfz  47413  altgsumbcALT  47417  flnn0ohalf  47607  dig2nn1st  47678  0dig2nn0o  47686  aacllem  48234