Theorem nn0zd 12489

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℕ₀cn0 12376  ℤcz 12463

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663  ax-1cn 11059  ax-icn 11060  ax-addcl 11061  ax-addrcl 11062  ax-mulcl 11063  ax-mulrcl 11064  ax-i2m1 11069  ax-1ne0 11070  ax-rnegex 11072  ax-rrecex 11073  ax-cnre 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3917  df-nul 4279  df-if 4471  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5506  df-eprel 5511  df-po 5519  df-so 5520  df-fr 5564  df-we 5566  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624  df-pred 6243  df-ord 6304  df-on 6305  df-lim 6306  df-suc 6307  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-ov 7344  df-om 7792  df-2nd 7917  df-frecs 8206  df-wrecs 8237  df-recs 8286  df-rdg 8324  df-neg 11342  df-nn 12121  df-n0 12377  df-z 12464

This theorem is referenced by:  nnzd  12490  eluzmn  12734  difelfznle  13537  elfzodif0  13665  zmodfz  13792  expnegz  13998  expaddzlem  14007  expaddz  14008  expmulz  14010  faclbnd  14192  bcpasc  14223  hashf1  14359  fz1isolem  14363  hashge2el2dif  14382  hashtpg  14387  wrdffz  14437  ffz0iswrd  14443  wrdsymb0  14451  wrdlenge1n0  14452  ccatcl  14476  ccatval3  14481  ccatdmss  14484  ccatsymb  14485  ccatval21sw  14488  ccatass  14491  ccatrn  14492  lswccatn0lsw  14494  ccats1val2  14530  swrdnd  14557  swrdccat2  14572  pfxtrcfv0  14596  pfxtrcfvl  14599  pfxccat1  14604  swrdccatin2  14631  pfxccatin12  14635  pfxccatpfx2  14639  pfxccat3a  14640  splfv2a  14658  splval2  14659  revcl  14663  revccat  14668  revrev  14669  cshwmodn  14697  cshwsublen  14698  cshwn  14699  cshwidxmod  14705  2cshwid  14716  3cshw  14720  cshweqdif2  14721  revco  14736  ccatco  14737  ccat2s1fvwALT  14857  ofccat  14871  zabscl  15215  absrdbnd  15244  iseraltlem3  15586  fsum0diaglem  15678  modfsummods  15695  binomlem  15731  binom1p  15733  incexc2  15740  climcndslem1  15751  geoser  15769  pwm1geoser  15771  geolim2  15773  mertenslem1  15786  mertenslem2  15787  mertens  15788  binomfallfaclem2  15942  binomrisefac  15944  fallfacval4  15945  bpolydiflem  15956  ruclem10  16143  sumodd  16294  divalglem9  16307  divalgmod  16312  bitsfzolem  16340  bitsfzo  16341  bitsmod  16342  bitsfi  16343  bitsinv1lem  16347  sadcaddlem  16363  sadadd3  16367  sadaddlem  16372  sadadd  16373  sadasslem  16376  sadass  16377  sadeq  16378  bitsres  16379  bitsuz  16380  bitsshft  16381  smuval2  16388  smupvallem  16389  smupval  16394  smueqlem  16396  smumullem  16398  smumul  16399  gcdcllem1  16405  zeqzmulgcd  16416  gcd0id  16425  gcdneg  16428  modgcd  16438  gcdmultipled  16440  bezoutlem4  16448  dvdsgcdb  16451  gcdass  16453  mulgcd  16454  gcdzeq  16458  dvdsmulgcd  16462  bezoutr  16474  bezoutr1  16475  nn0seqcvgd  16476  algfx  16486  eucalginv  16490  eucalg  16493  gcddvdslcm  16508  lcmneg  16509  lcmgcdlem  16512  lcmdvds  16514  lcmgcdeq  16518  lcmdvdsb  16519  lcmass  16520  lcmftp  16542  lcmfunsnlem1  16543  lcmfunsnlem2lem1  16544  lcmfunsnlem2lem2  16545  lcmfunsnlem2  16546  lcmfdvdsb  16549  lcmfun  16551  lcmfass  16552  mulgcddvds  16561  rpmulgcd2  16562  qredeu  16564  divgcdcoprm0  16571  sqnprm  16608  prmdvdsbc  16632  divnumden  16654  powm2modprm  16710  coprimeprodsq  16715  iserodd  16742  pclem  16745  pcpre1  16749  pcpremul  16750  pcqcl  16763  pcdvdsb  16776  pcidlem  16779  pc2dvds  16786  pcprmpw2  16789  dvdsprmpweqle  16793  pcadd  16796  pcfac  16806  pcbc  16807  pockthlem  16812  prmreclem2  16824  prmreclem3  16825  mul4sqlem  16860  4sqlem11  16862  4sqlem12  16863  4sqlem14  16865  vdwapun  16881  prmgaplcmlem1  16958  chnind  18522  chnub  18523  chnpolfz  18534  lagsubg  19102  psgnuni  19406  psgnran  19422  odmodnn0  19447  mndodconglem  19448  mndodcong  19449  odm1inv  19460  odmulg2  19462  odmulg  19463  odmulgeq  19464  odbezout  19465  odinv  19468  odf1  19469  gexod  19493  gexdvds3  19497  sylow1lem1  19505  sylow1lem3  19507  pgpfi  19512  pgpssslw  19521  sylow2alem2  19525  sylow2blem3  19529  fislw  19532  sylow3lem4  19537  sylow3lem6  19539  efginvrel2  19634  efgredlemf  19648  efgredlemd  19651  efgredlemc  19652  efgredlem  19654  efgcpbllemb  19662  odadd1  19755  odadd2  19756  gexexlem  19759  gexex  19760  torsubg  19761  lt6abl  19802  gsummulg  19849  ablfacrplem  19974  ablfacrp  19975  ablfacrp2  19976  ablfac1b  19979  ablfac1c  19980  ablfac1eulem  19981  ablfac1eu  19982  pgpfac1lem2  19984  pgpfaclem1  19990  ablfaclem3  19996  srgbinomlem3  20141  srgbinomlem4  20142  chrid  21457  znunit  21495  freshmansdream  21506  psgnghm  21512  asclmulg  21834  psrbaglefi  21858  psdvsca  22074  psdmul  22076  chfacfscmulfsupp  22769  chfacfpmmulfsupp  22773  cpmadugsumlemF  22786  dyadss  25517  dyaddisjlem  25518  ply1divex  26064  ply1termlem  26130  plyeq0lem  26137  plyaddlem1  26140  plymullem1  26141  coeeulem  26151  coeidlem  26164  coeeq2  26169  coemulhi  26181  dvply1  26213  dvply2g  26214  dvply2gOLD  26215  plydivex  26227  elqaalem2  26250  aareccl  26256  aannenlem1  26258  aalioulem1  26262  taylplem1  26292  taylplem2  26293  taylpfval  26294  dvtaylp  26300  taylthlem2  26304  taylthlem2OLD  26305  dvradcnv  26352  abelthlem7  26370  cxpeq  26689  birthdaylem2  26884  ftalem1  27005  basellem3  27015  isppw2  27047  isnsqf  27067  mule1  27080  ppinncl  27106  musum  27123  chtublem  27144  pclogsum  27148  vmasum  27149  dchrabs  27193  bcmax  27211  bposlem1  27217  bposlem6  27222  lgsval2lem  27240  lgsmod  27256  lgsne0  27268  gausslemma2dlem0h  27296  gausslemma2dlem0i  27297  gausslemma2dlem2  27300  gausslemma2dlem6  27305  gausslemma2d  27307  lgseisenlem1  27308  lgseisenlem2  27309  lgseisenlem3  27310  lgseisenlem4  27311  lgsquadlem1  27313  m1lgs  27321  2lgslem1a  27324  2lgslem3a  27329  2lgslem3b  27330  2lgslem3c  27331  2lgslem3d  27332  2lgslem3d1  27336  2lgsoddprmlem2  27342  2sqlem8  27359  2sqcoprm  27368  2sqmod  27369  chebbnd1lem1  27402  dchrisumlem1  27422  dchrisum0flblem1  27441  selberg2lem  27483  ostth2lem2  27567  ostth2lem3  27568  finsumvtxdg2sstep  29523  finsumvtxdgeven  29526  vtxdgoddnumeven  29527  redwlklem  29643  wlkdlem1  29654  pthdlem1  29739  crctcshwlkn0lem4  29786  wwlksnredwwlkn0  29869  wwlksnextproplem2  29883  clwwlkccatlem  29961  clwlkclwwlkfo  29981  clwwlkwwlksb  30026  clwwlkndivn  30052  eupth2lem3lem3  30202  eupth2lem3lem4  30203  eupth2lem3  30208  eupth2lems  30210  numclwwlk5  30360  numclwwlk6  30362  ex-ind-dvds  30433  nndiffz1  32761  fzo0opth  32777  ccatf1  32922  pfxlsw2ccat  32923  wrdt2ind  32926  gsumwrd2dccatlem  33038  cycpmfv1  33074  cycpmco2lem2  33088  cycpmco2lem3  33089  cycpmco2lem4  33090  cycpmco2lem5  33091  cycpmco2lem6  33092  cycpmco2  33094  cycpmrn  33104  cyc3genpm  33113  cycpmconjslem2  33116  cyc3conja  33118  archirng  33149  archirngz  33150  archiabllem1a  33152  gsumind  33302  elrspunidl  33385  ply1degltel  33547  esplympl  33580  ply1degltdimlem  33627  fldextrspundgdvds  33686  algextdeglem8  33729  rtelextdg2  33732  constrext2chnlem  33755  cos9thpiminplylem2  33788  cos9thpiminplylem3  33789  cos9thpiminplylem6  33792  cos9thpiminply  33793  madjusmdetlem4  33835  zrhcntr  33984  qqhval2lem  33986  oddpwdc  34359  eulerpartlems  34365  eulerpartlemb  34373  sseqfv1  34394  sseqfn  34395  sseqmw  34396  sseqf  34397  sseqfv2  34399  sseqp1  34400  ccatmulgnn0dir  34547  signsplypnf  34555  signsply0  34556  signslema  34567  signstfvn  34574  signstfvp  34576  signstfvc  34579  fsum2dsub  34612  reprinfz1  34627  reprfi2  34628  hashrepr  34630  reprdifc  34632  breprexplema  34635  breprexplemc  34637  circlemeth  34645  circlevma  34647  circlemethhgt  34648  hgt750lema  34662  tgoldbachgtde  34665  lpadlem3  34683  revpfxsfxrev  35152  revwlk  35161  subfacval3  35225  bcprod  35774  bccolsum  35775  fwddifnp1  36199  knoppndvlem6  36551  knoppndvlem7  36552  knoppndvlem10  36555  knoppndvlem14  36559  knoppndvlem15  36560  knoppndvlem16  36561  knoppndvlem17  36562  knoppndvlem19  36564  knoppndvlem21  36566  dfgcd3  37358  poimirlem3  37663  poimirlem4  37664  poimirlem6  37666  poimirlem13  37673  poimirlem14  37674  poimirlem17  37677  poimirlem21  37681  poimirlem22  37682  poimirlem23  37683  poimirlem26  37686  poimirlem27  37687  poimirlem31  37691  geomcau  37799  bccl2d  42024  lcmineqlem12  42073  lcmineqlem17  42078  dvrelogpow2b  42101  aks4d1p1p2  42103  aks4d1p1p4  42104  aks4d1p1p6  42106  aks4d1p1p7  42107  aks4d1p1p5  42108  aks4d1p1  42109  aks4d1p3  42111  aks4d1p6  42114  aks4d1p8d2  42118  aks4d1p8d3  42119  aks4d1p8  42120  primrootscoprmpow  42132  primrootlekpowne0  42138  aks6d1c1  42149  aks6d1c2p2  42152  aks6d1c2lem4  42160  aks6d1c2  42163  aks6d1c5lem3  42170  aks6d1c5lem2  42171  2np3bcnp1  42177  sticksstones5  42183  sticksstones6  42184  sticksstones7  42185  sticksstones10  42188  sticksstones11  42189  sticksstones12a  42190  sticksstones12  42191  sticksstones22  42201  aks6d1c6lem3  42205  bcled  42211  bcle2d  42212  aks6d1c7lem1  42213  aks6d1c7lem2  42214  grpods  42227  unitscyglem2  42229  unitscyglem4  42231  aks5lem8  42234  sumcubes  42346  gcdle1d  42363  gcdle2d  42364  frlmvscadiccat  42539  fltdiv  42669  flt4lem4  42682  fltnltalem  42695  eldioph2lem1  42793  pellexlem5  42866  congrep  43006  jm2.18  43021  jm2.19lem1  43022  jm2.19lem2  43023  jm2.19  43026  jm2.22  43028  jm2.23  43029  jm2.20nn  43030  jm2.25  43032  jm2.26a  43033  jm2.26lem3  43034  jm2.26  43035  jm2.27a  43038  jm2.27b  43039  jm2.27c  43040  jm3.1  43053  expdiophlem1  43054  hbtlem5  43161  radcnvrat  44347  nzin  44351  bccbc  44378  binomcxplemnn0  44382  binomcxplemnotnn0  44389  fprodexp  45634  mccllem  45637  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  dvnxpaek  45980  dvnmul  45981  dvnprodlem1  45984  dvnprodlem2  45985  wallispilem1  46103  wallispilem5  46107  stirlinglem3  46114  stirlinglem5  46116  stirlinglem7  46118  stirlinglem8  46119  fourierdlem102  46246  fourierdlem114  46258  sqwvfoura  46266  elaa2lem  46271  etransclem10  46282  etransclem20  46292  etransclem21  46293  etransclem22  46294  etransclem23  46295  etransclem24  46296  etransclem27  46299  etransclem28  46300  etransclem35  46307  etransclem38  46310  etransclem44  46316  etransclem45  46317  etransclem46  46318  sge0ad2en  46469  fsummmodsnunz  47406  fmtnoge3  47561  fmtnof1  47566  fmtnorec1  47568  sqrtpwpw2p  47569  fmtnodvds  47575  goldbachthlem2  47577  fmtnoprmfac2lem1  47597  lighneallem3  47638  lighneallem4b  47640  lighneallem4  47641  ssnn0ssfz  48380  altgsumbcALT  48384  flnn0ohalf  48566  dig2nn1st  48637  0dig2nn0o  48645  aacllem  49833