Theorem nngt0d 12295

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   class class class wbr 5112  0cc0 11110   < clt 11253  ℕcn 12243

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5260  ax-nul 5272  ax-pow 5339  ax-pr 5407  ax-un 7738  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4876  df-iun 4961  df-br 5113  df-opab 5177  df-mpt 5196  df-tr 5222  df-id 5559  df-eprel 5564  df-po 5572  df-so 5573  df-fr 5617  df-we 5619  df-xp 5670  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-res 5676  df-ima 5677  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7373  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7865  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8360  df-rdg 8399  df-er 8696  df-en 8946  df-dom 8947  df-sdom 8948  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11453  df-neg 11454  df-nn 12244

This theorem is used by:  nnge2recico01  13544  expmulnbnd  14282  faclbnd5  14345  facubnd  14347  harmonic  15924  efcllem  16141  ege2le3  16154  eftlub  16175  eflegeo  16187  eirrlem  16270  bitsfzo  16503  sqgcd  16630  nn0expgcd  16632  prmind2  16753  nprm  16756  isprm5  16776  divdenle  16818  qnumgt0  16819  hashdvds  16844  odzdvds  16865  pythagtriplem11  16895  pythagtriplem13  16897  pythagtriplem19  16903  pcadd  16959  pcfaclem  16968  qexpz  16971  pockthlem  16975  pockthg  16976  prmreclem1  16986  prmreclem5  16990  4sqlem12  17026  4sqlem14  17028  4sqlem16  17030  vdwlem3  17053  vdwlem9  17059  ressmulgnnd  19154  psgnunilem3  19576  pgpfaclem2  20164  fvmptnn04ifd  23025  lebnumii  25140  dyadf  25765  dyadovol  25767  dyaddisjlem  25769  dyadmaxlem  25771  opnmbllem  25775  mbfi1fseqlem1  25889  mbfi1fseqlem4  25892  mbfi1fseqlem5  25893  mbfi1fseqlem6  25894  itg2gt0  25934  itg2cnlem2  25936  dgrcolem2  26446  rtprmirr  26940  leibpi  27122  log2tlbnd  27125  birthdaylem3  27133  amgm  27170  emcllem2  27176  harmonicbnd4  27190  lgamgulmlem1  27208  basellem1  27260  basellem4  27263  basellem6  27265  dvdsflf1o  27366  fsumfldivdiaglem  27368  fsumvma2  27393  chpchtsum  27398  perfectlem2  27409  bposlem1  27463  bposlem2  27464  bposlem6  27468  lgsqrlem4  27528  lgseisenlem1  27554  lgsquadlem1  27559  lgsquadlem2  27560  2sqlem8  27605  chebbnd1lem3  27650  rplogsumlem1  27663  rplogsumlem2  27664  rpvmasumlem  27666  dchrisumlema  27667  dchrisumlem1  27668  dchrisumlem3  27670  dchrisum0flblem2  27688  dchrisum0re  27692  logdivbnd  27735  pntpbnd1a  27764  pntpbnd1  27765  ostth2lem2  27813  ostth2lem3  27814  crctcsh  30188  clwwlknonex2  30475  minvecolem4  31247  cycpmrn  33476  fldextrspundgdvdslem  34083  eulerpartlemgc  34765  subfaclim  35692  cvmliftlem2  35790  cvmliftlem6  35794  cvmliftlem7  35795  cvmliftlem8  35796  cvmliftlem9  35797  cvmliftlem10  35798  cvmliftlem13  35800  knoppndvlem18  37150  knoppndvlem19  37151  knoppndvlem21  37153  poimirlem12  38315  poimirlem14  38317  poimirlem22  38325  opnmbllem0  38339  mblfinlem2  38341  lcmineqlem15  42842  aks4d1p1p3  42868  aks4d1p1p2  42869  aks4d1p1p4  42870  aks4d1p6  42880  aks4d1p8  42886  aks4d1p9  42887  posbezout  42899  aks6d1c1  42915  aks6d1c3  42922  aks6d1c4  42923  2ap1caineq  42944  sticksstones12a  42956  sticksstones12  42957  aks6d1c6lem4  42972  aks6d1c7lem1  42979  unitscyglem4  42997  unitscyglem5  42998  oexpreposd  43115  flt4lem5e  43420  flt4lem6  43422  flt4lem7  43423  irrapxlem4  43584  irrapxlem5  43585  pellexlem2  43589  pellexlem6  43593  rmxypos  43706  jm2.17b  43720  jm2.17c  43721  jm2.27a  43764  jm2.27c  43766  jm3.1lem1  43776  jm3.1lem2  43777  jm3.1lem3  43778  relexpxpmin  44475  hashnzfz2  45063  sumnnodd  46378  stoweidlem1  46747  stoweidlem11  46757  stoweidlem26  46772  stoweidlem38  46784  stoweidlem42  46788  stoweidlem44  46790  stoweidlem51  46797  stoweidlem59  46805  stirlinglem3  46822  stirlinglem15  46834  dirkertrigeqlem3  46846  dirkercncflem2  46850  fourierdlem11  46864  fourierdlem14  46867  fourierdlem20  46873  fourierdlem25  46878  fourierdlem37  46890  fourierdlem41  46894  fourierdlem48  46900  fourierdlem64  46916  fourierdlem73  46925  fourierdlem79  46931  fourierdlem93  46945  etransclem35  47015  etransclem48  47028  qndenserrnbllem  47040  hoiqssbllem1  47368  hoiqssbllem2  47369  cjnpoly  47658  2timesltsq  48147  lighneallem4a  48392  proththdlem  48397  stgrusgra  48756  ztprmneprm  49159  expnegico01  49330  dignnld  49415