Theorem nn0zd 12555

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕ₀cn0 12442  ℤcz 12529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-i2m1 11136  ax-1ne0 11137  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-neg 11408  df-nn 12187  df-n0 12443  df-z 12530

This theorem is referenced by:  nnzd  12556  eluzmn  12800  difelfznle  13603  zmodfz  13855  expnegz  14061  expaddzlem  14070  expaddz  14071  expmulz  14073  faclbnd  14255  bcpasc  14286  hashf1  14422  fz1isolem  14426  hashge2el2dif  14445  hashtpg  14450  wrdffz  14500  ffz0iswrd  14506  wrdsymb0  14514  wrdlenge1n0  14515  ccatcl  14539  ccatval3  14544  ccatsymb  14547  ccatval21sw  14550  ccatass  14553  ccatrn  14554  lswccatn0lsw  14556  ccats1val2  14592  swrdnd  14619  swrdccat2  14634  pfxtrcfv0  14659  pfxtrcfvl  14662  pfxccat1  14667  swrdccatin2  14694  pfxccatin12  14698  pfxccatpfx2  14702  pfxccat3a  14703  splfv2a  14721  splval2  14722  revcl  14726  revccat  14731  revrev  14732  cshwmodn  14760  cshwsublen  14761  cshwn  14762  cshwidxmod  14768  2cshwid  14779  3cshw  14783  cshweqdif2  14784  revco  14800  ccatco  14801  ccat2s1fvwALT  14921  ofccat  14935  zabscl  15279  absrdbnd  15308  iseraltlem3  15650  fsum0diaglem  15742  modfsummods  15759  binomlem  15795  binom1p  15797  incexc2  15804  climcndslem1  15815  geoser  15833  pwm1geoser  15835  geolim2  15837  mertenslem1  15850  mertenslem2  15851  mertens  15852  binomfallfaclem2  16006  binomrisefac  16008  fallfacval4  16009  bpolydiflem  16020  ruclem10  16207  sumodd  16358  divalglem9  16371  divalgmod  16376  bitsfzolem  16404  bitsfzo  16405  bitsmod  16406  bitsfi  16407  bitsinv1lem  16411  sadcaddlem  16427  sadadd3  16431  sadaddlem  16436  sadadd  16437  sadasslem  16440  sadass  16441  sadeq  16442  bitsres  16443  bitsuz  16444  bitsshft  16445  smuval2  16452  smupvallem  16453  smupval  16458  smueqlem  16460  smumullem  16462  smumul  16463  gcdcllem1  16469  zeqzmulgcd  16480  gcd0id  16489  gcdneg  16492  modgcd  16502  gcdmultipled  16504  bezoutlem4  16512  dvdsgcdb  16515  gcdass  16517  mulgcd  16518  gcdzeq  16522  dvdsmulgcd  16526  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  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  lagsubg  19127  psgnuni  19429  psgnran  19445  odmodnn0  19470  mndodconglem  19471  mndodcong  19472  odm1inv  19483  odmulg2  19485  odmulg  19486  odmulgeq  19487  odbezout  19488  odinv  19491  odf1  19492  gexod  19516  gexdvds3  19520  sylow1lem1  19528  sylow1lem3  19530  pgpfi  19535  pgpssslw  19544  sylow2alem2  19548  sylow2blem3  19552  fislw  19555  sylow3lem4  19560  sylow3lem6  19562  efginvrel2  19657  efgredlemf  19671  efgredlemd  19674  efgredlemc  19675  efgredlem  19677  efgcpbllemb  19685  odadd1  19778  odadd2  19779  gexexlem  19782  gexex  19783  torsubg  19784  lt6abl  19825  gsummulg  19872  ablfacrplem  19997  ablfacrp  19998  ablfacrp2  19999  ablfac1b  20002  ablfac1c  20003  ablfac1eulem  20004  ablfac1eu  20005  pgpfac1lem2  20007  pgpfaclem1  20013  ablfaclem3  20019  srgbinomlem3  20137  srgbinomlem4  20138  chrid  21435  znunit  21473  freshmansdream  21484  psgnghm  21489  asclmulg  21811  psrbaglefi  21835  psdvsca  22051  psdmul  22053  chfacfscmulfsupp  22746  chfacfpmmulfsupp  22750  cpmadugsumlemF  22763  dyadss  25495  dyaddisjlem  25496  ply1divex  26042  ply1termlem  26108  plyeq0lem  26115  plyaddlem1  26118  plymullem1  26119  coeeulem  26129  coeidlem  26142  coeeq2  26147  coemulhi  26159  dvply1  26191  dvply2g  26192  dvply2gOLD  26193  plydivex  26205  elqaalem2  26228  aareccl  26234  aannenlem1  26236  aalioulem1  26240  taylplem1  26270  taylplem2  26271  taylpfval  26272  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  dvradcnv  26330  abelthlem7  26348  cxpeq  26667  birthdaylem2  26862  ftalem1  26983  basellem3  26993  isppw2  27025  isnsqf  27045  mule1  27058  ppinncl  27084  musum  27101  chtublem  27122  pclogsum  27126  vmasum  27127  dchrabs  27171  bcmax  27189  bposlem1  27195  bposlem6  27200  lgsval2lem  27218  lgsmod  27234  lgsne0  27246  gausslemma2dlem0h  27274  gausslemma2dlem0i  27275  gausslemma2dlem2  27278  gausslemma2dlem6  27283  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquadlem1  27291  m1lgs  27299  2lgslem1a  27302  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgslem3d1  27314  2lgsoddprmlem2  27320  2sqlem8  27337  2sqcoprm  27346  2sqmod  27347  chebbnd1lem1  27380  dchrisumlem1  27400  dchrisum0flblem1  27419  selberg2lem  27461  ostth2lem2  27545  ostth2lem3  27546  finsumvtxdg2sstep  29477  finsumvtxdgeven  29480  vtxdgoddnumeven  29481  redwlklem  29599  wlkdlem1  29610  pthdlem1  29696  crctcshwlkn0lem4  29743  wwlksnredwwlkn0  29826  wwlksnextproplem2  29840  clwwlkccatlem  29918  clwlkclwwlkfo  29938  clwwlkwwlksb  29983  clwwlkndivn  30009  eupth2lem3lem3  30159  eupth2lem3lem4  30160  eupth2lem3  30165  eupth2lems  30167  numclwwlk5  30317  numclwwlk6  30319  ex-ind-dvds  30390  nndiffz1  32709  elfzodif0  32717  fzo0opth  32728  ccatf1  32870  ccatdmss  32871  pfxlsw2ccat  32872  wrdt2ind  32875  chnind  32937  chnub  32938  gsumwrd2dccatlem  33006  cycpmfv1  33070  cycpmco2lem2  33084  cycpmco2lem3  33085  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2  33090  cycpmrn  33100  cyc3genpm  33109  cycpmconjslem2  33112  cyc3conja  33114  archirng  33142  archirngz  33143  archiabllem1a  33145  elrspunidl  33399  ply1degltel  33560  ply1degltdimlem  33618  fldextrspundgdvds  33676  algextdeglem8  33714  rtelextdg2  33717  constrext2chnlem  33740  cos9thpiminplylem2  33773  cos9thpiminplylem3  33774  cos9thpiminplylem6  33777  cos9thpiminply  33778  madjusmdetlem4  33820  zrhcntr  33969  qqhval2lem  33971  oddpwdc  34345  eulerpartlems  34351  eulerpartlemb  34359  sseqfv1  34380  sseqfn  34381  sseqmw  34382  sseqf  34383  sseqfv2  34385  sseqp1  34386  ccatmulgnn0dir  34533  signsplypnf  34541  signsply0  34542  signslema  34553  signstfvn  34560  signstfvp  34562  signstfvc  34565  fsum2dsub  34598  reprinfz1  34613  reprfi2  34614  hashrepr  34616  reprdifc  34618  breprexplema  34621  breprexplemc  34623  circlemeth  34631  circlevma  34633  circlemethhgt  34634  hgt750lema  34648  tgoldbachgtde  34651  lpadlem3  34669  revpfxsfxrev  35103  revwlk  35112  subfacval3  35176  bcprod  35725  bccolsum  35726  fwddifnp1  36153  knoppndvlem6  36505  knoppndvlem7  36506  knoppndvlem10  36509  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem16  36515  knoppndvlem17  36516  knoppndvlem19  36518  knoppndvlem21  36520  dfgcd3  37312  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem13  37627  poimirlem14  37628  poimirlem17  37631  poimirlem21  37635  poimirlem22  37636  poimirlem23  37637  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  geomcau  37753  bccl2d  41979  lcmineqlem12  42028  lcmineqlem17  42033  dvrelogpow2b  42056  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p6  42061  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p3  42066  aks4d1p6  42069  aks4d1p8d2  42073  aks4d1p8d3  42074  aks4d1p8  42075  primrootscoprmpow  42087  primrootlekpowne0  42093  aks6d1c1  42104  aks6d1c2p2  42107  aks6d1c2lem4  42115  aks6d1c2  42118  aks6d1c5lem3  42125  aks6d1c5lem2  42126  2np3bcnp1  42132  sticksstones5  42138  sticksstones6  42139  sticksstones7  42140  sticksstones10  42143  sticksstones11  42144  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem3  42160  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7lem2  42169  grpods  42182  unitscyglem2  42184  unitscyglem4  42186  aks5lem8  42189  sumcubes  42301  gcdle1d  42318  gcdle2d  42319  frlmvscadiccat  42494  fltdiv  42624  flt4lem4  42637  fltnltalem  42650  eldioph2lem1  42748  pellexlem5  42821  congrep  42962  jm2.18  42977  jm2.19lem1  42978  jm2.19lem2  42979  jm2.19  42982  jm2.22  42984  jm2.23  42985  jm2.20nn  42986  jm2.25  42988  jm2.26a  42989  jm2.26lem3  42990  jm2.26  42991  jm2.27a  42994  jm2.27b  42995  jm2.27c  42996  jm3.1  43009  expdiophlem1  43010  hbtlem5  43117  radcnvrat  44303  nzin  44307  bccbc  44334  binomcxplemnn0  44338  binomcxplemnotnn0  44345  fprodexp  45592  mccllem  45595  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnxpaek  45940  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  wallispilem1  46063  wallispilem5  46067  stirlinglem3  46074  stirlinglem5  46076  stirlinglem7  46078  stirlinglem8  46079  fourierdlem102  46206  fourierdlem114  46218  sqwvfoura  46226  elaa2lem  46231  etransclem10  46242  etransclem20  46252  etransclem21  46253  etransclem22  46254  etransclem23  46255  etransclem24  46256  etransclem27  46259  etransclem28  46260  etransclem35  46267  etransclem38  46270  etransclem44  46276  etransclem45  46277  etransclem46  46278  sge0ad2en  46429  fsummmodsnunz  47376  fmtnoge3  47531  fmtnof1  47536  fmtnorec1  47538  sqrtpwpw2p  47539  fmtnodvds  47545  goldbachthlem2  47547  fmtnoprmfac2lem1  47567  lighneallem3  47608  lighneallem4b  47610  lighneallem4  47611  ssnn0ssfz  48337  altgsumbcALT  48341  flnn0ohalf  48523  dig2nn1st  48594  0dig2nn0o  48602  aacllem  49790