Theorem nn0zd 9644

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

Syntax hints:   → wi 4   ∈ wcel 2202  ℕ₀cn0 9444  ℤcz 9523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641  ax-cnex 8166  ax-resscn 8167  ax-1cn 8168  ax-1re 8169  ax-icn 8170  ax-addcl 8171  ax-addrcl 8172  ax-mulcl 8173  ax-addcom 8175  ax-addass 8177  ax-distr 8179  ax-i2m1 8180  ax-0lt1 8181  ax-0id 8183  ax-rnegex 8184  ax-cnre 8186  ax-pre-ltirr 8187  ax-pre-ltwlin 8188  ax-pre-lttrn 8189  ax-pre-ltadd 8191

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-nel 2499  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fv 5341  df-riota 5981  df-ov 6031  df-oprab 6032  df-mpo 6033  df-pnf 8258  df-mnf 8259  df-xr 8260  df-ltxr 8261  df-le 8262  df-sub 8394  df-neg 8395  df-inn 9186  df-n0 9445  df-z 9524

This theorem is referenced by:  nnzd  9645  eluzmn  9806  xnn0dcle  10081  xnn0letri  10082  fseq1p1m1  10374  difelfznle  10415  flltdivnn0lt  10610  zmodfz  10654  addmodid  10680  modaddmodup  10695  modaddmodlo  10696  modsumfzodifsn  10704  addmodlteq  10706  expnegzap  10881  expaddzaplem  10890  expaddzap  10891  expmulzap  10893  nn0ltexp2  11017  nn0opthd  11030  facdiv  11046  facwordi  11048  faclbnd  11049  facavg  11054  bcval  11057  bcval5  11071  bcpasc  11074  hashfiv01gt1  11090  isfinite4im  11100  fihashneq0  11102  fseq1hash  11110  fnfz0hash  11142  ffzo0hash  11144  zfz1isolemiso  11149  wrdfin  11181  wrdffz  11183  wrdsymb0  11195  wrdlenge1n0  11196  lswwrd  11209  ccatfvalfi  11218  ccatcl  11219  ccatlen  11221  ccatval2  11224  ccatval3  11225  ccatvalfn  11227  ccatsymb  11228  ccatval21sw  11231  ccatass  11234  ccatrn  11235  lswccatn0lsw  11237  ccatalpha  11239  ccats1val2  11266  ccat1st1st  11267  fzowrddc  11277  swrdnd  11289  swrdspsleq  11297  swrdccat2  11301  pfxval  11304  pfxwrdsymbg  11320  pfxtrcfv0  11324  pfxtrcfvl  11327  ccatpfx  11331  pfxccat1  11332  lenrevpfxcctswrd  11342  wrdind  11352  wrd2ind  11353  swrdccatin1  11355  swrdccatin2  11359  pfxccatin12  11363  swrdccat  11365  pfxccatpfx2  11367  pfxccat3a  11368  swrdccat3blem  11369  swrdccat3b  11370  resqrexlemga  11646  zabscl  11709  fsum0diaglem  12064  modfsummodlemstep  12081  binomlem  12107  binom1p  12109  binom1dif  12111  arisum2  12123  geosergap  12130  geoserap  12131  pwm1geoserap1  12132  geolim2  12136  cvgratnnlemrate  12154  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  efcvgfsum  12291  efaddlem  12298  dvdsdc  12422  divalglemnn  12542  divalgmod  12551  bitsfzolem  12578  bitsfzo  12579  bitsmod  12580  bitsfi  12581  bitsinv1lem  12585  bitsinv1  12586  zeqzmulgcd  12604  gcd0id  12613  gcdneg  12616  gcdaddm  12618  modgcd  12625  gcdmultipled  12627  bezoutlemnewy  12630  bezoutlemstep  12631  bezoutlemmain  12632  bezoutlemzz  12636  bezoutlemmo  12640  bezoutlemle  12642  bezoutlemsup  12643  dfgcd3  12644  dvdsgcdb  12647  gcdass  12649  mulgcd  12650  gcdzeq  12656  dvdsmulgcd  12659  bezoutr  12666  bezoutr1  12667  nn0seqcvgd  12676  algfx  12687  eucalgval2  12688  eucalginv  12691  eucalglt  12692  eucalg  12694  gcddvdslcm  12708  lcmneg  12709  lcmgcdlem  12712  lcmdvds  12714  lcmgcdeq  12718  lcmdvdsb  12719  lcmass  12720  mulgcddvds  12729  rpmulgcd2  12730  qredeu  12732  divgcdcoprm0  12736  divgcdcoprmex  12737  cncongr1  12738  cncongr2  12739  sqnprm  12771  rpexp  12788  sqpweven  12810  2sqpwodd  12811  divnumden  12831  phivalfi  12847  phicl2  12849  phiprmpw  12857  crth  12859  phimullem  12860  eulerthlemfi  12863  eulerthlema  12865  hashgcdeq  12875  phisum  12876  odzdvds  12881  powm2modprm  12888  coprimeprodsq  12893  pcprendvds  12926  pcpremul  12929  pceu  12931  pcdiv  12938  pcqcl  12942  pcdvdsb  12956  pc2dvds  12966  pcprmpw2  12969  dvdsprmpweqle  12973  pcadd  12976  fldivp1  12984  pcfaclem  12985  pcfac  12986  pcbc  12987  pockthlem  12992  1arith  13003  mul4sqlem  13029  4sqlemafi  13031  4sqlemffi  13032  4sqleminfi  13033  4sqexercise1  13034  4sqlemsdc  13036  4sqlem11  13037  4sqlem12  13038  4sqlem14  13040  ennnfoneleminc  13095  ennnfonelemrnh  13100  ennnfonelemim  13108  znunit  14738  psrbaglesuppg  14751  psrbagfi  14753  psrbaglecl  14754  psrbagcon  14755  psrbagconf1o  14757  psr1clfi  14772  elply2  15529  plyf  15531  elplyd  15535  ply1termlem  15536  ply1term  15537  plyaddlem1  15541  plymullem1  15542  plyaddlem  15543  plycoeid3  15551  plycolemc  15552  plycjlemc  15554  plycn  15556  plyrecj  15557  dvply1  15559  dvply2g  15560  wilthlem1  15777  sgmppw  15789  lgsval  15806  lgsfvalg  15807  lgsfcl2  15808  lgsval2lem  15812  lgsmod  15828  lgsdir2  15835  lgsne0  15840  lgsprme0  15844  gausslemma2dlem0h  15858  gausslemma2dlem0i  15859  gausslemma2dlem2  15864  gausslemma2dlem6  15869  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem2  15880  m1lgs  15887  2lgslem1a  15890  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgslem3d1  15902  2lgs  15906  2lgsoddprmlem2  15908  2lgsoddprm  15915  2sqlem8  15925  vdegp1bid  16239  wksfval  16246  wlkex  16249  iswlkg  16253  clwwlkccatlem  16324  umgrclwwlkge2  16326  clwwlknonex2lem2  16362  eupthfi  16375  eupth2lem3lem3fi  16394  eupth2lem3lem4fi  16397  eupth2lem3fi  16400  eupth2lemsfi  16402  konigsberglem5  16416  nninffeq  16729  gfsumval  16792  gsumgfsum1  16793