Theorem nngt0d 12308

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

Syntax hints:   → wi 4   ∈ wcel 2098   class class class wbr 5152  0cc0 11154   < clt 11294  ℕcn 12259

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5303  ax-nul 5310  ax-pow 5368  ax-pr 5432  ax-un 7745  ax-resscn 11211  ax-1cn 11212  ax-icn 11213  ax-addcl 11214  ax-addrcl 11215  ax-mulcl 11216  ax-mulrcl 11217  ax-mulcom 11218  ax-addass 11219  ax-mulass 11220  ax-distr 11221  ax-i2m1 11222  ax-1ne0 11223  ax-1rid 11224  ax-rnegex 11225  ax-rrecex 11226  ax-cnre 11227  ax-pre-lttri 11228  ax-pre-lttrn 11229  ax-pre-ltadd 11230  ax-pre-mulgt0 11231

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4325  df-if 4533  df-pw 4608  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-iun 5002  df-br 5153  df-opab 5215  df-mpt 5236  df-tr 5270  df-id 5579  df-eprel 5585  df-po 5593  df-so 5594  df-fr 5636  df-we 5638  df-xp 5687  df-rel 5688  df-cnv 5689  df-co 5690  df-dm 5691  df-rn 5692  df-res 5693  df-ima 5694  df-pred 6311  df-ord 6378  df-on 6379  df-lim 6380  df-suc 6381  df-iota 6505  df-fun 6555  df-fn 6556  df-f 6557  df-f1 6558  df-fo 6559  df-f1o 6560  df-fv 6561  df-riota 7379  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7876  df-2nd 8003  df-frecs 8295  df-wrecs 8326  df-recs 8400  df-rdg 8439  df-er 8733  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11296  df-mnf 11297  df-xr 11298  df-ltxr 11299  df-le 11300  df-sub 11492  df-neg 11493  df-nn 12260

This theorem is referenced by:  expmulnbnd  14247  faclbnd5  14310  facubnd  14312  harmonic  15858  efcllem  16074  ege2le3  16087  eftlub  16106  eflegeo  16118  eirrlem  16201  bitsfzo  16430  sqgcd  16558  nn0expgcd  16560  prmind2  16681  nprm  16684  isprm5  16703  divdenle  16746  qnumgt0  16747  hashdvds  16772  odzdvds  16792  pythagtriplem11  16822  pythagtriplem13  16824  pythagtriplem19  16830  pcadd  16886  pcfaclem  16895  qexpz  16898  pockthlem  16902  pockthg  16903  prmreclem1  16913  prmreclem5  16917  4sqlem12  16953  4sqlem14  16955  4sqlem16  16957  vdwlem3  16980  vdwlem9  16986  ressmulgnnd  19067  psgnunilem3  19489  pgpfaclem2  20077  fvmptnn04ifd  22838  lebnumii  24975  dyadf  25603  dyadovol  25605  dyaddisjlem  25607  dyadmaxlem  25609  opnmbllem  25613  mbfi1fseqlem1  25728  mbfi1fseqlem4  25731  mbfi1fseqlem5  25732  mbfi1fseqlem6  25733  itg2gt0  25773  itg2cnlem2  25775  dgrcolem2  26294  rtprmirr  26780  leibpi  26962  log2tlbnd  26965  birthdaylem3  26973  amgm  27011  emcllem2  27017  harmonicbnd4  27031  lgamgulmlem1  27049  basellem1  27101  basellem4  27104  basellem6  27106  dvdsflf1o  27207  fsumfldivdiaglem  27209  fsumvma2  27235  chpchtsum  27240  perfectlem2  27251  bposlem1  27305  bposlem2  27306  bposlem6  27310  lgsqrlem4  27370  lgseisenlem1  27396  lgsquadlem1  27401  lgsquadlem2  27402  2sqlem8  27447  chebbnd1lem3  27492  rplogsumlem1  27505  rplogsumlem2  27506  rpvmasumlem  27508  dchrisumlema  27509  dchrisumlem1  27510  dchrisumlem3  27512  dchrisum0flblem2  27530  dchrisum0re  27534  logdivbnd  27577  pntpbnd1a  27606  pntpbnd1  27607  ostth2lem2  27655  ostth2lem3  27656  crctcsh  29750  clwwlknonex2  30034  minvecolem4  30805  cycpmrn  32998  eulerpartlemgc  34152  subfaclim  34968  cvmliftlem2  35066  cvmliftlem6  35070  cvmliftlem7  35071  cvmliftlem8  35072  cvmliftlem9  35073  cvmliftlem10  35074  cvmliftlem13  35076  knoppndvlem18  36180  knoppndvlem19  36181  knoppndvlem21  36183  poimirlem12  37281  poimirlem14  37283  poimirlem22  37291  opnmbllem0  37305  mblfinlem2  37307  lcmineqlem15  41690  aks4d1p1p3  41716  aks4d1p1p2  41717  aks4d1p1p4  41718  aks4d1p6  41728  aks4d1p8  41734  aks4d1p9  41735  posbezout  41746  aks6d1c1  41762  aks6d1c3  41769  aks6d1c4  41770  2ap1caineq  41791  sticksstones12a  41803  sticksstones12  41804  aks6d1c6lem4  41819  aks6d1c7lem1  41826  oexpreposd  42062  flt4lem5e  42247  flt4lem6  42249  flt4lem7  42250  irrapxlem4  42419  irrapxlem5  42420  pellexlem2  42424  pellexlem6  42428  rmxypos  42542  jm2.17b  42556  jm2.17c  42557  jm2.27a  42600  jm2.27c  42602  jm3.1lem1  42612  jm3.1lem2  42613  jm3.1lem3  42614  relexpxpmin  43321  hashnzfz2  43932  sumnnodd  45188  stoweidlem1  45559  stoweidlem11  45569  stoweidlem26  45584  stoweidlem38  45596  stoweidlem42  45600  stoweidlem44  45602  stoweidlem51  45609  stoweidlem59  45617  stirlinglem3  45634  stirlinglem15  45646  dirkertrigeqlem3  45658  dirkercncflem2  45662  fourierdlem11  45676  fourierdlem14  45679  fourierdlem20  45685  fourierdlem25  45690  fourierdlem37  45702  fourierdlem41  45706  fourierdlem48  45712  fourierdlem64  45728  fourierdlem73  45737  fourierdlem79  45743  fourierdlem93  45757  etransclem35  45827  etransclem48  45840  qndenserrnbllem  45852  hoiqssbllem1  46180  hoiqssbllem2  46181  lighneallem4a  47117  proththdlem  47122  ztprmneprm  47663  expnegico01  47838  dignnld  47928