Theorem nnge1d 12021

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

Syntax hints:   → wi 4   ∈ wcel 2106   class class class wbr 5074  1c1 10872   ≤ cle 11010  ℕcn 11973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-1cn 10929  ax-icn 10930  ax-addcl 10931  ax-addrcl 10932  ax-mulcl 10933  ax-mulrcl 10934  ax-mulcom 10935  ax-addass 10936  ax-mulass 10937  ax-distr 10938  ax-i2m1 10939  ax-1ne0 10940  ax-1rid 10941  ax-rnegex 10942  ax-rrecex 10943  ax-cnre 10944  ax-pre-lttri 10945  ax-pre-lttrn 10946  ax-pre-ltadd 10947  ax-pre-mulgt0 10948

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-mpo 7280  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-xr 11013  df-ltxr 11014  df-le 11015  df-sub 11207  df-neg 11208  df-nn 11974

This theorem is referenced by:  bernneq3  13946  facwordi  14003  faclbnd  14004  faclbnd3  14006  faclbnd4lem3  14009  facavg  14015  hashge1  14104  seqcoll  14178  wrdind  14435  wrd2ind  14436  eftlub  15818  eflegeo  15830  eirrlem  15913  divdenle  16453  eulerthlem2  16483  infpnlem2  16612  4sqlem11  16656  4sqlem12  16657  prmolefac  16747  2expltfac  16794  cshwshash  16806  fislw  19230  gzrngunitlem  20663  ovoliunlem1  24666  aalioulem2  25493  aalioulem4  25495  aalioulem5  25496  aaliou2b  25501  aaliou3lem2  25503  aaliou3lem8  25505  lgamgulmlem5  26182  vmage0  26270  chpge0  26275  vma1  26315  sqff1o  26331  fsumfldivdiaglem  26338  vmalelog  26353  chtublem  26359  fsumvma2  26362  chpchtsum  26367  logfacubnd  26369  perfectlem2  26378  dchrelbas4  26391  bposlem1  26432  bposlem2  26433  bposlem5  26436  lgsdir  26480  lgsdilem2  26481  lgseisenlem1  26523  2sqlem8  26574  chebbnd1lem1  26617  chebbnd1lem2  26618  chebbnd1lem3  26619  dchrisumlem3  26639  dchrisum0flblem1  26656  dchrisum0lem1b  26663  dirith2  26676  selbergb  26697  selberg3lem2  26706  pntrlog2bndlem1  26725  pntrlog2bndlem3  26727  pntrlog2bndlem4  26728  pntrlog2bndlem5  26729  pntrlog2bnd  26732  pntpbnd1a  26733  pntlemj  26751  pntlemk  26754  submateqlem2  31758  nexple  31977  plymulx0  32526  hgt750lemb  32636  poimirlem7  35784  poimirlem19  35796  poimirlem28  35805  lcmineqlem10  40046  lcmineqlem11  40047  lcmineqlem13  40049  lcmineqlem19  40055  lcmineqlem20  40056  aks4d1p1p2  40078  aks4d1p3  40086  aks4d1p5  40088  aks4d1p6  40089  aks4d1p8  40095  aks4d1p9  40096  sticksstones6  40107  sticksstones7  40108  sticksstones10  40111  sticksstones12a  40113  sticksstones12  40114  metakunt1  40125  metakunt2  40126  metakunt5  40129  metakunt10  40134  metakunt16  40140  metakunt21  40145  metakunt24  40148  metakunt26  40150  metakunt28  40152  metakunt29  40153  flt4lem7  40496  diophin  40594  irrapxlem4  40647  irrapxlem5  40648  pellexlem2  40652  pell14qrgapw  40698  pellfundgt1  40705  ltrmynn0  40770  jm2.27c  40829  jm3.1lem2  40840  fzisoeu  42839  fmuldfeq  43124  stoweidlem3  43544  stoweidlem20  43561  stoweidlem42  43583  stoweidlem51  43592  stoweidlem59  43600  stirlinglem8  43622  fourierdlem11  43659  fourierdlem41  43689  fourierdlem48  43695  fourierdlem79  43726  etransclem23  43798  etransclem28  43803  etransclem35  43810  etransclem38  43813  etransclem44  43819  etransc  43824  hoicvrrex  44094  iccpartlt  44876  lighneallem4a  45060  perfectALTVlem2  45174