Theorem nn0zd 12640

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

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

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398  ax-un 7736  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-i2m1 11192  ax-1ne0 11193  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  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 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7416  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11468  df-nn 12258  df-n0 12529  df-z 12616

This theorem is used by:  nnzd  12641  eluzmn  12894  difelfznle  13697  elfzodif0  13826  zmodfz  13954  expnegz  14160  expaddzlem  14169  expaddz  14170  expmulz  14172  faclbnd  14354  bcpasc  14385  hashf1  14522  fz1isolem  14526  hashge2el2dif  14545  hashtpg  14550  wrdffz  14600  ffz0iswrd  14606  wrdsymb0  14614  wrdlenge1n0  14615  ccatcl  14639  ccatval3  14644  ccatdmss  14647  ccatsymb  14648  ccatval21sw  14651  ccatass  14654  ccatrn  14655  ccatf1  14656  lswccatn0lsw  14658  ccats1val2  14695  swrdnd  14724  swrdccat2  14739  pfxtrcfv0  14763  pfxtrcfvl  14766  pfxccat1  14771  swrdccatin2  14798  pfxccatin12  14802  pfxccatpfx2  14806  pfxccat3a  14807  splfv2a  14825  splval2  14826  revcl  14830  revccat  14835  revrev  14836  revpfxsfxrev  14837  cshwmodn  14866  cshwsublen  14867  cshwn  14868  cshwidxmod  14874  2cshwid  14885  3cshw  14889  cshweqdif2  14890  revco  14905  ccatco  14906  ccat2s1fvwALT  15028  ofccat  15042  zabscl  15400  absrdbnd  15429  iseraltlem3  15771  fsum0diaglem  15862  modfsummods  15880  binomlem  15918  binom1p  15920  incexc2  15927  climcndslem1  15938  geoser  15956  pwm1geoser  15958  geolim2  15960  mertenslem1  15973  mertenslem2  15974  mertens  15975  binomfallfaclem2  16126  binomrisefac  16128  fallfacval4  16129  bpolydiflem  16140  ruclem10  16327  sumodd  16478  divalglem9  16491  divalgmod  16496  bitsfzolem  16524  bitsfzo  16525  bitsmod  16526  bitsfi  16527  bitsinv1lem  16531  sadcaddlem  16547  sadadd3  16551  sadaddlem  16556  sadadd  16557  sadasslem  16560  sadass  16561  sadeq  16562  bitsres  16563  bitsuz  16564  bitsshft  16565  smuval2  16572  smupvallem  16573  smupval  16578  smueqlem  16580  smumullem  16582  smumul  16583  gcdcllem1  16589  zeqzmulgcd  16600  gcd0id  16609  gcdneg  16612  modgcd  16622  gcdmultipled  16624  bezoutlem4  16632  dvdsgcdb  16635  gcdass  16637  mulgcd  16638  gcdzeq  16642  dvdsmulgcd  16646  bezoutr  16658  bezoutr1  16659  nn0seqcvgd  16660  algfx  16670  eucalginv  16674  eucalg  16677  gcddvdslcm  16692  lcmneg  16693  lcmgcdlem  16696  lcmdvds  16698  lcmgcdeq  16702  lcmdvdsb  16703  lcmass  16704  lcmftp  16726  lcmfunsnlem1  16727  lcmfunsnlem2lem1  16728  lcmfunsnlem2lem2  16729  lcmfunsnlem2  16730  lcmfdvdsb  16733  lcmfun  16735  lcmfass  16736  mulgcddvds  16745  rpmulgcd2  16746  qredeu  16748  divgcdcoprm0  16755  sqnprm  16793  prmdvdsbc  16817  divnumden  16839  powm2modprm  16895  coprimeprodsq  16900  iserodd  16927  pclem  16930  pcpre1  16934  pcpremul  16935  pcqcl  16948  pcdvdsb  16961  pcidlem  16964  pc2dvds  16971  pcprmpw2  16974  dvdsprmpweqle  16978  pcadd  16981  pcfac  16991  pcbc  16992  pockthlem  16997  prmreclem2  17009  prmreclem3  17010  mul4sqlem  17045  4sqlem11  17047  4sqlem12  17048  4sqlem14  17050  vdwapun  17066  prmgaplcmlem1  17143  chnind  18709  chnub  18710  chnpolfz  18721  lagsubg  19323  psgnuni  19626  psgnran  19642  odmodnn0  19667  mndodconglem  19668  mndodcong  19669  odm1inv  19680  odmulg2  19682  odmulg  19683  odmulgeq  19684  odbezout  19685  odinv  19688  odf1  19689  gexod  19713  gexdvds3  19717  sylow1lem1  19725  sylow1lem3  19727  pgpfi  19732  pgpssslw  19741  sylow2alem2  19745  sylow2blem3  19749  fislw  19752  sylow3lem4  19757  sylow3lem6  19759  efginvrel2  19854  efgredlemf  19868  efgredlemd  19871  efgredlemc  19872  efgredlem  19874  efgcpbllemb  19882  odadd1  19975  odadd2  19976  gexexlem  19979  gexex  19980  torsubg  19981  lt6abl  20022  gsummulg  20069  ablfacrplem  20194  ablfacrp  20195  ablfacrp2  20196  ablfac1b  20199  ablfac1c  20200  ablfac1eulem  20201  ablfac1eu  20202  pgpfac1lem2  20204  pgpfaclem1  20210  ablfaclem3  20216  srgbinomlem3  20367  srgbinomlem4  20368  chrid  21738  znunit  21776  freshmansdream  21787  psgnghm  21793  asclmulg  22117  psrbaglefi  22141  psdvsca  22392  psdmul  22394  chfacfscmulfsupp  23084  chfacfpmmulfsupp  23088  cpmadugsumlemF  23101  dyadss  25822  dyaddisjlem  25823  ply1divex  26362  ply1termlem  26428  plyeq0lem  26436  plyaddlem1  26439  plymullem1  26440  coeeulem  26450  coeidlem  26463  coeeq2  26468  coemulhi  26480  dvply1  26514  dvply2g  26515  plydivex  26527  elqaalem2  26552  aareccl  26562  aannenlem1  26564  aalioulem1  26568  taylplem1  26599  taylplem2  26600  taylpfval  26601  dvtaylp  26606  taylthlem2  26610  dvradcnv  26657  abelthlem7  26674  cxpeq  26994  birthdaylem2  27189  ftalem1  27309  basellem3  27319  isppw2  27351  isnsqf  27371  mule1  27384  ppinncl  27410  musum  27427  chtublem  27447  pclogsum  27451  vmasum  27452  dchrabs  27496  bcmax  27514  bposlem1  27520  bposlem6  27525  lgsval2lem  27543  lgsmod  27559  lgsne0  27571  gausslemma2dlem0h  27599  gausslemma2dlem0i  27600  gausslemma2dlem2  27603  gausslemma2dlem6  27608  gausslemma2d  27610  lgseisenlem1  27611  lgseisenlem2  27612  lgseisenlem3  27613  lgseisenlem4  27614  lgsquadlem1  27616  m1lgs  27624  2lgslem1a  27627  2lgslem3a  27632  2lgslem3b  27633  2lgslem3c  27634  2lgslem3d  27635  2lgslem3d1  27639  2lgsoddprmlem2  27645  2sqlem8  27662  2sqcoprm  27671  2sqmod  27672  chebbnd1lem1  27705  dchrisumlem1  27725  dchrisum0flblem1  27744  selberg2lem  27786  ostth2lem2  27870  ostth2lem3  27871  finsumvtxdg2sstep  30009  finsumvtxdgeven  30012  vtxdgoddnumeven  30013  redwlklem  30129  wlkdlem1  30140  revwlk  30146  pthdlem1  30231  crctcshwlkn0lem4  30281  wwlksnredwwlkn0  30364  wwlksnextproplem2  30378  clwwlkccatlem  30459  clwlkclwwlkfo  30479  clwwlkwwlksb  30524  clwwlkndivn  30550  eupth2lem3lem3  30710  eupth2lem3lem4  30711  eupth2lem3  30716  eupth2lems  30718  numclwwlk5  30868  numclwwlk6  30870  ex-ind-dvds  30941  nndiffz1  33257  fzo0opth  33274  pfxlsw2ccat  33392  wrdt2ind  33395  gsummulsubdishift1  33508  gsumwrd2dccatlem  33517  cycpmfv1  33553  cycpmco2lem2  33567  cycpmco2lem3  33568  cycpmco2lem4  33569  cycpmco2lem5  33570  cycpmco2lem6  33571  cycpmco2  33573  cycpmrn  33583  cyc3genpm  33592  cycpmconjslem2  33595  cyc3conja  33597  archirng  33628  archirngz  33629  archiabllem1a  33631  gsumind  33785  elrspunidl  33856  ply1coedeg  33999  ply1degltel  34004  gsummoncoe1fz  34008  selvply1rhmlemb  34029  esplyfval2  34075  esplympl  34077  esplyfval3  34082  esplyindfv  34086  vietalem  34089  ply1degltdimlem  34132  fldextrspundgdvds  34191  algextdeglem8  34234  rtelextdg2  34237  constrext2chnlem  34260  cos9thpiminplylem2  34293  cos9thpiminplylem3  34294  cos9thpiminplylem6  34297  cos9thpiminply  34298  madjusmdetlem4  34340  zrhcntr  34489  qqhval2lem  34491  oddpwdc  34865  eulerpartlems  34871  eulerpartlemb  34879  sseqfv1  34900  sseqfn  34901  sseqmw  34902  sseqf  34903  sseqfv2  34905  sseqp1  34906  ccatmulgnn0dir  35053  signsplypnf  35058  signsply0  35059  signslema  35070  signstfvn  35077  signstfvp  35079  signstfvc  35082  fsum2dsub  35115  reprinfz1  35130  reprfi2  35131  hashrepr  35133  reprdifc  35135  breprexplema  35138  breprexplemc  35140  circlemeth  35148  circlevma  35150  circlemethhgt  35151  hgt750lema  35165  tgoldbachgtde  35168  lpadlem3  35189  subfacval3  35768  bcprod  36317  bccolsum  36318  fwddifnp1  36745  knoppndvlem6  37214  knoppndvlem7  37215  knoppndvlem10  37218  knoppndvlem14  37222  knoppndvlem15  37223  knoppndvlem16  37224  knoppndvlem17  37225  knoppndvlem19  37227  knoppndvlem21  37229  dfgcd3  38076  poimirlem3  38372  poimirlem4  38373  poimirlem6  38375  poimirlem13  38382  poimirlem14  38383  poimirlem17  38386  poimirlem21  38390  poimirlem22  38391  poimirlem23  38392  poimirlem26  38395  poimirlem27  38396  poimirlem31  38400  geomcau  38509  bccl2d  42857  lcmineqlem12  42906  lcmineqlem17  42911  dvrelogpow2b  42934  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  aks4d1p3  42944  aks4d1p6  42947  aks4d1p8d2  42951  aks4d1p8d3  42952  aks4d1p8  42953  primrootscoprmpow  42965  primrootlekpowne0  42971  aks6d1c1  42982  aks6d1c2p2  42985  aks6d1c2lem4  42993  aks6d1c2  42996  aks6d1c5lem3  43003  aks6d1c5lem2  43004  2np3bcnp1  43010  sticksstones5  43016  sticksstones6  43017  sticksstones7  43018  sticksstones10  43021  sticksstones11  43022  sticksstones12a  43023  sticksstones12  43024  sticksstones22  43034  aks6d1c6lem3  43038  bcled  43044  bcle2d  43045  aks6d1c7lem1  43046  aks6d1c7lem2  43047  grpods  43060  unitscyglem2  43062  unitscyglem4  43064  aks5lem8  43067  sumcubes  43188  gcdle1d  43205  gcdle2d  43206  frlmvscadiccat  43394  fltdiv  43482  flt4lem4  43495  fltnltalem  43508  eldioph2lem1  43605  pellexlem5  43674  congrep  43814  jm2.18  43829  jm2.19lem1  43830  jm2.19lem2  43831  jm2.19  43834  jm2.22  43836  jm2.23  43837  jm2.20nn  43838  jm2.25  43840  jm2.26a  43841  jm2.26lem3  43842  jm2.26  43843  jm2.27a  43846  jm2.27b  43847  jm2.27c  43848  jm3.1  43861  expdiophlem1  43862  hbtlem5  43969  radcnvrat  45138  nzin  45142  bccbc  45169  binomcxplemnn0  45173  binomcxplemnotnn0  45180  fprodexp  46424  mccllem  46427  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnxpaek  46770  dvnmul  46771  dvnprodlem1  46774  dvnprodlem2  46775  wallispilem1  46893  wallispilem5  46897  stirlinglem3  46904  stirlinglem5  46906  stirlinglem7  46908  stirlinglem8  46909  fourierdlem102  47036  fourierdlem114  47048  sqwvfoura  47056  elaa2lem  47061  etransclem10  47072  etransclem20  47082  etransclem21  47083  etransclem22  47084  etransclem23  47085  etransclem24  47086  etransclem27  47089  etransclem28  47090  etransclem35  47097  etransclem38  47100  etransclem44  47106  etransclem45  47107  etransclem46  47108  sge0ad2en  47259  chnsubseqwl  47707  chnsubseq  47708  sqrtnpoly  47761  fsummmodsnunz  48271  fmtnoge3  48433  fmtnof1  48438  fmtnorec1  48440  sqrtpwpw2p  48441  fmtnodvds  48447  goldbachthlem2  48449  fmtnoprmfac2lem1  48469  lighneallem3  48510  lighneallem4b  48512  lighneallem4  48513  ssnn0ssfz  49279  altgsumbcALT  49283  flnn0ohalf  49464  dig2nn1st  49535  0dig2nn0o  49543  aacllem  50772