Theorem nn0zd 12615

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

Syntax hints:   → wi 4   ∈ wcel 2149  ℕ₀cn0 12503  ℤcz 12590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405  ax-un 7733  ax-1cn 11157  ax-icn 11158  ax-addcl 11159  ax-addrcl 11160  ax-mulcl 11161  ax-mulrcl 11162  ax-i2m1 11167  ax-1ne0 11168  ax-rnegex 11170  ax-rrecex 11171  ax-cnre 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-iun 4962  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-ov 7414  df-om 7862  df-2nd 7986  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-neg 11443  df-nn 12233  df-n0 12504  df-z 12591

This theorem is referenced by:  nnzd  12616  eluzmn  12868  difelfznle  13669  elfzodif0  13798  zmodfz  13925  expnegz  14131  expaddzlem  14140  expaddz  14141  expmulz  14143  faclbnd  14325  bcpasc  14356  hashf1  14493  fz1isolem  14497  hashge2el2dif  14516  hashtpg  14521  wrdffz  14571  ffz0iswrd  14577  wrdsymb0  14585  wrdlenge1n0  14586  ccatcl  14610  ccatval3  14615  ccatdmss  14618  ccatsymb  14619  ccatval21sw  14622  ccatass  14625  ccatrn  14626  lswccatn0lsw  14628  ccats1val2  14664  swrdnd  14691  swrdccat2  14706  pfxtrcfv0  14730  pfxtrcfvl  14733  pfxccat1  14738  swrdccatin2  14765  pfxccatin12  14769  pfxccatpfx2  14773  pfxccat3a  14774  splfv2a  14792  splval2  14793  revcl  14797  revccat  14802  revrev  14803  cshwmodn  14831  cshwsublen  14832  cshwn  14833  cshwidxmod  14839  2cshwid  14850  3cshw  14854  cshweqdif2  14855  revco  14870  ccatco  14871  ccat2s1fvwALT  14991  ofccat  15005  zabscl  15363  absrdbnd  15392  iseraltlem3  15734  fsum0diaglem  15826  modfsummods  15844  binomlem  15882  binom1p  15884  incexc2  15891  climcndslem1  15902  geoser  15920  pwm1geoser  15922  geolim2  15924  mertenslem1  15937  mertenslem2  15938  mertens  15939  binomfallfaclem2  16093  binomrisefac  16095  fallfacval4  16096  bpolydiflem  16107  ruclem10  16294  sumodd  16445  divalglem9  16458  divalgmod  16463  bitsfzolem  16491  bitsfzo  16492  bitsmod  16493  bitsfi  16494  bitsinv1lem  16498  sadcaddlem  16514  sadadd3  16518  sadaddlem  16523  sadadd  16524  sadasslem  16527  sadass  16528  sadeq  16529  bitsres  16530  bitsuz  16531  bitsshft  16532  smuval2  16539  smupvallem  16540  smupval  16545  smueqlem  16547  smumullem  16549  smumul  16550  gcdcllem1  16556  zeqzmulgcd  16567  gcd0id  16576  gcdneg  16579  modgcd  16589  gcdmultipled  16591  bezoutlem4  16599  dvdsgcdb  16602  gcdass  16604  mulgcd  16605  gcdzeq  16609  dvdsmulgcd  16613  bezoutr  16625  bezoutr1  16626  nn0seqcvgd  16627  algfx  16637  eucalginv  16641  eucalg  16644  gcddvdslcm  16659  lcmneg  16660  lcmgcdlem  16663  lcmdvds  16665  lcmgcdeq  16669  lcmdvdsb  16670  lcmass  16671  lcmftp  16693  lcmfunsnlem1  16694  lcmfunsnlem2lem1  16695  lcmfunsnlem2lem2  16696  lcmfunsnlem2  16697  lcmfdvdsb  16700  lcmfun  16702  lcmfass  16703  mulgcddvds  16712  rpmulgcd2  16713  qredeu  16715  divgcdcoprm0  16722  sqnprm  16760  prmdvdsbc  16784  divnumden  16806  powm2modprm  16862  coprimeprodsq  16867  iserodd  16894  pclem  16897  pcpre1  16901  pcpremul  16902  pcqcl  16915  pcdvdsb  16928  pcidlem  16931  pc2dvds  16938  pcprmpw2  16941  dvdsprmpweqle  16945  pcadd  16948  pcfac  16958  pcbc  16959  pockthlem  16964  prmreclem2  16976  prmreclem3  16977  mul4sqlem  17012  4sqlem11  17014  4sqlem12  17015  4sqlem14  17017  vdwapun  17033  prmgaplcmlem1  17110  chnind  18676  chnub  18677  chnpolfz  18688  lagsubg  19265  psgnuni  19568  psgnran  19584  odmodnn0  19609  mndodconglem  19610  mndodcong  19611  odm1inv  19622  odmulg2  19624  odmulg  19625  odmulgeq  19626  odbezout  19627  odinv  19630  odf1  19631  gexod  19655  gexdvds3  19659  sylow1lem1  19667  sylow1lem3  19669  pgpfi  19674  pgpssslw  19683  sylow2alem2  19687  sylow2blem3  19691  fislw  19694  sylow3lem4  19699  sylow3lem6  19701  efginvrel2  19796  efgredlemf  19810  efgredlemd  19813  efgredlemc  19814  efgredlem  19816  efgcpbllemb  19824  odadd1  19917  odadd2  19918  gexexlem  19921  gexex  19922  torsubg  19923  lt6abl  19964  gsummulg  20011  ablfacrplem  20136  ablfacrp  20137  ablfacrp2  20138  ablfac1b  20141  ablfac1c  20142  ablfac1eulem  20143  ablfac1eu  20144  pgpfac1lem2  20146  pgpfaclem1  20152  ablfaclem3  20158  srgbinomlem3  20309  srgbinomlem4  20310  chrid  21643  znunit  21681  freshmansdream  21692  psgnghm  21698  asclmulg  22020  psrbaglefi  22044  psdvsca  22295  psdmul  22297  chfacfscmulfsupp  22984  chfacfpmmulfsupp  22988  cpmadugsumlemF  23001  dyadss  25721  dyaddisjlem  25722  ply1divex  26262  ply1termlem  26328  plyeq0lem  26335  plyaddlem1  26338  plymullem1  26339  coeeulem  26349  coeidlem  26362  coeeq2  26367  coemulhi  26379  dvply1  26413  dvply2g  26414  plydivex  26426  elqaalem2  26449  aareccl  26455  aannenlem1  26457  aalioulem1  26461  taylplem1  26491  taylplem2  26492  taylpfval  26493  dvtaylp  26498  taylthlem2  26502  dvradcnv  26549  abelthlem7  26566  cxpeq  26887  birthdaylem2  27082  ftalem1  27202  basellem3  27212  isppw2  27244  isnsqf  27264  mule1  27277  ppinncl  27303  musum  27320  chtublem  27340  pclogsum  27344  vmasum  27345  dchrabs  27389  bcmax  27407  bposlem1  27413  bposlem6  27418  lgsval2lem  27436  lgsmod  27452  lgsne0  27464  gausslemma2dlem0h  27492  gausslemma2dlem0i  27493  gausslemma2dlem2  27496  gausslemma2dlem6  27501  gausslemma2d  27503  lgseisenlem1  27504  lgseisenlem2  27505  lgseisenlem3  27506  lgseisenlem4  27507  lgsquadlem1  27509  m1lgs  27517  2lgslem1a  27520  2lgslem3a  27525  2lgslem3b  27526  2lgslem3c  27527  2lgslem3d  27528  2lgslem3d1  27532  2lgsoddprmlem2  27538  2sqlem8  27555  2sqcoprm  27564  2sqmod  27565  chebbnd1lem1  27598  dchrisumlem1  27618  dchrisum0flblem1  27637  selberg2lem  27679  ostth2lem2  27763  ostth2lem3  27764  finsumvtxdg2sstep  29839  finsumvtxdgeven  29842  vtxdgoddnumeven  29843  redwlklem  29959  wlkdlem1  29970  pthdlem1  30055  crctcshwlkn0lem4  30102  wwlksnredwwlkn0  30185  wwlksnextproplem2  30199  clwwlkccatlem  30280  clwlkclwwlkfo  30300  clwwlkwwlksb  30345  clwwlkndivn  30371  eupth2lem3lem3  30521  eupth2lem3lem4  30522  eupth2lem3  30527  eupth2lems  30529  numclwwlk5  30679  numclwwlk6  30681  ex-ind-dvds  30752  nndiffz1  33071  fzo0opth  33088  ccatf1  33209  pfxlsw2ccat  33210  wrdt2ind  33213  gsummulsubdishift1  33328  gsumwrd2dccatlem  33337  cycpmfv1  33373  cycpmco2lem2  33387  cycpmco2lem3  33388  cycpmco2lem4  33389  cycpmco2lem5  33390  cycpmco2lem6  33391  cycpmco2  33393  cycpmrn  33403  cyc3genpm  33412  cycpmconjslem2  33415  cyc3conja  33417  archirng  33448  archirngz  33449  archiabllem1a  33451  gsumind  33607  elrspunidl  33679  ply1coedeg  33823  ply1degltel  33828  gsummoncoe1fz  33832  selvply1rhmlemb  33853  esplyfval2  33899  esplympl  33901  esplyfval3  33906  esplyindfv  33910  vietalem  33913  ply1degltdimlem  33956  fldextrspundgdvds  34015  algextdeglem8  34058  rtelextdg2  34061  constrext2chnlem  34084  cos9thpiminplylem2  34117  cos9thpiminplylem3  34118  cos9thpiminplylem6  34121  cos9thpiminply  34122  madjusmdetlem4  34164  zrhcntr  34313  qqhval2lem  34315  oddpwdc  34688  eulerpartlems  34694  eulerpartlemb  34702  sseqfv1  34723  sseqfn  34724  sseqmw  34725  sseqf  34726  sseqfv2  34728  sseqp1  34729  ccatmulgnn0dir  34876  signsplypnf  34881  signsply0  34882  signslema  34893  signstfvn  34900  signstfvp  34902  signstfvc  34905  fsum2dsub  34938  reprinfz1  34953  reprfi2  34954  hashrepr  34956  reprdifc  34958  breprexplema  34961  breprexplemc  34963  circlemeth  34971  circlevma  34973  circlemethhgt  34974  hgt750lema  34988  tgoldbachgtde  34991  lpadlem3  35012  revpfxsfxrev  35505  revwlk  35515  subfacval3  35579  bcprod  36128  bccolsum  36129  fwddifnp1  36555  knoppndvlem6  36994  knoppndvlem7  36995  knoppndvlem10  36998  knoppndvlem14  37002  knoppndvlem15  37003  knoppndvlem16  37004  knoppndvlem17  37005  knoppndvlem19  37007  knoppndvlem21  37009  dfgcd3  37855  poimirlem3  38161  poimirlem4  38162  poimirlem6  38164  poimirlem13  38171  poimirlem14  38172  poimirlem17  38175  poimirlem21  38179  poimirlem22  38180  poimirlem23  38181  poimirlem26  38184  poimirlem27  38185  poimirlem31  38189  geomcau  38297  bccl2d  42647  lcmineqlem12  42696  lcmineqlem17  42701  dvrelogpow2b  42724  aks4d1p1p2  42726  aks4d1p1p4  42727  aks4d1p1p6  42729  aks4d1p1p7  42730  aks4d1p1p5  42731  aks4d1p1  42732  aks4d1p3  42734  aks4d1p6  42737  aks4d1p8d2  42741  aks4d1p8d3  42742  aks4d1p8  42743  primrootscoprmpow  42755  primrootlekpowne0  42761  aks6d1c1  42772  aks6d1c2p2  42775  aks6d1c2lem4  42783  aks6d1c2  42786  aks6d1c5lem3  42793  aks6d1c5lem2  42794  2np3bcnp1  42800  sticksstones5  42806  sticksstones6  42807  sticksstones7  42808  sticksstones10  42811  sticksstones11  42812  sticksstones12a  42813  sticksstones12  42814  sticksstones22  42824  aks6d1c6lem3  42828  bcled  42834  bcle2d  42835  aks6d1c7lem1  42836  aks6d1c7lem2  42837  grpods  42850  unitscyglem2  42852  unitscyglem4  42854  aks5lem8  42857  sumcubes  42963  gcdle1d  42980  gcdle2d  42981  frlmvscadiccat  43169  fltdiv  43259  flt4lem4  43272  fltnltalem  43285  eldioph2lem1  43382  pellexlem5  43451  congrep  43591  jm2.18  43606  jm2.19lem1  43607  jm2.19lem2  43608  jm2.19  43611  jm2.22  43613  jm2.23  43614  jm2.20nn  43615  jm2.25  43617  jm2.26a  43618  jm2.26lem3  43619  jm2.26  43620  jm2.27a  43623  jm2.27b  43624  jm2.27c  43625  jm3.1  43638  expdiophlem1  43639  hbtlem5  43746  radcnvrat  44915  nzin  44919  bccbc  44946  binomcxplemnn0  44950  binomcxplemnotnn0  44957  fprodexp  46201  mccllem  46204  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  dvnxpaek  46547  dvnmul  46548  dvnprodlem1  46551  dvnprodlem2  46552  wallispilem1  46670  wallispilem5  46674  stirlinglem3  46681  stirlinglem5  46683  stirlinglem7  46685  stirlinglem8  46686  fourierdlem102  46813  fourierdlem114  46825  sqwvfoura  46833  elaa2lem  46838  etransclem10  46849  etransclem20  46859  etransclem21  46860  etransclem22  46861  etransclem23  46862  etransclem24  46863  etransclem27  46866  etransclem28  46867  etransclem35  46874  etransclem38  46877  etransclem44  46883  etransclem45  46884  etransclem46  46885  sge0ad2en  47036  chnsubseqwl  47486  chnsubseq  47487  fsummmodsnunz  48008  fmtnoge3  48170  fmtnof1  48175  fmtnorec1  48177  sqrtpwpw2p  48178  fmtnodvds  48184  goldbachthlem2  48186  fmtnoprmfac2lem1  48206  lighneallem3  48247  lighneallem4b  48249  lighneallem4  48250  ssnn0ssfz  49013  altgsumbcALT  49017  flnn0ohalf  49198  dig2nn1st  49269  0dig2nn0o  49277  aacllem  50474