Theorem nngt0d 12211

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

Syntax hints:   → wi 4   ∈ wcel 2109   class class class wbr 5102  0cc0 11044   < clt 11184  ℕcn 12162

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-nn 12163

This theorem is referenced by:  expmulnbnd  14176  faclbnd5  14239  facubnd  14241  harmonic  15801  efcllem  16019  ege2le3  16032  eftlub  16053  eflegeo  16065  eirrlem  16148  bitsfzo  16381  sqgcd  16508  nn0expgcd  16510  prmind2  16631  nprm  16634  isprm5  16653  divdenle  16695  qnumgt0  16696  hashdvds  16721  odzdvds  16742  pythagtriplem11  16772  pythagtriplem13  16774  pythagtriplem19  16780  pcadd  16836  pcfaclem  16845  qexpz  16848  pockthlem  16852  pockthg  16853  prmreclem1  16863  prmreclem5  16867  4sqlem12  16903  4sqlem14  16905  4sqlem16  16907  vdwlem3  16930  vdwlem9  16936  ressmulgnnd  18986  psgnunilem3  19402  pgpfaclem2  19990  fvmptnn04ifd  22716  lebnumii  24841  dyadf  25468  dyadovol  25470  dyaddisjlem  25472  dyadmaxlem  25474  opnmbllem  25478  mbfi1fseqlem1  25592  mbfi1fseqlem4  25595  mbfi1fseqlem5  25596  mbfi1fseqlem6  25597  itg2gt0  25637  itg2cnlem2  25639  dgrcolem2  26156  rtprmirr  26646  leibpi  26828  log2tlbnd  26831  birthdaylem3  26839  amgm  26877  emcllem2  26883  harmonicbnd4  26897  lgamgulmlem1  26915  basellem1  26967  basellem4  26970  basellem6  26972  dvdsflf1o  27073  fsumfldivdiaglem  27075  fsumvma2  27101  chpchtsum  27106  perfectlem2  27117  bposlem1  27171  bposlem2  27172  bposlem6  27176  lgsqrlem4  27236  lgseisenlem1  27262  lgsquadlem1  27267  lgsquadlem2  27268  2sqlem8  27313  chebbnd1lem3  27358  rplogsumlem1  27371  rplogsumlem2  27372  rpvmasumlem  27374  dchrisumlema  27375  dchrisumlem1  27376  dchrisumlem3  27378  dchrisum0flblem2  27396  dchrisum0re  27400  logdivbnd  27443  pntpbnd1a  27472  pntpbnd1  27473  ostth2lem2  27521  ostth2lem3  27522  crctcsh  29727  clwwlknonex2  30011  minvecolem4  30782  cycpmrn  33073  fldextrspundgdvdslem  33648  eulerpartlemgc  34326  subfaclim  35148  cvmliftlem2  35246  cvmliftlem6  35250  cvmliftlem7  35251  cvmliftlem8  35252  cvmliftlem9  35253  cvmliftlem10  35254  cvmliftlem13  35256  knoppndvlem18  36490  knoppndvlem19  36491  knoppndvlem21  36493  poimirlem12  37599  poimirlem14  37601  poimirlem22  37609  opnmbllem0  37623  mblfinlem2  37625  lcmineqlem15  42004  aks4d1p1p3  42030  aks4d1p1p2  42031  aks4d1p1p4  42032  aks4d1p6  42042  aks4d1p8  42048  aks4d1p9  42049  posbezout  42061  aks6d1c1  42077  aks6d1c3  42084  aks6d1c4  42085  2ap1caineq  42106  sticksstones12a  42118  sticksstones12  42119  aks6d1c6lem4  42134  aks6d1c7lem1  42141  unitscyglem4  42159  unitscyglem5  42160  oexpreposd  42283  flt4lem5e  42617  flt4lem6  42619  flt4lem7  42620  irrapxlem4  42786  irrapxlem5  42787  pellexlem2  42791  pellexlem6  42795  rmxypos  42909  jm2.17b  42923  jm2.17c  42924  jm2.27a  42967  jm2.27c  42969  jm3.1lem1  42979  jm3.1lem2  42980  jm3.1lem3  42981  relexpxpmin  43679  hashnzfz2  44283  sumnnodd  45601  stoweidlem1  45972  stoweidlem11  45982  stoweidlem26  45997  stoweidlem38  46009  stoweidlem42  46013  stoweidlem44  46015  stoweidlem51  46022  stoweidlem59  46030  stirlinglem3  46047  stirlinglem15  46059  dirkertrigeqlem3  46071  dirkercncflem2  46075  fourierdlem11  46089  fourierdlem14  46092  fourierdlem20  46098  fourierdlem25  46103  fourierdlem37  46115  fourierdlem41  46119  fourierdlem48  46125  fourierdlem64  46141  fourierdlem73  46150  fourierdlem79  46156  fourierdlem93  46170  etransclem35  46240  etransclem48  46253  qndenserrnbllem  46265  hoiqssbllem1  46593  hoiqssbllem2  46594  cjnpoly  46863  lighneallem4a  47582  proththdlem  47587  stgrusgra  47931  ztprmneprm  48308  expnegico01  48480  dignnld  48565