Theorem nngt0d 12280

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  0cc0 11095   < clt 11238  ℕcn 12228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-1cn 11153  ax-icn 11154  ax-addcl 11155  ax-addrcl 11156  ax-mulcl 11157  ax-mulrcl 11158  ax-mulcom 11159  ax-addass 11160  ax-mulass 11161  ax-distr 11162  ax-i2m1 11163  ax-1ne0 11164  ax-1rid 11165  ax-rnegex 11166  ax-rrecex 11167  ax-cnre 11168  ax-pre-lttri 11169  ax-pre-lttrn 11170  ax-pre-ltadd 11171  ax-pre-mulgt0 11172

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244  df-sub 11438  df-neg 11439  df-nn 12229

This theorem is referenced by:  nnge2recico01  13529  expmulnbnd  14267  faclbnd5  14330  facubnd  14332  harmonic  15909  efcllem  16126  ege2le3  16139  eftlub  16160  eflegeo  16172  eirrlem  16255  bitsfzo  16488  sqgcd  16615  nn0expgcd  16617  prmind2  16738  nprm  16741  isprm5  16761  divdenle  16803  qnumgt0  16804  hashdvds  16829  odzdvds  16850  pythagtriplem11  16880  pythagtriplem13  16882  pythagtriplem19  16888  pcadd  16944  pcfaclem  16953  qexpz  16956  pockthlem  16960  pockthg  16961  prmreclem1  16971  prmreclem5  16975  4sqlem12  17011  4sqlem14  17013  4sqlem16  17015  vdwlem3  17038  vdwlem9  17044  ressmulgnnd  19139  psgnunilem3  19561  pgpfaclem2  20149  fvmptnn04ifd  23010  lebnumii  25125  dyadf  25750  dyadovol  25752  dyaddisjlem  25754  dyadmaxlem  25756  opnmbllem  25760  mbfi1fseqlem1  25874  mbfi1fseqlem4  25877  mbfi1fseqlem5  25878  mbfi1fseqlem6  25879  itg2gt0  25919  itg2cnlem2  25921  dgrcolem2  26431  rtprmirr  26925  leibpi  27107  log2tlbnd  27110  birthdaylem3  27118  amgm  27155  emcllem2  27161  harmonicbnd4  27175  lgamgulmlem1  27193  basellem1  27245  basellem4  27248  basellem6  27250  dvdsflf1o  27351  fsumfldivdiaglem  27353  fsumvma2  27378  chpchtsum  27383  perfectlem2  27394  bposlem1  27448  bposlem2  27449  bposlem6  27453  lgsqrlem4  27513  lgseisenlem1  27539  lgsquadlem1  27544  lgsquadlem2  27545  2sqlem8  27590  chebbnd1lem3  27635  rplogsumlem1  27648  rplogsumlem2  27649  rpvmasumlem  27651  dchrisumlema  27652  dchrisumlem1  27653  dchrisumlem3  27655  dchrisum0flblem2  27673  dchrisum0re  27677  logdivbnd  27720  pntpbnd1a  27749  pntpbnd1  27750  ostth2lem2  27798  ostth2lem3  27799  crctcsh  30173  clwwlknonex2  30460  minvecolem4  31232  cycpmrn  33463  fldextrspundgdvdslem  34070  eulerpartlemgc  34752  subfaclim  35680  cvmliftlem2  35778  cvmliftlem6  35782  cvmliftlem7  35783  cvmliftlem8  35784  cvmliftlem9  35785  cvmliftlem10  35786  cvmliftlem13  35788  knoppndvlem18  37118  knoppndvlem19  37119  knoppndvlem21  37121  poimirlem12  38283  poimirlem14  38285  poimirlem22  38293  opnmbllem0  38307  mblfinlem2  38309  lcmineqlem15  42810  aks4d1p1p3  42836  aks4d1p1p2  42837  aks4d1p1p4  42838  aks4d1p6  42848  aks4d1p8  42854  aks4d1p9  42855  posbezout  42867  aks6d1c1  42883  aks6d1c3  42890  aks6d1c4  42891  2ap1caineq  42912  sticksstones12a  42924  sticksstones12  42925  aks6d1c6lem4  42940  aks6d1c7lem1  42947  unitscyglem4  42965  unitscyglem5  42966  oexpreposd  43083  flt4lem5e  43388  flt4lem6  43390  flt4lem7  43391  irrapxlem4  43552  irrapxlem5  43553  pellexlem2  43557  pellexlem6  43561  rmxypos  43674  jm2.17b  43688  jm2.17c  43689  jm2.27a  43732  jm2.27c  43734  jm3.1lem1  43744  jm3.1lem2  43745  jm3.1lem3  43746  relexpxpmin  44443  hashnzfz2  45031  sumnnodd  46346  stoweidlem1  46715  stoweidlem11  46725  stoweidlem26  46740  stoweidlem38  46752  stoweidlem42  46756  stoweidlem44  46758  stoweidlem51  46765  stoweidlem59  46773  stirlinglem3  46790  stirlinglem15  46802  dirkertrigeqlem3  46814  dirkercncflem2  46818  fourierdlem11  46832  fourierdlem14  46835  fourierdlem20  46841  fourierdlem25  46846  fourierdlem37  46858  fourierdlem41  46862  fourierdlem48  46868  fourierdlem64  46884  fourierdlem73  46893  fourierdlem79  46899  fourierdlem93  46913  etransclem35  46983  etransclem48  46996  qndenserrnbllem  47008  hoiqssbllem1  47336  hoiqssbllem2  47337  cjnpoly  47626  2timesltsq  48115  lighneallem4a  48360  proththdlem  48365  stgrusgra  48724  ztprmneprm  49127  expnegico01  49298  dignnld  49383