Theorem nn0zd 12534

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

Syntax hints:   → wi 4   ∈ wcel 2106  ℕ₀cn0 12422  ℤcz 12508

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677  ax-1cn 11118  ax-icn 11119  ax-addcl 11120  ax-addrcl 11121  ax-mulcl 11122  ax-mulrcl 11123  ax-i2m1 11128  ax-1ne0 11129  ax-rnegex 11131  ax-rrecex 11132  ax-cnre 11133

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-iun 4961  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-ov 7365  df-om 7808  df-2nd 7927  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-neg 11397  df-nn 12163  df-n0 12423  df-z 12509

This theorem is referenced by:  nnzd  12535  eluzmn  12779  difelfznle  13565  zmodfz  13808  expnegz  14012  expaddzlem  14021  expaddz  14022  expmulz  14024  faclbnd  14200  bcpasc  14231  hashf1  14368  fz1isolem  14372  hashge2el2dif  14391  hashtpg  14396  wrdffz  14435  ffz0iswrd  14441  wrdsymb0  14449  wrdlenge1n0  14450  ccatcl  14474  ccatval3  14479  ccatsymb  14482  ccatval21sw  14485  ccatass  14488  ccatrn  14489  lswccatn0lsw  14491  ccats1val2  14527  swrdnd  14554  swrdccat2  14569  pfxtrcfv0  14594  pfxtrcfvl  14597  pfxccat1  14602  swrdccatin2  14629  pfxccatin12  14633  pfxccatpfx2  14637  pfxccat3a  14638  splfv2a  14656  splval2  14657  revcl  14661  revccat  14666  revrev  14667  cshwmodn  14695  cshwsublen  14696  cshwn  14697  cshwidxmod  14703  2cshwid  14714  3cshw  14718  cshweqdif2  14719  revco  14735  ccatco  14736  ccat2s1fvwALT  14856  ofccat  14866  zabscl  15210  absrdbnd  15238  iseraltlem3  15580  fsum0diaglem  15672  modfsummods  15689  binomlem  15725  binom1p  15727  incexc2  15734  climcndslem1  15745  geoser  15763  pwm1geoser  15765  geolim2  15767  mertenslem1  15780  mertenslem2  15781  mertens  15782  binomfallfaclem2  15934  binomrisefac  15936  fallfacval4  15937  bpolydiflem  15948  ruclem10  16132  sumodd  16281  divalglem9  16294  divalgmod  16299  bitsfzolem  16325  bitsfzo  16326  bitsmod  16327  bitsfi  16328  bitsinv1lem  16332  sadcaddlem  16348  sadadd3  16352  sadaddlem  16357  sadadd  16358  sadasslem  16361  sadass  16362  sadeq  16363  bitsres  16364  bitsuz  16365  bitsshft  16366  smuval2  16373  smupvallem  16374  smupval  16379  smueqlem  16381  smumullem  16383  smumul  16384  gcdcllem1  16390  zeqzmulgcd  16401  gcd0id  16410  gcdneg  16413  modgcd  16424  gcdmultipled  16426  bezoutlem4  16434  dvdsgcdb  16437  gcdass  16439  mulgcd  16440  gcdzeq  16444  dvdsmulgcd  16447  bezoutr  16455  bezoutr1  16456  nn0seqcvgd  16457  algfx  16467  eucalginv  16471  eucalg  16474  gcddvdslcm  16489  lcmneg  16490  lcmgcdlem  16493  lcmdvds  16495  lcmgcdeq  16499  lcmdvdsb  16500  lcmass  16501  lcmftp  16523  lcmfunsnlem1  16524  lcmfunsnlem2lem1  16525  lcmfunsnlem2lem2  16526  lcmfunsnlem2  16527  lcmfdvdsb  16530  lcmfun  16532  lcmfass  16533  mulgcddvds  16542  rpmulgcd2  16543  qredeu  16545  divgcdcoprm0  16552  sqnprm  16589  divnumden  16634  powm2modprm  16686  coprimeprodsq  16691  iserodd  16718  pclem  16721  pcpre1  16725  pcpremul  16726  pcqcl  16739  pcdvdsb  16752  pcidlem  16755  pc2dvds  16762  pcprmpw2  16765  dvdsprmpweqle  16769  pcadd  16772  pcfac  16782  pcbc  16783  pockthlem  16788  prmreclem2  16800  prmreclem3  16801  mul4sqlem  16836  4sqlem11  16838  4sqlem12  16839  4sqlem14  16841  vdwapun  16857  prmgaplcmlem1  16934  lagsubg  19006  psgnuni  19295  psgnran  19311  odmodnn0  19336  mndodconglem  19337  mndodcong  19338  odm1inv  19349  odmulg2  19351  odmulg  19352  odmulgeq  19353  odbezout  19354  odinv  19357  odf1  19358  gexod  19382  gexdvds3  19386  sylow1lem1  19394  sylow1lem3  19396  pgpfi  19401  pgpssslw  19410  sylow2alem2  19414  sylow2blem3  19418  fislw  19421  sylow3lem4  19426  sylow3lem6  19428  efginvrel2  19523  efgredlemf  19537  efgredlemd  19540  efgredlemc  19541  efgredlem  19543  efgcpbllemb  19551  odadd1  19640  odadd2  19641  gexexlem  19644  gexex  19645  torsubg  19646  lt6abl  19686  gsummulg  19733  ablfacrplem  19858  ablfacrp  19859  ablfacrp2  19860  ablfac1b  19863  ablfac1c  19864  ablfac1eulem  19865  ablfac1eu  19866  pgpfac1lem2  19868  pgpfaclem1  19874  ablfaclem3  19880  srgbinomlem3  19973  srgbinomlem4  19974  chrid  20967  znunit  21007  psgnghm  21021  psrbaglefi  21371  psrbaglefiOLD  21372  chfacfscmulfsupp  22245  chfacfpmmulfsupp  22249  cpmadugsumlemF  22262  dyadss  24995  dyaddisjlem  24996  ply1divex  25538  ply1termlem  25601  plyeq0lem  25608  plyaddlem1  25611  plymullem1  25612  coeeulem  25622  coeidlem  25635  coeeq2  25640  coemulhi  25652  dvply1  25681  dvply2g  25682  plydivex  25694  elqaalem2  25717  aareccl  25723  aannenlem1  25725  aalioulem1  25729  taylplem1  25759  taylplem2  25760  taylpfval  25761  dvtaylp  25766  taylthlem2  25770  dvradcnv  25817  abelthlem7  25834  cxpeq  26147  birthdaylem2  26339  ftalem1  26459  basellem3  26469  isppw2  26501  isnsqf  26521  mule1  26534  ppinncl  26560  musum  26577  chtublem  26596  pclogsum  26600  vmasum  26601  dchrabs  26645  bcmax  26663  bposlem1  26669  bposlem6  26674  lgsval2lem  26692  lgsmod  26708  lgsne0  26720  gausslemma2dlem0h  26748  gausslemma2dlem0i  26749  gausslemma2dlem2  26752  gausslemma2dlem6  26757  gausslemma2d  26759  lgseisenlem1  26760  lgseisenlem2  26761  lgseisenlem3  26762  lgseisenlem4  26763  lgsquadlem1  26765  m1lgs  26773  2lgslem1a  26776  2lgslem3a  26781  2lgslem3b  26782  2lgslem3c  26783  2lgslem3d  26784  2lgslem3d1  26788  2lgsoddprmlem2  26794  2sqlem8  26811  2sqcoprm  26820  2sqmod  26821  chebbnd1lem1  26854  dchrisumlem1  26874  dchrisum0flblem1  26893  selberg2lem  26935  ostth2lem2  27019  ostth2lem3  27020  finsumvtxdg2sstep  28560  finsumvtxdgeven  28563  vtxdgoddnumeven  28564  redwlklem  28682  wlkdlem1  28693  pthdlem1  28777  crctcshwlkn0lem4  28821  wwlksnredwwlkn0  28904  wwlksnextproplem2  28918  clwwlkccatlem  28996  clwlkclwwlkfo  29016  clwwlkwwlksb  29061  clwwlkndivn  29087  eupth2lem3lem3  29237  eupth2lem3lem4  29238  eupth2lem3  29243  eupth2lems  29245  numclwwlk5  29395  numclwwlk6  29397  ex-ind-dvds  29468  nndiffz1  31757  prmdvdsbc  31782  ccatf1  31875  pfxlsw2ccat  31876  wrdt2ind  31877  cycpmfv1  32032  cycpmco2lem2  32046  cycpmco2lem3  32047  cycpmco2lem4  32048  cycpmco2lem5  32049  cycpmco2lem6  32050  cycpmco2  32052  cycpmrn  32062  cyc3genpm  32071  cycpmconjslem2  32074  cyc3conja  32076  archirng  32094  archirngz  32095  archiabllem1a  32097  freshmansdream  32137  elrspunidl  32279  asclmulg  32339  ply1degltel  32365  ply1degltdimlem  32404  madjusmdetlem4  32500  qqhval2lem  32651  oddpwdc  33043  eulerpartlems  33049  eulerpartlemb  33057  sseqfv1  33078  sseqfn  33079  sseqmw  33080  sseqf  33081  sseqfv2  33083  sseqp1  33084  ccatmulgnn0dir  33243  signsplypnf  33251  signsply0  33252  signslema  33263  signstfvn  33270  signstfvp  33272  signstfvc  33275  fsum2dsub  33309  reprinfz1  33324  reprfi2  33325  hashrepr  33327  reprdifc  33329  breprexplema  33332  breprexplemc  33334  circlemeth  33342  circlevma  33344  circlemethhgt  33345  hgt750lema  33359  tgoldbachgtde  33362  lpadlem3  33380  revpfxsfxrev  33796  revwlk  33805  subfacval3  33870  bcprod  34397  bccolsum  34398  fwddifnp1  34826  knoppndvlem6  35056  knoppndvlem7  35057  knoppndvlem10  35060  knoppndvlem14  35064  knoppndvlem15  35065  knoppndvlem16  35066  knoppndvlem17  35067  knoppndvlem19  35069  knoppndvlem21  35071  dfgcd3  35868  poimirlem3  36154  poimirlem4  36155  poimirlem6  36157  poimirlem13  36164  poimirlem14  36165  poimirlem17  36168  poimirlem21  36172  poimirlem22  36173  poimirlem23  36174  poimirlem26  36177  poimirlem27  36178  poimirlem31  36182  geomcau  36291  bccl2d  40522  lcmineqlem12  40570  lcmineqlem17  40575  dvrelogpow2b  40598  aks4d1p1p2  40600  aks4d1p1p4  40601  aks4d1p1p6  40603  aks4d1p1p7  40604  aks4d1p1p5  40605  aks4d1p1  40606  aks4d1p3  40608  aks4d1p6  40611  aks4d1p8d2  40615  aks4d1p8d3  40616  aks4d1p8  40617  aks6d1c2p2  40622  2np3bcnp1  40625  sticksstones5  40631  sticksstones6  40632  sticksstones7  40633  sticksstones10  40636  sticksstones11  40637  sticksstones12a  40638  sticksstones12  40639  sticksstones22  40649  prodsplit  40686  frlmvscadiccat  40749  gcdle1d  40874  gcdle2d  40875  fltdiv  41032  flt4lem4  41045  fltnltalem  41058  eldioph2lem1  41141  pellexlem5  41214  congrep  41355  jm2.18  41370  jm2.19lem1  41371  jm2.19lem2  41372  jm2.19  41375  jm2.22  41377  jm2.23  41378  jm2.20nn  41379  jm2.25  41381  jm2.26a  41382  jm2.26lem3  41383  jm2.26  41384  jm2.27a  41387  jm2.27b  41388  jm2.27c  41389  jm3.1  41402  expdiophlem1  41403  hbtlem5  41513  radcnvrat  42716  nzin  42720  bccbc  42747  binomcxplemnn0  42751  binomcxplemnotnn0  42758  fprodexp  43955  mccllem  43958  ioodvbdlimc1lem2  44293  ioodvbdlimc2lem  44295  dvnxpaek  44303  dvnmul  44304  dvnprodlem1  44307  dvnprodlem2  44308  wallispilem1  44426  wallispilem5  44430  stirlinglem3  44437  stirlinglem5  44439  stirlinglem7  44441  stirlinglem8  44442  fourierdlem102  44569  fourierdlem114  44581  sqwvfoura  44589  elaa2lem  44594  etransclem10  44605  etransclem20  44615  etransclem21  44616  etransclem22  44617  etransclem23  44618  etransclem24  44619  etransclem27  44622  etransclem28  44623  etransclem35  44630  etransclem38  44633  etransclem44  44639  etransclem45  44640  etransclem46  44641  sge0ad2en  44792  fsummmodsnunz  45687  fmtnoge3  45842  fmtnof1  45847  fmtnorec1  45849  sqrtpwpw2p  45850  fmtnodvds  45856  goldbachthlem2  45858  fmtnoprmfac2lem1  45878  lighneallem3  45919  lighneallem4b  45921  lighneallem4  45922  ssnn0ssfz  46545  altgsumbcALT  46549  flnn0ohalf  46740  dig2nn1st  46811  0dig2nn0o  46819  aacllem  47368