Theorem nn0zd 12540

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

Syntax hints:   → wi 4   ∈ wcel 2119  ℕ₀cn0 12428  ℤcz 12515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362  ax-un 7678  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-i2m1 11097  ax-1ne0 11098  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-iun 4923  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-ov 7359  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-neg 11371  df-nn 12166  df-n0 12429  df-z 12516

This theorem is referenced by:  nnzd  12541  eluzmn  12786  difelfznle  13587  elfzodif0  13716  zmodfz  13843  expnegz  14049  expaddzlem  14058  expaddz  14059  expmulz  14061  faclbnd  14243  bcpasc  14274  hashf1  14410  fz1isolem  14414  hashge2el2dif  14433  hashtpg  14438  wrdffz  14488  ffz0iswrd  14494  wrdsymb0  14502  wrdlenge1n0  14503  ccatcl  14527  ccatval3  14532  ccatdmss  14535  ccatsymb  14536  ccatval21sw  14539  ccatass  14542  ccatrn  14543  lswccatn0lsw  14545  ccats1val2  14581  swrdnd  14608  swrdccat2  14623  pfxtrcfv0  14647  pfxtrcfvl  14650  pfxccat1  14655  swrdccatin2  14682  pfxccatin12  14686  pfxccatpfx2  14690  pfxccat3a  14691  splfv2a  14709  splval2  14710  revcl  14714  revccat  14719  revrev  14720  cshwmodn  14748  cshwsublen  14749  cshwn  14750  cshwidxmod  14756  2cshwid  14767  3cshw  14771  cshweqdif2  14772  revco  14787  ccatco  14788  ccat2s1fvwALT  14908  ofccat  14922  zabscl  15266  absrdbnd  15295  iseraltlem3  15637  fsum0diaglem  15729  modfsummods  15747  binomlem  15785  binom1p  15787  incexc2  15794  climcndslem1  15805  geoser  15823  pwm1geoser  15825  geolim2  15827  mertenslem1  15840  mertenslem2  15841  mertens  15842  binomfallfaclem2  15996  binomrisefac  15998  fallfacval4  15999  bpolydiflem  16010  ruclem10  16197  sumodd  16348  divalglem9  16361  divalgmod  16366  bitsfzolem  16394  bitsfzo  16395  bitsmod  16396  bitsfi  16397  bitsinv1lem  16401  sadcaddlem  16417  sadadd3  16421  sadaddlem  16426  sadadd  16427  sadasslem  16430  sadass  16431  sadeq  16432  bitsres  16433  bitsuz  16434  bitsshft  16435  smuval2  16442  smupvallem  16443  smupval  16448  smueqlem  16450  smumullem  16452  smumul  16453  gcdcllem1  16459  zeqzmulgcd  16470  gcd0id  16479  gcdneg  16482  modgcd  16492  gcdmultipled  16494  bezoutlem4  16502  dvdsgcdb  16505  gcdass  16507  mulgcd  16508  gcdzeq  16512  dvdsmulgcd  16516  bezoutr  16528  bezoutr1  16529  nn0seqcvgd  16530  algfx  16540  eucalginv  16544  eucalg  16547  gcddvdslcm  16562  lcmneg  16563  lcmgcdlem  16566  lcmdvds  16568  lcmgcdeq  16572  lcmdvdsb  16573  lcmass  16574  lcmftp  16596  lcmfunsnlem1  16597  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  lcmfunsnlem2  16600  lcmfdvdsb  16603  lcmfun  16605  lcmfass  16606  mulgcddvds  16615  rpmulgcd2  16616  qredeu  16618  divgcdcoprm0  16625  sqnprm  16663  prmdvdsbc  16687  divnumden  16709  powm2modprm  16765  coprimeprodsq  16770  iserodd  16797  pclem  16800  pcpre1  16804  pcpremul  16805  pcqcl  16818  pcdvdsb  16831  pcidlem  16834  pc2dvds  16841  pcprmpw2  16844  dvdsprmpweqle  16848  pcadd  16851  pcfac  16861  pcbc  16862  pockthlem  16867  prmreclem2  16879  prmreclem3  16880  mul4sqlem  16915  4sqlem11  16917  4sqlem12  16918  4sqlem14  16920  vdwapun  16936  prmgaplcmlem1  17013  chnind  18578  chnub  18579  chnpolfz  18590  lagsubg  19161  psgnuni  19465  psgnran  19481  odmodnn0  19506  mndodconglem  19507  mndodcong  19508  odm1inv  19519  odmulg2  19521  odmulg  19522  odmulgeq  19523  odbezout  19524  odinv  19527  odf1  19528  gexod  19552  gexdvds3  19556  sylow1lem1  19564  sylow1lem3  19566  pgpfi  19571  pgpssslw  19580  sylow2alem2  19584  sylow2blem3  19588  fislw  19591  sylow3lem4  19596  sylow3lem6  19598  efginvrel2  19693  efgredlemf  19707  efgredlemd  19710  efgredlemc  19711  efgredlem  19713  efgcpbllemb  19721  odadd1  19814  odadd2  19815  gexexlem  19818  gexex  19819  torsubg  19820  lt6abl  19861  gsummulg  19908  ablfacrplem  20033  ablfacrp  20034  ablfacrp2  20035  ablfac1b  20038  ablfac1c  20039  ablfac1eulem  20040  ablfac1eu  20041  pgpfac1lem2  20043  pgpfaclem1  20049  ablfaclem3  20055  srgbinomlem3  20200  srgbinomlem4  20201  chrid  21500  znunit  21538  freshmansdream  21549  psgnghm  21555  asclmulg  21877  psrbaglefi  21901  psdvsca  22152  psdmul  22154  chfacfscmulfsupp  22842  chfacfpmmulfsupp  22846  cpmadugsumlemF  22859  dyadss  25579  dyaddisjlem  25580  ply1divex  26120  ply1termlem  26186  plyeq0lem  26193  plyaddlem1  26196  plymullem1  26197  coeeulem  26207  coeidlem  26220  coeeq2  26225  coemulhi  26237  dvply1  26268  dvply2g  26269  plydivex  26281  elqaalem2  26304  aareccl  26310  aannenlem1  26312  aalioulem1  26316  taylplem1  26346  taylplem2  26347  taylpfval  26348  dvtaylp  26353  taylthlem2  26357  dvradcnv  26404  abelthlem7  26421  cxpeq  26739  birthdaylem2  26934  ftalem1  27054  basellem3  27064  isppw2  27096  isnsqf  27116  mule1  27129  ppinncl  27155  musum  27172  chtublem  27192  pclogsum  27196  vmasum  27197  dchrabs  27241  bcmax  27259  bposlem1  27265  bposlem6  27270  lgsval2lem  27288  lgsmod  27304  lgsne0  27316  gausslemma2dlem0h  27344  gausslemma2dlem0i  27345  gausslemma2dlem2  27348  gausslemma2dlem6  27353  gausslemma2d  27355  lgseisenlem1  27356  lgseisenlem2  27357  lgseisenlem3  27358  lgseisenlem4  27359  lgsquadlem1  27361  m1lgs  27369  2lgslem1a  27372  2lgslem3a  27377  2lgslem3b  27378  2lgslem3c  27379  2lgslem3d  27380  2lgslem3d1  27384  2lgsoddprmlem2  27390  2sqlem8  27407  2sqcoprm  27416  2sqmod  27417  chebbnd1lem1  27450  dchrisumlem1  27470  dchrisum0flblem1  27489  selberg2lem  27531  ostth2lem2  27615  ostth2lem3  27616  finsumvtxdg2sstep  29636  finsumvtxdgeven  29639  vtxdgoddnumeven  29640  redwlklem  29756  wlkdlem1  29767  pthdlem1  29852  crctcshwlkn0lem4  29899  wwlksnredwwlkn0  29982  wwlksnextproplem2  29996  clwwlkccatlem  30077  clwlkclwwlkfo  30097  clwwlkwwlksb  30142  clwwlkndivn  30168  eupth2lem3lem3  30318  eupth2lem3lem4  30319  eupth2lem3  30324  eupth2lems  30326  numclwwlk5  30476  numclwwlk6  30478  ex-ind-dvds  30549  nndiffz1  32878  fzo0opth  32895  ccatf1  33028  pfxlsw2ccat  33029  wrdt2ind  33032  gsummulsubdishift1  33149  gsumwrd2dccatlem  33158  cycpmfv1  33194  cycpmco2lem2  33208  cycpmco2lem3  33209  cycpmco2lem4  33210  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2  33214  cycpmrn  33224  cyc3genpm  33233  cycpmconjslem2  33236  cyc3conja  33238  archirng  33269  archirngz  33270  archiabllem1a  33272  gsumind  33428  elrspunidl  33511  ply1coedeg  33672  ply1degltel  33677  gsummoncoe1fz  33681  selvply1rhmlemb  33703  esplyfval2  33749  esplympl  33751  esplyfval3  33756  esplyindfv  33760  vietalem  33763  ply1degltdimlem  33806  fldextrspundgdvds  33865  algextdeglem8  33908  rtelextdg2  33911  constrext2chnlem  33934  cos9thpiminplylem2  33967  cos9thpiminplylem3  33968  cos9thpiminplylem6  33971  cos9thpiminply  33972  madjusmdetlem4  34014  zrhcntr  34163  qqhval2lem  34165  oddpwdc  34538  eulerpartlems  34544  eulerpartlemb  34552  sseqfv1  34573  sseqfn  34574  sseqmw  34575  sseqf  34576  sseqfv2  34578  sseqp1  34579  ccatmulgnn0dir  34726  signsplypnf  34734  signsply0  34735  signslema  34746  signstfvn  34753  signstfvp  34755  signstfvc  34758  fsum2dsub  34791  reprinfz1  34806  reprfi2  34807  hashrepr  34809  reprdifc  34811  breprexplema  34814  breprexplemc  34816  circlemeth  34824  circlevma  34826  circlemethhgt  34827  hgt750lema  34841  tgoldbachgtde  34844  lpadlem3  34862  revpfxsfxrev  35344  revwlk  35353  subfacval3  35417  bcprod  35966  bccolsum  35967  fwddifnp1  36393  knoppndvlem6  36823  knoppndvlem7  36824  knoppndvlem10  36827  knoppndvlem14  36831  knoppndvlem15  36832  knoppndvlem16  36833  knoppndvlem17  36834  knoppndvlem19  36836  knoppndvlem21  36838  dfgcd3  37684  poimirlem3  37990  poimirlem4  37991  poimirlem6  37993  poimirlem13  38000  poimirlem14  38001  poimirlem17  38004  poimirlem21  38008  poimirlem22  38009  poimirlem23  38010  poimirlem26  38013  poimirlem27  38014  poimirlem31  38018  geomcau  38126  bccl2d  42476  lcmineqlem12  42525  lcmineqlem17  42530  dvrelogpow2b  42553  aks4d1p1p2  42555  aks4d1p1p4  42556  aks4d1p1p6  42558  aks4d1p1p7  42559  aks4d1p1p5  42560  aks4d1p1  42561  aks4d1p3  42563  aks4d1p6  42566  aks4d1p8d2  42570  aks4d1p8d3  42571  aks4d1p8  42572  primrootscoprmpow  42584  primrootlekpowne0  42590  aks6d1c1  42601  aks6d1c2p2  42604  aks6d1c2lem4  42612  aks6d1c2  42615  aks6d1c5lem3  42622  aks6d1c5lem2  42623  2np3bcnp1  42629  sticksstones5  42635  sticksstones6  42636  sticksstones7  42637  sticksstones10  42640  sticksstones11  42641  sticksstones12a  42642  sticksstones12  42643  sticksstones22  42653  aks6d1c6lem3  42657  bcled  42663  bcle2d  42664  aks6d1c7lem1  42665  aks6d1c7lem2  42666  grpods  42679  unitscyglem2  42681  unitscyglem4  42683  aks5lem8  42686  sumcubes  42790  gcdle1d  42807  gcdle2d  42808  frlmvscadiccat  42996  fltdiv  43086  flt4lem4  43099  fltnltalem  43112  eldioph2lem1  43209  pellexlem5  43278  congrep  43418  jm2.18  43433  jm2.19lem1  43434  jm2.19lem2  43435  jm2.19  43438  jm2.22  43440  jm2.23  43441  jm2.20nn  43442  jm2.25  43444  jm2.26a  43445  jm2.26lem3  43446  jm2.26  43447  jm2.27a  43450  jm2.27b  43451  jm2.27c  43452  jm3.1  43465  expdiophlem1  43466  hbtlem5  43573  radcnvrat  44758  nzin  44762  bccbc  44789  binomcxplemnn0  44793  binomcxplemnotnn0  44800  fprodexp  46039  mccllem  46042  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnxpaek  46385  dvnmul  46386  dvnprodlem1  46389  dvnprodlem2  46390  wallispilem1  46508  wallispilem5  46512  stirlinglem3  46519  stirlinglem5  46521  stirlinglem7  46523  stirlinglem8  46524  fourierdlem102  46651  fourierdlem114  46663  sqwvfoura  46671  elaa2lem  46676  etransclem10  46687  etransclem20  46697  etransclem21  46698  etransclem22  46699  etransclem23  46700  etransclem24  46701  etransclem27  46704  etransclem28  46705  etransclem35  46712  etransclem38  46715  etransclem44  46721  etransclem45  46722  etransclem46  46723  sge0ad2en  46874  chnsubseqwl  47324  chnsubseq  47325  fsummmodsnunz  47846  fmtnoge3  48008  fmtnof1  48013  fmtnorec1  48015  sqrtpwpw2p  48016  fmtnodvds  48022  goldbachthlem2  48024  fmtnoprmfac2lem1  48044  lighneallem3  48085  lighneallem4b  48087  lighneallem4  48088  ssnn0ssfz  48840  altgsumbcALT  48844  flnn0ohalf  49025  dig2nn1st  49096  0dig2nn0o  49104  aacllem  50291