Theorem nngt0d 10681

Description: A positive integer is positive. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnge1d.1	|- ( ph -> A e. NN )

Assertion

Ref	Expression
nngt0d	|- ( ph -> 0 < A )

Proof of Theorem nngt0d

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 |- ( ph -> A e. NN )
2		nngt0 10666	. 2 |- ( A e. NN -> 0 < A )
3	1, 2	syl 17	1 |- ( ph -> 0 < A )

Syntax hints:   -> wi 4   e. wcel 1898   class class class wbr 4416   0cc0 9565   < clt 9701   NNcn 10637

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638

This theorem is referenced by:  expmulnbnd  12436  faclbnd5  12515  facubnd  12517  harmonic  13966  efcllem  14181  ege2le3  14193  eftlub  14212  eflegeo  14224  eirrlem  14305  bitsfzo  14458  sqgcd  14575  prmind2  14684  nprm  14687  isprm5  14700  divdenle  14747  qnumgt0  14748  hashdvds  14772  odzdvds  14789  odzdvdsOLD  14795  pythagtriplem11  14824  pythagtriplem13  14826  pythagtriplem19  14832  pcadd  14883  pcfaclem  14892  qexpz  14895  pockthlem  14898  pockthg  14899  prmreclem1  14909  prmreclem5  14913  4sqlem12  14949  4sqlem14OLD  14951  4sqlem16OLD  14953  4sqlem14  14957  4sqlem16  14959  vdwlem3  14982  vdwlem9  14988  psgnunilem3  17186  pgpfaclem2  17764  fvmptnn04ifd  19926  lebnumii  22046  dyadf  22598  dyadovol  22600  dyaddisjlem  22602  dyadmaxlem  22604  opnmbllem  22608  mbfi1fseqlem1  22722  mbfi1fseqlem4  22725  mbfi1fseqlem5  22726  mbfi1fseqlem6  22727  itg2gt0  22767  itg2cnlem2  22769  dgrcolem2  23277  leibpi  23917  log2tlbnd  23920  birthdaylem3  23928  amgm  23965  emcllem2  23971  harmonicbnd4  23985  lgamgulmlem1  24003  basellem1  24056  basellem4  24059  basellem6  24061  dvdsflf1o  24165  fsumfldivdiaglem  24167  fsumvma2  24191  chpchtsum  24196  perfectlem2  24207  bposlem1  24261  bposlem2  24262  bposlem6  24266  lgsqrlem4  24321  lgseisenlem1  24326  lgsquadlem1  24331  lgsquadlem2  24332  2sqlem8  24349  chebbnd1lem3  24358  rplogsumlem1  24371  rplogsumlem2  24372  rpvmasumlem  24374  dchrisumlema  24375  dchrisumlem1  24376  dchrisumlem3  24378  dchrisum0flblem2  24396  dchrisum0re  24400  logdivbnd  24443  pntpbnd1a  24472  pntpbnd1  24473  ostth2lem2  24521  ostth2lem3  24522  numclwwlkovf2ex  25863  minvecolem4  26571  minvecolem4OLD  26581  eulerpartlemgc  29244  subfaclim  29960  cvmliftlem2  30058  cvmliftlem6  30062  cvmliftlem7  30063  cvmliftlem8  30064  cvmliftlem9  30065  cvmliftlem10  30066  cvmliftlem13  30068  poimirlem12  31997  poimirlem14  31999  poimirlem22  32007  opnmbllem0  32021  mblfinlem2  32023  irrapxlem4  35714  irrapxlem5  35715  pellexlem2  35719  pellexlem6  35723  rmxypos  35842  jm2.17b  35856  jm2.17c  35857  jm2.27a  35905  jm2.27c  35907  jm3.1lem1  35917  jm3.1lem2  35918  jm3.1lem3  35919  relexpxpmin  36354  hashnzfz2  36714  sumnnodd  37748  stoweidlem1  37899  stoweidlem11  37909  stoweidlem26  37924  stoweidlem38  37937  stoweidlem42  37941  stoweidlem44  37943  stoweidlem51  37950  stoweidlem59  37958  stirlinglem3  37976  stirlinglem15  37988  dirkertrigeqlem3  38000  dirkercncflem2  38004  fourierdlem11  38018  fourierdlem14  38021  fourierdlem20  38027  fourierdlem25  38032  fourierdlem37  38045  fourierdlem41  38049  fourierdlem48  38056  fourierdlem64  38072  fourierdlem73  38081  fourierdlem79  38087  fourierdlem93  38101  etransclem35  38172  etransclem48OLD  38185  etransclem48  38186  qndenserrnbllem  38201  hoiqssbllem1  38482  hoiqssbllem2  38483  proththdlem  38951  ztprmneprm  40401  expnegico01  40588  dignnld  40687