Theorem nn0zd 9493

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

Syntax hints:   -> wi 4   e. wcel 2176   NN0cn0 9295   ZZcz 9372

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 615  ax-in2 616  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-13 2178  ax-14 2179  ax-ext 2187  ax-sep 4162  ax-pow 4218  ax-pr 4253  ax-un 4480  ax-setind 4585  ax-cnex 8016  ax-resscn 8017  ax-1cn 8018  ax-1re 8019  ax-icn 8020  ax-addcl 8021  ax-addrcl 8022  ax-mulcl 8023  ax-addcom 8025  ax-addass 8027  ax-distr 8029  ax-i2m1 8030  ax-0lt1 8031  ax-0id 8033  ax-rnegex 8034  ax-cnre 8036  ax-pre-ltirr 8037  ax-pre-ltwlin 8038  ax-pre-lttrn 8039  ax-pre-ltadd 8041

This theorem depends on definitions:  df-bi 117  df-3or 982  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1484  df-sb 1786  df-eu 2057  df-mo 2058  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-ne 2377  df-nel 2472  df-ral 2489  df-rex 2490  df-reu 2491  df-rab 2493  df-v 2774  df-sbc 2999  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pw 3618  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-int 3886  df-br 4045  df-opab 4106  df-id 4340  df-xp 4681  df-rel 4682  df-cnv 4683  df-co 4684  df-dm 4685  df-iota 5232  df-fun 5273  df-fv 5279  df-riota 5899  df-ov 5947  df-oprab 5948  df-mpo 5949  df-pnf 8109  df-mnf 8110  df-xr 8111  df-ltxr 8112  df-le 8113  df-sub 8245  df-neg 8246  df-inn 9037  df-n0 9296  df-z 9373

This theorem is referenced by:  nnzd  9494  xnn0dcle  9924  xnn0letri  9925  fseq1p1m1  10216  difelfznle  10257  flltdivnn0lt  10447  zmodfz  10491  addmodid  10517  modaddmodup  10532  modaddmodlo  10533  modsumfzodifsn  10541  addmodlteq  10543  expnegzap  10718  expaddzaplem  10727  expaddzap  10728  expmulzap  10730  nn0ltexp2  10854  nn0opthd  10867  facdiv  10883  facwordi  10885  faclbnd  10886  facavg  10891  bcval  10894  bcval5  10908  bcpasc  10911  hashfiv01gt1  10927  isfinite4im  10937  fihashneq0  10939  fseq1hash  10946  fnfz0hash  10977  ffzo0hash  10979  zfz1isolemiso  10984  wrdfin  11013  wrdffz  11015  wrdsymb0  11026  wrdlenge1n0  11027  lswwrd  11040  ccatfvalfi  11048  ccatcl  11049  ccatlen  11051  ccatval2  11054  ccatval3  11055  ccatvalfn  11057  ccatsymb  11058  ccatval21sw  11061  ccatass  11064  ccatrn  11065  lswccatn0lsw  11067  ccats1val2  11092  ccat1st1st  11093  fzowrddc  11100  swrdnd  11112  swrdspsleq  11120  swrdccat2  11124  resqrexlemga  11334  zabscl  11397  fsum0diaglem  11751  modfsummodlemstep  11768  binomlem  11794  binom1p  11796  binom1dif  11798  arisum2  11810  geosergap  11817  geoserap  11818  pwm1geoserap1  11819  geolim2  11823  cvgratnnlemrate  11841  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  efcvgfsum  11978  efaddlem  11985  dvdsdc  12109  divalglemnn  12229  divalgmod  12238  bitsfzolem  12265  bitsfzo  12266  bitsmod  12267  bitsfi  12268  bitsinv1lem  12272  bitsinv1  12273  zeqzmulgcd  12291  gcd0id  12300  gcdneg  12303  gcdaddm  12305  modgcd  12312  gcdmultipled  12314  bezoutlemnewy  12317  bezoutlemstep  12318  bezoutlemmain  12319  bezoutlemzz  12323  bezoutlemmo  12327  bezoutlemle  12329  bezoutlemsup  12330  dfgcd3  12331  dvdsgcdb  12334  gcdass  12336  mulgcd  12337  gcdzeq  12343  dvdsmulgcd  12346  bezoutr  12353  bezoutr1  12354  nn0seqcvgd  12363  algfx  12374  eucalgval2  12375  eucalginv  12378  eucalglt  12379  eucalg  12381  gcddvdslcm  12395  lcmneg  12396  lcmgcdlem  12399  lcmdvds  12401  lcmgcdeq  12405  lcmdvdsb  12406  lcmass  12407  mulgcddvds  12416  rpmulgcd2  12417  qredeu  12419  divgcdcoprm0  12423  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  sqnprm  12458  rpexp  12475  sqpweven  12497  2sqpwodd  12498  divnumden  12518  phivalfi  12534  phicl2  12536  phiprmpw  12544  crth  12546  phimullem  12547  eulerthlemfi  12550  eulerthlema  12552  hashgcdeq  12562  phisum  12563  odzdvds  12568  powm2modprm  12575  coprimeprodsq  12580  pcprendvds  12613  pcpremul  12616  pceu  12618  pcdiv  12625  pcqcl  12629  pcdvdsb  12643  pc2dvds  12653  pcprmpw2  12656  dvdsprmpweqle  12660  pcadd  12663  fldivp1  12671  pcfaclem  12672  pcfac  12673  pcbc  12674  pockthlem  12679  1arith  12690  mul4sqlem  12716  4sqlemafi  12718  4sqlemffi  12719  4sqleminfi  12720  4sqexercise1  12721  4sqlemsdc  12723  4sqlem11  12724  4sqlem12  12725  4sqlem14  12727  ennnfoneleminc  12782  ennnfonelemrnh  12787  ennnfonelemim  12795  znunit  14421  psrbaglesuppg  14434  psrbagfi  14435  psr1clfi  14450  elply2  15207  plyf  15209  elplyd  15213  ply1termlem  15214  ply1term  15215  plyaddlem1  15219  plymullem1  15220  plyaddlem  15221  plycoeid3  15229  plycolemc  15230  plycjlemc  15232  plycn  15234  plyrecj  15235  dvply1  15237  dvply2g  15238  wilthlem1  15452  sgmppw  15464  lgsval  15481  lgsfvalg  15482  lgsfcl2  15483  lgsval2lem  15487  lgsmod  15503  lgsdir2  15510  lgsne0  15515  lgsprme0  15519  gausslemma2dlem0h  15533  gausslemma2dlem0i  15534  gausslemma2dlem2  15539  gausslemma2dlem6  15544  gausslemma2d  15546  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgsquadlem1  15554  lgsquadlem2  15555  m1lgs  15562  2lgslem1a  15565  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgslem3d1  15577  2lgs  15581  2lgsoddprmlem2  15583  2lgsoddprm  15590  2sqlem8  15600  nninffeq  15957