Theorem nngt0d 12257

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5147  0cc0 11106   < clt 11244  ℕcn 12208

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-nn 12209

This theorem is referenced by:  expmulnbnd  14194  faclbnd5  14254  facubnd  14256  harmonic  15801  efcllem  16017  ege2le3  16029  eftlub  16048  eflegeo  16060  eirrlem  16143  bitsfzo  16372  sqgcd  16498  prmind2  16618  nprm  16621  isprm5  16640  divdenle  16681  qnumgt0  16682  hashdvds  16704  odzdvds  16724  pythagtriplem11  16754  pythagtriplem13  16756  pythagtriplem19  16762  pcadd  16818  pcfaclem  16827  qexpz  16830  pockthlem  16834  pockthg  16835  prmreclem1  16845  prmreclem5  16849  4sqlem12  16885  4sqlem14  16887  4sqlem16  16889  vdwlem3  16912  vdwlem9  16918  psgnunilem3  19358  pgpfaclem2  19946  fvmptnn04ifd  22346  lebnumii  24473  dyadf  25099  dyadovol  25101  dyaddisjlem  25103  dyadmaxlem  25105  opnmbllem  25109  mbfi1fseqlem1  25224  mbfi1fseqlem4  25227  mbfi1fseqlem5  25228  mbfi1fseqlem6  25229  itg2gt0  25269  itg2cnlem2  25271  dgrcolem2  25779  leibpi  26436  log2tlbnd  26439  birthdaylem3  26447  amgm  26484  emcllem2  26490  harmonicbnd4  26504  lgamgulmlem1  26522  basellem1  26574  basellem4  26577  basellem6  26579  dvdsflf1o  26680  fsumfldivdiaglem  26682  fsumvma2  26706  chpchtsum  26711  perfectlem2  26722  bposlem1  26776  bposlem2  26777  bposlem6  26781  lgsqrlem4  26841  lgseisenlem1  26867  lgsquadlem1  26872  lgsquadlem2  26873  2sqlem8  26918  chebbnd1lem3  26963  rplogsumlem1  26976  rplogsumlem2  26977  rpvmasumlem  26979  dchrisumlema  26980  dchrisumlem1  26981  dchrisumlem3  26983  dchrisum0flblem2  27001  dchrisum0re  27005  logdivbnd  27048  pntpbnd1a  27077  pntpbnd1  27078  ostth2lem2  27126  ostth2lem3  27127  crctcsh  29067  clwwlknonex2  29351  minvecolem4  30120  cycpmrn  32289  eulerpartlemgc  33349  subfaclim  34167  cvmliftlem2  34265  cvmliftlem6  34269  cvmliftlem7  34270  cvmliftlem8  34271  cvmliftlem9  34272  cvmliftlem10  34273  cvmliftlem13  34275  knoppndvlem18  35393  knoppndvlem19  35394  knoppndvlem21  35396  poimirlem12  36488  poimirlem14  36490  poimirlem22  36498  opnmbllem0  36512  mblfinlem2  36514  lcmineqlem15  40896  aks4d1p1p3  40922  aks4d1p1p2  40923  aks4d1p1p4  40924  aks4d1p6  40934  aks4d1p8  40940  aks4d1p9  40941  2ap1caineq  40949  sticksstones12a  40961  sticksstones12  40962  oexpreposd  41207  nn0expgcd  41221  rtprmirr  41233  flt4lem5e  41394  flt4lem6  41396  flt4lem7  41397  irrapxlem4  41548  irrapxlem5  41549  pellexlem2  41553  pellexlem6  41557  rmxypos  41671  jm2.17b  41685  jm2.17c  41686  jm2.27a  41729  jm2.27c  41731  jm3.1lem1  41741  jm3.1lem2  41742  jm3.1lem3  41743  relexpxpmin  42453  hashnzfz2  43065  sumnnodd  44332  stoweidlem1  44703  stoweidlem11  44713  stoweidlem26  44728  stoweidlem38  44740  stoweidlem42  44744  stoweidlem44  44746  stoweidlem51  44753  stoweidlem59  44761  stirlinglem3  44778  stirlinglem15  44790  dirkertrigeqlem3  44802  dirkercncflem2  44806  fourierdlem11  44820  fourierdlem14  44823  fourierdlem20  44829  fourierdlem25  44834  fourierdlem37  44846  fourierdlem41  44850  fourierdlem48  44856  fourierdlem64  44872  fourierdlem73  44881  fourierdlem79  44887  fourierdlem93  44901  etransclem35  44971  etransclem48  44984  qndenserrnbllem  44996  hoiqssbllem1  45324  hoiqssbllem2  45325  lighneallem4a  46262  proththdlem  46267  ztprmneprm  46976  expnegico01  47152  dignnld  47242