Theorem nngt0d 12206

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5100  0cc0 11038   < clt 11178  ℕcn 12157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-riota 7325  df-ov 7371  df-oprab 7372  df-mpo 7373  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184  df-sub 11378  df-neg 11379  df-nn 12158

This theorem is referenced by:  expmulnbnd  14170  faclbnd5  14233  facubnd  14235  harmonic  15794  efcllem  16012  ege2le3  16025  eftlub  16046  eflegeo  16058  eirrlem  16141  bitsfzo  16374  sqgcd  16501  nn0expgcd  16503  prmind2  16624  nprm  16627  isprm5  16646  divdenle  16688  qnumgt0  16689  hashdvds  16714  odzdvds  16735  pythagtriplem11  16765  pythagtriplem13  16767  pythagtriplem19  16773  pcadd  16829  pcfaclem  16838  qexpz  16841  pockthlem  16845  pockthg  16846  prmreclem1  16856  prmreclem5  16860  4sqlem12  16896  4sqlem14  16898  4sqlem16  16900  vdwlem3  16923  vdwlem9  16929  ressmulgnnd  19020  psgnunilem3  19437  pgpfaclem2  20025  fvmptnn04ifd  22809  lebnumii  24933  dyadf  25560  dyadovol  25562  dyaddisjlem  25564  dyadmaxlem  25566  opnmbllem  25570  mbfi1fseqlem1  25684  mbfi1fseqlem4  25687  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  itg2gt0  25729  itg2cnlem2  25731  dgrcolem2  26248  rtprmirr  26738  leibpi  26920  log2tlbnd  26923  birthdaylem3  26931  amgm  26969  emcllem2  26975  harmonicbnd4  26989  lgamgulmlem1  27007  basellem1  27059  basellem4  27062  basellem6  27064  dvdsflf1o  27165  fsumfldivdiaglem  27167  fsumvma2  27193  chpchtsum  27198  perfectlem2  27209  bposlem1  27263  bposlem2  27264  bposlem6  27268  lgsqrlem4  27328  lgseisenlem1  27354  lgsquadlem1  27359  lgsquadlem2  27360  2sqlem8  27405  chebbnd1lem3  27450  rplogsumlem1  27463  rplogsumlem2  27464  rpvmasumlem  27466  dchrisumlema  27467  dchrisumlem1  27468  dchrisumlem3  27470  dchrisum0flblem2  27488  dchrisum0re  27492  logdivbnd  27535  pntpbnd1a  27564  pntpbnd1  27565  ostth2lem2  27613  ostth2lem3  27614  crctcsh  29909  clwwlknonex2  30196  minvecolem4  30968  cycpmrn  33237  fldextrspundgdvdslem  33858  eulerpartlemgc  34540  subfaclim  35404  cvmliftlem2  35502  cvmliftlem6  35506  cvmliftlem7  35507  cvmliftlem8  35508  cvmliftlem9  35509  cvmliftlem10  35510  cvmliftlem13  35512  knoppndvlem18  36751  knoppndvlem19  36752  knoppndvlem21  36754  poimirlem12  37883  poimirlem14  37885  poimirlem22  37893  opnmbllem0  37907  mblfinlem2  37909  lcmineqlem15  42413  aks4d1p1p3  42439  aks4d1p1p2  42440  aks4d1p1p4  42441  aks4d1p6  42451  aks4d1p8  42457  aks4d1p9  42458  posbezout  42470  aks6d1c1  42486  aks6d1c3  42493  aks6d1c4  42494  2ap1caineq  42515  sticksstones12a  42527  sticksstones12  42528  aks6d1c6lem4  42543  aks6d1c7lem1  42550  unitscyglem4  42568  unitscyglem5  42569  oexpreposd  42692  flt4lem5e  43014  flt4lem6  43016  flt4lem7  43017  irrapxlem4  43182  irrapxlem5  43183  pellexlem2  43187  pellexlem6  43191  rmxypos  43304  jm2.17b  43318  jm2.17c  43319  jm2.27a  43362  jm2.27c  43364  jm3.1lem1  43374  jm3.1lem2  43375  jm3.1lem3  43376  relexpxpmin  44073  hashnzfz2  44677  sumnnodd  45990  stoweidlem1  46359  stoweidlem11  46369  stoweidlem26  46384  stoweidlem38  46396  stoweidlem42  46400  stoweidlem44  46402  stoweidlem51  46409  stoweidlem59  46417  stirlinglem3  46434  stirlinglem15  46446  dirkertrigeqlem3  46458  dirkercncflem2  46462  fourierdlem11  46476  fourierdlem14  46479  fourierdlem20  46485  fourierdlem25  46490  fourierdlem37  46502  fourierdlem41  46506  fourierdlem48  46512  fourierdlem64  46528  fourierdlem73  46537  fourierdlem79  46543  fourierdlem93  46557  etransclem35  46627  etransclem48  46640  qndenserrnbllem  46652  hoiqssbllem1  46980  hoiqssbllem2  46981  cjnpoly  47249  lighneallem4a  47968  proththdlem  47973  stgrusgra  48319  ztprmneprm  48707  expnegico01  48878  dignnld  48963