Theorem nngt0d 12309

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  0cc0 11124   < clt 11267  ℕcn 12257

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-1cn 11182  ax-icn 11183  ax-addcl 11184  ax-addrcl 11185  ax-mulcl 11186  ax-mulrcl 11187  ax-mulcom 11188  ax-addass 11189  ax-mulass 11190  ax-distr 11191  ax-i2m1 11192  ax-1ne0 11193  ax-1rid 11194  ax-rnegex 11195  ax-rrecex 11196  ax-cnre 11197  ax-pre-lttri 11198  ax-pre-lttrn 11199  ax-pre-ltadd 11200  ax-pre-mulgt0 11201

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6299  df-ord 6360  df-on 6361  df-lim 6362  df-suc 6363  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-riota 7370  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7863  df-2nd 7987  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273  df-sub 11467  df-neg 11468  df-nn 12258

This theorem is used by:  nnge2recico01  13560  expmulnbnd  14299  faclbnd5  14362  facubnd  14364  harmonic  15948  efcllem  16163  ege2le3  16176  eftlub  16197  eflegeo  16209  eirrlem  16292  bitsfzo  16525  sqgcd  16652  nn0expgcd  16654  prmind2  16775  nprm  16778  isprm5  16798  divdenle  16840  qnumgt0  16841  hashdvds  16866  odzdvds  16887  pythagtriplem11  16917  pythagtriplem13  16919  pythagtriplem19  16925  pcadd  16981  pcfaclem  16990  qexpz  16993  pockthlem  16997  pockthg  16998  prmreclem1  17008  prmreclem5  17012  4sqlem12  17048  4sqlem14  17050  4sqlem16  17052  vdwlem3  17075  vdwlem9  17081  ressmulgnnd  19201  psgnunilem3  19623  pgpfaclem2  20211  fvmptnn04ifd  23078  lebnumii  25194  dyadf  25819  dyadovol  25821  dyaddisjlem  25823  dyadmaxlem  25825  opnmbllem  25829  mbfi1fseqlem1  25943  mbfi1fseqlem4  25946  mbfi1fseqlem5  25947  mbfi1fseqlem6  25948  itg2gt0  25988  itg2cnlem2  25990  dgrcolem2  26500  rtprmirr  26997  leibpi  27179  log2tlbnd  27182  birthdaylem3  27190  amgm  27227  emcllem2  27233  harmonicbnd4  27247  lgamgulmlem1  27265  basellem1  27317  basellem4  27320  basellem6  27322  dvdsflf1o  27423  fsumfldivdiaglem  27425  fsumvma2  27450  chpchtsum  27455  perfectlem2  27466  bposlem1  27520  bposlem2  27521  bposlem6  27525  lgsqrlem4  27585  lgseisenlem1  27611  lgsquadlem1  27616  lgsquadlem2  27617  2sqlem8  27662  chebbnd1lem3  27707  rplogsumlem1  27720  rplogsumlem2  27721  rpvmasumlem  27723  dchrisumlema  27724  dchrisumlem1  27725  dchrisumlem3  27727  dchrisum0flblem2  27745  dchrisum0re  27749  logdivbnd  27792  pntpbnd1a  27821  pntpbnd1  27822  ostth2lem2  27870  ostth2lem3  27871  crctcsh  30292  clwwlknonex2  30579  minvecolem4  31361  cycpmrn  33583  fldextrspundgdvdslem  34190  eulerpartlemgc  34873  subfaclim  35767  cvmliftlem2  35865  cvmliftlem6  35869  cvmliftlem7  35870  cvmliftlem8  35871  cvmliftlem9  35872  cvmliftlem10  35873  cvmliftlem13  35875  knoppndvlem18  37226  knoppndvlem19  37227  knoppndvlem21  37229  poimirlem12  38381  poimirlem14  38383  poimirlem22  38391  opnmbllem0  38405  mblfinlem2  38407  lcmineqlem15  42909  aks4d1p1p3  42935  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p6  42947  aks4d1p8  42953  aks4d1p9  42954  posbezout  42966  aks6d1c1  42982  aks6d1c3  42989  aks6d1c4  42990  2ap1caineq  43011  sticksstones12a  43023  sticksstones12  43024  aks6d1c6lem4  43039  aks6d1c7lem1  43046  unitscyglem4  43064  unitscyglem5  43065  oexpreposd  43197  flt4lem5e  43502  flt4lem6  43504  flt4lem7  43505  irrapxlem4  43666  irrapxlem5  43667  pellexlem2  43671  pellexlem6  43675  rmxypos  43788  jm2.17b  43802  jm2.17c  43803  jm2.27a  43846  jm2.27c  43848  jm3.1lem1  43858  jm3.1lem2  43859  jm3.1lem3  43860  relexpxpmin  44557  hashnzfz2  45145  sumnnodd  46460  stoweidlem1  46829  stoweidlem11  46839  stoweidlem26  46854  stoweidlem38  46866  stoweidlem42  46870  stoweidlem44  46872  stoweidlem51  46879  stoweidlem59  46887  stirlinglem3  46904  stirlinglem15  46916  dirkertrigeqlem3  46928  dirkercncflem2  46932  fourierdlem11  46946  fourierdlem14  46949  fourierdlem20  46955  fourierdlem25  46960  fourierdlem37  46972  fourierdlem41  46976  fourierdlem48  46982  fourierdlem64  46998  fourierdlem73  47007  fourierdlem79  47013  fourierdlem93  47027  etransclem35  47097  etransclem48  47110  qndenserrnbllem  47122  hoiqssbllem1  47450  hoiqssbllem2  47451  cjnpoly  47757  2timesltsq  48266  lighneallem4a  48511  proththdlem  48516  stgrusgra  48875  ztprmneprm  49277  expnegico01  49448  dignnld  49533