Theorem nnge1d 12101

Description: A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)

Hypothesis

Ref	Expression
nnge1d.1	⊢ (𝜑 → 𝐴 ∈ ℕ)

Assertion

Ref	Expression
nnge1d	⊢ (𝜑 → 1 ≤ 𝐴)

Proof of Theorem nnge1d

Step	Hyp	Ref	Expression
1		nnge1d.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2		nnge1 12081	. 2 ⊢ (𝐴 ∈ ℕ → 1 ≤ 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 1 ≤ 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2105   class class class wbr 5087  1c1 10952   ≤ cle 11090  ℕcn 12053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-om 7760  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-er 8548  df-en 8784  df-dom 8785  df-sdom 8786  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-nn 12054

This theorem is referenced by:  bernneq3  14026  facwordi  14083  faclbnd  14084  faclbnd3  14086  faclbnd4lem3  14089  facavg  14095  hashge1  14183  seqcoll  14257  wrdind  14514  wrd2ind  14515  eftlub  15897  eflegeo  15909  eirrlem  15992  divdenle  16530  eulerthlem2  16560  infpnlem2  16689  4sqlem11  16733  4sqlem12  16734  prmolefac  16824  2expltfac  16871  cshwshash  16883  fislw  19306  gzrngunitlem  20746  ovoliunlem1  24749  aalioulem2  25576  aalioulem4  25578  aalioulem5  25579  aaliou2b  25584  aaliou3lem2  25586  aaliou3lem8  25588  lgamgulmlem5  26265  vmage0  26353  chpge0  26358  vma1  26398  sqff1o  26414  fsumfldivdiaglem  26421  vmalelog  26436  chtublem  26442  fsumvma2  26445  chpchtsum  26450  logfacubnd  26452  perfectlem2  26461  dchrelbas4  26474  bposlem1  26515  bposlem2  26516  bposlem5  26519  lgsdir  26563  lgsdilem2  26564  lgseisenlem1  26606  2sqlem8  26657  chebbnd1lem1  26700  chebbnd1lem2  26701  chebbnd1lem3  26702  dchrisumlem3  26722  dchrisum0flblem1  26739  dchrisum0lem1b  26746  dirith2  26759  selbergb  26780  selberg3lem2  26789  pntrlog2bndlem1  26808  pntrlog2bndlem3  26810  pntrlog2bndlem4  26811  pntrlog2bndlem5  26812  pntrlog2bnd  26815  pntpbnd1a  26816  pntlemj  26834  pntlemk  26837  submateqlem2  31898  nexple  32117  plymulx0  32666  hgt750lemb  32776  poimirlem7  35856  poimirlem19  35868  poimirlem28  35877  lcmineqlem10  40267  lcmineqlem11  40268  lcmineqlem13  40270  lcmineqlem19  40276  lcmineqlem20  40277  aks4d1p1p2  40299  aks4d1p3  40307  aks4d1p5  40309  aks4d1p6  40310  aks4d1p8  40316  aks4d1p9  40317  sticksstones6  40331  sticksstones7  40332  sticksstones10  40335  sticksstones12a  40337  sticksstones12  40338  metakunt1  40349  metakunt2  40350  metakunt5  40353  metakunt10  40358  metakunt16  40364  metakunt21  40369  metakunt24  40372  metakunt26  40374  metakunt28  40376  metakunt29  40377  flt4lem7  40712  diophin  40810  irrapxlem4  40863  irrapxlem5  40864  pellexlem2  40868  pell14qrgapw  40914  pellfundgt1  40921  ltrmynn0  40987  jm2.27c  41046  jm3.1lem2  41057  fzisoeu  43088  fmuldfeq  43374  stoweidlem3  43794  stoweidlem20  43811  stoweidlem42  43833  stoweidlem51  43842  stoweidlem59  43850  stirlinglem8  43872  fourierdlem11  43909  fourierdlem41  43939  fourierdlem48  43945  fourierdlem79  43976  etransclem23  44048  etransclem28  44053  etransclem35  44060  etransclem38  44063  etransclem44  44069  etransc  44074  hoicvrrex  44345  iccpartlt  45141  lighneallem4a  45325  perfectALTVlem2  45439