Theorem nn0zd 9164

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 9065	. 2 |- NN0 C_ ZZ
2		nn0zd.1	. 2 |- ( ph -> A e. NN0 )
3	1, 2	sseldi 3090	1 |- ( ph -> A e. ZZ )

Syntax hints:   -> wi 4   e. wcel 1480   NN0cn0 8970   ZZcz 9047

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119  ax-sep 4041  ax-pow 4093  ax-pr 4126  ax-un 4350  ax-setind 4447  ax-cnex 7704  ax-resscn 7705  ax-1cn 7706  ax-1re 7707  ax-icn 7708  ax-addcl 7709  ax-addrcl 7710  ax-mulcl 7711  ax-addcom 7713  ax-addass 7715  ax-distr 7717  ax-i2m1 7718  ax-0lt1 7719  ax-0id 7721  ax-rnegex 7722  ax-cnre 7724  ax-pre-ltirr 7725  ax-pre-ltwlin 7726  ax-pre-lttrn 7727  ax-pre-ltadd 7729

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2000  df-mo 2001  df-clab 2124  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ne 2307  df-nel 2402  df-ral 2419  df-rex 2420  df-reu 2421  df-rab 2423  df-v 2683  df-sbc 2905  df-dif 3068  df-un 3070  df-in 3072  df-ss 3079  df-pw 3507  df-sn 3528  df-pr 3529  df-op 3531  df-uni 3732  df-int 3767  df-br 3925  df-opab 3985  df-id 4210  df-xp 4540  df-rel 4541  df-cnv 4542  df-co 4543  df-dm 4544  df-iota 5083  df-fun 5120  df-fv 5126  df-riota 5723  df-ov 5770  df-oprab 5771  df-mpo 5772  df-pnf 7795  df-mnf 7796  df-xr 7797  df-ltxr 7798  df-le 7799  df-sub 7928  df-neg 7929  df-inn 8714  df-n0 8971  df-z 9048

This theorem is referenced by:  nnzd  9165  fseq1p1m1  9867  difelfznle  9905  flltdivnn0lt  10070  zmodfz  10112  addmodid  10138  modaddmodup  10153  modaddmodlo  10154  modsumfzodifsn  10162  addmodlteq  10164  expnegzap  10320  expaddzaplem  10329  expaddzap  10330  expmulzap  10332  nn0opthd  10461  facdiv  10477  facwordi  10479  faclbnd  10480  facavg  10485  bcval  10488  bcval5  10502  bcpasc  10505  hashfiv01gt1  10521  isfinite4im  10532  fihashneq0  10534  fseq1hash  10540  fnfz0hash  10568  ffzo0hash  10570  zfz1isolemiso  10575  resqrexlemga  10788  zabscl  10851  fsum0diaglem  11202  modfsummodlemstep  11219  binomlem  11245  binom1p  11247  binom1dif  11249  arisum2  11261  geosergap  11268  geoserap  11269  pwm1geoserap1  11270  geolim2  11274  cvgratnnlemrate  11292  mertenslemi1  11297  mertenslem2  11298  mertensabs  11299  efcvgfsum  11362  efaddlem  11369  dvdsdc  11490  divalglemnn  11604  divalgmod  11613  zeqzmulgcd  11648  gcd0id  11656  gcdneg  11659  gcdaddm  11661  modgcd  11668  gcdmultipled  11670  bezoutlemnewy  11673  bezoutlemstep  11674  bezoutlemmain  11675  bezoutlemzz  11679  bezoutlemmo  11683  bezoutlemle  11685  bezoutlemsup  11686  dfgcd3  11687  dvdsgcdb  11690  gcdass  11692  mulgcd  11693  gcdzeq  11699  dvdsmulgcd  11702  bezoutr  11709  bezoutr1  11710  nn0seqcvgd  11711  algfx  11722  eucalgval2  11723  eucalginv  11726  eucalglt  11727  eucalg  11729  gcddvdslcm  11743  lcmneg  11744  lcmgcdlem  11747  lcmdvds  11749  lcmgcdeq  11753  lcmdvdsb  11754  lcmass  11755  mulgcddvds  11764  rpmulgcd2  11765  qredeu  11767  divgcdcoprm0  11771  divgcdcoprmex  11772  cncongr1  11773  cncongr2  11774  sqnprm  11805  rpexp  11820  sqpweven  11842  2sqpwodd  11843  divnumden  11863  phivalfi  11877  phicl2  11879  phiprmpw  11887  crth  11889  phimullem  11890  hashgcdeq  11893  ennnfoneleminc  11913  ennnfonelemrnh  11918  ennnfonelemim  11926  nninffeq  13205