Theorem nn0zd 12758

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ℕ₀cn0 12646  ℤcz 12733

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-i2m1 11307  ax-1ne0 11308  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-neg 11583  df-nn 12376  df-n0 12647  df-z 12734

This theorem is used by:  nnzd  12759  eluzmn  13012  difelfznle  13816  elfzodif0  13945  zmodfz  14073  expnegz  14279  expaddzlem  14288  expaddz  14289  expmulz  14291  faclbnd  14475  bcpasc  14506  hashf1  14643  fz1isolem  14647  hashge2el2dif  14666  hashtpg  14671  wrdffz  14721  ffz0iswrd  14727  wrdsymb0  14735  wrdlenge1n0  14736  ccatcl  14760  ccatval3  14765  ccatdmss  14768  ccatsymb  14769  ccatval21sw  14772  ccatass  14775  ccatrn  14776  ccatf1  14777  lswccatn0lsw  14779  ccats1val2  14817  swrdnd  14846  swrdccat2  14861  pfxtrcfv0  14885  pfxtrcfvl  14888  pfxccat1  14893  swrdccatin2  14920  pfxccatin12  14924  pfxccatpfx2  14928  pfxccat3a  14929  splfv2a  14947  splval2  14948  revcl  14952  revccat  14957  revrev  14958  revpfxsfxrev  14959  cshwmodn  14988  cshwsublen  14989  cshwn  14990  cshwidxmod  14996  2cshwid  15007  3cshw  15011  cshweqdif2  15012  revco  15027  ccatco  15028  ccat2s1fvwALT  15151  ofccat  15165  zabscl  15523  absrdbnd  15553  iseraltlem3  15895  fsum0diaglem  15986  modfsummods  16004  binomlem  16042  binom1p  16044  incexc2  16051  climcndslem1  16062  geoser  16080  pwm1geoser  16082  geolim2  16084  mertenslem1  16097  mertenslem2  16098  mertens  16099  binomfallfaclem2  16250  binomrisefac  16252  fallfacval4  16253  bpolydiflem  16264  ruclem10  16451  sumodd  16602  divalglem9  16615  divalgmod  16620  bitsfzolem  16648  bitsfzo  16649  bitsmod  16650  bitsfi  16651  bitsinv1lem  16655  sadcaddlem  16671  sadadd3  16675  sadaddlem  16680  sadadd  16681  sadasslem  16684  sadass  16685  sadeq  16686  bitsres  16687  bitsuz  16688  bitsshft  16689  smuval2  16696  smupvallem  16697  smupval  16702  smueqlem  16704  smumullem  16706  smumul  16707  gcdcllem1  16713  gcdle1d  16724  gcdle2d  16725  zeqzmulgcd  16726  gcd0id  16735  gcdneg  16738  modgcd  16749  gcdmultipled  16751  bezoutlem4  16759  dvdsgcdb  16762  gcdass  16764  mulgcd  16765  gcdzeq  16769  dvdsmulgcd  16774  bezoutr  16787  bezoutr1  16788  nn0seqcvgd  16789  algfx  16799  eucalginv  16803  eucalg  16806  gcddvdslcm  16821  lcmneg  16822  lcmgcdlem  16825  lcmdvds  16827  lcmgcdeq  16831  lcmdvdsb  16832  lcmass  16833  lcmftp  16855  lcmfunsnlem1  16856  lcmfunsnlem2lem1  16857  lcmfunsnlem2lem2  16858  lcmfunsnlem2  16859  lcmfdvdsb  16862  lcmfun  16864  lcmfass  16865  mulgcddvds  16874  rpmulgcd2  16875  qredeu  16877  divgcdcoprm0  16884  sqnprm  16922  prmdvdsbc  16946  divnumden  16968  powm2modprm  17025  coprimeprodsq  17030  iserodd  17057  pclem  17060  pcpre1  17064  pcpremul  17065  pcqcl  17078  pcdvdsb  17091  pcidlem  17094  pc2dvds  17101  pcprmpw2  17104  dvdsprmpweqle  17108  pcadd  17111  pcfac  17121  pcbc  17122  pockthlem  17127  prmreclem2  17139  prmreclem3  17140  mul4sqlem  17175  4sqlem11  17177  4sqlem12  17178  4sqlem14  17180  vdwapun  17196  prmgaplcmlem1  17273  chnind  18845  chnub  18846  chnpolfz  18857  lagsubg  19460  psgnuni  19764  psgnran  19780  odmodnn0  19805  mndodconglem  19806  mndodcong  19807  odm1inv  19818  odmulg2  19820  odmulg  19821  odmulgeq  19822  odbezout  19823  odinv  19826  odf1  19827  gexod  19851  gexdvds3  19855  sylow1lem1  19863  sylow1lem3  19865  pgpfi  19870  pgpssslw  19879  sylow2alem2  19883  sylow2blem3  19887  fislw  19890  sylow3lem4  19895  sylow3lem6  19897  efginvrel2  19992  efgredlemf  20006  efgredlemd  20009  efgredlemc  20010  efgredlem  20012  efgcpbllemb  20020  odadd1  20113  odadd2  20114  gexexlem  20117  gexex  20118  torsubg  20119  lt6abl  20160  gsummulg  20207  ablfacrplem  20332  ablfacrp  20333  ablfacrp2  20334  ablfac1b  20337  ablfac1c  20338  ablfac1eulem  20339  ablfac1eu  20340  pgpfac1lem2  20342  pgpfaclem1  20348  ablfaclem3  20354  srgbinomlem3  20505  srgbinomlem4  20506  chrid  21886  znunit  21924  freshmansdream  21935  psgnghm  21941  asclmulg  22265  psrbaglefi  22289  psdvsca  22540  psdmul  22542  chfacfscmulfsupp  23232  chfacfpmmulfsupp  23236  cpmadugsumlemF  23249  dyadss  25970  dyaddisjlem  25971  ply1divex  26510  ply1termlem  26576  plyeq0lem  26584  plyaddlem1  26587  plymullem1  26588  coeeulem  26598  coeidlem  26611  coeeq2  26616  coemulhi  26628  dvply1  26660  dvply2g  26661  plydivex  26673  elqaalem2  26700  aareccl  26710  aannenlem1  26712  aalioulem1  26716  taylplem1  26747  taylplem2  26748  taylpfval  26749  dvtaylp  26754  taylthlem2  26758  dvradcnv  26805  abelthlem7  26822  cxpeq  27142  birthdaylem2  27337  ftalem1  27457  basellem3  27467  isppw2  27499  isnsqf  27519  mule1  27532  ppinncl  27558  musum  27575  chtublem  27595  pclogsum  27599  vmasum  27600  dchrabs  27644  bcmax  27662  bposlem1  27668  bposlem6  27673  lgsval2lem  27691  lgsmod  27707  lgsne0  27719  gausslemma2dlem0h  27747  gausslemma2dlem0i  27748  gausslemma2dlem2  27751  gausslemma2dlem6  27756  gausslemma2d  27758  lgseisenlem1  27759  lgseisenlem2  27760  lgseisenlem3  27761  lgseisenlem4  27762  lgsquadlem1  27764  m1lgs  27772  2lgslem1a  27775  2lgslem3a  27780  2lgslem3b  27781  2lgslem3c  27782  2lgslem3d  27783  2lgslem3d1  27787  2lgsoddprmlem2  27793  2sqlem8  27810  2sqcoprm  27819  2sqmod  27820  chebbnd1lem1  27853  dchrisumlem1  27873  dchrisum0flblem1  27892  selberg2lem  27934  ostth2lem2  28018  ostth2lem3  28019  fltdiv  28025  flt4lem4  28036  finsumvtxdg2sstep  30187  finsumvtxdgeven  30190  vtxdgoddnumeven  30191  redwlklem  30307  wlkdlem1  30318  revwlk  30324  pthdlem1  30409  crctcshwlkn0lem4  30459  wwlksnredwwlkn0  30542  wwlksnextproplem2  30556  clwwlkccatlem  30637  clwlkclwwlkfo  30657  clwwlkwwlksb  30702  clwwlkndivn  30728  eupth2lem3lem3  30888  eupth2lem3lem4  30889  eupth2lem3  30894  eupth2lems  30896  numclwwlk5  31046  numclwwlk6  31048  ex-ind-dvds  31119  nndiffz1  33474  fzo0opth  33491  pfxlsw2ccat  33609  wrdt2ind  33612  gsummulsubdishift1  33728  gsumwrd2dccatlem  33737  cycpmfv1  33773  cycpmco2lem2  33787  cycpmco2lem3  33788  cycpmco2lem4  33789  cycpmco2lem5  33790  cycpmco2lem6  33791  cycpmco2  33793  cycpmrn  33803  cyc3genpm  33812  cycpmconjslem2  33815  cyc3conja  33817  archirng  33848  archirngz  33849  archiabllem1a  33851  gsumind  34010  elrspunidl  34082  ply1coedeg  34224  ply1degltel  34229  gsummoncoe1fz  34233  selvply1rhmlemb  34262  esplyfval2  34308  esplympl  34310  esplyfval3  34315  esplyindfv  34319  vietalem  34322  ply1degltdimlem  34365  fldextrspundgdvds  34424  algextdeglem8  34467  rtelextdg2  34470  constrext2chnlem  34493  cos9thpiminplylem2  34526  cos9thpiminplylem3  34527  cos9thpiminplylem6  34530  cos9thpiminply  34531  madjusmdetlem4  34573  zrhcntr  34722  qqhval2lem  34724  oddpwdc  35097  eulerpartlems  35103  eulerpartlemb  35111  sseqfv1  35132  sseqfn  35133  sseqmw  35134  sseqf  35135  sseqfv2  35137  sseqp1  35138  ccatmulgnn0dir  35285  signsplypnf  35290  signsply0  35291  signslema  35302  signstfvn  35309  signstfvp  35311  signstfvc  35314  fsum2dsub  35347  reprinfz1  35362  reprfi2  35363  hashrepr  35365  reprdifc  35367  breprexplema  35370  breprexplemc  35372  circlemeth  35380  circlevma  35382  circlemethhgt  35383  hgt750lema  35397  tgoldbachgtde  35400  lpadlem3  35421  subfacval3  36162  bcprod  36718  bccolsum  36719  fwddifnp1  37145  knoppndvlem6  37598  knoppndvlem7  37599  knoppndvlem10  37602  knoppndvlem14  37606  knoppndvlem15  37607  knoppndvlem16  37608  knoppndvlem17  37609  knoppndvlem19  37611  knoppndvlem21  37613  dfgcd3  38513  poimirlem3  38809  poimirlem4  38810  poimirlem6  38812  poimirlem13  38819  poimirlem14  38820  poimirlem17  38823  poimirlem21  38827  poimirlem22  38828  poimirlem23  38829  poimirlem26  38832  poimirlem27  38833  poimirlem31  38837  geomcau  38959  bccl2d  43307  lcmineqlem12  43356  lcmineqlem17  43361  dvrelogpow2b  43384  aks4d1p1p2  43386  aks4d1p1p4  43387  aks4d1p1p6  43389  aks4d1p1p7  43390  aks4d1p1p5  43391  aks4d1p1  43392  aks4d1p3  43394  aks4d1p6  43397  aks4d1p8d2  43401  aks4d1p8d3  43402  aks4d1p8  43403  primrootscoprmpow  43415  primrootlekpowne0  43421  aks6d1c1  43432  aks6d1c2p2  43435  aks6d1c2lem4  43443  aks6d1c2  43446  aks6d1c5lem3  43453  aks6d1c5lem2  43454  2np3bcnp1  43460  sticksstones5  43466  sticksstones6  43467  sticksstones7  43468  sticksstones10  43471  sticksstones11  43472  sticksstones12a  43473  sticksstones12  43474  sticksstones22  43484  aks6d1c6lem3  43488  bcled  43494  bcle2d  43495  aks6d1c7lem1  43496  aks6d1c7lem2  43497  grpods  43510  unitscyglem2  43512  unitscyglem4  43514  aks5lem8  43517  sumcubes  43636  frlmvscadiccat  43839  fltnltalem  43939  eldioph2lem1  44037  pellexlem5  44106  congrep  44246  jm2.18  44261  jm2.19lem1  44262  jm2.19lem2  44263  jm2.19  44266  jm2.22  44268  jm2.23  44269  jm2.20nn  44270  jm2.25  44272  jm2.26a  44273  jm2.26lem3  44274  jm2.26  44275  jm2.27a  44278  jm2.27b  44279  jm2.27c  44280  jm3.1  44293  expdiophlem1  44294  hbtlem5  44395  radcnvrat  45559  nzin  45563  bccbc  45590  binomcxplemnn0  45594  binomcxplemnotnn0  45601  fprodexp  46879  mccllem  46882  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnxpaek  47225  dvnmul  47226  dvnprodlem1  47229  dvnprodlem2  47230  wallispilem1  47348  wallispilem5  47352  stirlinglem3  47359  stirlinglem5  47361  stirlinglem7  47363  stirlinglem8  47364  fourierdlem102  47491  fourierdlem114  47503  sqwvfoura  47511  elaa2lem  47516  etransclem10  47527  etransclem20  47537  etransclem21  47538  etransclem22  47539  etransclem23  47540  etransclem24  47541  etransclem27  47544  etransclem28  47545  etransclem35  47552  etransclem38  47555  etransclem44  47561  etransclem45  47562  etransclem46  47563  sge0ad2en  47714  chnsubseqwl  48162  chnsubseq  48163  sqrtnpoly  48216  fsummmodsnunz  48726  fmtnoge3  48888  fmtnof1  48893  fmtnorec1  48895  sqrtpwpw2p  48896  fmtnodvds  48902  goldbachthlem2  48904  fmtnoprmfac2lem1  48924  lighneallem3  48965  lighneallem4b  48967  lighneallem4  48968  ssnn0ssfz  49792  altgsumbcALT  49796  flnn0ohalf  49977  dig2nn1st  50048  0dig2nn0o  50056  aacllem  51367