Theorem nn0zd 8965

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

Syntax hints:   -> wi 4   e. wcel 1445   NN0cn0 8771   ZZcz 8848

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-cnex 7533  ax-resscn 7534  ax-1cn 7535  ax-1re 7536  ax-icn 7537  ax-addcl 7538  ax-addrcl 7539  ax-mulcl 7540  ax-addcom 7542  ax-addass 7544  ax-distr 7546  ax-i2m1 7547  ax-0lt1 7548  ax-0id 7550  ax-rnegex 7551  ax-cnre 7553  ax-pre-ltirr 7554  ax-pre-ltwlin 7555  ax-pre-lttrn 7556  ax-pre-ltadd 7558

This theorem depends on definitions:  df-bi 116  df-3or 928  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-nel 2358  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-int 3711  df-br 3868  df-opab 3922  df-id 4144  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-iota 5014  df-fun 5051  df-fv 5057  df-riota 5646  df-ov 5693  df-oprab 5694  df-mpt2 5695  df-pnf 7621  df-mnf 7622  df-xr 7623  df-ltxr 7624  df-le 7625  df-sub 7752  df-neg 7753  df-inn 8521  df-n0 8772  df-z 8849

This theorem is referenced by:  nnzd  8966  fseq1p1m1  9657  difelfznle  9695  flltdivnn0lt  9860  zmodfz  9902  addmodid  9928  modaddmodup  9943  modaddmodlo  9944  modsumfzodifsn  9952  addmodlteq  9954  expnegzap  10120  expaddzaplem  10129  expaddzap  10130  expmulzap  10132  nn0opthd  10261  facdiv  10277  facwordi  10279  faclbnd  10280  facavg  10285  bcval  10288  bcval5  10302  bcpasc  10305  hashfiv01gt1  10321  isfinite4im  10332  fihashneq0  10334  fseq1hash  10340  fnfz0hash  10368  ffzo0hash  10370  zfz1isolemiso  10375  resqrexlemga  10587  zabscl  10650  fsum0diaglem  10999  modfsummodlemstep  11016  binomlem  11042  binom1p  11044  binom1dif  11046  arisum2  11058  geosergap  11065  geoserap  11066  pwm1geoserap1  11067  geolim2  11071  cvgratnnlemrate  11089  mertenslemi1  11094  mertenslem2  11095  mertensabs  11096  efcvgfsum  11122  efaddlem  11129  dvdsdc  11247  divalglemnn  11361  divalgmod  11370  zeqzmulgcd  11405  gcd0id  11413  gcdneg  11416  gcdaddm  11418  modgcd  11425  bezoutlemnewy  11428  bezoutlemstep  11429  bezoutlemmain  11430  bezoutlemzz  11434  bezoutlemmo  11438  bezoutlemle  11440  bezoutlemsup  11441  dfgcd3  11442  dvdsgcdb  11445  gcdass  11447  mulgcd  11448  gcdzeq  11454  dvdsmulgcd  11457  bezoutr  11464  bezoutr1  11465  nn0seqcvgd  11466  algfx  11477  eucalgval2  11478  eucalginv  11481  eucalglt  11482  eucalg  11484  gcddvdslcm  11498  lcmneg  11499  lcmgcdlem  11502  lcmdvds  11504  lcmgcdeq  11508  lcmdvdsb  11509  lcmass  11510  mulgcddvds  11519  rpmulgcd2  11520  qredeu  11522  divgcdcoprm0  11526  divgcdcoprmex  11527  cncongr1  11528  cncongr2  11529  sqnprm  11560  rpexp  11575  sqpweven  11596  2sqpwodd  11597  divnumden  11617  phivalfi  11631  phicl2  11633  phiprmpw  11641  crth  11643  phimullem  11644  hashgcdeq  11647