Theorem nn0zd 12549

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 12547	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3919	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2114  ℕ₀cn0 12437  ℤcz 12524

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-i2m1 11106  ax-1ne0 11107  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3909  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-tr 5193  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6265  df-ord 6326  df-on 6327  df-lim 6328  df-suc 6329  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-ov 7370  df-om 7818  df-2nd 7943  df-frecs 8231  df-wrecs 8262  df-recs 8311  df-rdg 8349  df-neg 11380  df-nn 12175  df-n0 12438  df-z 12525

This theorem is referenced by:  nnzd  12550  eluzmn  12795  difelfznle  13596  elfzodif0  13725  zmodfz  13852  expnegz  14058  expaddzlem  14067  expaddz  14068  expmulz  14070  faclbnd  14252  bcpasc  14283  hashf1  14419  fz1isolem  14423  hashge2el2dif  14442  hashtpg  14447  wrdffz  14497  ffz0iswrd  14503  wrdsymb0  14511  wrdlenge1n0  14512  ccatcl  14536  ccatval3  14541  ccatdmss  14544  ccatsymb  14545  ccatval21sw  14548  ccatass  14551  ccatrn  14552  lswccatn0lsw  14554  ccats1val2  14590  swrdnd  14617  swrdccat2  14632  pfxtrcfv0  14656  pfxtrcfvl  14659  pfxccat1  14664  swrdccatin2  14691  pfxccatin12  14695  pfxccatpfx2  14699  pfxccat3a  14700  splfv2a  14718  splval2  14719  revcl  14723  revccat  14728  revrev  14729  cshwmodn  14757  cshwsublen  14758  cshwn  14759  cshwidxmod  14765  2cshwid  14776  3cshw  14780  cshweqdif2  14781  revco  14796  ccatco  14797  ccat2s1fvwALT  14917  ofccat  14931  zabscl  15275  absrdbnd  15304  iseraltlem3  15646  fsum0diaglem  15738  modfsummods  15756  binomlem  15794  binom1p  15796  incexc2  15803  climcndslem1  15814  geoser  15832  pwm1geoser  15834  geolim2  15836  mertenslem1  15849  mertenslem2  15850  mertens  15851  binomfallfaclem2  16005  binomrisefac  16007  fallfacval4  16008  bpolydiflem  16019  ruclem10  16206  sumodd  16357  divalglem9  16370  divalgmod  16375  bitsfzolem  16403  bitsfzo  16404  bitsmod  16405  bitsfi  16406  bitsinv1lem  16410  sadcaddlem  16426  sadadd3  16430  sadaddlem  16435  sadadd  16436  sadasslem  16439  sadass  16440  sadeq  16441  bitsres  16442  bitsuz  16443  bitsshft  16444  smuval2  16451  smupvallem  16452  smupval  16457  smueqlem  16459  smumullem  16461  smumul  16462  gcdcllem1  16468  zeqzmulgcd  16479  gcd0id  16488  gcdneg  16491  modgcd  16501  gcdmultipled  16503  bezoutlem4  16511  dvdsgcdb  16514  gcdass  16516  mulgcd  16517  gcdzeq  16521  dvdsmulgcd  16525  bezoutr  16537  bezoutr1  16538  nn0seqcvgd  16539  algfx  16549  eucalginv  16553  eucalg  16556  gcddvdslcm  16571  lcmneg  16572  lcmgcdlem  16575  lcmdvds  16577  lcmgcdeq  16581  lcmdvdsb  16582  lcmass  16583  lcmftp  16605  lcmfunsnlem1  16606  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  lcmfunsnlem2  16609  lcmfdvdsb  16612  lcmfun  16614  lcmfass  16615  mulgcddvds  16624  rpmulgcd2  16625  qredeu  16627  divgcdcoprm0  16634  sqnprm  16672  prmdvdsbc  16696  divnumden  16718  powm2modprm  16774  coprimeprodsq  16779  iserodd  16806  pclem  16809  pcpre1  16813  pcpremul  16814  pcqcl  16827  pcdvdsb  16840  pcidlem  16843  pc2dvds  16850  pcprmpw2  16853  dvdsprmpweqle  16857  pcadd  16860  pcfac  16870  pcbc  16871  pockthlem  16876  prmreclem2  16888  prmreclem3  16889  mul4sqlem  16924  4sqlem11  16926  4sqlem12  16927  4sqlem14  16929  vdwapun  16945  prmgaplcmlem1  17022  chnind  18587  chnub  18588  chnpolfz  18599  lagsubg  19170  psgnuni  19474  psgnran  19490  odmodnn0  19515  mndodconglem  19516  mndodcong  19517  odm1inv  19528  odmulg2  19530  odmulg  19531  odmulgeq  19532  odbezout  19533  odinv  19536  odf1  19537  gexod  19561  gexdvds3  19565  sylow1lem1  19573  sylow1lem3  19575  pgpfi  19580  pgpssslw  19589  sylow2alem2  19593  sylow2blem3  19597  fislw  19600  sylow3lem4  19605  sylow3lem6  19607  efginvrel2  19702  efgredlemf  19716  efgredlemd  19719  efgredlemc  19720  efgredlem  19722  efgcpbllemb  19730  odadd1  19823  odadd2  19824  gexexlem  19827  gexex  19828  torsubg  19829  lt6abl  19870  gsummulg  19917  ablfacrplem  20042  ablfacrp  20043  ablfacrp2  20044  ablfac1b  20047  ablfac1c  20048  ablfac1eulem  20049  ablfac1eu  20050  pgpfac1lem2  20052  pgpfaclem1  20058  ablfaclem3  20064  srgbinomlem3  20209  srgbinomlem4  20210  chrid  21505  znunit  21543  freshmansdream  21554  psgnghm  21560  asclmulg  21882  psrbaglefi  21906  psdvsca  22130  psdmul  22132  chfacfscmulfsupp  22824  chfacfpmmulfsupp  22828  cpmadugsumlemF  22841  dyadss  25561  dyaddisjlem  25562  ply1divex  26102  ply1termlem  26168  plyeq0lem  26175  plyaddlem1  26178  plymullem1  26179  coeeulem  26189  coeidlem  26202  coeeq2  26207  coemulhi  26219  dvply1  26250  dvply2g  26251  plydivex  26263  elqaalem2  26286  aareccl  26292  aannenlem1  26294  aalioulem1  26298  taylplem1  26328  taylplem2  26329  taylpfval  26330  dvtaylp  26335  taylthlem2  26339  dvradcnv  26386  abelthlem7  26403  cxpeq  26721  birthdaylem2  26916  ftalem1  27036  basellem3  27046  isppw2  27078  isnsqf  27098  mule1  27111  ppinncl  27137  musum  27154  chtublem  27174  pclogsum  27178  vmasum  27179  dchrabs  27223  bcmax  27241  bposlem1  27247  bposlem6  27252  lgsval2lem  27270  lgsmod  27286  lgsne0  27298  gausslemma2dlem0h  27326  gausslemma2dlem0i  27327  gausslemma2dlem2  27330  gausslemma2dlem6  27335  gausslemma2d  27337  lgseisenlem1  27338  lgseisenlem2  27339  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  m1lgs  27351  2lgslem1a  27354  2lgslem3a  27359  2lgslem3b  27360  2lgslem3c  27361  2lgslem3d  27362  2lgslem3d1  27366  2lgsoddprmlem2  27372  2sqlem8  27389  2sqcoprm  27398  2sqmod  27399  chebbnd1lem1  27432  dchrisumlem1  27452  dchrisum0flblem1  27471  selberg2lem  27513  ostth2lem2  27597  ostth2lem3  27598  finsumvtxdg2sstep  29618  finsumvtxdgeven  29621  vtxdgoddnumeven  29622  redwlklem  29738  wlkdlem1  29749  pthdlem1  29834  crctcshwlkn0lem4  29881  wwlksnredwwlkn0  29964  wwlksnextproplem2  29978  clwwlkccatlem  30059  clwlkclwwlkfo  30079  clwwlkwwlksb  30124  clwwlkndivn  30150  eupth2lem3lem3  30300  eupth2lem3lem4  30301  eupth2lem3  30306  eupth2lems  30308  numclwwlk5  30458  numclwwlk6  30460  ex-ind-dvds  30531  nndiffz1  32859  fzo0opth  32876  ccatf1  33009  pfxlsw2ccat  33010  wrdt2ind  33013  gsummulsubdishift1  33129  gsumwrd2dccatlem  33138  cycpmfv1  33174  cycpmco2lem2  33188  cycpmco2lem3  33189  cycpmco2lem4  33190  cycpmco2lem5  33191  cycpmco2lem6  33192  cycpmco2  33194  cycpmrn  33204  cyc3genpm  33213  cycpmconjslem2  33216  cyc3conja  33218  archirng  33249  archirngz  33250  archiabllem1a  33252  gsumind  33405  elrspunidl  33488  ply1coedeg  33649  ply1degltel  33654  gsummoncoe1fz  33658  esplyfval2  33709  esplympl  33711  esplyfval3  33716  esplyindfv  33720  vietalem  33723  ply1degltdimlem  33766  fldextrspundgdvds  33825  algextdeglem8  33868  rtelextdg2  33871  constrext2chnlem  33894  cos9thpiminplylem2  33927  cos9thpiminplylem3  33928  cos9thpiminplylem6  33931  cos9thpiminply  33932  madjusmdetlem4  33974  zrhcntr  34123  qqhval2lem  34125  oddpwdc  34498  eulerpartlems  34504  eulerpartlemb  34512  sseqfv1  34533  sseqfn  34534  sseqmw  34535  sseqf  34536  sseqfv2  34538  sseqp1  34539  ccatmulgnn0dir  34686  signsplypnf  34694  signsply0  34695  signslema  34706  signstfvn  34713  signstfvp  34715  signstfvc  34718  fsum2dsub  34751  reprinfz1  34766  reprfi2  34767  hashrepr  34769  reprdifc  34771  breprexplema  34774  breprexplemc  34776  circlemeth  34784  circlevma  34786  circlemethhgt  34787  hgt750lema  34801  tgoldbachgtde  34804  lpadlem3  34822  revpfxsfxrev  35298  revwlk  35307  subfacval3  35371  bcprod  35920  bccolsum  35921  fwddifnp1  36347  knoppndvlem6  36777  knoppndvlem7  36778  knoppndvlem10  36781  knoppndvlem14  36785  knoppndvlem15  36786  knoppndvlem16  36787  knoppndvlem17  36788  knoppndvlem19  36790  knoppndvlem21  36792  dfgcd3  37638  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem13  37954  poimirlem14  37955  poimirlem17  37958  poimirlem21  37962  poimirlem22  37963  poimirlem23  37964  poimirlem26  37967  poimirlem27  37968  poimirlem31  37972  geomcau  38080  bccl2d  42430  lcmineqlem12  42479  lcmineqlem17  42484  dvrelogpow2b  42507  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p3  42517  aks4d1p6  42520  aks4d1p8d2  42524  aks4d1p8d3  42525  aks4d1p8  42526  primrootscoprmpow  42538  primrootlekpowne0  42544  aks6d1c1  42555  aks6d1c2p2  42558  aks6d1c2lem4  42566  aks6d1c2  42569  aks6d1c5lem3  42576  aks6d1c5lem2  42577  2np3bcnp1  42583  sticksstones5  42589  sticksstones6  42590  sticksstones7  42591  sticksstones10  42594  sticksstones11  42595  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  aks6d1c6lem3  42611  bcled  42617  bcle2d  42618  aks6d1c7lem1  42619  aks6d1c7lem2  42620  grpods  42633  unitscyglem2  42635  unitscyglem4  42637  aks5lem8  42640  sumcubes  42745  gcdle1d  42762  gcdle2d  42763  frlmvscadiccat  42951  fltdiv  43069  flt4lem4  43082  fltnltalem  43095  eldioph2lem1  43192  pellexlem5  43261  congrep  43401  jm2.18  43416  jm2.19lem1  43417  jm2.19lem2  43418  jm2.19  43421  jm2.22  43423  jm2.23  43424  jm2.20nn  43425  jm2.25  43427  jm2.26a  43428  jm2.26lem3  43429  jm2.26  43430  jm2.27a  43433  jm2.27b  43434  jm2.27c  43435  jm3.1  43448  expdiophlem1  43449  hbtlem5  43556  radcnvrat  44741  nzin  44745  bccbc  44772  binomcxplemnn0  44776  binomcxplemnotnn0  44783  fprodexp  46024  mccllem  46027  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnxpaek  46370  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  wallispilem1  46493  wallispilem5  46497  stirlinglem3  46504  stirlinglem5  46506  stirlinglem7  46508  stirlinglem8  46509  fourierdlem102  46636  fourierdlem114  46648  sqwvfoura  46656  elaa2lem  46661  etransclem10  46672  etransclem20  46682  etransclem21  46683  etransclem22  46684  etransclem23  46685  etransclem24  46686  etransclem27  46689  etransclem28  46690  etransclem35  46697  etransclem38  46700  etransclem44  46706  etransclem45  46707  etransclem46  46708  sge0ad2en  46859  chnsubseqwl  47309  chnsubseq  47310  fsummmodsnunz  47831  fmtnoge3  47993  fmtnof1  47998  fmtnorec1  48000  sqrtpwpw2p  48001  fmtnodvds  48007  goldbachthlem2  48009  fmtnoprmfac2lem1  48029  lighneallem3  48070  lighneallem4b  48072  lighneallem4  48073  ssnn0ssfz  48825  altgsumbcALT  48829  flnn0ohalf  49010  dig2nn1st  49081  0dig2nn0o  49089  aacllem  50276