Theorem nngt0d 12427

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5108  0cc0 11239   < clt 11382  ℕcn 12375

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316

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 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-nn 12376

This theorem is used by:  nnge2recico01  13678  expmulnbnd  14420  faclbnd5  14483  facubnd  14485  harmonic  16072  efcllem  16287  ege2le3  16300  eftlub  16321  eflegeo  16333  eirrlem  16416  bitsfzo  16649  sqgcd  16780  nn0expgcd  16782  prmind2  16904  nprm  16907  isprm5  16927  divdenle  16969  qnumgt0  16970  hashdvds  16996  odzdvds  17017  pythagtriplem11  17047  pythagtriplem13  17049  pythagtriplem19  17055  pcadd  17111  pcfaclem  17120  qexpz  17123  pockthlem  17127  pockthg  17128  prmreclem1  17138  prmreclem5  17142  4sqlem12  17178  4sqlem14  17180  4sqlem16  17182  vdwlem3  17205  vdwlem9  17211  ressmulgnnd  19338  psgnunilem3  19761  pgpfaclem2  20349  fvmptnn04ifd  23226  lebnumii  25342  dyadf  25967  dyadovol  25969  dyaddisjlem  25971  dyadmaxlem  25973  opnmbllem  25977  mbfi1fseqlem1  26091  mbfi1fseqlem4  26094  mbfi1fseqlem5  26095  mbfi1fseqlem6  26096  itg2gt0  26136  itg2cnlem2  26138  dgrcolem2  26648  rtprmirr  27145  leibpi  27327  log2tlbnd  27330  birthdaylem3  27338  amgm  27375  emcllem2  27381  harmonicbnd4  27395  lgamgulmlem1  27413  basellem1  27465  basellem4  27468  basellem6  27470  dvdsflf1o  27571  fsumfldivdiaglem  27573  fsumvma2  27598  chpchtsum  27603  perfectlem2  27614  bposlem1  27668  bposlem2  27669  bposlem6  27673  lgsqrlem4  27733  lgseisenlem1  27759  lgsquadlem1  27764  lgsquadlem2  27765  2sqlem8  27810  chebbnd1lem3  27855  rplogsumlem1  27868  rplogsumlem2  27869  rpvmasumlem  27871  dchrisumlema  27872  dchrisumlem1  27873  dchrisumlem3  27875  dchrisum0flblem2  27893  dchrisum0re  27897  logdivbnd  27940  pntpbnd1a  27969  pntpbnd1  27970  ostth2lem2  28018  ostth2lem3  28019  flt4lem5e  28043  flt4lem6  28045  flt4lem7  28046  crctcsh  30470  clwwlknonex2  30757  minvecolem4  31539  cycpmrn  33803  fldextrspundgdvdslem  34423  eulerpartlemgc  35105  subfaclim  36161  cvmliftlem2  36259  cvmliftlem6  36263  cvmliftlem7  36264  cvmliftlem8  36265  cvmliftlem9  36266  cvmliftlem10  36267  cvmliftlem13  36269  knoppndvlem18  37610  knoppndvlem19  37611  knoppndvlem21  37613  poimirlem12  38818  poimirlem14  38820  poimirlem22  38828  opnmbllem0  38842  mblfinlem2  38844  lcmineqlem15  43359  aks4d1p1p3  43385  aks4d1p1p2  43386  aks4d1p1p4  43387  aks4d1p6  43397  aks4d1p8  43403  aks4d1p9  43404  posbezout  43416  aks6d1c1  43432  aks6d1c3  43439  aks6d1c4  43440  2ap1caineq  43461  sticksstones12a  43473  sticksstones12  43474  aks6d1c6lem4  43489  aks6d1c7lem1  43496  unitscyglem4  43514  unitscyglem5  43515  oexpreposd  43645  irrapxlem4  44098  irrapxlem5  44099  pellexlem2  44103  pellexlem6  44107  rmxypos  44220  jm2.17b  44234  jm2.17c  44235  jm2.27a  44278  jm2.27c  44280  jm3.1lem1  44290  jm3.1lem2  44291  jm3.1lem3  44292  relexpxpmin  44978  hashnzfz2  45566  sumnnodd  46915  stoweidlem1  47284  stoweidlem11  47294  stoweidlem26  47309  stoweidlem38  47321  stoweidlem42  47325  stoweidlem44  47327  stoweidlem51  47334  stoweidlem59  47342  stirlinglem3  47359  stirlinglem15  47371  dirkertrigeqlem3  47383  dirkercncflem2  47387  fourierdlem11  47401  fourierdlem14  47404  fourierdlem20  47410  fourierdlem25  47415  fourierdlem37  47427  fourierdlem41  47431  fourierdlem48  47437  fourierdlem64  47453  fourierdlem73  47462  fourierdlem79  47468  fourierdlem93  47482  etransclem35  47552  etransclem48  47565  qndenserrnbllem  47577  hoiqssbllem1  47905  hoiqssbllem2  47906  cjnpoly  48212  2timesltsq  48721  lighneallem4a  48966  proththdlem  48971  stgrusgra  49330  ztprmneprm  49790  expnegico01  49961  dignnld  50046