Theorem nn0zd 12406

Description: A positive 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 12324	. 2 ⊢ ℕ0 ⊆ ℤ
2		nn0zd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0)
3	1, 2	sselid 3923	1 ⊢ (𝜑 → 𝐴 ∈ ℤ)

Syntax hints:   → wi 4   ∈ wcel 2109  ℕ₀cn0 12216  ℤcz 12302

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7579  ax-1cn 10913  ax-icn 10914  ax-addcl 10915  ax-addrcl 10916  ax-mulcl 10917  ax-mulrcl 10918  ax-i2m1 10923  ax-1ne0 10924  ax-rnegex 10926  ax-rrecex 10927  ax-cnre 10928

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-reu 3072  df-rab 3074  df-v 3432  df-sbc 3720  df-csb 3837  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-pss 3910  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4845  df-iun 4931  df-br 5079  df-opab 5141  df-mpt 5162  df-tr 5196  df-id 5488  df-eprel 5494  df-po 5502  df-so 5503  df-fr 5543  df-we 5545  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-rn 5599  df-res 5600  df-ima 5601  df-pred 6199  df-ord 6266  df-on 6267  df-lim 6268  df-suc 6269  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-f1 6435  df-fo 6436  df-f1o 6437  df-fv 6438  df-ov 7271  df-om 7701  df-2nd 7818  df-frecs 8081  df-wrecs 8112  df-recs 8186  df-rdg 8225  df-neg 11191  df-nn 11957  df-n0 12217  df-z 12303

This theorem is referenced by:  nnzd  12407  eluzmn  12571  difelfznle  13352  zmodfz  13594  expnegz  13798  expaddzlem  13807  expaddz  13808  expmulz  13810  faclbnd  13985  bcpasc  14016  hashf1  14152  fz1isolem  14156  hashge2el2dif  14175  hashtpg  14180  wrdffz  14219  ffz0iswrd  14225  wrdsymb0  14233  wrdlenge1n0  14234  ccatcl  14258  ccatval3  14265  ccatsymb  14268  ccatval21sw  14271  ccatass  14274  ccatrn  14275  lswccatn0lsw  14277  ccats1val2  14315  swrdnd  14348  swrdccat2  14363  pfxtrcfv0  14388  pfxtrcfvl  14391  pfxccat1  14396  swrdccatin2  14423  pfxccatin12  14427  pfxccatpfx2  14431  pfxccat3a  14432  splfv2a  14450  splval2  14451  revcl  14455  revccat  14460  revrev  14461  cshwmodn  14489  cshwsublen  14490  cshwn  14491  cshwidxmod  14497  2cshwid  14508  3cshw  14512  cshweqdif2  14513  revco  14528  ccatco  14529  ccat2s1fvwALT  14650  ccat2s1fvwALTOLD  14651  ofccat  14661  zabscl  15006  absrdbnd  15034  iseraltlem3  15376  fsum0diaglem  15469  modfsummods  15486  binomlem  15522  binom1p  15524  incexc2  15531  climcndslem1  15542  geoser  15560  pwm1geoser  15562  geolim2  15564  mertenslem1  15577  mertenslem2  15578  mertens  15579  binomfallfaclem2  15731  binomrisefac  15733  fallfacval4  15734  bpolydiflem  15745  ruclem10  15929  sumodd  16078  divalglem9  16091  divalgmod  16096  bitsfzolem  16122  bitsfzo  16123  bitsmod  16124  bitsfi  16125  bitsinv1lem  16129  sadcaddlem  16145  sadadd3  16149  sadaddlem  16154  sadadd  16155  sadasslem  16158  sadass  16159  sadeq  16160  bitsres  16161  bitsuz  16162  bitsshft  16163  smuval2  16170  smupvallem  16171  smupval  16176  smueqlem  16178  smumullem  16180  smumul  16181  gcdcllem1  16187  zeqzmulgcd  16198  gcd0id  16207  gcdneg  16210  modgcd  16221  gcdmultipled  16223  bezoutlem4  16231  dvdsgcdb  16234  gcdass  16236  mulgcd  16237  gcdzeq  16243  dvdsmulgcd  16246  bezoutr  16254  bezoutr1  16255  nn0seqcvgd  16256  algfx  16266  eucalginv  16270  eucalg  16273  gcddvdslcm  16288  lcmneg  16289  lcmgcdlem  16292  lcmdvds  16294  lcmgcdeq  16298  lcmdvdsb  16299  lcmass  16300  lcmftp  16322  lcmfunsnlem1  16323  lcmfunsnlem2lem1  16324  lcmfunsnlem2lem2  16325  lcmfunsnlem2  16326  lcmfdvdsb  16329  lcmfun  16331  lcmfass  16332  mulgcddvds  16341  rpmulgcd2  16342  qredeu  16344  divgcdcoprm0  16351  sqnprm  16388  divnumden  16433  powm2modprm  16485  coprimeprodsq  16490  iserodd  16517  pclem  16520  pcpre1  16524  pcpremul  16525  pcqcl  16538  pcdvdsb  16551  pcidlem  16554  pc2dvds  16561  pcprmpw2  16564  dvdsprmpweqle  16568  pcadd  16571  pcfac  16581  pcbc  16582  pockthlem  16587  prmreclem2  16599  prmreclem3  16600  mul4sqlem  16635  4sqlem11  16637  4sqlem12  16638  4sqlem14  16640  vdwapun  16656  prmgaplcmlem1  16733  lagsubg  18799  psgnuni  19088  psgnran  19104  odmodnn0  19129  mndodconglem  19130  mndodcong  19131  odmulg2  19143  odmulg  19144  odmulgeq  19145  odbezout  19146  odinv  19149  odf1  19150  gexod  19172  gexdvds3  19176  sylow1lem1  19184  sylow1lem3  19186  pgpfi  19191  pgpssslw  19200  sylow2alem2  19204  sylow2blem3  19208  fislw  19211  sylow3lem4  19216  sylow3lem6  19218  efginvrel2  19314  efgredlemf  19328  efgredlemd  19331  efgredlemc  19332  efgredlem  19334  efgcpbllemb  19342  odadd1  19430  odadd2  19431  gexexlem  19434  gexex  19435  torsubg  19436  lt6abl  19477  gsummulg  19524  ablfacrplem  19649  ablfacrp  19650  ablfacrp2  19651  ablfac1b  19654  ablfac1c  19655  ablfac1eulem  19656  ablfac1eu  19657  pgpfac1lem2  19659  pgpfaclem1  19665  ablfaclem3  19671  srgbinomlem3  19759  srgbinomlem4  19760  chrid  20712  znunit  20752  psgnghm  20766  psrbaglefi  21116  psrbaglefiOLD  21117  chfacfscmulfsupp  21989  chfacfpmmulfsupp  21993  cpmadugsumlemF  22006  dyadss  24739  dyaddisjlem  24740  ply1divex  25282  ply1termlem  25345  plyeq0lem  25352  plyaddlem1  25355  plymullem1  25356  coeeulem  25366  coeidlem  25379  coeeq2  25384  coemulhi  25396  dvply1  25425  dvply2g  25426  plydivex  25438  elqaalem2  25461  aareccl  25467  aannenlem1  25469  aalioulem1  25473  taylplem1  25503  taylplem2  25504  taylpfval  25505  dvtaylp  25510  taylthlem2  25514  dvradcnv  25561  abelthlem7  25578  cxpeq  25891  birthdaylem2  26083  ftalem1  26203  basellem3  26213  isppw2  26245  isnsqf  26265  mule1  26278  ppinncl  26304  musum  26321  chtublem  26340  pclogsum  26344  vmasum  26345  dchrabs  26389  bcmax  26407  bposlem1  26413  bposlem6  26418  lgsval2lem  26436  lgsmod  26452  lgsne0  26464  gausslemma2dlem0h  26492  gausslemma2dlem0i  26493  gausslemma2dlem2  26496  gausslemma2dlem6  26501  gausslemma2d  26503  lgseisenlem1  26504  lgseisenlem2  26505  lgseisenlem3  26506  lgseisenlem4  26507  lgsquadlem1  26509  m1lgs  26517  2lgslem1a  26520  2lgslem3a  26525  2lgslem3b  26526  2lgslem3c  26527  2lgslem3d  26528  2lgslem3d1  26532  2lgsoddprmlem2  26538  2sqlem8  26555  2sqcoprm  26564  2sqmod  26565  chebbnd1lem1  26598  dchrisumlem1  26618  dchrisum0flblem1  26637  selberg2lem  26679  ostth2lem2  26763  ostth2lem3  26764  finsumvtxdg2sstep  27897  finsumvtxdgeven  27900  vtxdgoddnumeven  27901  redwlklem  28019  wlkdlem1  28030  pthdlem1  28113  crctcshwlkn0lem4  28157  wwlksnredwwlkn0  28240  wwlksnextproplem2  28254  clwwlkccatlem  28332  clwlkclwwlkfo  28352  clwwlkwwlksb  28397  clwwlkndivn  28423  eupth2lem3lem3  28573  eupth2lem3lem4  28574  eupth2lem3  28579  eupth2lems  28581  numclwwlk5  28731  numclwwlk6  28733  ex-ind-dvds  28804  nndiffz1  31086  prmdvdsbc  31109  ccatf1  31202  pfxlsw2ccat  31203  wrdt2ind  31204  cycpmfv1  31359  cycpmco2lem2  31373  cycpmco2lem3  31374  cycpmco2lem4  31375  cycpmco2lem5  31376  cycpmco2lem6  31377  cycpmco2  31379  cycpmrn  31389  cyc3genpm  31398  cycpmconjslem2  31401  cyc3conja  31403  archirng  31421  archirngz  31422  archiabllem1a  31424  freshmansdream  31463  elrspunidl  31585  asclmulg  31645  madjusmdetlem4  31759  qqhval2lem  31910  oddpwdc  32300  eulerpartlems  32306  eulerpartlemb  32314  sseqfv1  32335  sseqfn  32336  sseqmw  32337  sseqf  32338  sseqfv2  32340  sseqp1  32341  ccatmulgnn0dir  32500  signsplypnf  32508  signsply0  32509  signslema  32520  signstfvn  32527  signstfvp  32529  signstfvc  32532  fsum2dsub  32566  reprinfz1  32581  reprfi2  32582  hashrepr  32584  reprdifc  32586  breprexplema  32589  breprexplemc  32591  circlemeth  32599  circlevma  32601  circlemethhgt  32602  hgt750lema  32616  tgoldbachgtde  32619  lpadlem3  32637  revpfxsfxrev  33056  revwlk  33065  subfacval3  33130  bcprod  33683  bccolsum  33684  fwddifnp1  34446  knoppndvlem6  34676  knoppndvlem7  34677  knoppndvlem10  34680  knoppndvlem14  34684  knoppndvlem15  34685  knoppndvlem16  34686  knoppndvlem17  34687  knoppndvlem19  34689  knoppndvlem21  34691  dfgcd3  35474  poimirlem3  35759  poimirlem4  35760  poimirlem6  35762  poimirlem13  35769  poimirlem14  35770  poimirlem17  35773  poimirlem21  35777  poimirlem22  35778  poimirlem23  35779  poimirlem26  35782  poimirlem27  35783  poimirlem31  35787  geomcau  35896  bccl2d  39980  lcmineqlem12  40028  lcmineqlem17  40033  dvrelogpow2b  40056  aks4d1p1p2  40058  aks4d1p1p4  40059  aks4d1p1p6  40061  aks4d1p1p7  40062  aks4d1p1p5  40063  aks4d1p1  40064  aks4d1p3  40066  aks4d1p6  40069  aks4d1p8d2  40073  aks4d1p8d3  40074  aks4d1p8  40075  2np3bcnp1  40080  sticksstones5  40086  sticksstones6  40087  sticksstones7  40088  sticksstones10  40091  sticksstones11  40092  sticksstones12a  40093  sticksstones12  40094  sticksstones22  40104  prodsplit  40141  frlmvscadiccat  40217  gcdle1d  40310  gcdle2d  40311  fltdiv  40453  flt4lem4  40466  fltnltalem  40479  eldioph2lem1  40562  pellexlem5  40635  congrep  40775  jm2.18  40790  jm2.19lem1  40791  jm2.19lem2  40792  jm2.19  40795  jm2.22  40797  jm2.23  40798  jm2.20nn  40799  jm2.25  40801  jm2.26a  40802  jm2.26lem3  40803  jm2.26  40804  jm2.27a  40807  jm2.27b  40808  jm2.27c  40809  jm3.1  40822  expdiophlem1  40823  hbtlem5  40933  radcnvrat  41885  nzin  41889  bccbc  41916  binomcxplemnn0  41920  binomcxplemnotnn0  41927  fprodexp  43089  mccllem  43092  ioodvbdlimc1lem2  43427  ioodvbdlimc2lem  43429  dvnxpaek  43437  dvnmul  43438  dvnprodlem1  43441  dvnprodlem2  43442  wallispilem1  43560  wallispilem5  43564  stirlinglem3  43571  stirlinglem5  43573  stirlinglem7  43575  stirlinglem8  43576  fourierdlem102  43703  fourierdlem114  43715  sqwvfoura  43723  elaa2lem  43728  etransclem10  43739  etransclem20  43749  etransclem21  43750  etransclem22  43751  etransclem23  43752  etransclem24  43753  etransclem27  43756  etransclem28  43757  etransclem35  43764  etransclem38  43767  etransclem44  43773  etransclem45  43774  etransclem46  43775  sge0ad2en  43923  fsummmodsnunz  44779  fmtnoge3  44934  fmtnof1  44939  fmtnorec1  44941  sqrtpwpw2p  44942  fmtnodvds  44948  goldbachthlem2  44950  fmtnoprmfac2lem1  44970  lighneallem3  45011  lighneallem4b  45013  lighneallem4  45014  ssnn0ssfz  45637  altgsumbcALT  45641  flnn0ohalf  45832  dig2nn1st  45903  0dig2nn0o  45911  aacllem  46457