Theorem nnge1d 12184

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

Syntax hints:   → wi 4   ∈ wcel 2113   class class class wbr 5095  1c1 11018   ≤ cle 11158  ℕcn 12136

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-resscn 11074  ax-1cn 11075  ax-icn 11076  ax-addcl 11077  ax-addrcl 11078  ax-mulcl 11079  ax-mulrcl 11080  ax-mulcom 11081  ax-addass 11082  ax-mulass 11083  ax-distr 11084  ax-i2m1 11085  ax-1ne0 11086  ax-1rid 11087  ax-rnegex 11088  ax-rrecex 11089  ax-cnre 11090  ax-pre-lttri 11091  ax-pre-lttrn 11092  ax-pre-ltadd 11093  ax-pre-mulgt0 11094

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6256  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-riota 7312  df-ov 7358  df-oprab 7359  df-mpo 7360  df-om 7806  df-2nd 7931  df-frecs 8220  df-wrecs 8251  df-recs 8300  df-rdg 8338  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163  df-sub 11357  df-neg 11358  df-nn 12137

This theorem is referenced by:  bernneq3  14145  facwordi  14203  faclbnd  14204  faclbnd3  14206  faclbnd4lem3  14209  facavg  14215  hashge1  14303  seqcoll  14378  wrdind  14636  wrd2ind  14637  eftlub  16025  eflegeo  16037  eirrlem  16120  divdenle  16667  eulerthlem2  16700  infpnlem2  16830  4sqlem11  16874  4sqlem12  16875  prmolefac  16965  2expltfac  17011  cshwshash  17023  fislw  19545  gzrngunitlem  21378  psdmul  22100  ovoliunlem1  25450  aalioulem2  26288  aalioulem4  26290  aalioulem5  26291  aaliou2b  26296  aaliou3lem2  26298  aaliou3lem8  26300  lgamgulmlem5  26990  vmage0  27078  chpge0  27083  vma1  27123  sqff1o  27139  fsumfldivdiaglem  27146  vmalelog  27163  chtublem  27169  fsumvma2  27172  chpchtsum  27177  logfacubnd  27179  perfectlem2  27188  dchrelbas4  27201  bposlem1  27242  bposlem2  27243  bposlem5  27246  lgsdir  27290  lgsdilem2  27291  lgseisenlem1  27333  2sqlem8  27384  chebbnd1lem1  27427  chebbnd1lem2  27428  chebbnd1lem3  27429  dchrisumlem3  27449  dchrisum0flblem1  27466  dchrisum0lem1b  27473  dirith2  27486  selbergb  27507  selberg3lem2  27516  pntrlog2bndlem1  27535  pntrlog2bndlem3  27537  pntrlog2bndlem4  27538  pntrlog2bndlem5  27539  pntrlog2bnd  27542  pntpbnd1a  27543  pntlemj  27561  pntlemk  27564  nexple  32853  mplmulmvr  33632  esplyind  33659  submateqlem2  33893  plymulx0  34632  hgt750lemb  34741  poimirlem7  37740  poimirlem19  37752  poimirlem28  37761  lcmineqlem10  42204  lcmineqlem11  42205  lcmineqlem13  42207  lcmineqlem19  42213  lcmineqlem20  42214  aks4d1p1p2  42236  aks4d1p3  42244  aks4d1p5  42246  aks4d1p6  42247  aks4d1p8  42253  aks4d1p9  42254  posbezout  42266  primrootspoweq0  42272  hashscontpow1  42287  aks6d1c2lem4  42293  sticksstones6  42317  sticksstones7  42318  sticksstones10  42321  sticksstones12a  42323  sticksstones12  42324  aks6d1c6lem4  42339  aks6d1c7lem2  42347  grpods  42360  unitscyglem2  42362  unitscyglem4  42364  unitscyglem5  42365  fimgmcyc  42704  flt4lem7  42817  diophin  42929  irrapxlem4  42982  irrapxlem5  42983  pellexlem2  42987  pell14qrgapw  43033  pellfundgt1  43040  ltrmynn0  43105  jm2.27c  43164  jm3.1lem2  43175  fzisoeu  45464  fmuldfeq  45745  stoweidlem3  46163  stoweidlem20  46180  stoweidlem42  46202  stoweidlem51  46211  stoweidlem59  46219  stirlinglem8  46241  fourierdlem11  46278  fourierdlem41  46308  fourierdlem48  46314  fourierdlem79  46345  etransclem23  46417  etransclem28  46422  etransclem35  46429  etransclem38  46432  etransclem44  46438  etransc  46443  hoicvrrex  46716  iccpartlt  47586  lighneallem4a  47770  perfectALTVlem2  47884