Theorem nn0zd 9697

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

Syntax hints:   -> wi 4   e. wcel 2203   NN0cn0 9495   ZZcz 9576

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 2205  ax-14 2206  ax-ext 2214  ax-sep 4227  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-cnex 8217  ax-resscn 8218  ax-1cn 8219  ax-1re 8220  ax-icn 8221  ax-addcl 8222  ax-addrcl 8223  ax-mulcl 8224  ax-addcom 8226  ax-addass 8228  ax-distr 8230  ax-i2m1 8231  ax-0lt1 8232  ax-0id 8234  ax-rnegex 8235  ax-cnre 8237  ax-pre-ltirr 8238  ax-pre-ltwlin 8239  ax-pre-lttrn 8240  ax-pre-ltadd 8242

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 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rab 2529  df-v 2814  df-sbc 3042  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-int 3949  df-br 4109  df-opab 4171  df-id 4413  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-iota 5311  df-fun 5353  df-fv 5359  df-riota 6002  df-ov 6052  df-oprab 6053  df-mpo 6054  df-pnf 8309  df-mnf 8310  df-xr 8311  df-ltxr 8312  df-le 8313  df-sub 8445  df-neg 8446  df-inn 9237  df-n0 9496  df-z 9577

This theorem is referenced by:  nnzd  9698  eluzmn  9859  xnn0dcle  10134  xnn0letri  10135  fseq1p1m1  10427  difelfznle  10468  flltdivnn0lt  10663  zmodfz  10707  addmodid  10733  modaddmodup  10748  modaddmodlo  10749  modsumfzodifsn  10757  addmodlteq  10759  expnegzap  10934  expaddzaplem  10943  expaddzap  10944  expmulzap  10946  nn0ltexp2  11070  nn0opthd  11083  facdiv  11099  facwordi  11101  faclbnd  11102  facavg  11107  bcval  11110  bcval5  11124  bcpasc  11127  hashfiv01gt1  11143  isfinite4im  11153  fihashneq0  11155  fseq1hash  11163  fnfz0hash  11195  ffzo0hash  11197  sseqn  11199  hashfibclem  11202  zfz1isolemiso  11207  wrdfin  11239  wrdffz  11241  wrdsymb0  11253  wrdlenge1n0  11254  lswwrd  11267  ccatfvalfi  11276  ccatcl  11277  ccatlen  11279  ccatval2  11282  ccatval3  11283  ccatvalfn  11285  ccatsymb  11286  ccatval21sw  11289  ccatass  11292  ccatrn  11293  lswccatn0lsw  11295  ccatalpha  11297  ccats1val2  11324  ccat1st1st  11325  fzowrddc  11335  swrdnd  11347  swrdspsleq  11355  swrdccat2  11359  pfxval  11362  pfxwrdsymbg  11378  pfxtrcfv0  11382  pfxtrcfvl  11385  ccatpfx  11389  pfxccat1  11390  lenrevpfxcctswrd  11400  wrdind  11410  wrd2ind  11411  swrdccatin1  11413  swrdccatin2  11417  pfxccatin12  11421  swrdccat  11423  pfxccatpfx2  11425  pfxccat3a  11426  swrdccat3blem  11427  swrdccat3b  11428  resqrexlemga  11704  zabscl  11767  fsum0diaglem  12122  modfsummodlemstep  12139  binomlem  12165  binom1p  12167  binom1dif  12169  arisum2  12181  geosergap  12188  geoserap  12189  pwm1geoserap1  12190  geolim2  12194  cvgratnnlemrate  12212  mertenslemi1  12217  mertenslem2  12218  mertensabs  12219  efcvgfsum  12349  efaddlem  12356  dvdsdc  12480  divalglemnn  12600  divalgmod  12609  bitsfzolem  12636  bitsfzo  12637  bitsmod  12638  bitsfi  12639  bitsinv1lem  12643  bitsinv1  12644  zeqzmulgcd  12662  gcd0id  12671  gcdneg  12674  gcdaddm  12676  modgcd  12683  gcdmultipled  12685  bezoutlemnewy  12688  bezoutlemstep  12689  bezoutlemmain  12690  bezoutlemzz  12694  bezoutlemmo  12698  bezoutlemle  12700  bezoutlemsup  12701  dfgcd3  12702  dvdsgcdb  12705  gcdass  12707  mulgcd  12708  gcdzeq  12714  dvdsmulgcd  12717  bezoutr  12724  bezoutr1  12725  nn0seqcvgd  12734  algfx  12745  eucalgval2  12746  eucalginv  12749  eucalglt  12750  eucalg  12752  gcddvdslcm  12766  lcmneg  12767  lcmgcdlem  12770  lcmdvds  12772  lcmgcdeq  12776  lcmdvdsb  12777  lcmass  12778  mulgcddvds  12787  rpmulgcd2  12788  qredeu  12790  divgcdcoprm0  12794  divgcdcoprmex  12795  cncongr1  12796  cncongr2  12797  sqnprm  12829  rpexp  12846  sqpweven  12868  2sqpwodd  12869  divnumden  12889  phivalfi  12905  phicl2  12907  phiprmpw  12915  crth  12917  phimullem  12918  eulerthlemfi  12921  eulerthlema  12923  hashgcdeq  12933  phisum  12934  odzdvds  12939  powm2modprm  12946  coprimeprodsq  12951  pcprendvds  12984  pcpremul  12987  pceu  12989  pcdiv  12996  pcqcl  13000  pcdvdsb  13014  pc2dvds  13024  pcprmpw2  13027  dvdsprmpweqle  13031  pcadd  13034  fldivp1  13042  pcfaclem  13043  pcfac  13044  pcbc  13045  pockthlem  13050  1arith  13061  mul4sqlem  13087  4sqlemafi  13089  4sqlemffi  13090  4sqleminfi  13091  4sqexercise1  13092  4sqlemsdc  13094  4sqlem11  13095  4sqlem12  13096  4sqlem14  13098  ballotfilemofi  13134  ennnfoneleminc  13154  ennnfonelemrnh  13159  ennnfonelemim  13167  znunit  14799  psrbaglesuppg  14813  psrbagfi  14815  psrbaglecl  14816  psrbagcon  14818  psrbagconf1o  14820  psr1clfi  14835  elply2  15592  plyf  15594  elplyd  15598  ply1termlem  15599  ply1term  15600  plyaddlem1  15604  plymullem1  15605  plyaddlem  15606  plycoeid3  15614  plycolemc  15615  plycjlemc  15617  plycn  15619  plyrecj  15620  dvply1  15622  dvply2g  15623  wilthlem1  15840  sgmppw  15852  lgsval  15869  lgsfvalg  15870  lgsfcl2  15871  lgsval2lem  15875  lgsmod  15891  lgsdir2  15898  lgsne0  15903  lgsprme0  15907  gausslemma2dlem0h  15921  gausslemma2dlem0i  15922  gausslemma2dlem2  15927  gausslemma2dlem6  15932  gausslemma2d  15934  lgseisenlem1  15935  lgseisenlem2  15936  lgseisenlem3  15937  lgseisenlem4  15938  lgsquadlem1  15942  lgsquadlem2  15943  m1lgs  15950  2lgslem1a  15953  2lgslem3a  15958  2lgslem3b  15959  2lgslem3c  15960  2lgslem3d  15961  2lgslem3d1  15965  2lgs  15969  2lgsoddprmlem2  15971  2lgsoddprm  15978  2sqlem8  15988  vdegp1bid  16302  wksfval  16309  wlkex  16312  iswlkg  16316  clwwlkccatlem  16387  umgrclwwlkge2  16389  clwwlknonex2lem2  16425  eupthfi  16438  eupth2lem3lem3fi  16457  eupth2lem3lem4fi  16460  eupth2lem3fi  16463  eupth2lemsfi  16465  konigsberglem5  16479  nninffeq  16790  gfsumval  16853  gsumgfsum1  16854