Theorem nn0zd 9567

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

Syntax hints:   -> wi 4   e. wcel 2200   NN0cn0 9369   ZZcz 9446

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8090  ax-resscn 8091  ax-1cn 8092  ax-1re 8093  ax-icn 8094  ax-addcl 8095  ax-addrcl 8096  ax-mulcl 8097  ax-addcom 8099  ax-addass 8101  ax-distr 8103  ax-i2m1 8104  ax-0lt1 8105  ax-0id 8107  ax-rnegex 8108  ax-cnre 8110  ax-pre-ltirr 8111  ax-pre-ltwlin 8112  ax-pre-lttrn 8113  ax-pre-ltadd 8115

This theorem depends on definitions:  df-bi 117  df-3or 1003  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2801  df-sbc 3029  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-int 3924  df-br 4084  df-opab 4146  df-id 4384  df-xp 4725  df-rel 4726  df-cnv 4727  df-co 4728  df-dm 4729  df-iota 5278  df-fun 5320  df-fv 5326  df-riota 5954  df-ov 6004  df-oprab 6005  df-mpo 6006  df-pnf 8183  df-mnf 8184  df-xr 8185  df-ltxr 8186  df-le 8187  df-sub 8319  df-neg 8320  df-inn 9111  df-n0 9370  df-z 9447

This theorem is referenced by:  nnzd  9568  xnn0dcle  9998  xnn0letri  9999  fseq1p1m1  10290  difelfznle  10331  flltdivnn0lt  10524  zmodfz  10568  addmodid  10594  modaddmodup  10609  modaddmodlo  10610  modsumfzodifsn  10618  addmodlteq  10620  expnegzap  10795  expaddzaplem  10804  expaddzap  10805  expmulzap  10807  nn0ltexp2  10931  nn0opthd  10944  facdiv  10960  facwordi  10962  faclbnd  10963  facavg  10968  bcval  10971  bcval5  10985  bcpasc  10988  hashfiv01gt1  11004  isfinite4im  11014  fihashneq0  11016  fseq1hash  11023  fnfz0hash  11054  ffzo0hash  11056  zfz1isolemiso  11061  wrdfin  11090  wrdffz  11092  wrdsymb0  11104  wrdlenge1n0  11105  lswwrd  11118  ccatfvalfi  11127  ccatcl  11128  ccatlen  11130  ccatval2  11133  ccatval3  11134  ccatvalfn  11136  ccatsymb  11137  ccatval21sw  11140  ccatass  11143  ccatrn  11144  lswccatn0lsw  11146  ccats1val2  11171  ccat1st1st  11172  fzowrddc  11179  swrdnd  11191  swrdspsleq  11199  swrdccat2  11203  pfxval  11206  pfxwrdsymbg  11222  pfxtrcfv0  11226  pfxtrcfvl  11229  ccatpfx  11233  pfxccat1  11234  lenrevpfxcctswrd  11244  wrdind  11254  wrd2ind  11255  swrdccatin1  11257  swrdccatin2  11261  pfxccatin12  11265  swrdccat  11267  pfxccatpfx2  11269  pfxccat3a  11270  swrdccat3blem  11271  swrdccat3b  11272  resqrexlemga  11534  zabscl  11597  fsum0diaglem  11951  modfsummodlemstep  11968  binomlem  11994  binom1p  11996  binom1dif  11998  arisum2  12010  geosergap  12017  geoserap  12018  pwm1geoserap1  12019  geolim2  12023  cvgratnnlemrate  12041  mertenslemi1  12046  mertenslem2  12047  mertensabs  12048  efcvgfsum  12178  efaddlem  12185  dvdsdc  12309  divalglemnn  12429  divalgmod  12438  bitsfzolem  12465  bitsfzo  12466  bitsmod  12467  bitsfi  12468  bitsinv1lem  12472  bitsinv1  12473  zeqzmulgcd  12491  gcd0id  12500  gcdneg  12503  gcdaddm  12505  modgcd  12512  gcdmultipled  12514  bezoutlemnewy  12517  bezoutlemstep  12518  bezoutlemmain  12519  bezoutlemzz  12523  bezoutlemmo  12527  bezoutlemle  12529  bezoutlemsup  12530  dfgcd3  12531  dvdsgcdb  12534  gcdass  12536  mulgcd  12537  gcdzeq  12543  dvdsmulgcd  12546  bezoutr  12553  bezoutr1  12554  nn0seqcvgd  12563  algfx  12574  eucalgval2  12575  eucalginv  12578  eucalglt  12579  eucalg  12581  gcddvdslcm  12595  lcmneg  12596  lcmgcdlem  12599  lcmdvds  12601  lcmgcdeq  12605  lcmdvdsb  12606  lcmass  12607  mulgcddvds  12616  rpmulgcd2  12617  qredeu  12619  divgcdcoprm0  12623  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  sqnprm  12658  rpexp  12675  sqpweven  12697  2sqpwodd  12698  divnumden  12718  phivalfi  12734  phicl2  12736  phiprmpw  12744  crth  12746  phimullem  12747  eulerthlemfi  12750  eulerthlema  12752  hashgcdeq  12762  phisum  12763  odzdvds  12768  powm2modprm  12775  coprimeprodsq  12780  pcprendvds  12813  pcpremul  12816  pceu  12818  pcdiv  12825  pcqcl  12829  pcdvdsb  12843  pc2dvds  12853  pcprmpw2  12856  dvdsprmpweqle  12860  pcadd  12863  fldivp1  12871  pcfaclem  12872  pcfac  12873  pcbc  12874  pockthlem  12879  1arith  12890  mul4sqlem  12916  4sqlemafi  12918  4sqlemffi  12919  4sqleminfi  12920  4sqexercise1  12921  4sqlemsdc  12923  4sqlem11  12924  4sqlem12  12925  4sqlem14  12927  ennnfoneleminc  12982  ennnfonelemrnh  12987  ennnfonelemim  12995  znunit  14623  psrbaglesuppg  14636  psrbagfi  14637  psr1clfi  14652  elply2  15409  plyf  15411  elplyd  15415  ply1termlem  15416  ply1term  15417  plyaddlem1  15421  plymullem1  15422  plyaddlem  15423  plycoeid3  15431  plycolemc  15432  plycjlemc  15434  plycn  15436  plyrecj  15437  dvply1  15439  dvply2g  15440  wilthlem1  15654  sgmppw  15666  lgsval  15683  lgsfvalg  15684  lgsfcl2  15685  lgsval2lem  15689  lgsmod  15705  lgsdir2  15712  lgsne0  15717  lgsprme0  15721  gausslemma2dlem0h  15735  gausslemma2dlem0i  15736  gausslemma2dlem2  15741  gausslemma2dlem6  15746  gausslemma2d  15748  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisenlem4  15752  lgsquadlem1  15756  lgsquadlem2  15757  m1lgs  15764  2lgslem1a  15767  2lgslem3a  15772  2lgslem3b  15773  2lgslem3c  15774  2lgslem3d  15775  2lgslem3d1  15779  2lgs  15783  2lgsoddprmlem2  15785  2lgsoddprm  15792  2sqlem8  15802  wksfval  16035  iswlkg  16041  nninffeq  16386