Theorem nn0zd 12639

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

Syntax hints:   → wi 4   ∈ wcel 2108  ℕ₀cn0 12526  ℤcz 12613

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-i2m1 11223  ax-1ne0 11224  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-neg 11495  df-nn 12267  df-n0 12527  df-z 12614

This theorem is referenced by:  nnzd  12640  eluzmn  12885  difelfznle  13682  zmodfz  13933  expnegz  14137  expaddzlem  14146  expaddz  14147  expmulz  14149  faclbnd  14329  bcpasc  14360  hashf1  14496  fz1isolem  14500  hashge2el2dif  14519  hashtpg  14524  wrdffz  14573  ffz0iswrd  14579  wrdsymb0  14587  wrdlenge1n0  14588  ccatcl  14612  ccatval3  14617  ccatsymb  14620  ccatval21sw  14623  ccatass  14626  ccatrn  14627  lswccatn0lsw  14629  ccats1val2  14665  swrdnd  14692  swrdccat2  14707  pfxtrcfv0  14732  pfxtrcfvl  14735  pfxccat1  14740  swrdccatin2  14767  pfxccatin12  14771  pfxccatpfx2  14775  pfxccat3a  14776  splfv2a  14794  splval2  14795  revcl  14799  revccat  14804  revrev  14805  cshwmodn  14833  cshwsublen  14834  cshwn  14835  cshwidxmod  14841  2cshwid  14852  3cshw  14856  cshweqdif2  14857  revco  14873  ccatco  14874  ccat2s1fvwALT  14994  ofccat  15008  zabscl  15352  absrdbnd  15380  iseraltlem3  15720  fsum0diaglem  15812  modfsummods  15829  binomlem  15865  binom1p  15867  incexc2  15874  climcndslem1  15885  geoser  15903  pwm1geoser  15905  geolim2  15907  mertenslem1  15920  mertenslem2  15921  mertens  15922  binomfallfaclem2  16076  binomrisefac  16078  fallfacval4  16079  bpolydiflem  16090  ruclem10  16275  sumodd  16425  divalglem9  16438  divalgmod  16443  bitsfzolem  16471  bitsfzo  16472  bitsmod  16473  bitsfi  16474  bitsinv1lem  16478  sadcaddlem  16494  sadadd3  16498  sadaddlem  16503  sadadd  16504  sadasslem  16507  sadass  16508  sadeq  16509  bitsres  16510  bitsuz  16511  bitsshft  16512  smuval2  16519  smupvallem  16520  smupval  16525  smueqlem  16527  smumullem  16529  smumul  16530  gcdcllem1  16536  zeqzmulgcd  16547  gcd0id  16556  gcdneg  16559  modgcd  16569  gcdmultipled  16571  bezoutlem4  16579  dvdsgcdb  16582  gcdass  16584  mulgcd  16585  gcdzeq  16589  dvdsmulgcd  16593  bezoutr  16605  bezoutr1  16606  nn0seqcvgd  16607  algfx  16617  eucalginv  16621  eucalg  16624  gcddvdslcm  16639  lcmneg  16640  lcmgcdlem  16643  lcmdvds  16645  lcmgcdeq  16649  lcmdvdsb  16650  lcmass  16651  lcmftp  16673  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  lcmfunsnlem2  16677  lcmfdvdsb  16680  lcmfun  16682  lcmfass  16683  mulgcddvds  16692  rpmulgcd2  16693  qredeu  16695  divgcdcoprm0  16702  sqnprm  16739  prmdvdsbc  16763  divnumden  16785  powm2modprm  16841  coprimeprodsq  16846  iserodd  16873  pclem  16876  pcpre1  16880  pcpremul  16881  pcqcl  16894  pcdvdsb  16907  pcidlem  16910  pc2dvds  16917  pcprmpw2  16920  dvdsprmpweqle  16924  pcadd  16927  pcfac  16937  pcbc  16938  pockthlem  16943  prmreclem2  16955  prmreclem3  16956  mul4sqlem  16991  4sqlem11  16993  4sqlem12  16994  4sqlem14  16996  vdwapun  17012  prmgaplcmlem1  17089  lagsubg  19213  psgnuni  19517  psgnran  19533  odmodnn0  19558  mndodconglem  19559  mndodcong  19560  odm1inv  19571  odmulg2  19573  odmulg  19574  odmulgeq  19575  odbezout  19576  odinv  19579  odf1  19580  gexod  19604  gexdvds3  19608  sylow1lem1  19616  sylow1lem3  19618  pgpfi  19623  pgpssslw  19632  sylow2alem2  19636  sylow2blem3  19640  fislw  19643  sylow3lem4  19648  sylow3lem6  19650  efginvrel2  19745  efgredlemf  19759  efgredlemd  19762  efgredlemc  19763  efgredlem  19765  efgcpbllemb  19773  odadd1  19866  odadd2  19867  gexexlem  19870  gexex  19871  torsubg  19872  lt6abl  19913  gsummulg  19960  ablfacrplem  20085  ablfacrp  20086  ablfacrp2  20087  ablfac1b  20090  ablfac1c  20091  ablfac1eulem  20092  ablfac1eu  20093  pgpfac1lem2  20095  pgpfaclem1  20101  ablfaclem3  20107  srgbinomlem3  20225  srgbinomlem4  20226  chrid  21540  znunit  21582  freshmansdream  21593  psgnghm  21598  asclmulg  21922  psrbaglefi  21946  psdvsca  22168  psdmul  22170  chfacfscmulfsupp  22865  chfacfpmmulfsupp  22869  cpmadugsumlemF  22882  dyadss  25629  dyaddisjlem  25630  ply1divex  26176  ply1termlem  26242  plyeq0lem  26249  plyaddlem1  26252  plymullem1  26253  coeeulem  26263  coeidlem  26276  coeeq2  26281  coemulhi  26293  dvply1  26325  dvply2g  26326  dvply2gOLD  26327  plydivex  26339  elqaalem2  26362  aareccl  26368  aannenlem1  26370  aalioulem1  26374  taylplem1  26404  taylplem2  26405  taylpfval  26406  dvtaylp  26412  taylthlem2  26416  taylthlem2OLD  26417  dvradcnv  26464  abelthlem7  26482  cxpeq  26800  birthdaylem2  26995  ftalem1  27116  basellem3  27126  isppw2  27158  isnsqf  27178  mule1  27191  ppinncl  27217  musum  27234  chtublem  27255  pclogsum  27259  vmasum  27260  dchrabs  27304  bcmax  27322  bposlem1  27328  bposlem6  27333  lgsval2lem  27351  lgsmod  27367  lgsne0  27379  gausslemma2dlem0h  27407  gausslemma2dlem0i  27408  gausslemma2dlem2  27411  gausslemma2dlem6  27416  gausslemma2d  27418  lgseisenlem1  27419  lgseisenlem2  27420  lgseisenlem3  27421  lgseisenlem4  27422  lgsquadlem1  27424  m1lgs  27432  2lgslem1a  27435  2lgslem3a  27440  2lgslem3b  27441  2lgslem3c  27442  2lgslem3d  27443  2lgslem3d1  27447  2lgsoddprmlem2  27453  2sqlem8  27470  2sqcoprm  27479  2sqmod  27480  chebbnd1lem1  27513  dchrisumlem1  27533  dchrisum0flblem1  27552  selberg2lem  27594  ostth2lem2  27678  ostth2lem3  27679  finsumvtxdg2sstep  29567  finsumvtxdgeven  29570  vtxdgoddnumeven  29571  redwlklem  29689  wlkdlem1  29700  pthdlem1  29786  crctcshwlkn0lem4  29833  wwlksnredwwlkn0  29916  wwlksnextproplem2  29930  clwwlkccatlem  30008  clwlkclwwlkfo  30028  clwwlkwwlksb  30073  clwwlkndivn  30099  eupth2lem3lem3  30249  eupth2lem3lem4  30250  eupth2lem3  30255  eupth2lems  30257  numclwwlk5  30407  numclwwlk6  30409  ex-ind-dvds  30480  nndiffz1  32788  elfzodif0  32796  fzo0opth  32807  ccatf1  32933  ccatdmss  32934  pfxlsw2ccat  32935  wrdt2ind  32938  chnind  33001  chnub  33002  gsumwrd2dccatlem  33069  cycpmfv1  33133  cycpmco2lem2  33147  cycpmco2lem3  33148  cycpmco2lem4  33149  cycpmco2lem5  33150  cycpmco2lem6  33151  cycpmco2  33153  cycpmrn  33163  cyc3genpm  33172  cycpmconjslem2  33175  cyc3conja  33177  archirng  33195  archirngz  33196  archiabllem1a  33198  elrspunidl  33456  ply1degltel  33615  ply1degltdimlem  33673  fldextrspundgdvds  33731  algextdeglem8  33765  rtelextdg2  33768  madjusmdetlem4  33829  zrhcntr  33980  qqhval2lem  33982  oddpwdc  34356  eulerpartlems  34362  eulerpartlemb  34370  sseqfv1  34391  sseqfn  34392  sseqmw  34393  sseqf  34394  sseqfv2  34396  sseqp1  34397  ccatmulgnn0dir  34557  signsplypnf  34565  signsply0  34566  signslema  34577  signstfvn  34584  signstfvp  34586  signstfvc  34589  fsum2dsub  34622  reprinfz1  34637  reprfi2  34638  hashrepr  34640  reprdifc  34642  breprexplema  34645  breprexplemc  34647  circlemeth  34655  circlevma  34657  circlemethhgt  34658  hgt750lema  34672  tgoldbachgtde  34675  lpadlem3  34693  revpfxsfxrev  35121  revwlk  35130  subfacval3  35194  bcprod  35738  bccolsum  35739  fwddifnp1  36166  knoppndvlem6  36518  knoppndvlem7  36519  knoppndvlem10  36522  knoppndvlem14  36526  knoppndvlem15  36527  knoppndvlem16  36528  knoppndvlem17  36529  knoppndvlem19  36531  knoppndvlem21  36533  dfgcd3  37325  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem13  37640  poimirlem14  37641  poimirlem17  37644  poimirlem21  37648  poimirlem22  37649  poimirlem23  37650  poimirlem26  37653  poimirlem27  37654  poimirlem31  37658  geomcau  37766  bccl2d  41992  lcmineqlem12  42041  lcmineqlem17  42046  dvrelogpow2b  42069  aks4d1p1p2  42071  aks4d1p1p4  42072  aks4d1p1p6  42074  aks4d1p1p7  42075  aks4d1p1p5  42076  aks4d1p1  42077  aks4d1p3  42079  aks4d1p6  42082  aks4d1p8d2  42086  aks4d1p8d3  42087  aks4d1p8  42088  primrootscoprmpow  42100  primrootlekpowne0  42106  aks6d1c1  42117  aks6d1c2p2  42120  aks6d1c2lem4  42128  aks6d1c2  42131  aks6d1c5lem3  42138  aks6d1c5lem2  42139  2np3bcnp1  42145  sticksstones5  42151  sticksstones6  42152  sticksstones7  42153  sticksstones10  42156  sticksstones11  42157  sticksstones12a  42158  sticksstones12  42159  sticksstones22  42169  aks6d1c6lem3  42173  bcled  42179  bcle2d  42180  aks6d1c7lem1  42181  aks6d1c7lem2  42182  grpods  42195  unitscyglem2  42197  unitscyglem4  42199  aks5lem8  42202  prodsplit  42241  sumcubes  42347  gcdle1d  42365  gcdle2d  42366  frlmvscadiccat  42516  fltdiv  42646  flt4lem4  42659  fltnltalem  42672  eldioph2lem1  42771  pellexlem5  42844  congrep  42985  jm2.18  43000  jm2.19lem1  43001  jm2.19lem2  43002  jm2.19  43005  jm2.22  43007  jm2.23  43008  jm2.20nn  43009  jm2.25  43011  jm2.26a  43012  jm2.26lem3  43013  jm2.26  43014  jm2.27a  43017  jm2.27b  43018  jm2.27c  43019  jm3.1  43032  expdiophlem1  43033  hbtlem5  43140  radcnvrat  44333  nzin  44337  bccbc  44364  binomcxplemnn0  44368  binomcxplemnotnn0  44375  fprodexp  45609  mccllem  45612  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnxpaek  45957  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  wallispilem1  46080  wallispilem5  46084  stirlinglem3  46091  stirlinglem5  46093  stirlinglem7  46095  stirlinglem8  46096  fourierdlem102  46223  fourierdlem114  46235  sqwvfoura  46243  elaa2lem  46248  etransclem10  46259  etransclem20  46269  etransclem21  46270  etransclem22  46271  etransclem23  46272  etransclem24  46273  etransclem27  46276  etransclem28  46277  etransclem35  46284  etransclem38  46287  etransclem44  46293  etransclem45  46294  etransclem46  46295  sge0ad2en  46446  fsummmodsnunz  47362  fmtnoge3  47517  fmtnof1  47522  fmtnorec1  47524  sqrtpwpw2p  47525  fmtnodvds  47531  goldbachthlem2  47533  fmtnoprmfac2lem1  47553  lighneallem3  47594  lighneallem4b  47596  lighneallem4  47597  ssnn0ssfz  48265  altgsumbcALT  48269  flnn0ohalf  48455  dig2nn1st  48526  0dig2nn0o  48534  aacllem  49320