Theorem nn0zd 9463

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

Syntax hints:   -> wi 4   e. wcel 2167   NN0cn0 9266   ZZcz 9343

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-sep 4152  ax-pow 4208  ax-pr 4243  ax-un 4469  ax-setind 4574  ax-cnex 7987  ax-resscn 7988  ax-1cn 7989  ax-1re 7990  ax-icn 7991  ax-addcl 7992  ax-addrcl 7993  ax-mulcl 7994  ax-addcom 7996  ax-addass 7998  ax-distr 8000  ax-i2m1 8001  ax-0lt1 8002  ax-0id 8004  ax-rnegex 8005  ax-cnre 8007  ax-pre-ltirr 8008  ax-pre-ltwlin 8009  ax-pre-lttrn 8010  ax-pre-ltadd 8012

This theorem depends on definitions:  df-bi 117  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-nel 2463  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-pw 3608  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-int 3876  df-br 4035  df-opab 4096  df-id 4329  df-xp 4670  df-rel 4671  df-cnv 4672  df-co 4673  df-dm 4674  df-iota 5220  df-fun 5261  df-fv 5267  df-riota 5880  df-ov 5928  df-oprab 5929  df-mpo 5930  df-pnf 8080  df-mnf 8081  df-xr 8082  df-ltxr 8083  df-le 8084  df-sub 8216  df-neg 8217  df-inn 9008  df-n0 9267  df-z 9344

This theorem is referenced by:  nnzd  9464  xnn0dcle  9894  xnn0letri  9895  fseq1p1m1  10186  difelfznle  10227  flltdivnn0lt  10411  zmodfz  10455  addmodid  10481  modaddmodup  10496  modaddmodlo  10497  modsumfzodifsn  10505  addmodlteq  10507  expnegzap  10682  expaddzaplem  10691  expaddzap  10692  expmulzap  10694  nn0ltexp2  10818  nn0opthd  10831  facdiv  10847  facwordi  10849  faclbnd  10850  facavg  10855  bcval  10858  bcval5  10872  bcpasc  10875  hashfiv01gt1  10891  isfinite4im  10901  fihashneq0  10903  fseq1hash  10910  fnfz0hash  10941  ffzo0hash  10943  zfz1isolemiso  10948  wrdfin  10971  wrdffz  10973  wrdsymb0  10984  wrdlenge1n0  10985  resqrexlemga  11205  zabscl  11268  fsum0diaglem  11622  modfsummodlemstep  11639  binomlem  11665  binom1p  11667  binom1dif  11669  arisum2  11681  geosergap  11688  geoserap  11689  pwm1geoserap1  11690  geolim2  11694  cvgratnnlemrate  11712  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  efcvgfsum  11849  efaddlem  11856  dvdsdc  11980  divalglemnn  12100  divalgmod  12109  bitsfzolem  12136  bitsfzo  12137  bitsmod  12138  bitsfi  12139  bitsinv1lem  12143  bitsinv1  12144  zeqzmulgcd  12162  gcd0id  12171  gcdneg  12174  gcdaddm  12176  modgcd  12183  gcdmultipled  12185  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlemzz  12194  bezoutlemmo  12198  bezoutlemle  12200  bezoutlemsup  12201  dfgcd3  12202  dvdsgcdb  12205  gcdass  12207  mulgcd  12208  gcdzeq  12214  dvdsmulgcd  12217  bezoutr  12224  bezoutr1  12225  nn0seqcvgd  12234  algfx  12245  eucalgval2  12246  eucalginv  12249  eucalglt  12250  eucalg  12252  gcddvdslcm  12266  lcmneg  12267  lcmgcdlem  12270  lcmdvds  12272  lcmgcdeq  12276  lcmdvdsb  12277  lcmass  12278  mulgcddvds  12287  rpmulgcd2  12288  qredeu  12290  divgcdcoprm0  12294  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  sqnprm  12329  rpexp  12346  sqpweven  12368  2sqpwodd  12369  divnumden  12389  phivalfi  12405  phicl2  12407  phiprmpw  12415  crth  12417  phimullem  12418  eulerthlemfi  12421  eulerthlema  12423  hashgcdeq  12433  phisum  12434  odzdvds  12439  powm2modprm  12446  coprimeprodsq  12451  pcprendvds  12484  pcpremul  12487  pceu  12489  pcdiv  12496  pcqcl  12500  pcdvdsb  12514  pc2dvds  12524  pcprmpw2  12527  dvdsprmpweqle  12531  pcadd  12534  fldivp1  12542  pcfaclem  12543  pcfac  12544  pcbc  12545  pockthlem  12550  1arith  12561  mul4sqlem  12587  4sqlemafi  12589  4sqlemffi  12590  4sqleminfi  12591  4sqexercise1  12592  4sqlemsdc  12594  4sqlem11  12595  4sqlem12  12596  4sqlem14  12598  ennnfoneleminc  12653  ennnfonelemrnh  12658  ennnfonelemim  12666  znunit  14291  psrbaglesuppg  14302  psr1clfi  14316  elply2  15055  plyf  15057  elplyd  15061  ply1termlem  15062  ply1term  15063  plyaddlem1  15067  plymullem1  15068  plyaddlem  15069  plycoeid3  15077  plycolemc  15078  plycjlemc  15080  plycn  15082  plyrecj  15083  dvply1  15085  dvply2g  15086  wilthlem1  15300  sgmppw  15312  lgsval  15329  lgsfvalg  15330  lgsfcl2  15331  lgsval2lem  15335  lgsmod  15351  lgsdir2  15358  lgsne0  15363  lgsprme0  15367  gausslemma2dlem0h  15381  gausslemma2dlem0i  15382  gausslemma2dlem2  15387  gausslemma2dlem6  15392  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem2  15403  m1lgs  15410  2lgslem1a  15413  2lgslem3a  15418  2lgslem3b  15419  2lgslem3c  15420  2lgslem3d  15421  2lgslem3d1  15425  2lgs  15429  2lgsoddprmlem2  15431  2lgsoddprm  15438  2sqlem8  15448  nninffeq  15751