Theorem nngt0d 12217

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

Syntax hints:   → wi 4   ∈ wcel 2114   class class class wbr 5086  0cc0 11029   < clt 11170  ℕcn 12165

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-pss 3910  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5519  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5577  df-we 5579  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-pred 6259  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-om 7811  df-2nd 7936  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166

This theorem is referenced by:  nnge2recico01  13451  expmulnbnd  14188  faclbnd5  14251  facubnd  14253  harmonic  15815  efcllem  16033  ege2le3  16046  eftlub  16067  eflegeo  16079  eirrlem  16162  bitsfzo  16395  sqgcd  16522  nn0expgcd  16524  prmind2  16645  nprm  16648  isprm5  16668  divdenle  16710  qnumgt0  16711  hashdvds  16736  odzdvds  16757  pythagtriplem11  16787  pythagtriplem13  16789  pythagtriplem19  16795  pcadd  16851  pcfaclem  16860  qexpz  16863  pockthlem  16867  pockthg  16868  prmreclem1  16878  prmreclem5  16882  4sqlem12  16918  4sqlem14  16920  4sqlem16  16922  vdwlem3  16945  vdwlem9  16951  ressmulgnnd  19045  psgnunilem3  19462  pgpfaclem2  20050  fvmptnn04ifd  22828  lebnumii  24943  dyadf  25568  dyadovol  25570  dyaddisjlem  25572  dyadmaxlem  25574  opnmbllem  25578  mbfi1fseqlem1  25692  mbfi1fseqlem4  25695  mbfi1fseqlem5  25696  mbfi1fseqlem6  25697  itg2gt0  25737  itg2cnlem2  25739  dgrcolem2  26249  rtprmirr  26737  leibpi  26919  log2tlbnd  26922  birthdaylem3  26930  amgm  26968  emcllem2  26974  harmonicbnd4  26988  lgamgulmlem1  27006  basellem1  27058  basellem4  27061  basellem6  27063  dvdsflf1o  27164  fsumfldivdiaglem  27166  fsumvma2  27191  chpchtsum  27196  perfectlem2  27207  bposlem1  27261  bposlem2  27262  bposlem6  27266  lgsqrlem4  27326  lgseisenlem1  27352  lgsquadlem1  27357  lgsquadlem2  27358  2sqlem8  27403  chebbnd1lem3  27448  rplogsumlem1  27461  rplogsumlem2  27462  rpvmasumlem  27464  dchrisumlema  27465  dchrisumlem1  27466  dchrisumlem3  27468  dchrisum0flblem2  27486  dchrisum0re  27490  logdivbnd  27533  pntpbnd1a  27562  pntpbnd1  27563  ostth2lem2  27611  ostth2lem3  27612  crctcsh  29907  clwwlknonex2  30194  minvecolem4  30966  cycpmrn  33219  fldextrspundgdvdslem  33840  eulerpartlemgc  34522  subfaclim  35386  cvmliftlem2  35484  cvmliftlem6  35488  cvmliftlem7  35489  cvmliftlem8  35490  cvmliftlem9  35491  cvmliftlem10  35492  cvmliftlem13  35494  knoppndvlem18  36805  knoppndvlem19  36806  knoppndvlem21  36808  poimirlem12  37967  poimirlem14  37969  poimirlem22  37977  opnmbllem0  37991  mblfinlem2  37993  lcmineqlem15  42496  aks4d1p1p3  42522  aks4d1p1p2  42523  aks4d1p1p4  42524  aks4d1p6  42534  aks4d1p8  42540  aks4d1p9  42541  posbezout  42553  aks6d1c1  42569  aks6d1c3  42576  aks6d1c4  42577  2ap1caineq  42598  sticksstones12a  42610  sticksstones12  42611  aks6d1c6lem4  42626  aks6d1c7lem1  42633  unitscyglem4  42651  unitscyglem5  42652  oexpreposd  42768  flt4lem5e  43103  flt4lem6  43105  flt4lem7  43106  irrapxlem4  43271  irrapxlem5  43272  pellexlem2  43276  pellexlem6  43280  rmxypos  43393  jm2.17b  43407  jm2.17c  43408  jm2.27a  43451  jm2.27c  43453  jm3.1lem1  43463  jm3.1lem2  43464  jm3.1lem3  43465  relexpxpmin  44162  hashnzfz2  44766  sumnnodd  46078  stoweidlem1  46447  stoweidlem11  46457  stoweidlem26  46472  stoweidlem38  46484  stoweidlem42  46488  stoweidlem44  46490  stoweidlem51  46497  stoweidlem59  46505  stirlinglem3  46522  stirlinglem15  46534  dirkertrigeqlem3  46546  dirkercncflem2  46550  fourierdlem11  46564  fourierdlem14  46567  fourierdlem20  46573  fourierdlem25  46578  fourierdlem37  46590  fourierdlem41  46594  fourierdlem48  46600  fourierdlem64  46616  fourierdlem73  46625  fourierdlem79  46631  fourierdlem93  46645  etransclem35  46715  etransclem48  46728  qndenserrnbllem  46740  hoiqssbllem1  47068  hoiqssbllem2  47069  cjnpoly  47349  2timesltsq  47838  lighneallem4a  48083  proththdlem  48088  stgrusgra  48447  ztprmneprm  48835  expnegico01  49006  dignnld  49091