Theorem nngt0d 12032

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

Hypothesis

Ref	Expression
nnge1d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nngt0d	⊢ (𝜑 → 0 < 𝐴)

Proof of Theorem nngt0d

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nngt0 12014	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5073  0cc0 10881   < clt 11019  ℕcn 11983

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5221  ax-nul 5228  ax-pow 5286  ax-pr 5350  ax-un 7578  ax-resscn 10938  ax-1cn 10939  ax-icn 10940  ax-addcl 10941  ax-addrcl 10942  ax-mulcl 10943  ax-mulrcl 10944  ax-mulcom 10945  ax-addass 10946  ax-mulass 10947  ax-distr 10948  ax-i2m1 10949  ax-1ne0 10950  ax-1rid 10951  ax-rnegex 10952  ax-rrecex 10953  ax-cnre 10954  ax-pre-lttri 10955  ax-pre-lttrn 10956  ax-pre-ltadd 10957  ax-pre-mulgt0 10958

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3431  df-sbc 3716  df-csb 3832  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-pss 3905  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5074  df-opab 5136  df-mpt 5157  df-tr 5191  df-id 5484  df-eprel 5490  df-po 5498  df-so 5499  df-fr 5539  df-we 5541  df-xp 5590  df-rel 5591  df-cnv 5592  df-co 5593  df-dm 5594  df-rn 5595  df-res 5596  df-ima 5597  df-pred 6195  df-ord 6262  df-on 6263  df-lim 6264  df-suc 6265  df-iota 6384  df-fun 6428  df-fn 6429  df-f 6430  df-f1 6431  df-fo 6432  df-f1o 6433  df-fv 6434  df-riota 7224  df-ov 7270  df-oprab 7271  df-mpo 7272  df-om 7703  df-2nd 7821  df-frecs 8084  df-wrecs 8115  df-recs 8189  df-rdg 8228  df-er 8485  df-en 8721  df-dom 8722  df-sdom 8723  df-pnf 11021  df-mnf 11022  df-xr 11023  df-ltxr 11024  df-le 11025  df-sub 11217  df-neg 11218  df-nn 11984

This theorem is referenced by:  expmulnbnd  13960  faclbnd5  14022  facubnd  14024  harmonic  15581  efcllem  15797  ege2le3  15809  eftlub  15828  eflegeo  15840  eirrlem  15923  bitsfzo  16152  sqgcd  16280  prmind2  16400  nprm  16403  isprm5  16422  divdenle  16463  qnumgt0  16464  hashdvds  16486  odzdvds  16506  pythagtriplem11  16536  pythagtriplem13  16538  pythagtriplem19  16544  pcadd  16600  pcfaclem  16609  qexpz  16612  pockthlem  16616  pockthg  16617  prmreclem1  16627  prmreclem5  16631  4sqlem12  16667  4sqlem14  16669  4sqlem16  16671  vdwlem3  16694  vdwlem9  16700  psgnunilem3  19114  pgpfaclem2  19695  fvmptnn04ifd  22012  lebnumii  24139  dyadf  24765  dyadovol  24767  dyaddisjlem  24769  dyadmaxlem  24771  opnmbllem  24775  mbfi1fseqlem1  24890  mbfi1fseqlem4  24893  mbfi1fseqlem5  24894  mbfi1fseqlem6  24895  itg2gt0  24935  itg2cnlem2  24937  dgrcolem2  25445  leibpi  26102  log2tlbnd  26105  birthdaylem3  26113  amgm  26150  emcllem2  26156  harmonicbnd4  26170  lgamgulmlem1  26188  basellem1  26240  basellem4  26243  basellem6  26245  dvdsflf1o  26346  fsumfldivdiaglem  26348  fsumvma2  26372  chpchtsum  26377  perfectlem2  26388  bposlem1  26442  bposlem2  26443  bposlem6  26447  lgsqrlem4  26507  lgseisenlem1  26533  lgsquadlem1  26538  lgsquadlem2  26539  2sqlem8  26584  chebbnd1lem3  26629  rplogsumlem1  26642  rplogsumlem2  26643  rpvmasumlem  26645  dchrisumlema  26646  dchrisumlem1  26647  dchrisumlem3  26649  dchrisum0flblem2  26667  dchrisum0re  26671  logdivbnd  26714  pntpbnd1a  26743  pntpbnd1  26744  ostth2lem2  26792  ostth2lem3  26793  crctcsh  28197  clwwlknonex2  28481  minvecolem4  29250  cycpmrn  31418  eulerpartlemgc  32337  subfaclim  33158  cvmliftlem2  33256  cvmliftlem6  33260  cvmliftlem7  33261  cvmliftlem8  33262  cvmliftlem9  33263  cvmliftlem10  33264  cvmliftlem13  33266  knoppndvlem18  34717  knoppndvlem19  34718  knoppndvlem21  34720  poimirlem12  35797  poimirlem14  35799  poimirlem22  35807  opnmbllem0  35821  mblfinlem2  35823  lcmineqlem15  40059  aks4d1p1p3  40085  aks4d1p1p2  40086  aks4d1p1p4  40087  aks4d1p6  40097  aks4d1p8  40103  aks4d1p9  40104  2ap1caineq  40109  sticksstones12a  40121  sticksstones12  40122  oexpreposd  40329  nn0expgcd  40343  rtprmirr  40355  flt4lem5e  40501  flt4lem6  40503  flt4lem7  40504  irrapxlem4  40655  irrapxlem5  40656  pellexlem2  40660  pellexlem6  40664  rmxypos  40777  jm2.17b  40791  jm2.17c  40792  jm2.27a  40835  jm2.27c  40837  jm3.1lem1  40847  jm3.1lem2  40848  jm3.1lem3  40849  relexpxpmin  41306  hashnzfz2  41920  sumnnodd  43152  stoweidlem1  43523  stoweidlem11  43533  stoweidlem26  43548  stoweidlem38  43560  stoweidlem42  43564  stoweidlem44  43566  stoweidlem51  43573  stoweidlem59  43581  stirlinglem3  43598  stirlinglem15  43610  dirkertrigeqlem3  43622  dirkercncflem2  43626  fourierdlem11  43640  fourierdlem14  43643  fourierdlem20  43649  fourierdlem25  43654  fourierdlem37  43666  fourierdlem41  43670  fourierdlem48  43676  fourierdlem64  43692  fourierdlem73  43701  fourierdlem79  43707  fourierdlem93  43721  etransclem35  43791  etransclem48  43804  qndenserrnbllem  43816  hoiqssbllem1  44141  hoiqssbllem2  44142  lighneallem4a  45038  proththdlem  45043  ztprmneprm  45661  expnegico01  45837  dignnld  45927