Theorem nngt0d 12312

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

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5147  0cc0 11152   < clt 11292  ℕcn 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-nn 12264

This theorem is referenced by:  expmulnbnd  14270  faclbnd5  14333  facubnd  14335  harmonic  15891  efcllem  16109  ege2le3  16122  eftlub  16141  eflegeo  16153  eirrlem  16236  bitsfzo  16468  sqgcd  16595  nn0expgcd  16597  prmind2  16718  nprm  16721  isprm5  16740  divdenle  16782  qnumgt0  16783  hashdvds  16808  odzdvds  16828  pythagtriplem11  16858  pythagtriplem13  16860  pythagtriplem19  16866  pcadd  16922  pcfaclem  16931  qexpz  16934  pockthlem  16938  pockthg  16939  prmreclem1  16949  prmreclem5  16953  4sqlem12  16989  4sqlem14  16991  4sqlem16  16993  vdwlem3  17016  vdwlem9  17022  ressmulgnnd  19108  psgnunilem3  19528  pgpfaclem2  20116  fvmptnn04ifd  22874  lebnumii  25011  dyadf  25639  dyadovol  25641  dyaddisjlem  25643  dyadmaxlem  25645  opnmbllem  25649  mbfi1fseqlem1  25764  mbfi1fseqlem4  25767  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  itg2gt0  25809  itg2cnlem2  25811  dgrcolem2  26328  rtprmirr  26817  leibpi  26999  log2tlbnd  27002  birthdaylem3  27010  amgm  27048  emcllem2  27054  harmonicbnd4  27068  lgamgulmlem1  27086  basellem1  27138  basellem4  27141  basellem6  27143  dvdsflf1o  27244  fsumfldivdiaglem  27246  fsumvma2  27272  chpchtsum  27277  perfectlem2  27288  bposlem1  27342  bposlem2  27343  bposlem6  27347  lgsqrlem4  27407  lgseisenlem1  27433  lgsquadlem1  27438  lgsquadlem2  27439  2sqlem8  27484  chebbnd1lem3  27529  rplogsumlem1  27542  rplogsumlem2  27543  rpvmasumlem  27545  dchrisumlema  27546  dchrisumlem1  27547  dchrisumlem3  27549  dchrisum0flblem2  27567  dchrisum0re  27571  logdivbnd  27614  pntpbnd1a  27643  pntpbnd1  27644  ostth2lem2  27692  ostth2lem3  27693  crctcsh  29853  clwwlknonex2  30137  minvecolem4  30908  cycpmrn  33145  eulerpartlemgc  34343  subfaclim  35172  cvmliftlem2  35270  cvmliftlem6  35274  cvmliftlem7  35275  cvmliftlem8  35276  cvmliftlem9  35277  cvmliftlem10  35278  cvmliftlem13  35280  knoppndvlem18  36511  knoppndvlem19  36512  knoppndvlem21  36514  poimirlem12  37618  poimirlem14  37620  poimirlem22  37628  opnmbllem0  37642  mblfinlem2  37644  lcmineqlem15  42024  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p6  42062  aks4d1p8  42068  aks4d1p9  42069  posbezout  42081  aks6d1c1  42097  aks6d1c3  42104  aks6d1c4  42105  2ap1caineq  42126  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem4  42154  aks6d1c7lem1  42161  unitscyglem4  42179  unitscyglem5  42180  oexpreposd  42335  flt4lem5e  42642  flt4lem6  42644  flt4lem7  42645  irrapxlem4  42812  irrapxlem5  42813  pellexlem2  42817  pellexlem6  42821  rmxypos  42935  jm2.17b  42949  jm2.17c  42950  jm2.27a  42993  jm2.27c  42995  jm3.1lem1  43005  jm3.1lem2  43006  jm3.1lem3  43007  relexpxpmin  43706  hashnzfz2  44316  sumnnodd  45585  stoweidlem1  45956  stoweidlem11  45966  stoweidlem26  45981  stoweidlem38  45993  stoweidlem42  45997  stoweidlem44  45999  stoweidlem51  46006  stoweidlem59  46014  stirlinglem3  46031  stirlinglem15  46043  dirkertrigeqlem3  46055  dirkercncflem2  46059  fourierdlem11  46073  fourierdlem14  46076  fourierdlem20  46082  fourierdlem25  46087  fourierdlem37  46099  fourierdlem41  46103  fourierdlem48  46109  fourierdlem64  46125  fourierdlem73  46134  fourierdlem79  46140  fourierdlem93  46154  etransclem35  46224  etransclem48  46237  qndenserrnbllem  46249  hoiqssbllem1  46577  hoiqssbllem2  46578  lighneallem4a  47532  proththdlem  47537  stgrusgra  47861  ztprmneprm  48191  expnegico01  48363  dignnld  48452