Theorem nnge1d 11481

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

Syntax hints:   → wi 4   ∈ wcel 2048   class class class wbr 4923  1c1 10328   ≤ cle 10467  ℕcn 11431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-resscn 10384  ax-1cn 10385  ax-icn 10386  ax-addcl 10387  ax-addrcl 10388  ax-mulcl 10389  ax-mulrcl 10390  ax-mulcom 10391  ax-addass 10392  ax-mulass 10393  ax-distr 10394  ax-i2m1 10395  ax-1ne0 10396  ax-1rid 10397  ax-rnegex 10398  ax-rrecex 10399  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402  ax-pre-ltadd 10403  ax-pre-mulgt0 10404

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-er 8081  df-en 8299  df-dom 8300  df-sdom 8301  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-sub 10664  df-neg 10665  df-nn 11432

This theorem is referenced by:  bernneq3  13400  facwordi  13457  faclbnd  13458  faclbnd3  13460  faclbnd4lem3  13463  facavg  13469  hashge1  13556  seqcoll  13625  wrdind  13905  wrdindOLD  13906  wrd2ind  13907  wrd2indOLD  13908  eftlub  15312  eflegeo  15324  eirrlem  15407  divdenle  15935  eulerthlem2  15965  infpnlem2  16093  4sqlem11  16137  4sqlem12  16138  prmolefac  16228  2expltfac  16272  cshwshash  16284  fislw  18501  gzrngunitlem  20302  ovoliunlem1  23796  aalioulem2  24615  aalioulem4  24617  aalioulem5  24618  aaliou2b  24623  aaliou3lem2  24625  aaliou3lem8  24627  lgamgulmlem5  25302  vmage0  25390  chpge0  25395  vma1  25435  sqff1o  25451  fsumfldivdiaglem  25458  vmalelog  25473  chtublem  25479  fsumvma2  25482  chpchtsum  25487  logfacubnd  25489  perfectlem2  25498  dchrelbas4  25511  bposlem1  25552  bposlem2  25553  bposlem5  25556  lgsdir  25600  lgsdilem2  25601  lgseisenlem1  25643  2sqlem8  25694  chebbnd1lem1  25737  chebbnd1lem2  25738  chebbnd1lem3  25739  dchrisumlem3  25759  dchrisum0flblem1  25776  dchrisum0lem1b  25783  dirith2  25796  selbergb  25817  selberg3lem2  25826  pntrlog2bndlem1  25845  pntrlog2bndlem3  25847  pntrlog2bndlem4  25848  pntrlog2bndlem5  25849  pntrlog2bnd  25852  pntpbnd1a  25853  pntlemj  25871  pntlemk  25874  submateqlem2  30672  nexple  30869  plymulx0  31424  hgt750lemb  31536  poimirlem7  34288  poimirlem19  34300  poimirlem28  34309  diophin  38710  irrapxlem4  38763  irrapxlem5  38764  pellexlem2  38768  pell14qrgapw  38814  pellfundgt1  38821  ltrmynn0  38886  jm2.27c  38945  jm3.1lem2  38956  fzisoeu  40942  fmuldfeq  41241  stoweidlem3  41665  stoweidlem20  41682  stoweidlem42  41704  stoweidlem51  41713  stoweidlem59  41721  stirlinglem8  41743  fourierdlem11  41780  fourierdlem41  41810  fourierdlem48  41816  fourierdlem79  41847  etransclem23  41919  etransclem28  41924  etransclem35  41931  etransclem38  41934  etransclem44  41940  etransc  41945  hoicvrrex  42215  iccpartlt  42902  lighneallem4a  43081  perfectALTVlem2  43195