Theorem nnge1d 12314

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

Syntax hints:   → wi 4   ∈ wcel 2108   class class class wbr 5143  1c1 11156   ≤ cle 11296  ℕcn 12266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267

This theorem is referenced by:  bernneq3  14270  facwordi  14328  faclbnd  14329  faclbnd3  14331  faclbnd4lem3  14334  facavg  14340  hashge1  14428  seqcoll  14503  wrdind  14760  wrd2ind  14761  eftlub  16145  eflegeo  16157  eirrlem  16240  divdenle  16786  eulerthlem2  16819  infpnlem2  16949  4sqlem11  16993  4sqlem12  16994  prmolefac  17084  2expltfac  17130  cshwshash  17142  fislw  19643  gzrngunitlem  21450  psdmul  22170  ovoliunlem1  25537  aalioulem2  26375  aalioulem4  26377  aalioulem5  26378  aaliou2b  26383  aaliou3lem2  26385  aaliou3lem8  26387  lgamgulmlem5  27076  vmage0  27164  chpge0  27169  vma1  27209  sqff1o  27225  fsumfldivdiaglem  27232  vmalelog  27249  chtublem  27255  fsumvma2  27258  chpchtsum  27263  logfacubnd  27265  perfectlem2  27274  dchrelbas4  27287  bposlem1  27328  bposlem2  27329  bposlem5  27332  lgsdir  27376  lgsdilem2  27377  lgseisenlem1  27419  2sqlem8  27470  chebbnd1lem1  27513  chebbnd1lem2  27514  chebbnd1lem3  27515  dchrisumlem3  27535  dchrisum0flblem1  27552  dchrisum0lem1b  27559  dirith2  27572  selbergb  27593  selberg3lem2  27602  pntrlog2bndlem1  27621  pntrlog2bndlem3  27623  pntrlog2bndlem4  27624  pntrlog2bndlem5  27625  pntrlog2bnd  27628  pntpbnd1a  27629  pntlemj  27647  pntlemk  27650  nexple  32833  submateqlem2  33807  plymulx0  34562  hgt750lemb  34671  poimirlem7  37634  poimirlem19  37646  poimirlem28  37655  lcmineqlem10  42039  lcmineqlem11  42040  lcmineqlem13  42042  lcmineqlem19  42048  lcmineqlem20  42049  aks4d1p1p2  42071  aks4d1p3  42079  aks4d1p5  42081  aks4d1p6  42082  aks4d1p8  42088  aks4d1p9  42089  posbezout  42101  primrootspoweq0  42107  hashscontpow1  42122  aks6d1c2lem4  42128  sticksstones6  42152  sticksstones7  42153  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem4  42174  aks6d1c7lem2  42182  grpods  42195  unitscyglem2  42197  unitscyglem4  42199  unitscyglem5  42200  metakunt1  42206  metakunt2  42207  metakunt5  42210  metakunt10  42215  metakunt16  42221  metakunt21  42226  metakunt24  42229  metakunt26  42231  metakunt28  42233  metakunt29  42234  fimgmcyc  42544  flt4lem7  42669  diophin  42783  irrapxlem4  42836  irrapxlem5  42837  pellexlem2  42841  pell14qrgapw  42887  pellfundgt1  42894  ltrmynn0  42960  jm2.27c  43019  jm3.1lem2  43030  fzisoeu  45312  fmuldfeq  45598  stoweidlem3  46018  stoweidlem20  46035  stoweidlem42  46057  stoweidlem51  46066  stoweidlem59  46074  stirlinglem8  46096  fourierdlem11  46133  fourierdlem41  46163  fourierdlem48  46169  fourierdlem79  46200  etransclem23  46272  etransclem28  46277  etransclem35  46284  etransclem38  46287  etransclem44  46293  etransc  46298  hoicvrrex  46571  iccpartlt  47411  lighneallem4a  47595  perfectALTVlem2  47709