Theorem nn0zd 9661

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 9558	. 2 |- NN0 C_ ZZ
2		nn0zd.1	. 2 |- ( ph -> A e. NN0 )
3	1, 2	sselid 3226	1 |- ( ph -> A e. ZZ )

Syntax hints:   -> wi 4   e. wcel 2202   NN0cn0 9461   ZZcz 9540

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 8183  ax-resscn 8184  ax-1cn 8185  ax-1re 8186  ax-icn 8187  ax-addcl 8188  ax-addrcl 8189  ax-mulcl 8190  ax-addcom 8192  ax-addass 8194  ax-distr 8196  ax-i2m1 8197  ax-0lt1 8198  ax-0id 8200  ax-rnegex 8201  ax-cnre 8203  ax-pre-ltirr 8204  ax-pre-ltwlin 8205  ax-pre-lttrn 8206  ax-pre-ltadd 8208

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 8275  df-mnf 8276  df-xr 8277  df-ltxr 8278  df-le 8279  df-sub 8411  df-neg 8412  df-inn 9203  df-n0 9462  df-z 9541

This theorem is referenced by:  nnzd  9662  eluzmn  9823  xnn0dcle  10098  xnn0letri  10099  fseq1p1m1  10391  difelfznle  10432  flltdivnn0lt  10627  zmodfz  10671  addmodid  10697  modaddmodup  10712  modaddmodlo  10713  modsumfzodifsn  10721  addmodlteq  10723  expnegzap  10898  expaddzaplem  10907  expaddzap  10908  expmulzap  10910  nn0ltexp2  11034  nn0opthd  11047  facdiv  11063  facwordi  11065  faclbnd  11066  facavg  11071  bcval  11074  bcval5  11088  bcpasc  11091  hashfiv01gt1  11107  isfinite4im  11117  fihashneq0  11119  fseq1hash  11127  fnfz0hash  11159  ffzo0hash  11161  zfz1isolemiso  11166  wrdfin  11198  wrdffz  11200  wrdsymb0  11212  wrdlenge1n0  11213  lswwrd  11226  ccatfvalfi  11235  ccatcl  11236  ccatlen  11238  ccatval2  11241  ccatval3  11242  ccatvalfn  11244  ccatsymb  11245  ccatval21sw  11248  ccatass  11251  ccatrn  11252  lswccatn0lsw  11254  ccatalpha  11256  ccats1val2  11283  ccat1st1st  11284  fzowrddc  11294  swrdnd  11306  swrdspsleq  11314  swrdccat2  11318  pfxval  11321  pfxwrdsymbg  11337  pfxtrcfv0  11341  pfxtrcfvl  11344  ccatpfx  11348  pfxccat1  11349  lenrevpfxcctswrd  11359  wrdind  11369  wrd2ind  11370  swrdccatin1  11372  swrdccatin2  11376  pfxccatin12  11380  swrdccat  11382  pfxccatpfx2  11384  pfxccat3a  11385  swrdccat3blem  11386  swrdccat3b  11387  resqrexlemga  11663  zabscl  11726  fsum0diaglem  12081  modfsummodlemstep  12098  binomlem  12124  binom1p  12126  binom1dif  12128  arisum2  12140  geosergap  12147  geoserap  12148  pwm1geoserap1  12149  geolim2  12153  cvgratnnlemrate  12171  mertenslemi1  12176  mertenslem2  12177  mertensabs  12178  efcvgfsum  12308  efaddlem  12315  dvdsdc  12439  divalglemnn  12559  divalgmod  12568  bitsfzolem  12595  bitsfzo  12596  bitsmod  12597  bitsfi  12598  bitsinv1lem  12602  bitsinv1  12603  zeqzmulgcd  12621  gcd0id  12630  gcdneg  12633  gcdaddm  12635  modgcd  12642  gcdmultipled  12644  bezoutlemnewy  12647  bezoutlemstep  12648  bezoutlemmain  12649  bezoutlemzz  12653  bezoutlemmo  12657  bezoutlemle  12659  bezoutlemsup  12660  dfgcd3  12661  dvdsgcdb  12664  gcdass  12666  mulgcd  12667  gcdzeq  12673  dvdsmulgcd  12676  bezoutr  12683  bezoutr1  12684  nn0seqcvgd  12693  algfx  12704  eucalgval2  12705  eucalginv  12708  eucalglt  12709  eucalg  12711  gcddvdslcm  12725  lcmneg  12726  lcmgcdlem  12729  lcmdvds  12731  lcmgcdeq  12735  lcmdvdsb  12736  lcmass  12737  mulgcddvds  12746  rpmulgcd2  12747  qredeu  12749  divgcdcoprm0  12753  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  sqnprm  12788  rpexp  12805  sqpweven  12827  2sqpwodd  12828  divnumden  12848  phivalfi  12864  phicl2  12866  phiprmpw  12874  crth  12876  phimullem  12877  eulerthlemfi  12880  eulerthlema  12882  hashgcdeq  12892  phisum  12893  odzdvds  12898  powm2modprm  12905  coprimeprodsq  12910  pcprendvds  12943  pcpremul  12946  pceu  12948  pcdiv  12955  pcqcl  12959  pcdvdsb  12973  pc2dvds  12983  pcprmpw2  12986  dvdsprmpweqle  12990  pcadd  12993  fldivp1  13001  pcfaclem  13002  pcfac  13003  pcbc  13004  pockthlem  13009  1arith  13020  mul4sqlem  13046  4sqlemafi  13048  4sqlemffi  13049  4sqleminfi  13050  4sqexercise1  13051  4sqlemsdc  13053  4sqlem11  13054  4sqlem12  13055  4sqlem14  13057  ennnfoneleminc  13112  ennnfonelemrnh  13117  ennnfonelemim  13125  znunit  14755  psrbaglesuppg  14768  psrbagfi  14770  psrbaglecl  14771  psrbagcon  14772  psrbagconf1o  14774  psr1clfi  14789  elply2  15546  plyf  15548  elplyd  15552  ply1termlem  15553  ply1term  15554  plyaddlem1  15558  plymullem1  15559  plyaddlem  15560  plycoeid3  15568  plycolemc  15569  plycjlemc  15571  plycn  15573  plyrecj  15574  dvply1  15576  dvply2g  15577  wilthlem1  15794  sgmppw  15806  lgsval  15823  lgsfvalg  15824  lgsfcl2  15825  lgsval2lem  15829  lgsmod  15845  lgsdir2  15852  lgsne0  15857  lgsprme0  15861  gausslemma2dlem0h  15875  gausslemma2dlem0i  15876  gausslemma2dlem2  15881  gausslemma2dlem6  15886  gausslemma2d  15888  lgseisenlem1  15889  lgseisenlem2  15890  lgseisenlem3  15891  lgseisenlem4  15892  lgsquadlem1  15896  lgsquadlem2  15897  m1lgs  15904  2lgslem1a  15907  2lgslem3a  15912  2lgslem3b  15913  2lgslem3c  15914  2lgslem3d  15915  2lgslem3d1  15919  2lgs  15923  2lgsoddprmlem2  15925  2lgsoddprm  15932  2sqlem8  15942  vdegp1bid  16256  wksfval  16263  wlkex  16266  iswlkg  16270  clwwlkccatlem  16341  umgrclwwlkge2  16343  clwwlknonex2lem2  16379  eupthfi  16392  eupth2lem3lem3fi  16411  eupth2lem3lem4fi  16414  eupth2lem3fi  16417  eupth2lemsfi  16419  konigsberglem5  16433  nninffeq  16746  gfsumval  16809  gsumgfsum1  16810