Theorem nn0zd 9195

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

Syntax hints:   -> wi 4   e. wcel 1481   NN0cn0 9001   ZZcz 9078

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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-sep 4054  ax-pow 4106  ax-pr 4139  ax-un 4363  ax-setind 4460  ax-cnex 7735  ax-resscn 7736  ax-1cn 7737  ax-1re 7738  ax-icn 7739  ax-addcl 7740  ax-addrcl 7741  ax-mulcl 7742  ax-addcom 7744  ax-addass 7746  ax-distr 7748  ax-i2m1 7749  ax-0lt1 7750  ax-0id 7752  ax-rnegex 7753  ax-cnre 7755  ax-pre-ltirr 7756  ax-pre-ltwlin 7757  ax-pre-lttrn 7758  ax-pre-ltadd 7760

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2691  df-sbc 2914  df-dif 3078  df-un 3080  df-in 3082  df-ss 3089  df-pw 3517  df-sn 3538  df-pr 3539  df-op 3541  df-uni 3745  df-int 3780  df-br 3938  df-opab 3998  df-id 4223  df-xp 4553  df-rel 4554  df-cnv 4555  df-co 4556  df-dm 4557  df-iota 5096  df-fun 5133  df-fv 5139  df-riota 5738  df-ov 5785  df-oprab 5786  df-mpo 5787  df-pnf 7826  df-mnf 7827  df-xr 7828  df-ltxr 7829  df-le 7830  df-sub 7959  df-neg 7960  df-inn 8745  df-n0 9002  df-z 9079

This theorem is referenced by:  nnzd  9196  fseq1p1m1  9905  difelfznle  9943  flltdivnn0lt  10108  zmodfz  10150  addmodid  10176  modaddmodup  10191  modaddmodlo  10192  modsumfzodifsn  10200  addmodlteq  10202  expnegzap  10358  expaddzaplem  10367  expaddzap  10368  expmulzap  10370  nn0opthd  10500  facdiv  10516  facwordi  10518  faclbnd  10519  facavg  10524  bcval  10527  bcval5  10541  bcpasc  10544  hashfiv01gt1  10560  isfinite4im  10571  fihashneq0  10573  fseq1hash  10579  fnfz0hash  10607  ffzo0hash  10609  zfz1isolemiso  10614  resqrexlemga  10827  zabscl  10890  fsum0diaglem  11241  modfsummodlemstep  11258  binomlem  11284  binom1p  11286  binom1dif  11288  arisum2  11300  geosergap  11307  geoserap  11308  pwm1geoserap1  11309  geolim2  11313  cvgratnnlemrate  11331  mertenslemi1  11336  mertenslem2  11337  mertensabs  11338  efcvgfsum  11410  efaddlem  11417  dvdsdc  11537  divalglemnn  11651  divalgmod  11660  zeqzmulgcd  11695  gcd0id  11703  gcdneg  11706  gcdaddm  11708  modgcd  11715  gcdmultipled  11717  bezoutlemnewy  11720  bezoutlemstep  11721  bezoutlemmain  11722  bezoutlemzz  11726  bezoutlemmo  11730  bezoutlemle  11732  bezoutlemsup  11733  dfgcd3  11734  dvdsgcdb  11737  gcdass  11739  mulgcd  11740  gcdzeq  11746  dvdsmulgcd  11749  bezoutr  11756  bezoutr1  11757  nn0seqcvgd  11758  algfx  11769  eucalgval2  11770  eucalginv  11773  eucalglt  11774  eucalg  11776  gcddvdslcm  11790  lcmneg  11791  lcmgcdlem  11794  lcmdvds  11796  lcmgcdeq  11800  lcmdvdsb  11801  lcmass  11802  mulgcddvds  11811  rpmulgcd2  11812  qredeu  11814  divgcdcoprm0  11818  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  sqnprm  11852  rpexp  11867  sqpweven  11889  2sqpwodd  11890  divnumden  11910  phivalfi  11924  phicl2  11926  phiprmpw  11934  crth  11936  phimullem  11937  hashgcdeq  11940  ennnfoneleminc  11960  ennnfonelemrnh  11965  ennnfonelemim  11973  nninffeq  13391