Theorem nngt0d 11952

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5070  0cc0 10802   < clt 10940  ℕcn 11903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904

This theorem is referenced by:  expmulnbnd  13878  faclbnd5  13940  facubnd  13942  harmonic  15499  efcllem  15715  ege2le3  15727  eftlub  15746  eflegeo  15758  eirrlem  15841  bitsfzo  16070  sqgcd  16198  prmind2  16318  nprm  16321  isprm5  16340  divdenle  16381  qnumgt0  16382  hashdvds  16404  odzdvds  16424  pythagtriplem11  16454  pythagtriplem13  16456  pythagtriplem19  16462  pcadd  16518  pcfaclem  16527  qexpz  16530  pockthlem  16534  pockthg  16535  prmreclem1  16545  prmreclem5  16549  4sqlem12  16585  4sqlem14  16587  4sqlem16  16589  vdwlem3  16612  vdwlem9  16618  psgnunilem3  19019  pgpfaclem2  19600  fvmptnn04ifd  21910  lebnumii  24035  dyadf  24660  dyadovol  24662  dyaddisjlem  24664  dyadmaxlem  24666  opnmbllem  24670  mbfi1fseqlem1  24785  mbfi1fseqlem4  24788  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  itg2gt0  24830  itg2cnlem2  24832  dgrcolem2  25340  leibpi  25997  log2tlbnd  26000  birthdaylem3  26008  amgm  26045  emcllem2  26051  harmonicbnd4  26065  lgamgulmlem1  26083  basellem1  26135  basellem4  26138  basellem6  26140  dvdsflf1o  26241  fsumfldivdiaglem  26243  fsumvma2  26267  chpchtsum  26272  perfectlem2  26283  bposlem1  26337  bposlem2  26338  bposlem6  26342  lgsqrlem4  26402  lgseisenlem1  26428  lgsquadlem1  26433  lgsquadlem2  26434  2sqlem8  26479  chebbnd1lem3  26524  rplogsumlem1  26537  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlema  26541  dchrisumlem1  26542  dchrisumlem3  26544  dchrisum0flblem2  26562  dchrisum0re  26566  logdivbnd  26609  pntpbnd1a  26638  pntpbnd1  26639  ostth2lem2  26687  ostth2lem3  26688  crctcsh  28090  clwwlknonex2  28374  minvecolem4  29143  cycpmrn  31312  eulerpartlemgc  32229  subfaclim  33050  cvmliftlem2  33148  cvmliftlem6  33152  cvmliftlem7  33153  cvmliftlem8  33154  cvmliftlem9  33155  cvmliftlem10  33156  cvmliftlem13  33158  knoppndvlem18  34636  knoppndvlem19  34637  knoppndvlem21  34639  poimirlem12  35716  poimirlem14  35718  poimirlem22  35726  opnmbllem0  35740  mblfinlem2  35742  lcmineqlem15  39979  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p6  40017  aks4d1p8  40023  aks4d1p9  40024  2ap1caineq  40029  sticksstones12a  40041  sticksstones12  40042  oexpreposd  40242  nn0expgcd  40256  rtprmirr  40268  flt4lem5e  40409  flt4lem6  40411  flt4lem7  40412  irrapxlem4  40563  irrapxlem5  40564  pellexlem2  40568  pellexlem6  40572  rmxypos  40685  jm2.17b  40699  jm2.17c  40700  jm2.27a  40743  jm2.27c  40745  jm3.1lem1  40755  jm3.1lem2  40756  jm3.1lem3  40757  relexpxpmin  41214  hashnzfz2  41828  sumnnodd  43061  stoweidlem1  43432  stoweidlem11  43442  stoweidlem26  43457  stoweidlem38  43469  stoweidlem42  43473  stoweidlem44  43475  stoweidlem51  43482  stoweidlem59  43490  stirlinglem3  43507  stirlinglem15  43519  dirkertrigeqlem3  43531  dirkercncflem2  43535  fourierdlem11  43549  fourierdlem14  43552  fourierdlem20  43558  fourierdlem25  43563  fourierdlem37  43575  fourierdlem41  43579  fourierdlem48  43585  fourierdlem64  43601  fourierdlem73  43610  fourierdlem79  43616  fourierdlem93  43630  etransclem35  43700  etransclem48  43713  qndenserrnbllem  43725  hoiqssbllem1  44050  hoiqssbllem2  44051  lighneallem4a  44948  proththdlem  44953  ztprmneprm  45571  expnegico01  45747  dignnld  45837