Theorem nn0zd 9777

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

This proof depends on syntax axioms:   -> wi 4   e. wcel 2209   NN0cn0 9574   ZZcz 9655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-pow 4313  ax-pr 4348  ax-un 4580  ax-setind 4686  ax-cnex 8276  ax-resscn 8277  ax-1cn 8278  ax-1re 8279  ax-icn 8280  ax-addcl 8281  ax-addrcl 8282  ax-mulcl 8283  ax-addcom 8285  ax-addass 8287  ax-distr 8289  ax-i2m1 8290  ax-0lt1 8291  ax-0id 8293  ax-rnegex 8294  ax-cnre 8296  ax-pre-ltirr 8297  ax-pre-ltwlin 8298  ax-pre-lttrn 8299  ax-pre-ltadd 8301

This proof depends on definitions:  df-bi 117  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-nel 2516  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-br 4132  df-opab 4194  df-id 4440  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-iota 5340  df-fun 5382  df-fv 5388  df-riota 6041  df-ov 6091  df-oprab 6092  df-mpo 6093  df-pnf 8368  df-mnf 8369  df-xr 8370  df-ltxr 8371  df-le 8372  df-sub 8506  df-neg 8507  df-inn 9314  df-n0 9575  df-z 9656

This theorem is used by:  nnzd  9778  eluzmn  9944  xnn0dcle  10221  xnn0letri  10222  fseq1p1m1  10518  difelfznle  10559  flltdivnn0lt  10760  zmodfz  10804  addmodid  10830  modaddmodup  10845  modaddmodlo  10846  modsumfzodifsn  10854  addmodlteq  10856  expnegzap  11031  expaddzaplem  11040  expaddzap  11041  expmulzap  11043  nn0ltexp2  11169  nn0opthd  11182  facdiv  11198  facwordi  11200  faclbnd  11201  facavg  11206  bcval  11209  bcval5  11223  bcpasc  11226  hashfiv01gt1  11243  isfinite4im  11253  fihashneq0  11255  fseq1hash  11263  fnfz0hash  11297  ffzo0hash  11299  sseqn  11301  hashfibclem  11304  hashf1  11309  zfz1isolemiso  11313  wrdfin  11345  wrdffz  11347  wrdsymb0  11359  wrdlenge1n0  11360  lswwrd  11373  ccatfvalfi  11382  ccatcl  11383  ccatlen  11385  ccatval2  11388  ccatval3  11389  ccatvalfn  11391  ccatsymb  11392  ccatval21sw  11395  ccatass  11398  ccatrn  11399  lswccatn0lsw  11401  ccatalpha  11403  ccats1val2  11430  ccat1st1st  11431  fzowrddc  11441  swrdnd  11453  swrdspsleq  11461  swrdccat2  11465  pfxval  11468  pfxwrdsymbg  11484  pfxtrcfv0  11488  pfxtrcfvl  11491  ccatpfx  11495  pfxccat1  11496  lenrevpfxcctswrd  11506  wrdind  11516  wrd2ind  11517  swrdccatin1  11519  swrdccatin2  11523  pfxccatin12  11527  swrdccat  11529  pfxccatpfx2  11531  pfxccat3a  11532  swrdccat3blem  11533  swrdccat3b  11534  resqrexlemga  11811  zabscl  11875  fsum0diaglem  12232  modfsummodlemstep  12249  binomlem  12275  binom1p  12277  binom1dif  12279  arisum2  12291  geosergap  12298  geoserap  12299  pwm1geoserap1  12300  geolim2  12304  cvgratnnlemrate  12322  mertenslemi1  12327  mertenslem2  12328  mertensabs  12329  efcvgfsum  12459  efaddlem  12466  dvdsdc  12590  divalglemnn  12710  divalgmod  12719  bitsfzolem  12746  bitsfzo  12747  bitsmod  12748  bitsfi  12749  bitsinv1lem  12753  bitsinv1  12754  zeqzmulgcd  12772  gcd0id  12781  gcdneg  12784  gcdaddm  12786  modgcd  12793  gcdmultipled  12795  bezoutlemnewy  12798  bezoutlemstep  12799  bezoutlemmain  12800  bezoutlemzz  12804  bezoutlemmo  12808  bezoutlemle  12810  bezoutlemsup  12811  dfgcd3  12812  dvdsgcdb  12815  gcdass  12817  mulgcd  12818  gcdzeq  12824  dvdsmulgcd  12827  bezoutr  12834  bezoutr1  12835  nn0seqcvgd  12844  algfx  12855  eucalgval2  12856  eucalginv  12859  eucalglt  12860  eucalg  12862  gcddvdslcm  12876  lcmneg  12877  lcmgcdlem  12880  lcmdvds  12882  lcmgcdeq  12886  lcmdvdsb  12887  lcmass  12888  mulgcddvds  12897  rpmulgcd2  12898  qredeu  12900  divgcdcoprm0  12904  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  sqnprm  12940  rpexp  12957  sqpweven  12980  2sqpwodd  12981  divnumden  13001  phivalfi  13019  phicl2  13021  phiprmpw  13029  crth  13031  phimullem  13032  eulerthlemfi  13035  eulerthlema  13037  hashgcdeq  13047  phisum  13048  odzdvds  13053  powm2modprm  13060  coprimeprodsq  13065  pcprendvds  13098  pcpremul  13101  pceu  13103  pcdiv  13110  pcqcl  13114  pcdvdsb  13128  pc2dvds  13138  pcprmpw2  13141  dvdsprmpweqle  13145  pcadd  13148  fldivp1  13156  pcfaclem  13157  pcfac  13158  pcbc  13159  pockthlem  13164  1arith  13175  mul4sqlem  13201  4sqlemafi  13203  4sqlemffi  13204  4sqleminfi  13205  4sqexercise1  13206  4sqlemsdc  13208  4sqlem11  13209  4sqlem12  13210  4sqlem14  13212  ballotfilemofi  13277  ballotfilemfval  13287  ballotfilemfelz  13288  ballotfilemgval  13325  ennnfoneleminc  13360  ennnfonelemrnh  13365  ennnfonelemim  13373  gsumvalfi  14242  gzsumgsum1  14243  gsumf1ofi  14250  gsummhmfi  14264  gsumressfi  14267  znunit  15103  asclmulg  15153  psrbaglesuppg  15166  psrbagfi  15168  psrbaglecl  15169  psrbagcon  15171  psrbaglefifi  15172  psrbagconf1o  15174  gsumbagdiaglem  15175  psrass1filem  15177  psr1clfi  15198  psrass1fi  15201  elply2  15961  plyf  15963  elplyd  15967  ply1termlem  15968  ply1term  15969  plyaddlem1  15973  plymullem1  15974  plyaddlem  15975  plycoeid3  15983  plycolemc  15984  plycjlemc  15986  plycn  15988  plyrecj  15989  dvply1  15991  dvply2g  15992  zprmlogbaplem1  16215  zprmlogbaplem2  16216  birthdaylem2  16226  wilthlem1  16232  ppiqnncl  16278  sgmppw  16286  ppiqub  16293  chtublem  16295  bcmax  16305  bposlem1  16311  bposlem5  16315  bposlem6  16316  lgsval  16328  lgsfvalg  16329  lgsfcl2  16330  lgsval2lem  16334  lgsmod  16350  lgsdir2  16357  lgsne0  16362  lgsprme0  16366  gausslemma2dlem0h  16380  gausslemma2dlem0i  16381  gausslemma2dlem2  16386  gausslemma2dlem6  16391  gausslemma2d  16393  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgsquadlem1  16401  lgsquadlem2  16402  m1lgs  16409  2lgslem1a  16412  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgslem3d1  16424  2lgs  16428  2lgsoddprmlem2  16430  2lgsoddprm  16437  2sqlem8  16447  vdegp1bid  16761  wksfval  16768  wlkex  16771  iswlkg  16775  clwwlkccatlem  16846  umgrclwwlkge2  16848  clwwlknonex2lem2  16884  eupthfi  16897  eupth2lem3lem3fi  16916  eupth2lem3lem4fi  16919  eupth2lem3fi  16922  eupth2lemsfi  16924  konigsberglem5  16938  nninffeq  17269