Theorem nn0zd 12531

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

Syntax hints:   → wi 4   ∈ wcel 2109  ℕ₀cn0 12418  ℤcz 12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-i2m1 11112  ax-1ne0 11113  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-ov 7372  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-neg 11384  df-nn 12163  df-n0 12419  df-z 12506

This theorem is referenced by:  nnzd  12532  eluzmn  12776  difelfznle  13579  zmodfz  13831  expnegz  14037  expaddzlem  14046  expaddz  14047  expmulz  14049  faclbnd  14231  bcpasc  14262  hashf1  14398  fz1isolem  14402  hashge2el2dif  14421  hashtpg  14426  wrdffz  14476  ffz0iswrd  14482  wrdsymb0  14490  wrdlenge1n0  14491  ccatcl  14515  ccatval3  14520  ccatsymb  14523  ccatval21sw  14526  ccatass  14529  ccatrn  14530  lswccatn0lsw  14532  ccats1val2  14568  swrdnd  14595  swrdccat2  14610  pfxtrcfv0  14635  pfxtrcfvl  14638  pfxccat1  14643  swrdccatin2  14670  pfxccatin12  14674  pfxccatpfx2  14678  pfxccat3a  14679  splfv2a  14697  splval2  14698  revcl  14702  revccat  14707  revrev  14708  cshwmodn  14736  cshwsublen  14737  cshwn  14738  cshwidxmod  14744  2cshwid  14755  3cshw  14759  cshweqdif2  14760  revco  14776  ccatco  14777  ccat2s1fvwALT  14897  ofccat  14911  zabscl  15255  absrdbnd  15284  iseraltlem3  15626  fsum0diaglem  15718  modfsummods  15735  binomlem  15771  binom1p  15773  incexc2  15780  climcndslem1  15791  geoser  15809  pwm1geoser  15811  geolim2  15813  mertenslem1  15826  mertenslem2  15827  mertens  15828  binomfallfaclem2  15982  binomrisefac  15984  fallfacval4  15985  bpolydiflem  15996  ruclem10  16183  sumodd  16334  divalglem9  16347  divalgmod  16352  bitsfzolem  16380  bitsfzo  16381  bitsmod  16382  bitsfi  16383  bitsinv1lem  16387  sadcaddlem  16403  sadadd3  16407  sadaddlem  16412  sadadd  16413  sadasslem  16416  sadass  16417  sadeq  16418  bitsres  16419  bitsuz  16420  bitsshft  16421  smuval2  16428  smupvallem  16429  smupval  16434  smueqlem  16436  smumullem  16438  smumul  16439  gcdcllem1  16445  zeqzmulgcd  16456  gcd0id  16465  gcdneg  16468  modgcd  16478  gcdmultipled  16480  bezoutlem4  16488  dvdsgcdb  16491  gcdass  16493  mulgcd  16494  gcdzeq  16498  dvdsmulgcd  16502  bezoutr  16514  bezoutr1  16515  nn0seqcvgd  16516  algfx  16526  eucalginv  16530  eucalg  16533  gcddvdslcm  16548  lcmneg  16549  lcmgcdlem  16552  lcmdvds  16554  lcmgcdeq  16558  lcmdvdsb  16559  lcmass  16560  lcmftp  16582  lcmfunsnlem1  16583  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  lcmfunsnlem2  16586  lcmfdvdsb  16589  lcmfun  16591  lcmfass  16592  mulgcddvds  16601  rpmulgcd2  16602  qredeu  16604  divgcdcoprm0  16611  sqnprm  16648  prmdvdsbc  16672  divnumden  16694  powm2modprm  16750  coprimeprodsq  16755  iserodd  16782  pclem  16785  pcpre1  16789  pcpremul  16790  pcqcl  16803  pcdvdsb  16816  pcidlem  16819  pc2dvds  16826  pcprmpw2  16829  dvdsprmpweqle  16833  pcadd  16836  pcfac  16846  pcbc  16847  pockthlem  16852  prmreclem2  16864  prmreclem3  16865  mul4sqlem  16900  4sqlem11  16902  4sqlem12  16903  4sqlem14  16905  vdwapun  16921  prmgaplcmlem1  16998  lagsubg  19103  psgnuni  19405  psgnran  19421  odmodnn0  19446  mndodconglem  19447  mndodcong  19448  odm1inv  19459  odmulg2  19461  odmulg  19462  odmulgeq  19463  odbezout  19464  odinv  19467  odf1  19468  gexod  19492  gexdvds3  19496  sylow1lem1  19504  sylow1lem3  19506  pgpfi  19511  pgpssslw  19520  sylow2alem2  19524  sylow2blem3  19528  fislw  19531  sylow3lem4  19536  sylow3lem6  19538  efginvrel2  19633  efgredlemf  19647  efgredlemd  19650  efgredlemc  19651  efgredlem  19653  efgcpbllemb  19661  odadd1  19754  odadd2  19755  gexexlem  19758  gexex  19759  torsubg  19760  lt6abl  19801  gsummulg  19848  ablfacrplem  19973  ablfacrp  19974  ablfacrp2  19975  ablfac1b  19978  ablfac1c  19979  ablfac1eulem  19980  ablfac1eu  19981  pgpfac1lem2  19983  pgpfaclem1  19989  ablfaclem3  19995  srgbinomlem3  20113  srgbinomlem4  20114  chrid  21411  znunit  21449  freshmansdream  21460  psgnghm  21465  asclmulg  21787  psrbaglefi  21811  psdvsca  22027  psdmul  22029  chfacfscmulfsupp  22722  chfacfpmmulfsupp  22726  cpmadugsumlemF  22739  dyadss  25471  dyaddisjlem  25472  ply1divex  26018  ply1termlem  26084  plyeq0lem  26091  plyaddlem1  26094  plymullem1  26095  coeeulem  26105  coeidlem  26118  coeeq2  26123  coemulhi  26135  dvply1  26167  dvply2g  26168  dvply2gOLD  26169  plydivex  26181  elqaalem2  26204  aareccl  26210  aannenlem1  26212  aalioulem1  26216  taylplem1  26246  taylplem2  26247  taylpfval  26248  dvtaylp  26254  taylthlem2  26258  taylthlem2OLD  26259  dvradcnv  26306  abelthlem7  26324  cxpeq  26643  birthdaylem2  26838  ftalem1  26959  basellem3  26969  isppw2  27001  isnsqf  27021  mule1  27034  ppinncl  27060  musum  27077  chtublem  27098  pclogsum  27102  vmasum  27103  dchrabs  27147  bcmax  27165  bposlem1  27171  bposlem6  27176  lgsval2lem  27194  lgsmod  27210  lgsne0  27222  gausslemma2dlem0h  27250  gausslemma2dlem0i  27251  gausslemma2dlem2  27254  gausslemma2dlem6  27259  gausslemma2d  27261  lgseisenlem1  27262  lgseisenlem2  27263  lgseisenlem3  27264  lgseisenlem4  27265  lgsquadlem1  27267  m1lgs  27275  2lgslem1a  27278  2lgslem3a  27283  2lgslem3b  27284  2lgslem3c  27285  2lgslem3d  27286  2lgslem3d1  27290  2lgsoddprmlem2  27296  2sqlem8  27313  2sqcoprm  27322  2sqmod  27323  chebbnd1lem1  27356  dchrisumlem1  27376  dchrisum0flblem1  27395  selberg2lem  27437  ostth2lem2  27521  ostth2lem3  27522  finsumvtxdg2sstep  29453  finsumvtxdgeven  29456  vtxdgoddnumeven  29457  redwlklem  29573  wlkdlem1  29584  pthdlem1  29669  crctcshwlkn0lem4  29716  wwlksnredwwlkn0  29799  wwlksnextproplem2  29813  clwwlkccatlem  29891  clwlkclwwlkfo  29911  clwwlkwwlksb  29956  clwwlkndivn  29982  eupth2lem3lem3  30132  eupth2lem3lem4  30133  eupth2lem3  30138  eupth2lems  30140  numclwwlk5  30290  numclwwlk6  30292  ex-ind-dvds  30363  nndiffz1  32682  elfzodif0  32690  fzo0opth  32701  ccatf1  32843  ccatdmss  32844  pfxlsw2ccat  32845  wrdt2ind  32848  chnind  32910  chnub  32911  gsumwrd2dccatlem  32979  cycpmfv1  33043  cycpmco2lem2  33057  cycpmco2lem3  33058  cycpmco2lem4  33059  cycpmco2lem5  33060  cycpmco2lem6  33061  cycpmco2  33063  cycpmrn  33073  cyc3genpm  33082  cycpmconjslem2  33085  cyc3conja  33087  archirng  33115  archirngz  33116  archiabllem1a  33118  elrspunidl  33372  ply1degltel  33533  ply1degltdimlem  33591  fldextrspundgdvds  33649  algextdeglem8  33687  rtelextdg2  33690  constrext2chnlem  33713  cos9thpiminplylem2  33746  cos9thpiminplylem3  33747  cos9thpiminplylem6  33750  cos9thpiminply  33751  madjusmdetlem4  33793  zrhcntr  33942  qqhval2lem  33944  oddpwdc  34318  eulerpartlems  34324  eulerpartlemb  34332  sseqfv1  34353  sseqfn  34354  sseqmw  34355  sseqf  34356  sseqfv2  34358  sseqp1  34359  ccatmulgnn0dir  34506  signsplypnf  34514  signsply0  34515  signslema  34526  signstfvn  34533  signstfvp  34535  signstfvc  34538  fsum2dsub  34571  reprinfz1  34586  reprfi2  34587  hashrepr  34589  reprdifc  34591  breprexplema  34594  breprexplemc  34596  circlemeth  34604  circlevma  34606  circlemethhgt  34607  hgt750lema  34621  tgoldbachgtde  34624  lpadlem3  34642  revpfxsfxrev  35076  revwlk  35085  subfacval3  35149  bcprod  35698  bccolsum  35699  fwddifnp1  36126  knoppndvlem6  36478  knoppndvlem7  36479  knoppndvlem10  36482  knoppndvlem14  36486  knoppndvlem15  36487  knoppndvlem16  36488  knoppndvlem17  36489  knoppndvlem19  36491  knoppndvlem21  36493  dfgcd3  37285  poimirlem3  37590  poimirlem4  37591  poimirlem6  37593  poimirlem13  37600  poimirlem14  37601  poimirlem17  37604  poimirlem21  37608  poimirlem22  37609  poimirlem23  37610  poimirlem26  37613  poimirlem27  37614  poimirlem31  37618  geomcau  37726  bccl2d  41952  lcmineqlem12  42001  lcmineqlem17  42006  dvrelogpow2b  42029  aks4d1p1p2  42031  aks4d1p1p4  42032  aks4d1p1p6  42034  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  aks4d1p3  42039  aks4d1p6  42042  aks4d1p8d2  42046  aks4d1p8d3  42047  aks4d1p8  42048  primrootscoprmpow  42060  primrootlekpowne0  42066  aks6d1c1  42077  aks6d1c2p2  42080  aks6d1c2lem4  42088  aks6d1c2  42091  aks6d1c5lem3  42098  aks6d1c5lem2  42099  2np3bcnp1  42105  sticksstones5  42111  sticksstones6  42112  sticksstones7  42113  sticksstones10  42116  sticksstones11  42117  sticksstones12a  42118  sticksstones12  42119  sticksstones22  42129  aks6d1c6lem3  42133  bcled  42139  bcle2d  42140  aks6d1c7lem1  42141  aks6d1c7lem2  42142  grpods  42155  unitscyglem2  42157  unitscyglem4  42159  aks5lem8  42162  sumcubes  42274  gcdle1d  42291  gcdle2d  42292  frlmvscadiccat  42467  fltdiv  42597  flt4lem4  42610  fltnltalem  42623  eldioph2lem1  42721  pellexlem5  42794  congrep  42935  jm2.18  42950  jm2.19lem1  42951  jm2.19lem2  42952  jm2.19  42955  jm2.22  42957  jm2.23  42958  jm2.20nn  42959  jm2.25  42961  jm2.26a  42962  jm2.26lem3  42963  jm2.26  42964  jm2.27a  42967  jm2.27b  42968  jm2.27c  42969  jm3.1  42982  expdiophlem1  42983  hbtlem5  43090  radcnvrat  44276  nzin  44280  bccbc  44307  binomcxplemnn0  44311  binomcxplemnotnn0  44318  fprodexp  45565  mccllem  45568  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnxpaek  45913  dvnmul  45914  dvnprodlem1  45917  dvnprodlem2  45918  wallispilem1  46036  wallispilem5  46040  stirlinglem3  46047  stirlinglem5  46049  stirlinglem7  46051  stirlinglem8  46052  fourierdlem102  46179  fourierdlem114  46191  sqwvfoura  46199  elaa2lem  46204  etransclem10  46215  etransclem20  46225  etransclem21  46226  etransclem22  46227  etransclem23  46228  etransclem24  46229  etransclem27  46232  etransclem28  46233  etransclem35  46240  etransclem38  46243  etransclem44  46249  etransclem45  46250  etransclem46  46251  sge0ad2en  46402  fsummmodsnunz  47349  fmtnoge3  47504  fmtnof1  47509  fmtnorec1  47511  sqrtpwpw2p  47512  fmtnodvds  47518  goldbachthlem2  47520  fmtnoprmfac2lem1  47540  lighneallem3  47581  lighneallem4b  47583  lighneallem4  47584  ssnn0ssfz  48310  altgsumbcALT  48314  flnn0ohalf  48496  dig2nn1st  48567  0dig2nn0o  48575  aacllem  49763