Theorem nngt0d 11346

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

Syntax hints:   → wi 4   ∈ wcel 2156   class class class wbr 4844  0cc0 10217   < clt 10355  ℕcn 11301

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-nn 11302

This theorem is referenced by:  expmulnbnd  13215  faclbnd5  13301  facubnd  13303  harmonic  14809  efcllem  15024  ege2le3  15036  eftlub  15055  eflegeo  15067  eirrlem  15148  bitsfzo  15372  sqgcd  15493  prmind2  15612  nprm  15615  isprm5  15632  divdenle  15670  qnumgt0  15671  hashdvds  15693  odzdvds  15713  pythagtriplem11  15743  pythagtriplem13  15745  pythagtriplem19  15751  pcadd  15806  pcfaclem  15815  qexpz  15818  pockthlem  15822  pockthg  15823  prmreclem1  15833  prmreclem5  15837  4sqlem12  15873  4sqlem14  15875  4sqlem16  15877  vdwlem3  15900  vdwlem9  15906  psgnunilem3  18113  pgpfaclem2  18679  fvmptnn04ifd  20867  lebnumii  22974  dyadf  23568  dyadovol  23570  dyaddisjlem  23572  dyadmaxlem  23574  opnmbllem  23578  mbfi1fseqlem1  23692  mbfi1fseqlem4  23695  mbfi1fseqlem5  23696  mbfi1fseqlem6  23697  itg2gt0  23737  itg2cnlem2  23739  dgrcolem2  24240  leibpi  24879  log2tlbnd  24882  birthdaylem3  24890  amgm  24927  emcllem2  24933  harmonicbnd4  24947  lgamgulmlem1  24965  basellem1  25017  basellem4  25020  basellem6  25022  dvdsflf1o  25123  fsumfldivdiaglem  25125  fsumvma2  25149  chpchtsum  25154  perfectlem2  25165  bposlem1  25219  bposlem2  25220  bposlem6  25224  lgsqrlem4  25284  lgseisenlem1  25310  lgsquadlem1  25315  lgsquadlem2  25316  2sqlem8  25361  chebbnd1lem3  25370  rplogsumlem1  25383  rplogsumlem2  25384  rpvmasumlem  25386  dchrisumlema  25387  dchrisumlem1  25388  dchrisumlem3  25390  dchrisum0flblem2  25408  dchrisum0re  25412  logdivbnd  25455  pntpbnd1a  25484  pntpbnd1  25485  ostth2lem2  25533  ostth2lem3  25534  crctcsh  26941  clwwlknonex2  27274  minvecolem4  28060  eulerpartlemgc  30745  subfaclim  31488  cvmliftlem2  31586  cvmliftlem6  31590  cvmliftlem7  31591  cvmliftlem8  31592  cvmliftlem9  31593  cvmliftlem10  31594  cvmliftlem13  31596  knoppndvlem18  32832  knoppndvlem19  32833  knoppndvlem21  32835  poimirlem12  33729  poimirlem14  33731  poimirlem22  33739  opnmbllem0  33753  mblfinlem2  33755  irrapxlem4  37885  irrapxlem5  37886  pellexlem2  37890  pellexlem6  37894  rmxypos  38009  jm2.17b  38023  jm2.17c  38024  jm2.27a  38067  jm2.27c  38069  jm3.1lem1  38079  jm3.1lem2  38080  jm3.1lem3  38081  relexpxpmin  38503  hashnzfz2  39014  sumnnodd  40336  stoweidlem1  40691  stoweidlem11  40701  stoweidlem26  40716  stoweidlem38  40728  stoweidlem42  40732  stoweidlem44  40734  stoweidlem51  40741  stoweidlem59  40749  stirlinglem3  40766  stirlinglem15  40778  dirkertrigeqlem3  40790  dirkercncflem2  40794  fourierdlem11  40808  fourierdlem14  40811  fourierdlem20  40817  fourierdlem25  40822  fourierdlem37  40834  fourierdlem41  40838  fourierdlem48  40844  fourierdlem64  40860  fourierdlem73  40869  fourierdlem79  40875  fourierdlem93  40889  etransclem35  40959  etransclem48  40972  qndenserrnbllem  40987  hoiqssbllem1  41312  hoiqssbllem2  41313  lighneallem4a  42094  proththdlem  42099  ztprmneprm  42687  expnegico01  42870  dignnld  42959