Theorem nngt0d 11844

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 11826	. 2 ⊢ (𝐴 ∈ ℕ → 0 < 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 0 < 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2112   class class class wbr 5039  0cc0 10694   < clt 10832  ℕcn 11795

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-1cn 10752  ax-icn 10753  ax-addcl 10754  ax-addrcl 10755  ax-mulcl 10756  ax-mulrcl 10757  ax-mulcom 10758  ax-addass 10759  ax-mulass 10760  ax-distr 10761  ax-i2m1 10762  ax-1ne0 10763  ax-1rid 10764  ax-rnegex 10765  ax-rrecex 10766  ax-cnre 10767  ax-pre-lttri 10768  ax-pre-lttrn 10769  ax-pre-ltadd 10770  ax-pre-mulgt0 10771

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-reu 3058  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-pss 3872  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-tp 4532  df-op 4534  df-uni 4806  df-iun 4892  df-br 5040  df-opab 5102  df-mpt 5121  df-tr 5147  df-id 5440  df-eprel 5445  df-po 5453  df-so 5454  df-fr 5494  df-we 5496  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-pred 6140  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-riota 7148  df-ov 7194  df-oprab 7195  df-mpo 7196  df-om 7623  df-wrecs 8025  df-recs 8086  df-rdg 8124  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-xr 10836  df-ltxr 10837  df-le 10838  df-sub 11029  df-neg 11030  df-nn 11796

This theorem is referenced by:  expmulnbnd  13767  faclbnd5  13829  facubnd  13831  harmonic  15386  efcllem  15602  ege2le3  15614  eftlub  15633  eflegeo  15645  eirrlem  15728  bitsfzo  15957  sqgcd  16085  prmind2  16205  nprm  16208  isprm5  16227  divdenle  16268  qnumgt0  16269  hashdvds  16291  odzdvds  16311  pythagtriplem11  16341  pythagtriplem13  16343  pythagtriplem19  16349  pcadd  16405  pcfaclem  16414  qexpz  16417  pockthlem  16421  pockthg  16422  prmreclem1  16432  prmreclem5  16436  4sqlem12  16472  4sqlem14  16474  4sqlem16  16476  vdwlem3  16499  vdwlem9  16505  psgnunilem3  18842  pgpfaclem2  19423  fvmptnn04ifd  21704  lebnumii  23817  dyadf  24442  dyadovol  24444  dyaddisjlem  24446  dyadmaxlem  24448  opnmbllem  24452  mbfi1fseqlem1  24567  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  mbfi1fseqlem6  24572  itg2gt0  24612  itg2cnlem2  24614  dgrcolem2  25122  leibpi  25779  log2tlbnd  25782  birthdaylem3  25790  amgm  25827  emcllem2  25833  harmonicbnd4  25847  lgamgulmlem1  25865  basellem1  25917  basellem4  25920  basellem6  25922  dvdsflf1o  26023  fsumfldivdiaglem  26025  fsumvma2  26049  chpchtsum  26054  perfectlem2  26065  bposlem1  26119  bposlem2  26120  bposlem6  26124  lgsqrlem4  26184  lgseisenlem1  26210  lgsquadlem1  26215  lgsquadlem2  26216  2sqlem8  26261  chebbnd1lem3  26306  rplogsumlem1  26319  rplogsumlem2  26320  rpvmasumlem  26322  dchrisumlema  26323  dchrisumlem1  26324  dchrisumlem3  26326  dchrisum0flblem2  26344  dchrisum0re  26348  logdivbnd  26391  pntpbnd1a  26420  pntpbnd1  26421  ostth2lem2  26469  ostth2lem3  26470  crctcsh  27862  clwwlknonex2  28146  minvecolem4  28915  cycpmrn  31083  eulerpartlemgc  31995  subfaclim  32817  cvmliftlem2  32915  cvmliftlem6  32919  cvmliftlem7  32920  cvmliftlem8  32921  cvmliftlem9  32922  cvmliftlem10  32923  cvmliftlem13  32925  knoppndvlem18  34395  knoppndvlem19  34396  knoppndvlem21  34398  poimirlem12  35475  poimirlem14  35477  poimirlem22  35485  opnmbllem0  35499  mblfinlem2  35501  lcmineqlem15  39734  aks4d1p1p3  39759  aks4d1p1p2  39760  aks4d1p1p4  39761  2ap1caineq  39770  sticksstones12a  39782  sticksstones12  39783  oexpreposd  39969  nn0expgcd  39984  rtprmirr  39996  flt4lem5e  40137  flt4lem6  40139  flt4lem7  40140  irrapxlem4  40291  irrapxlem5  40292  pellexlem2  40296  pellexlem6  40300  rmxypos  40413  jm2.17b  40427  jm2.17c  40428  jm2.27a  40471  jm2.27c  40473  jm3.1lem1  40483  jm3.1lem2  40484  jm3.1lem3  40485  relexpxpmin  40943  hashnzfz2  41553  sumnnodd  42789  stoweidlem1  43160  stoweidlem11  43170  stoweidlem26  43185  stoweidlem38  43197  stoweidlem42  43201  stoweidlem44  43203  stoweidlem51  43210  stoweidlem59  43218  stirlinglem3  43235  stirlinglem15  43247  dirkertrigeqlem3  43259  dirkercncflem2  43263  fourierdlem11  43277  fourierdlem14  43280  fourierdlem20  43286  fourierdlem25  43291  fourierdlem37  43303  fourierdlem41  43307  fourierdlem48  43313  fourierdlem64  43329  fourierdlem73  43338  fourierdlem79  43344  fourierdlem93  43358  etransclem35  43428  etransclem48  43441  qndenserrnbllem  43453  hoiqssbllem1  43778  hoiqssbllem2  43779  lighneallem4a  44676  proththdlem  44681  ztprmneprm  45299  expnegico01  45475  dignnld  45565