Theorem nn0zd 12711

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ℕ₀cn0 12599  ℤcz 12686

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7749  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-i2m1 11261  ax-1ne0 11262  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7421  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-neg 11537  df-nn 12329  df-n0 12600  df-z 12687

This theorem is used by:  nnzd  12712  eluzmn  12965  difelfznle  13769  elfzodif0  13898  zmodfz  14026  expnegz  14232  expaddzlem  14241  expaddz  14242  expmulz  14244  faclbnd  14427  bcpasc  14458  hashf1  14595  fz1isolem  14599  hashge2el2dif  14618  hashtpg  14623  wrdffz  14673  ffz0iswrd  14679  wrdsymb0  14687  wrdlenge1n0  14688  ccatcl  14712  ccatval3  14717  ccatdmss  14720  ccatsymb  14721  ccatval21sw  14724  ccatass  14727  ccatrn  14728  ccatf1  14729  lswccatn0lsw  14731  ccats1val2  14768  swrdnd  14797  swrdccat2  14812  pfxtrcfv0  14836  pfxtrcfvl  14839  pfxccat1  14844  swrdccatin2  14871  pfxccatin12  14875  pfxccatpfx2  14879  pfxccat3a  14880  splfv2a  14898  splval2  14899  revcl  14903  revccat  14908  revrev  14909  revpfxsfxrev  14910  cshwmodn  14939  cshwsublen  14940  cshwn  14941  cshwidxmod  14947  2cshwid  14958  3cshw  14962  cshweqdif2  14963  revco  14978  ccatco  14979  ccat2s1fvwALT  15101  ofccat  15115  zabscl  15473  absrdbnd  15502  iseraltlem3  15844  fsum0diaglem  15935  modfsummods  15953  binomlem  15991  binom1p  15993  incexc2  16000  climcndslem1  16011  geoser  16029  pwm1geoser  16031  geolim2  16033  mertenslem1  16046  mertenslem2  16047  mertens  16048  binomfallfaclem2  16199  binomrisefac  16201  fallfacval4  16202  bpolydiflem  16213  ruclem10  16400  sumodd  16551  divalglem9  16564  divalgmod  16569  bitsfzolem  16597  bitsfzo  16598  bitsmod  16599  bitsfi  16600  bitsinv1lem  16604  sadcaddlem  16620  sadadd3  16624  sadaddlem  16629  sadadd  16630  sadasslem  16633  sadass  16634  sadeq  16635  bitsres  16636  bitsuz  16637  bitsshft  16638  smuval2  16645  smupvallem  16646  smupval  16651  smueqlem  16653  smumullem  16655  smumul  16656  gcdcllem1  16662  gcdle1d  16673  gcdle2d  16674  zeqzmulgcd  16675  gcd0id  16684  gcdneg  16687  modgcd  16698  gcdmultipled  16700  bezoutlem4  16708  dvdsgcdb  16711  gcdass  16713  mulgcd  16714  gcdzeq  16718  dvdsmulgcd  16723  bezoutr  16736  bezoutr1  16737  nn0seqcvgd  16738  algfx  16748  eucalginv  16752  eucalg  16755  gcddvdslcm  16770  lcmneg  16771  lcmgcdlem  16774  lcmdvds  16776  lcmgcdeq  16780  lcmdvdsb  16781  lcmass  16782  lcmftp  16804  lcmfunsnlem1  16805  lcmfunsnlem2lem1  16806  lcmfunsnlem2lem2  16807  lcmfunsnlem2  16808  lcmfdvdsb  16811  lcmfun  16813  lcmfass  16814  mulgcddvds  16823  rpmulgcd2  16824  qredeu  16826  divgcdcoprm0  16833  sqnprm  16871  prmdvdsbc  16895  divnumden  16917  powm2modprm  16974  coprimeprodsq  16979  iserodd  17006  pclem  17009  pcpre1  17013  pcpremul  17014  pcqcl  17027  pcdvdsb  17040  pcidlem  17043  pc2dvds  17050  pcprmpw2  17053  dvdsprmpweqle  17057  pcadd  17060  pcfac  17070  pcbc  17071  pockthlem  17076  prmreclem2  17088  prmreclem3  17089  mul4sqlem  17124  4sqlem11  17126  4sqlem12  17127  4sqlem14  17129  vdwapun  17145  prmgaplcmlem1  17222  chnind  18788  chnub  18789  chnpolfz  18800  lagsubg  19403  psgnuni  19706  psgnran  19722  odmodnn0  19747  mndodconglem  19748  mndodcong  19749  odm1inv  19760  odmulg2  19762  odmulg  19763  odmulgeq  19764  odbezout  19765  odinv  19768  odf1  19769  gexod  19793  gexdvds3  19797  sylow1lem1  19805  sylow1lem3  19807  pgpfi  19812  pgpssslw  19821  sylow2alem2  19825  sylow2blem3  19829  fislw  19832  sylow3lem4  19837  sylow3lem6  19839  efginvrel2  19934  efgredlemf  19948  efgredlemd  19951  efgredlemc  19952  efgredlem  19954  efgcpbllemb  19962  odadd1  20055  odadd2  20056  gexexlem  20059  gexex  20060  torsubg  20061  lt6abl  20102  gsummulg  20149  ablfacrplem  20274  ablfacrp  20275  ablfacrp2  20276  ablfac1b  20279  ablfac1c  20280  ablfac1eulem  20281  ablfac1eu  20282  pgpfac1lem2  20284  pgpfaclem1  20290  ablfaclem3  20296  srgbinomlem3  20447  srgbinomlem4  20448  chrid  21824  znunit  21862  freshmansdream  21873  psgnghm  21879  asclmulg  22203  psrbaglefi  22227  psdvsca  22478  psdmul  22480  chfacfscmulfsupp  23170  chfacfpmmulfsupp  23174  cpmadugsumlemF  23187  dyadss  25908  dyaddisjlem  25909  ply1divex  26448  ply1termlem  26514  plyeq0lem  26522  plyaddlem1  26525  plymullem1  26526  coeeulem  26536  coeidlem  26549  coeeq2  26554  coemulhi  26566  dvply1  26598  dvply2g  26599  plydivex  26611  elqaalem2  26636  aareccl  26646  aannenlem1  26648  aalioulem1  26652  taylplem1  26683  taylplem2  26684  taylpfval  26685  dvtaylp  26690  taylthlem2  26694  dvradcnv  26741  abelthlem7  26758  cxpeq  27078  birthdaylem2  27273  ftalem1  27393  basellem3  27403  isppw2  27435  isnsqf  27455  mule1  27468  ppinncl  27494  musum  27511  chtublem  27531  pclogsum  27535  vmasum  27536  dchrabs  27580  bcmax  27598  bposlem1  27604  bposlem6  27609  lgsval2lem  27627  lgsmod  27643  lgsne0  27655  gausslemma2dlem0h  27683  gausslemma2dlem0i  27684  gausslemma2dlem2  27687  gausslemma2dlem6  27692  gausslemma2d  27694  lgseisenlem1  27695  lgseisenlem2  27696  lgseisenlem3  27697  lgseisenlem4  27698  lgsquadlem1  27700  m1lgs  27708  2lgslem1a  27711  2lgslem3a  27716  2lgslem3b  27717  2lgslem3c  27718  2lgslem3d  27719  2lgslem3d1  27723  2lgsoddprmlem2  27729  2sqlem8  27746  2sqcoprm  27755  2sqmod  27756  chebbnd1lem1  27789  dchrisumlem1  27809  dchrisum0flblem1  27828  selberg2lem  27870  ostth2lem2  27954  ostth2lem3  27955  fltdiv  27961  flt4lem4  27972  finsumvtxdg2sstep  30123  finsumvtxdgeven  30126  vtxdgoddnumeven  30127  redwlklem  30243  wlkdlem1  30254  revwlk  30260  pthdlem1  30345  crctcshwlkn0lem4  30395  wwlksnredwwlkn0  30478  wwlksnextproplem2  30492  clwwlkccatlem  30573  clwlkclwwlkfo  30593  clwwlkwwlksb  30638  clwwlkndivn  30664  eupth2lem3lem3  30824  eupth2lem3lem4  30825  eupth2lem3  30830  eupth2lems  30832  numclwwlk5  30982  numclwwlk6  30984  ex-ind-dvds  31055  nndiffz1  33371  fzo0opth  33388  pfxlsw2ccat  33506  wrdt2ind  33509  gsummulsubdishift1  33622  gsumwrd2dccatlem  33631  cycpmfv1  33667  cycpmco2lem2  33681  cycpmco2lem3  33682  cycpmco2lem4  33683  cycpmco2lem5  33684  cycpmco2lem6  33685  cycpmco2  33687  cycpmrn  33697  cyc3genpm  33706  cycpmconjslem2  33709  cyc3conja  33711  archirng  33742  archirngz  33743  archiabllem1a  33745  gsumind  33899  elrspunidl  33971  ply1coedeg  34114  ply1degltel  34119  gsummoncoe1fz  34123  selvply1rhmlemb  34144  esplyfval2  34190  esplympl  34192  esplyfval3  34197  esplyindfv  34201  vietalem  34204  ply1degltdimlem  34247  fldextrspundgdvds  34306  algextdeglem8  34349  rtelextdg2  34352  constrext2chnlem  34375  cos9thpiminplylem2  34408  cos9thpiminplylem3  34409  cos9thpiminplylem6  34412  cos9thpiminply  34413  madjusmdetlem4  34455  zrhcntr  34604  qqhval2lem  34606  oddpwdc  34979  eulerpartlems  34985  eulerpartlemb  34993  sseqfv1  35014  sseqfn  35015  sseqmw  35016  sseqf  35017  sseqfv2  35019  sseqp1  35020  ccatmulgnn0dir  35167  signsplypnf  35172  signsply0  35173  signslema  35184  signstfvn  35191  signstfvp  35193  signstfvc  35196  fsum2dsub  35229  reprinfz1  35244  reprfi2  35245  hashrepr  35247  reprdifc  35249  breprexplema  35252  breprexplemc  35254  circlemeth  35262  circlevma  35264  circlemethhgt  35265  hgt750lema  35279  tgoldbachgtde  35282  lpadlem3  35303  subfacval3  35933  bcprod  36482  bccolsum  36483  fwddifnp1  36910  knoppndvlem6  37363  knoppndvlem7  37364  knoppndvlem10  37367  knoppndvlem14  37371  knoppndvlem15  37372  knoppndvlem16  37373  knoppndvlem17  37374  knoppndvlem19  37376  knoppndvlem21  37378  dfgcd3  38225  poimirlem3  38521  poimirlem4  38522  poimirlem6  38524  poimirlem13  38531  poimirlem14  38532  poimirlem17  38535  poimirlem21  38539  poimirlem22  38540  poimirlem23  38541  poimirlem26  38544  poimirlem27  38545  poimirlem31  38549  geomcau  38673  bccl2d  43021  lcmineqlem12  43070  lcmineqlem17  43075  dvrelogpow2b  43098  aks4d1p1p2  43100  aks4d1p1p4  43101  aks4d1p1p6  43103  aks4d1p1p7  43104  aks4d1p1p5  43105  aks4d1p1  43106  aks4d1p3  43108  aks4d1p6  43111  aks4d1p8d2  43115  aks4d1p8d3  43116  aks4d1p8  43117  primrootscoprmpow  43129  primrootlekpowne0  43135  aks6d1c1  43146  aks6d1c2p2  43149  aks6d1c2lem4  43157  aks6d1c2  43160  aks6d1c5lem3  43167  aks6d1c5lem2  43168  2np3bcnp1  43174  sticksstones5  43180  sticksstones6  43181  sticksstones7  43182  sticksstones10  43185  sticksstones11  43186  sticksstones12a  43187  sticksstones12  43188  sticksstones22  43198  aks6d1c6lem3  43202  bcled  43208  bcle2d  43209  aks6d1c7lem1  43210  aks6d1c7lem2  43211  grpods  43224  unitscyglem2  43226  unitscyglem4  43228  aks5lem8  43231  sumcubes  43350  frlmvscadiccat  43553  fltnltalem  43653  eldioph2lem1  43750  pellexlem5  43819  congrep  43959  jm2.18  43974  jm2.19lem1  43975  jm2.19lem2  43976  jm2.19  43979  jm2.22  43981  jm2.23  43982  jm2.20nn  43983  jm2.25  43985  jm2.26a  43986  jm2.26lem3  43987  jm2.26  43988  jm2.27a  43991  jm2.27b  43992  jm2.27c  43993  jm3.1  44006  expdiophlem1  44007  hbtlem5  44114  radcnvrat  45283  nzin  45287  bccbc  45314  binomcxplemnn0  45318  binomcxplemnotnn0  45325  fprodexp  46575  mccllem  46578  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnxpaek  46921  dvnmul  46922  dvnprodlem1  46925  dvnprodlem2  46926  wallispilem1  47044  wallispilem5  47048  stirlinglem3  47055  stirlinglem5  47057  stirlinglem7  47059  stirlinglem8  47060  fourierdlem102  47187  fourierdlem114  47199  sqwvfoura  47207  elaa2lem  47212  etransclem10  47223  etransclem20  47233  etransclem21  47234  etransclem22  47235  etransclem23  47236  etransclem24  47237  etransclem27  47240  etransclem28  47241  etransclem35  47248  etransclem38  47251  etransclem44  47257  etransclem45  47258  etransclem46  47259  sge0ad2en  47410  chnsubseqwl  47858  chnsubseq  47859  sqrtnpoly  47912  fsummmodsnunz  48422  fmtnoge3  48584  fmtnof1  48589  fmtnorec1  48591  sqrtpwpw2p  48592  fmtnodvds  48598  goldbachthlem2  48600  fmtnoprmfac2lem1  48620  lighneallem3  48661  lighneallem4b  48663  lighneallem4  48664  ssnn0ssfz  49430  altgsumbcALT  49434  flnn0ohalf  49615  dig2nn1st  49686  0dig2nn0o  49694  aacllem  50908