Theorem nn0zd 12627

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  ℕ₀cn0 12515  ℤcz 12602

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406  ax-un 7738  ax-1cn 11169  ax-icn 11170  ax-addcl 11171  ax-addrcl 11172  ax-mulcl 11173  ax-mulrcl 11174  ax-i2m1 11179  ax-1ne0 11180  ax-rnegex 11182  ax-rrecex 11183  ax-cnre 11184

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-reu 3372  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-iun 4960  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5558  df-eprel 5563  df-po 5571  df-so 5572  df-fr 5616  df-we 5618  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7419  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-neg 11455  df-nn 12245  df-n0 12516  df-z 12603

This theorem is used by:  nnzd  12628  eluzmn  12881  difelfznle  13683  elfzodif0  13812  zmodfz  13940  expnegz  14146  expaddzlem  14155  expaddz  14156  expmulz  14158  faclbnd  14340  bcpasc  14371  hashf1  14508  fz1isolem  14512  hashge2el2dif  14531  hashtpg  14536  wrdffz  14586  ffz0iswrd  14592  wrdsymb0  14600  wrdlenge1n0  14601  ccatcl  14625  ccatval3  14630  ccatdmss  14633  ccatsymb  14634  ccatval21sw  14637  ccatass  14640  ccatrn  14641  ccatf1  14642  lswccatn0lsw  14644  ccats1val2  14681  swrdnd  14710  swrdccat2  14725  pfxtrcfv0  14749  pfxtrcfvl  14752  pfxccat1  14757  swrdccatin2  14784  pfxccatin12  14788  pfxccatpfx2  14792  pfxccat3a  14793  splfv2a  14811  splval2  14812  revcl  14816  revccat  14821  revrev  14822  revpfxsfxrev  14823  cshwmodn  14852  cshwsublen  14853  cshwn  14854  cshwidxmod  14860  2cshwid  14871  3cshw  14875  cshweqdif2  14876  revco  14891  ccatco  14892  ccat2s1fvwALT  15012  ofccat  15026  zabscl  15384  absrdbnd  15413  iseraltlem3  15755  fsum0diaglem  15846  modfsummods  15864  binomlem  15902  binom1p  15904  incexc2  15911  climcndslem1  15922  geoser  15940  pwm1geoser  15942  geolim2  15944  mertenslem1  15957  mertenslem2  15958  mertens  15959  binomfallfaclem2  16112  binomrisefac  16114  fallfacval4  16115  bpolydiflem  16126  ruclem10  16313  sumodd  16464  divalglem9  16477  divalgmod  16482  bitsfzolem  16510  bitsfzo  16511  bitsmod  16512  bitsfi  16513  bitsinv1lem  16517  sadcaddlem  16533  sadadd3  16537  sadaddlem  16542  sadadd  16543  sadasslem  16546  sadass  16547  sadeq  16548  bitsres  16549  bitsuz  16550  bitsshft  16551  smuval2  16558  smupvallem  16559  smupval  16564  smueqlem  16566  smumullem  16568  smumul  16569  gcdcllem1  16575  zeqzmulgcd  16586  gcd0id  16595  gcdneg  16598  modgcd  16608  gcdmultipled  16610  bezoutlem4  16618  dvdsgcdb  16621  gcdass  16623  mulgcd  16624  gcdzeq  16628  dvdsmulgcd  16632  bezoutr  16644  bezoutr1  16645  nn0seqcvgd  16646  algfx  16656  eucalginv  16660  eucalg  16663  gcddvdslcm  16678  lcmneg  16679  lcmgcdlem  16682  lcmdvds  16684  lcmgcdeq  16688  lcmdvdsb  16689  lcmass  16690  lcmftp  16712  lcmfunsnlem1  16713  lcmfunsnlem2lem1  16714  lcmfunsnlem2lem2  16715  lcmfunsnlem2  16716  lcmfdvdsb  16719  lcmfun  16721  lcmfass  16722  mulgcddvds  16731  rpmulgcd2  16732  qredeu  16734  divgcdcoprm0  16741  sqnprm  16779  prmdvdsbc  16803  divnumden  16825  powm2modprm  16881  coprimeprodsq  16886  iserodd  16913  pclem  16916  pcpre1  16920  pcpremul  16921  pcqcl  16934  pcdvdsb  16947  pcidlem  16950  pc2dvds  16957  pcprmpw2  16960  dvdsprmpweqle  16964  pcadd  16967  pcfac  16977  pcbc  16978  pockthlem  16983  prmreclem2  16995  prmreclem3  16996  mul4sqlem  17031  4sqlem11  17033  4sqlem12  17034  4sqlem14  17036  vdwapun  17052  prmgaplcmlem1  17129  chnind  18695  chnub  18696  chnpolfz  18707  lagsubg  19290  psgnuni  19593  psgnran  19609  odmodnn0  19634  mndodconglem  19635  mndodcong  19636  odm1inv  19647  odmulg2  19649  odmulg  19650  odmulgeq  19651  odbezout  19652  odinv  19655  odf1  19656  gexod  19680  gexdvds3  19684  sylow1lem1  19692  sylow1lem3  19694  pgpfi  19699  pgpssslw  19708  sylow2alem2  19712  sylow2blem3  19716  fislw  19719  sylow3lem4  19724  sylow3lem6  19726  efginvrel2  19821  efgredlemf  19835  efgredlemd  19838  efgredlemc  19839  efgredlem  19841  efgcpbllemb  19849  odadd1  19942  odadd2  19943  gexexlem  19946  gexex  19947  torsubg  19948  lt6abl  19989  gsummulg  20036  ablfacrplem  20161  ablfacrp  20162  ablfacrp2  20163  ablfac1b  20166  ablfac1c  20167  ablfac1eulem  20168  ablfac1eu  20169  pgpfac1lem2  20171  pgpfaclem1  20177  ablfaclem3  20183  srgbinomlem3  20334  srgbinomlem4  20335  chrid  21705  znunit  21743  freshmansdream  21754  psgnghm  21760  asclmulg  22082  psrbaglefi  22106  psdvsca  22357  psdmul  22359  chfacfscmulfsupp  23046  chfacfpmmulfsupp  23050  cpmadugsumlemF  23063  dyadss  25784  dyaddisjlem  25785  ply1divex  26325  ply1termlem  26391  plyeq0lem  26398  plyaddlem1  26401  plymullem1  26402  coeeulem  26412  coeidlem  26425  coeeq2  26430  coemulhi  26442  dvply1  26476  dvply2g  26477  plydivex  26489  elqaalem2  26512  aareccl  26520  aannenlem1  26522  aalioulem1  26526  taylplem1  26557  taylplem2  26558  taylpfval  26559  dvtaylp  26564  taylthlem2  26568  dvradcnv  26615  abelthlem7  26632  cxpeq  26953  birthdaylem2  27148  ftalem1  27268  basellem3  27278  isppw2  27310  isnsqf  27330  mule1  27343  ppinncl  27369  musum  27386  chtublem  27406  pclogsum  27410  vmasum  27411  dchrabs  27455  bcmax  27473  bposlem1  27479  bposlem6  27484  lgsval2lem  27502  lgsmod  27518  lgsne0  27530  gausslemma2dlem0h  27558  gausslemma2dlem0i  27559  gausslemma2dlem2  27562  gausslemma2dlem6  27567  gausslemma2d  27569  lgseisenlem1  27570  lgseisenlem2  27571  lgseisenlem3  27572  lgseisenlem4  27573  lgsquadlem1  27575  m1lgs  27583  2lgslem1a  27586  2lgslem3a  27591  2lgslem3b  27592  2lgslem3c  27593  2lgslem3d  27594  2lgslem3d1  27598  2lgsoddprmlem2  27604  2sqlem8  27621  2sqcoprm  27630  2sqmod  27631  chebbnd1lem1  27664  dchrisumlem1  27684  dchrisum0flblem1  27703  selberg2lem  27745  ostth2lem2  27829  ostth2lem3  27830  finsumvtxdg2sstep  29933  finsumvtxdgeven  29936  vtxdgoddnumeven  29937  redwlklem  30053  wlkdlem1  30064  revwlk  30070  pthdlem1  30155  crctcshwlkn0lem4  30205  wwlksnredwwlkn0  30288  wwlksnextproplem2  30302  clwwlkccatlem  30383  clwlkclwwlkfo  30403  clwwlkwwlksb  30448  clwwlkndivn  30474  eupth2lem3lem3  30628  eupth2lem3lem4  30629  eupth2lem3  30634  eupth2lems  30636  numclwwlk5  30786  numclwwlk6  30788  ex-ind-dvds  30859  nndiffz1  33177  fzo0opth  33194  pfxlsw2ccat  33312  wrdt2ind  33315  gsummulsubdishift1  33428  gsumwrd2dccatlem  33437  cycpmfv1  33473  cycpmco2lem2  33487  cycpmco2lem3  33488  cycpmco2lem4  33489  cycpmco2lem5  33490  cycpmco2lem6  33491  cycpmco2  33493  cycpmrn  33503  cyc3genpm  33512  cycpmconjslem2  33515  cyc3conja  33517  archirng  33548  archirngz  33549  archiabllem1a  33551  gsumind  33705  elrspunidl  33776  ply1coedeg  33919  ply1degltel  33924  gsummoncoe1fz  33928  selvply1rhmlemb  33949  esplyfval2  33995  esplympl  33997  esplyfval3  34002  esplyindfv  34006  vietalem  34009  ply1degltdimlem  34052  fldextrspundgdvds  34111  algextdeglem8  34154  rtelextdg2  34157  constrext2chnlem  34180  cos9thpiminplylem2  34213  cos9thpiminplylem3  34214  cos9thpiminplylem6  34217  cos9thpiminply  34218  madjusmdetlem4  34260  zrhcntr  34409  qqhval2lem  34411  oddpwdc  34785  eulerpartlems  34791  eulerpartlemb  34799  sseqfv1  34820  sseqfn  34821  sseqmw  34822  sseqf  34823  sseqfv2  34825  sseqp1  34826  ccatmulgnn0dir  34973  signsplypnf  34978  signsply0  34979  signslema  34990  signstfvn  34997  signstfvp  34999  signstfvc  35002  fsum2dsub  35035  reprinfz1  35050  reprfi2  35051  hashrepr  35053  reprdifc  35055  breprexplema  35058  breprexplemc  35060  circlemeth  35068  circlevma  35070  circlemethhgt  35071  hgt750lema  35085  tgoldbachgtde  35088  lpadlem3  35109  subfacval3  35694  bcprod  36243  bccolsum  36244  fwddifnp1  36670  knoppndvlem6  37139  knoppndvlem7  37140  knoppndvlem10  37143  knoppndvlem14  37147  knoppndvlem15  37148  knoppndvlem16  37149  knoppndvlem17  37150  knoppndvlem19  37152  knoppndvlem21  37154  dfgcd3  38001  poimirlem3  38307  poimirlem4  38308  poimirlem6  38310  poimirlem13  38317  poimirlem14  38318  poimirlem17  38321  poimirlem21  38325  poimirlem22  38326  poimirlem23  38327  poimirlem26  38330  poimirlem27  38331  poimirlem31  38335  geomcau  38443  bccl2d  42791  lcmineqlem12  42840  lcmineqlem17  42845  dvrelogpow2b  42868  aks4d1p1p2  42870  aks4d1p1p4  42871  aks4d1p1p6  42873  aks4d1p1p7  42874  aks4d1p1p5  42875  aks4d1p1  42876  aks4d1p3  42878  aks4d1p6  42881  aks4d1p8d2  42885  aks4d1p8d3  42886  aks4d1p8  42887  primrootscoprmpow  42899  primrootlekpowne0  42905  aks6d1c1  42916  aks6d1c2p2  42919  aks6d1c2lem4  42927  aks6d1c2  42930  aks6d1c5lem3  42937  aks6d1c5lem2  42938  2np3bcnp1  42944  sticksstones5  42950  sticksstones6  42951  sticksstones7  42952  sticksstones10  42955  sticksstones11  42956  sticksstones12a  42957  sticksstones12  42958  sticksstones22  42968  aks6d1c6lem3  42972  bcled  42978  bcle2d  42979  aks6d1c7lem1  42980  aks6d1c7lem2  42981  grpods  42994  unitscyglem2  42996  unitscyglem4  42998  aks5lem8  43001  sumcubes  43107  gcdle1d  43124  gcdle2d  43125  frlmvscadiccat  43313  fltdiv  43401  flt4lem4  43414  fltnltalem  43427  eldioph2lem1  43524  pellexlem5  43593  congrep  43733  jm2.18  43748  jm2.19lem1  43749  jm2.19lem2  43750  jm2.19  43753  jm2.22  43755  jm2.23  43756  jm2.20nn  43757  jm2.25  43759  jm2.26a  43760  jm2.26lem3  43761  jm2.26  43762  jm2.27a  43765  jm2.27b  43766  jm2.27c  43767  jm3.1  43780  expdiophlem1  43781  hbtlem5  43888  radcnvrat  45057  nzin  45061  bccbc  45088  binomcxplemnn0  45092  binomcxplemnotnn0  45099  fprodexp  46343  mccllem  46346  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvnxpaek  46689  dvnmul  46690  dvnprodlem1  46693  dvnprodlem2  46694  wallispilem1  46812  wallispilem5  46816  stirlinglem3  46823  stirlinglem5  46825  stirlinglem7  46827  stirlinglem8  46828  fourierdlem102  46955  fourierdlem114  46967  sqwvfoura  46975  elaa2lem  46980  etransclem10  46991  etransclem20  47001  etransclem21  47002  etransclem22  47003  etransclem23  47004  etransclem24  47005  etransclem27  47008  etransclem28  47009  etransclem35  47016  etransclem38  47019  etransclem44  47025  etransclem45  47026  etransclem46  47027  sge0ad2en  47178  chnsubseqwl  47628  chnsubseq  47629  fsummmodsnunz  48153  fmtnoge3  48315  fmtnof1  48320  fmtnorec1  48322  sqrtpwpw2p  48323  fmtnodvds  48329  goldbachthlem2  48331  fmtnoprmfac2lem1  48351  lighneallem3  48392  lighneallem4b  48394  lighneallem4  48395  ssnn0ssfz  49162  altgsumbcALT  49166  flnn0ohalf  49347  dig2nn1st  49418  0dig2nn0o  49426  aacllem  50654