Theorem nngt0d 12380

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   class class class wbr 5103  0cc0 11193   < clt 11336  ℕcn 12328

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-1cn 11251  ax-icn 11252  ax-addcl 11253  ax-addrcl 11254  ax-mulcl 11255  ax-mulrcl 11256  ax-mulcom 11257  ax-addass 11258  ax-mulass 11259  ax-distr 11260  ax-i2m1 11261  ax-1ne0 11262  ax-1rid 11263  ax-rnegex 11264  ax-rrecex 11265  ax-cnre 11266  ax-pre-lttri 11267  ax-pre-lttrn 11268  ax-pre-ltadd 11269  ax-pre-mulgt0 11270

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-iun 4953  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7375  df-ov 7421  df-oprab 7422  df-mpo 7423  df-om 7876  df-2nd 8000  df-frecs 8292  df-wrecs 8323  df-recs 8372  df-rdg 8411  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342  df-sub 11536  df-neg 11537  df-nn 12329

This theorem is used by:  nnge2recico01  13631  expmulnbnd  14372  faclbnd5  14435  facubnd  14437  harmonic  16021  efcllem  16236  ege2le3  16249  eftlub  16270  eflegeo  16282  eirrlem  16365  bitsfzo  16598  sqgcd  16729  nn0expgcd  16731  prmind2  16853  nprm  16856  isprm5  16876  divdenle  16918  qnumgt0  16919  hashdvds  16945  odzdvds  16966  pythagtriplem11  16996  pythagtriplem13  16998  pythagtriplem19  17004  pcadd  17060  pcfaclem  17069  qexpz  17072  pockthlem  17076  pockthg  17077  prmreclem1  17087  prmreclem5  17091  4sqlem12  17127  4sqlem14  17129  4sqlem16  17131  vdwlem3  17154  vdwlem9  17160  ressmulgnnd  19281  psgnunilem3  19703  pgpfaclem2  20291  fvmptnn04ifd  23164  lebnumii  25280  dyadf  25905  dyadovol  25907  dyaddisjlem  25909  dyadmaxlem  25911  opnmbllem  25915  mbfi1fseqlem1  26029  mbfi1fseqlem4  26032  mbfi1fseqlem5  26033  mbfi1fseqlem6  26034  itg2gt0  26074  itg2cnlem2  26076  dgrcolem2  26586  rtprmirr  27081  leibpi  27263  log2tlbnd  27266  birthdaylem3  27274  amgm  27311  emcllem2  27317  harmonicbnd4  27331  lgamgulmlem1  27349  basellem1  27401  basellem4  27404  basellem6  27406  dvdsflf1o  27507  fsumfldivdiaglem  27509  fsumvma2  27534  chpchtsum  27539  perfectlem2  27550  bposlem1  27604  bposlem2  27605  bposlem6  27609  lgsqrlem4  27669  lgseisenlem1  27695  lgsquadlem1  27700  lgsquadlem2  27701  2sqlem8  27746  chebbnd1lem3  27791  rplogsumlem1  27804  rplogsumlem2  27805  rpvmasumlem  27807  dchrisumlema  27808  dchrisumlem1  27809  dchrisumlem3  27811  dchrisum0flblem2  27829  dchrisum0re  27833  logdivbnd  27876  pntpbnd1a  27905  pntpbnd1  27906  ostth2lem2  27954  ostth2lem3  27955  flt4lem5e  27979  flt4lem6  27981  flt4lem7  27982  crctcsh  30406  clwwlknonex2  30693  minvecolem4  31475  cycpmrn  33697  fldextrspundgdvdslem  34305  eulerpartlemgc  34987  subfaclim  35932  cvmliftlem2  36030  cvmliftlem6  36034  cvmliftlem7  36035  cvmliftlem8  36036  cvmliftlem9  36037  cvmliftlem10  36038  cvmliftlem13  36040  knoppndvlem18  37375  knoppndvlem19  37376  knoppndvlem21  37378  poimirlem12  38530  poimirlem14  38532  poimirlem22  38540  opnmbllem0  38554  mblfinlem2  38556  lcmineqlem15  43073  aks4d1p1p3  43099  aks4d1p1p2  43100  aks4d1p1p4  43101  aks4d1p6  43111  aks4d1p8  43117  aks4d1p9  43118  posbezout  43130  aks6d1c1  43146  aks6d1c3  43153  aks6d1c4  43154  2ap1caineq  43175  sticksstones12a  43187  sticksstones12  43188  aks6d1c6lem4  43203  aks6d1c7lem1  43210  unitscyglem4  43228  unitscyglem5  43229  oexpreposd  43359  irrapxlem4  43811  irrapxlem5  43812  pellexlem2  43816  pellexlem6  43820  rmxypos  43933  jm2.17b  43947  jm2.17c  43948  jm2.27a  43991  jm2.27c  43993  jm3.1lem1  44003  jm3.1lem2  44004  jm3.1lem3  44005  relexpxpmin  44702  hashnzfz2  45290  sumnnodd  46611  stoweidlem1  46980  stoweidlem11  46990  stoweidlem26  47005  stoweidlem38  47017  stoweidlem42  47021  stoweidlem44  47023  stoweidlem51  47030  stoweidlem59  47038  stirlinglem3  47055  stirlinglem15  47067  dirkertrigeqlem3  47079  dirkercncflem2  47083  fourierdlem11  47097  fourierdlem14  47100  fourierdlem20  47106  fourierdlem25  47111  fourierdlem37  47123  fourierdlem41  47127  fourierdlem48  47133  fourierdlem64  47149  fourierdlem73  47158  fourierdlem79  47164  fourierdlem93  47178  etransclem35  47248  etransclem48  47261  qndenserrnbllem  47273  hoiqssbllem1  47601  hoiqssbllem2  47602  cjnpoly  47908  2timesltsq  48417  lighneallem4a  48662  proththdlem  48667  stgrusgra  49026  ztprmneprm  49428  expnegico01  49599  dignnld  49684