Theorem nn0zd 12587

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

Syntax hints:   → wi 4   ∈ wcel 2141  ℕ₀cn0 12475  ℤcz 12562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387  ax-un 7713  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-i2m1 11135  ax-1ne0 11136  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-ov 7394  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-neg 11411  df-nn 12205  df-n0 12476  df-z 12563

This theorem is referenced by:  nnzd  12588  eluzmn  12840  difelfznle  13641  elfzodif0  13770  zmodfz  13897  expnegz  14103  expaddzlem  14112  expaddz  14113  expmulz  14115  faclbnd  14297  bcpasc  14328  hashf1  14464  fz1isolem  14468  hashge2el2dif  14487  hashtpg  14492  wrdffz  14542  ffz0iswrd  14548  wrdsymb0  14556  wrdlenge1n0  14557  ccatcl  14581  ccatval3  14586  ccatdmss  14589  ccatsymb  14590  ccatval21sw  14593  ccatass  14596  ccatrn  14597  lswccatn0lsw  14599  ccats1val2  14635  swrdnd  14662  swrdccat2  14677  pfxtrcfv0  14701  pfxtrcfvl  14704  pfxccat1  14709  swrdccatin2  14736  pfxccatin12  14740  pfxccatpfx2  14744  pfxccat3a  14745  splfv2a  14763  splval2  14764  revcl  14768  revccat  14773  revrev  14774  cshwmodn  14802  cshwsublen  14803  cshwn  14804  cshwidxmod  14810  2cshwid  14821  3cshw  14825  cshweqdif2  14826  revco  14841  ccatco  14842  ccat2s1fvwALT  14962  ofccat  14976  zabscl  15331  absrdbnd  15360  iseraltlem3  15702  fsum0diaglem  15794  modfsummods  15812  binomlem  15850  binom1p  15852  incexc2  15859  climcndslem1  15870  geoser  15888  pwm1geoser  15890  geolim2  15892  mertenslem1  15905  mertenslem2  15906  mertens  15907  binomfallfaclem2  16061  binomrisefac  16063  fallfacval4  16064  bpolydiflem  16075  ruclem10  16262  sumodd  16413  divalglem9  16426  divalgmod  16431  bitsfzolem  16459  bitsfzo  16460  bitsmod  16461  bitsfi  16462  bitsinv1lem  16466  sadcaddlem  16482  sadadd3  16486  sadaddlem  16491  sadadd  16492  sadasslem  16495  sadass  16496  sadeq  16497  bitsres  16498  bitsuz  16499  bitsshft  16500  smuval2  16507  smupvallem  16508  smupval  16513  smueqlem  16515  smumullem  16517  smumul  16518  gcdcllem1  16524  zeqzmulgcd  16535  gcd0id  16544  gcdneg  16547  modgcd  16557  gcdmultipled  16559  bezoutlem4  16567  dvdsgcdb  16570  gcdass  16572  mulgcd  16573  gcdzeq  16577  dvdsmulgcd  16581  bezoutr  16593  bezoutr1  16594  nn0seqcvgd  16595  algfx  16605  eucalginv  16609  eucalg  16612  gcddvdslcm  16627  lcmneg  16628  lcmgcdlem  16631  lcmdvds  16633  lcmgcdeq  16637  lcmdvdsb  16638  lcmass  16639  lcmftp  16661  lcmfunsnlem1  16662  lcmfunsnlem2lem1  16663  lcmfunsnlem2lem2  16664  lcmfunsnlem2  16665  lcmfdvdsb  16668  lcmfun  16670  lcmfass  16671  mulgcddvds  16680  rpmulgcd2  16681  qredeu  16683  divgcdcoprm0  16690  sqnprm  16728  prmdvdsbc  16752  divnumden  16774  powm2modprm  16830  coprimeprodsq  16835  iserodd  16862  pclem  16865  pcpre1  16869  pcpremul  16870  pcqcl  16883  pcdvdsb  16896  pcidlem  16899  pc2dvds  16906  pcprmpw2  16909  dvdsprmpweqle  16913  pcadd  16916  pcfac  16926  pcbc  16927  pockthlem  16932  prmreclem2  16944  prmreclem3  16945  mul4sqlem  16980  4sqlem11  16982  4sqlem12  16983  4sqlem14  16985  vdwapun  17001  prmgaplcmlem1  17078  chnind  18644  chnub  18645  chnpolfz  18656  lagsubg  19227  psgnuni  19530  psgnran  19546  odmodnn0  19571  mndodconglem  19572  mndodcong  19573  odm1inv  19584  odmulg2  19586  odmulg  19587  odmulgeq  19588  odbezout  19589  odinv  19592  odf1  19593  gexod  19617  gexdvds3  19621  sylow1lem1  19629  sylow1lem3  19631  pgpfi  19636  pgpssslw  19645  sylow2alem2  19649  sylow2blem3  19653  fislw  19656  sylow3lem4  19661  sylow3lem6  19663  efginvrel2  19758  efgredlemf  19772  efgredlemd  19775  efgredlemc  19776  efgredlem  19778  efgcpbllemb  19786  odadd1  19879  odadd2  19880  gexexlem  19883  gexex  19884  torsubg  19885  lt6abl  19926  gsummulg  19973  ablfacrplem  20098  ablfacrp  20099  ablfacrp2  20100  ablfac1b  20103  ablfac1c  20104  ablfac1eulem  20105  ablfac1eu  20106  pgpfac1lem2  20108  pgpfaclem1  20114  ablfaclem3  20120  srgbinomlem3  20265  srgbinomlem4  20266  chrid  21565  znunit  21603  freshmansdream  21614  psgnghm  21620  asclmulg  21942  psrbaglefi  21966  psdvsca  22217  psdmul  22219  chfacfscmulfsupp  22907  chfacfpmmulfsupp  22911  cpmadugsumlemF  22924  dyadss  25644  dyaddisjlem  25645  ply1divex  26185  ply1termlem  26251  plyeq0lem  26258  plyaddlem1  26261  plymullem1  26262  coeeulem  26272  coeidlem  26285  coeeq2  26290  coemulhi  26302  dvply1  26336  dvply2g  26337  plydivex  26349  elqaalem2  26372  aareccl  26378  aannenlem1  26380  aalioulem1  26384  taylplem1  26414  taylplem2  26415  taylpfval  26416  dvtaylp  26421  taylthlem2  26425  dvradcnv  26472  abelthlem7  26489  cxpeq  26810  birthdaylem2  27005  ftalem1  27125  basellem3  27135  isppw2  27167  isnsqf  27187  mule1  27200  ppinncl  27226  musum  27243  chtublem  27263  pclogsum  27267  vmasum  27268  dchrabs  27312  bcmax  27330  bposlem1  27336  bposlem6  27341  lgsval2lem  27359  lgsmod  27375  lgsne0  27387  gausslemma2dlem0h  27415  gausslemma2dlem0i  27416  gausslemma2dlem2  27419  gausslemma2dlem6  27424  gausslemma2d  27426  lgseisenlem1  27427  lgseisenlem2  27428  lgseisenlem3  27429  lgseisenlem4  27430  lgsquadlem1  27432  m1lgs  27440  2lgslem1a  27443  2lgslem3a  27448  2lgslem3b  27449  2lgslem3c  27450  2lgslem3d  27451  2lgslem3d1  27455  2lgsoddprmlem2  27461  2sqlem8  27478  2sqcoprm  27487  2sqmod  27488  chebbnd1lem1  27521  dchrisumlem1  27541  dchrisum0flblem1  27560  selberg2lem  27602  ostth2lem2  27686  ostth2lem3  27687  finsumvtxdg2sstep  29707  finsumvtxdgeven  29710  vtxdgoddnumeven  29711  redwlklem  29827  wlkdlem1  29838  pthdlem1  29923  crctcshwlkn0lem4  29970  wwlksnredwwlkn0  30053  wwlksnextproplem2  30067  clwwlkccatlem  30148  clwlkclwwlkfo  30168  clwwlkwwlksb  30213  clwwlkndivn  30239  eupth2lem3lem3  30389  eupth2lem3lem4  30390  eupth2lem3  30395  eupth2lems  30397  numclwwlk5  30547  numclwwlk6  30549  ex-ind-dvds  30620  nndiffz1  32949  fzo0opth  32966  ccatf1  33088  pfxlsw2ccat  33089  wrdt2ind  33092  gsummulsubdishift1  33209  gsumwrd2dccatlem  33218  cycpmfv1  33254  cycpmco2lem2  33268  cycpmco2lem3  33269  cycpmco2lem4  33270  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2  33274  cycpmrn  33284  cyc3genpm  33293  cycpmconjslem2  33296  cyc3conja  33298  archirng  33329  archirngz  33330  archiabllem1a  33332  gsumind  33492  elrspunidl  33575  ply1coedeg  33746  ply1degltel  33751  gsummoncoe1fz  33755  selvply1rhmlemb  33777  esplyfval2  33823  esplympl  33825  esplyfval3  33830  esplyindfv  33834  vietalem  33837  ply1degltdimlem  33880  fldextrspundgdvds  33939  algextdeglem8  33982  rtelextdg2  33985  constrext2chnlem  34008  cos9thpiminplylem2  34041  cos9thpiminplylem3  34042  cos9thpiminplylem6  34045  cos9thpiminply  34046  madjusmdetlem4  34088  zrhcntr  34237  qqhval2lem  34239  oddpwdc  34612  eulerpartlems  34618  eulerpartlemb  34626  sseqfv1  34647  sseqfn  34648  sseqmw  34649  sseqf  34650  sseqfv2  34652  sseqp1  34653  ccatmulgnn0dir  34800  signsplypnf  34805  signsply0  34806  signslema  34817  signstfvn  34824  signstfvp  34826  signstfvc  34829  fsum2dsub  34862  reprinfz1  34877  reprfi2  34878  hashrepr  34880  reprdifc  34882  breprexplema  34885  breprexplemc  34887  circlemeth  34895  circlevma  34897  circlemethhgt  34898  hgt750lema  34912  tgoldbachgtde  34915  lpadlem3  34936  revpfxsfxrev  35427  revwlk  35436  subfacval3  35500  bcprod  36049  bccolsum  36050  fwddifnp1  36476  knoppndvlem6  36916  knoppndvlem7  36917  knoppndvlem10  36920  knoppndvlem14  36924  knoppndvlem15  36925  knoppndvlem16  36926  knoppndvlem17  36927  knoppndvlem19  36929  knoppndvlem21  36931  dfgcd3  37777  poimirlem3  38083  poimirlem4  38084  poimirlem6  38086  poimirlem13  38093  poimirlem14  38094  poimirlem17  38097  poimirlem21  38101  poimirlem22  38102  poimirlem23  38103  poimirlem26  38106  poimirlem27  38107  poimirlem31  38111  geomcau  38219  bccl2d  42569  lcmineqlem12  42618  lcmineqlem17  42623  dvrelogpow2b  42646  aks4d1p1p2  42648  aks4d1p1p4  42649  aks4d1p1p6  42651  aks4d1p1p7  42652  aks4d1p1p5  42653  aks4d1p1  42654  aks4d1p3  42656  aks4d1p6  42659  aks4d1p8d2  42663  aks4d1p8d3  42664  aks4d1p8  42665  primrootscoprmpow  42677  primrootlekpowne0  42683  aks6d1c1  42694  aks6d1c2p2  42697  aks6d1c2lem4  42705  aks6d1c2  42708  aks6d1c5lem3  42715  aks6d1c5lem2  42716  2np3bcnp1  42722  sticksstones5  42728  sticksstones6  42729  sticksstones7  42730  sticksstones10  42733  sticksstones11  42734  sticksstones12a  42735  sticksstones12  42736  sticksstones22  42746  aks6d1c6lem3  42750  bcled  42756  bcle2d  42757  aks6d1c7lem1  42758  aks6d1c7lem2  42759  grpods  42772  unitscyglem2  42774  unitscyglem4  42776  aks5lem8  42779  sumcubes  42883  gcdle1d  42900  gcdle2d  42901  frlmvscadiccat  43089  fltdiv  43179  flt4lem4  43192  fltnltalem  43205  eldioph2lem1  43302  pellexlem5  43371  congrep  43511  jm2.18  43526  jm2.19lem1  43527  jm2.19lem2  43528  jm2.19  43531  jm2.22  43533  jm2.23  43534  jm2.20nn  43535  jm2.25  43537  jm2.26a  43538  jm2.26lem3  43539  jm2.26  43540  jm2.27a  43543  jm2.27b  43544  jm2.27c  43545  jm3.1  43558  expdiophlem1  43559  hbtlem5  43666  radcnvrat  44851  nzin  44855  bccbc  44882  binomcxplemnn0  44886  binomcxplemnotnn0  44893  fprodexp  46131  mccllem  46134  ioodvbdlimc1lem2  46467  ioodvbdlimc2lem  46469  dvnxpaek  46477  dvnmul  46478  dvnprodlem1  46481  dvnprodlem2  46482  wallispilem1  46600  wallispilem5  46604  stirlinglem3  46611  stirlinglem5  46613  stirlinglem7  46615  stirlinglem8  46616  fourierdlem102  46743  fourierdlem114  46755  sqwvfoura  46763  elaa2lem  46768  etransclem10  46779  etransclem20  46789  etransclem21  46790  etransclem22  46791  etransclem23  46792  etransclem24  46793  etransclem27  46796  etransclem28  46797  etransclem35  46804  etransclem38  46807  etransclem44  46813  etransclem45  46814  etransclem46  46815  sge0ad2en  46966  chnsubseqwl  47416  chnsubseq  47417  fsummmodsnunz  47938  fmtnoge3  48100  fmtnof1  48105  fmtnorec1  48107  sqrtpwpw2p  48108  fmtnodvds  48114  goldbachthlem2  48116  fmtnoprmfac2lem1  48136  lighneallem3  48177  lighneallem4b  48179  lighneallem4  48180  ssnn0ssfz  48932  altgsumbcALT  48936  flnn0ohalf  49117  dig2nn1st  49188  0dig2nn0o  49196  aacllem  50383