Theorem nn0zd 12073

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

Syntax hints:   → wi 4   ∈ wcel 2111  ℕ₀cn0 11885  ℤcz 11969

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-i2m1 10594  ax-1ne0 10595  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-neg 10862  df-nn 11626  df-n0 11886  df-z 11970

This theorem is referenced by:  nnzd  12074  eluzmn  12238  difelfznle  13016  zmodfz  13256  expnegz  13459  expaddzlem  13468  expaddz  13469  expmulz  13471  faclbnd  13646  bcpasc  13677  hashf1  13811  fz1isolem  13815  hashge2el2dif  13834  hashtpg  13839  wrdffz  13878  ffz0iswrd  13884  wrdsymb0  13892  wrdlenge1n0  13893  ccatcl  13917  ccatval3  13924  ccatsymb  13927  ccatval21sw  13930  ccatass  13933  ccatrn  13934  lswccatn0lsw  13936  ccats1val2  13974  swrdnd  14007  swrdccat2  14022  pfxtrcfv0  14047  pfxtrcfvl  14050  pfxccat1  14055  swrdccatin2  14082  pfxccatin12  14086  pfxccatpfx2  14090  pfxccat3a  14091  splfv2a  14109  splval2  14110  revcl  14114  revccat  14119  revrev  14120  cshwmodn  14148  cshwsublen  14149  cshwn  14150  cshwidxmod  14156  2cshwid  14167  3cshw  14171  cshweqdif2  14172  revco  14187  ccatco  14188  ccat2s1fvwALT  14309  ccat2s1fvwALTOLD  14310  ofccat  14320  zabscl  14665  absrdbnd  14693  iseraltlem3  15032  fsum0diaglem  15123  modfsummods  15140  binomlem  15176  binom1p  15178  incexc2  15185  climcndslem1  15196  geoser  15214  pwm1geoser  15216  pwm1geoserOLD  15217  geolim2  15219  mertenslem1  15232  mertenslem2  15233  mertens  15234  binomfallfaclem2  15386  binomrisefac  15388  fallfacval4  15389  bpolydiflem  15400  ruclem10  15584  sumodd  15729  divalglem9  15742  divalgmod  15747  bitsfzolem  15773  bitsfzo  15774  bitsmod  15775  bitsfi  15776  bitsinv1lem  15780  sadcaddlem  15796  sadadd3  15800  sadaddlem  15805  sadadd  15806  sadasslem  15809  sadass  15810  sadeq  15811  bitsres  15812  bitsuz  15813  bitsshft  15814  smuval2  15821  smupvallem  15822  smupval  15827  smueqlem  15829  smumullem  15831  smumul  15832  gcdcllem1  15838  zeqzmulgcd  15849  gcd0id  15857  gcdneg  15860  modgcd  15870  gcdmultipled  15872  bezoutlem4  15880  dvdsgcdb  15883  gcdass  15885  mulgcd  15886  gcdzeq  15892  dvdsmulgcd  15895  bezoutr  15902  bezoutr1  15903  nn0seqcvgd  15904  algfx  15914  eucalginv  15918  eucalg  15921  gcddvdslcm  15936  lcmneg  15937  lcmgcdlem  15940  lcmdvds  15942  lcmgcdeq  15946  lcmdvdsb  15947  lcmass  15948  lcmftp  15970  lcmfunsnlem1  15971  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  lcmfunsnlem2  15974  lcmfdvdsb  15977  lcmfun  15979  lcmfass  15980  mulgcddvds  15989  rpmulgcd2  15990  qredeu  15992  divgcdcoprm0  15999  sqnprm  16036  divnumden  16078  powm2modprm  16130  coprimeprodsq  16135  iserodd  16162  pclem  16165  pcpre1  16169  pcpremul  16170  pcqcl  16183  pcdvdsb  16195  pcidlem  16198  pc2dvds  16205  pcprmpw2  16208  dvdsprmpweqle  16212  pcadd  16215  pcfac  16225  pcbc  16226  pockthlem  16231  prmreclem2  16243  prmreclem3  16244  mul4sqlem  16279  4sqlem11  16281  4sqlem12  16282  4sqlem14  16284  vdwapun  16300  prmgaplcmlem1  16377  lagsubg  18334  psgnuni  18619  psgnran  18635  odmodnn0  18660  mndodconglem  18661  mndodcong  18662  odmulg2  18674  odmulg  18675  odmulgeq  18676  odbezout  18677  odinv  18680  odf1  18681  gexod  18703  gexdvds3  18707  sylow1lem1  18715  sylow1lem3  18717  pgpfi  18722  pgpssslw  18731  sylow2alem2  18735  sylow2blem3  18739  fislw  18742  sylow3lem4  18747  sylow3lem6  18749  efginvrel2  18845  efgredlemf  18859  efgredlemd  18862  efgredlemc  18863  efgredlem  18865  efgcpbllemb  18873  odadd1  18961  odadd2  18962  gexexlem  18965  gexex  18966  torsubg  18967  lt6abl  19008  gsummulg  19055  ablfacrplem  19180  ablfacrp  19181  ablfacrp2  19182  ablfac1b  19185  ablfac1c  19186  ablfac1eulem  19187  ablfac1eu  19188  pgpfac1lem2  19190  pgpfaclem1  19196  ablfaclem3  19202  srgbinomlem3  19285  srgbinomlem4  19286  chrid  20219  znunit  20255  psgnghm  20269  psrbaglefi  20610  chfacfscmulfsupp  21464  chfacfpmmulfsupp  21468  cpmadugsumlemF  21481  dyadss  24198  dyaddisjlem  24199  ply1divex  24737  ply1termlem  24800  plyeq0lem  24807  plyaddlem1  24810  plymullem1  24811  coeeulem  24821  coeidlem  24834  coeeq2  24839  coemulhi  24851  dvply1  24880  dvply2g  24881  plydivex  24893  elqaalem2  24916  aareccl  24922  aannenlem1  24924  aalioulem1  24928  taylplem1  24958  taylplem2  24959  taylpfval  24960  dvtaylp  24965  taylthlem2  24969  dvradcnv  25016  abelthlem7  25033  cxpeq  25346  birthdaylem2  25538  ftalem1  25658  basellem3  25668  isppw2  25700  isnsqf  25720  mule1  25733  ppinncl  25759  musum  25776  chtublem  25795  pclogsum  25799  vmasum  25800  dchrabs  25844  bcmax  25862  bposlem1  25868  bposlem6  25873  lgsval2lem  25891  lgsmod  25907  lgsne0  25919  gausslemma2dlem0h  25947  gausslemma2dlem0i  25948  gausslemma2dlem2  25951  gausslemma2dlem6  25956  gausslemma2d  25958  lgseisenlem1  25959  lgseisenlem2  25960  lgseisenlem3  25961  lgseisenlem4  25962  lgsquadlem1  25964  m1lgs  25972  2lgslem1a  25975  2lgslem3a  25980  2lgslem3b  25981  2lgslem3c  25982  2lgslem3d  25983  2lgslem3d1  25987  2lgsoddprmlem2  25993  2sqlem8  26010  2sqcoprm  26019  2sqmod  26020  chebbnd1lem1  26053  dchrisumlem1  26073  dchrisum0flblem1  26092  selberg2lem  26134  ostth2lem2  26218  ostth2lem3  26219  finsumvtxdg2sstep  27339  finsumvtxdgeven  27342  vtxdgoddnumeven  27343  redwlklem  27461  wlkdlem1  27472  pthdlem1  27555  crctcshwlkn0lem4  27599  wwlksnredwwlkn0  27682  wwlksnextproplem2  27696  clwwlkccatlem  27774  clwlkclwwlkfo  27794  clwwlkwwlksb  27839  clwwlkndivn  27865  eupth2lem3lem3  28015  eupth2lem3lem4  28016  eupth2lem3  28021  eupth2lems  28023  numclwwlk5  28173  numclwwlk6  28175  ex-ind-dvds  28246  nndiffz1  30535  prmdvdsbc  30558  ccatf1  30651  pfxlsw2ccat  30652  wrdt2ind  30653  cycpmfv1  30805  cycpmco2lem2  30819  cycpmco2lem3  30820  cycpmco2lem4  30821  cycpmco2lem5  30822  cycpmco2lem6  30823  cycpmco2lem7  30824  cycpmco2  30825  cycpmrn  30835  cyc3genpm  30844  cycpmconjslem2  30847  cyc3conja  30849  archirng  30867  archirngz  30868  archiabllem1a  30870  freshmansdream  30909  elrspunidl  31014  madjusmdetlem4  31183  qqhval2lem  31332  oddpwdc  31722  eulerpartlems  31728  eulerpartlemb  31736  sseqfv1  31757  sseqfn  31758  sseqmw  31759  sseqf  31760  sseqfv2  31762  sseqp1  31763  ccatmulgnn0dir  31922  signsplypnf  31930  signsply0  31931  signslema  31942  signstfvn  31949  signstfvp  31951  signstfvc  31954  fsum2dsub  31988  reprinfz1  32003  reprfi2  32004  hashrepr  32006  reprdifc  32008  breprexplema  32011  breprexplemc  32013  circlemeth  32021  circlevma  32023  circlemethhgt  32024  hgt750lema  32038  tgoldbachgtde  32041  lpadlem3  32059  revpfxsfxrev  32475  revwlk  32484  subfacval3  32549  bcprod  33083  bccolsum  33084  fwddifnp1  33739  knoppndvlem6  33969  knoppndvlem7  33970  knoppndvlem10  33973  knoppndvlem14  33977  knoppndvlem15  33978  knoppndvlem16  33979  knoppndvlem17  33980  knoppndvlem19  33982  knoppndvlem21  33984  dfgcd3  34738  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem13  35070  poimirlem14  35071  poimirlem17  35074  poimirlem21  35078  poimirlem22  35079  poimirlem23  35080  poimirlem24  35081  poimirlem26  35083  poimirlem27  35084  poimirlem31  35088  geomcau  35197  bccl2d  39279  lcmineqlem12  39328  lcmineqlem17  39333  3lexlogpow5ineq2  39342  2np3bcnp1  39348  prodsplit  39386  frlmvscadiccat  39440  fltnltalem  39618  eldioph2lem1  39701  pellexlem5  39774  congrep  39914  jm2.18  39929  jm2.19lem1  39930  jm2.19lem2  39931  jm2.19  39934  jm2.22  39936  jm2.23  39937  jm2.20nn  39938  jm2.25  39940  jm2.26a  39941  jm2.26lem3  39942  jm2.26  39943  jm2.27a  39946  jm2.27b  39947  jm2.27c  39948  jm3.1  39961  expdiophlem1  39962  hbtlem5  40072  radcnvrat  41018  nzin  41022  bccbc  41049  binomcxplemnn0  41053  binomcxplemnotnn0  41060  fprodexp  42236  mccllem  42239  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnxpaek  42584  dvnmul  42585  dvnprodlem1  42588  dvnprodlem2  42589  wallispilem1  42707  wallispilem5  42711  stirlinglem3  42718  stirlinglem5  42720  stirlinglem7  42722  stirlinglem8  42723  fourierdlem102  42850  fourierdlem114  42862  sqwvfoura  42870  elaa2lem  42875  etransclem10  42886  etransclem20  42896  etransclem21  42897  etransclem22  42898  etransclem23  42899  etransclem24  42900  etransclem27  42903  etransclem28  42904  etransclem35  42911  etransclem38  42914  etransclem44  42920  etransclem45  42921  etransclem46  42922  sge0ad2en  43070  fsummmodsnunz  43892  fmtnoge3  44047  fmtnof1  44052  fmtnorec1  44054  sqrtpwpw2p  44055  fmtnodvds  44061  goldbachthlem2  44063  fmtnoprmfac2lem1  44083  lighneallem3  44125  lighneallem4b  44127  lighneallem4  44128  ssnn0ssfz  44751  altgsumbcALT  44755  flnn0ohalf  44948  dig2nn1st  45019  0dig2nn0o  45027  aacllem  45329