Theorem nn0zd 9321

Description: A positive integer is an integer. (Contributed by Mario Carneiro, 28-May-2016.)

Hypothesis

Ref	Expression
nn0zd.1	|- ( ph -> A e. NN0 )

Assertion

Ref	Expression
nn0zd	|- ( ph -> A e. ZZ )

Proof of Theorem nn0zd

Step	Hyp	Ref	Expression
1		nn0ssz 9219	. 2 |- NN0 C_ ZZ
2		nn0zd.1	. 2 |- ( ph -> A e. NN0 )
3	1, 2	sselid 3145	1 |- ( ph -> A e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2141   NN0cn0 9124   ZZcz 9201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-setind 4519  ax-cnex 7854  ax-resscn 7855  ax-1cn 7856  ax-1re 7857  ax-icn 7858  ax-addcl 7859  ax-addrcl 7860  ax-mulcl 7861  ax-addcom 7863  ax-addass 7865  ax-distr 7867  ax-i2m1 7868  ax-0lt1 7869  ax-0id 7871  ax-rnegex 7872  ax-cnre 7874  ax-pre-ltirr 7875  ax-pre-ltwlin 7876  ax-pre-lttrn 7877  ax-pre-ltadd 7879

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-br 3988  df-opab 4049  df-id 4276  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-iota 5158  df-fun 5198  df-fv 5204  df-riota 5807  df-ov 5854  df-oprab 5855  df-mpo 5856  df-pnf 7945  df-mnf 7946  df-xr 7947  df-ltxr 7948  df-le 7949  df-sub 8081  df-neg 8082  df-inn 8868  df-n0 9125  df-z 9202

This theorem is referenced by:  nnzd  9322  xnn0dcle  9748  xnn0letri  9749  fseq1p1m1  10039  difelfznle  10080  flltdivnn0lt  10249  zmodfz  10291  addmodid  10317  modaddmodup  10332  modaddmodlo  10333  modsumfzodifsn  10341  addmodlteq  10343  expnegzap  10499  expaddzaplem  10508  expaddzap  10509  expmulzap  10511  nn0ltexp2  10633  nn0opthd  10645  facdiv  10661  facwordi  10663  faclbnd  10664  facavg  10669  bcval  10672  bcval5  10686  bcpasc  10689  hashfiv01gt1  10705  isfinite4im  10716  fihashneq0  10718  fseq1hash  10725  fnfz0hash  10756  ffzo0hash  10758  zfz1isolemiso  10763  resqrexlemga  10976  zabscl  11039  fsum0diaglem  11392  modfsummodlemstep  11409  binomlem  11435  binom1p  11437  binom1dif  11439  arisum2  11451  geosergap  11458  geoserap  11459  pwm1geoserap1  11460  geolim2  11464  cvgratnnlemrate  11482  mertenslemi1  11487  mertenslem2  11488  mertensabs  11489  efcvgfsum  11619  efaddlem  11626  dvdsdc  11749  divalglemnn  11866  divalgmod  11875  zeqzmulgcd  11914  gcd0id  11923  gcdneg  11926  gcdaddm  11928  modgcd  11935  gcdmultipled  11937  bezoutlemnewy  11940  bezoutlemstep  11941  bezoutlemmain  11942  bezoutlemzz  11946  bezoutlemmo  11950  bezoutlemle  11952  bezoutlemsup  11953  dfgcd3  11954  dvdsgcdb  11957  gcdass  11959  mulgcd  11960  gcdzeq  11966  dvdsmulgcd  11969  bezoutr  11976  bezoutr1  11977  nn0seqcvgd  11984  algfx  11995  eucalgval2  11996  eucalginv  11999  eucalglt  12000  eucalg  12002  gcddvdslcm  12016  lcmneg  12017  lcmgcdlem  12020  lcmdvds  12022  lcmgcdeq  12026  lcmdvdsb  12027  lcmass  12028  mulgcddvds  12037  rpmulgcd2  12038  qredeu  12040  divgcdcoprm0  12044  divgcdcoprmex  12045  cncongr1  12046  cncongr2  12047  sqnprm  12079  rpexp  12096  sqpweven  12118  2sqpwodd  12119  divnumden  12139  phivalfi  12155  phicl2  12157  phiprmpw  12165  crth  12167  phimullem  12168  eulerthlemfi  12171  eulerthlema  12173  hashgcdeq  12182  phisum  12183  odzdvds  12188  powm2modprm  12195  coprimeprodsq  12200  pcprendvds  12233  pcpremul  12236  pceu  12238  pcdiv  12245  pcqcl  12249  pcdvdsb  12262  pc2dvds  12272  pcprmpw2  12275  dvdsprmpweqle  12279  pcadd  12282  fldivp1  12289  pcfaclem  12290  pcfac  12291  pcbc  12292  pockthlem  12297  1arith  12308  mul4sqlem  12334  ennnfoneleminc  12355  ennnfonelemrnh  12360  ennnfonelemim  12368  lgsval  13660  lgsfvalg  13661  lgsfcl2  13662  lgsval2lem  13666  lgsmod  13682  lgsdir2  13689  lgsne0  13694  lgsprme0  13698  2sqlem8  13714  nninffeq  14015