Theorem nnge1d 12255

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

Syntax hints:   → wi 4   ∈ wcel 2141   class class class wbr 5097  1c1 11068   ≤ cle 11211  ℕcn 12204

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-resscn 11124  ax-1cn 11125  ax-icn 11126  ax-addcl 11127  ax-addrcl 11128  ax-mulcl 11129  ax-mulrcl 11130  ax-mulcom 11131  ax-addass 11132  ax-mulass 11133  ax-distr 11134  ax-i2m1 11135  ax-1ne0 11136  ax-1rid 11137  ax-rnegex 11138  ax-rrecex 11139  ax-cnre 11140  ax-pre-lttri 11141  ax-pre-lttrn 11142  ax-pre-ltadd 11143  ax-pre-mulgt0 11144

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-iun 4948  df-br 5098  df-opab 5160  df-mpt 5179  df-tr 5205  df-id 5538  df-eprel 5543  df-po 5551  df-so 5552  df-fr 5596  df-we 5598  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-pred 6283  df-ord 6344  df-on 6345  df-lim 6346  df-suc 6347  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-riota 7348  df-ov 7394  df-oprab 7395  df-mpo 7396  df-om 7842  df-2nd 7966  df-frecs 8256  df-wrecs 8287  df-recs 8336  df-rdg 8375  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216  df-sub 11410  df-neg 11411  df-nn 12205

This theorem is referenced by:  bernneq3  14238  facwordi  14296  faclbnd  14297  faclbnd3  14299  faclbnd4lem3  14302  facavg  14308  hashge1  14396  seqcoll  14471  wrdind  14729  wrd2ind  14730  eftlub  16132  eflegeo  16144  eirrlem  16227  divdenle  16775  eulerthlem2  16808  infpnlem2  16938  4sqlem11  16982  4sqlem12  16983  prmolefac  17073  2expltfac  17119  cshwshash  17131  fislw  19656  gzrngunitlem  21472  psdmul  22219  ovoliunlem1  25552  plyn0mulidp  26333  aalioulem2  26385  aalioulem4  26387  aalioulem5  26388  aaliou2b  26393  aaliou3lem2  26395  aaliou3lem8  26397  lgamgulmlem5  27085  vmage0  27173  chpge0  27178  vma1  27218  sqff1o  27234  fsumfldivdiaglem  27241  vmalelog  27257  chtublem  27263  fsumvma2  27266  chpchtsum  27271  logfacubnd  27273  perfectlem2  27282  dchrelbas4  27295  bposlem1  27336  bposlem2  27337  bposlem5  27340  lgsdir  27384  lgsdilem2  27385  lgseisenlem1  27427  2sqlem8  27478  chebbnd1lem1  27521  chebbnd1lem2  27522  chebbnd1lem3  27523  dchrisumlem3  27543  dchrisum0flblem1  27560  dchrisum0lem1b  27567  dirith2  27580  selbergb  27601  selberg3lem2  27610  pntrlog2bndlem1  27629  pntrlog2bndlem3  27631  pntrlog2bndlem4  27632  pntrlog2bndlem5  27633  pntrlog2bnd  27636  pntpbnd1a  27637  pntlemj  27655  pntlemk  27658  nexple  32996  mplmulmvr  33797  esplyind  33833  submateqlem2  34066  hgt750lemb  34911  poimirlem7  38087  poimirlem19  38099  poimirlem28  38108  lcmineqlem10  42616  lcmineqlem11  42617  lcmineqlem13  42619  lcmineqlem19  42625  lcmineqlem20  42626  aks4d1p1p2  42648  aks4d1p3  42656  aks4d1p5  42658  aks4d1p6  42659  aks4d1p8  42665  aks4d1p9  42666  posbezout  42678  primrootspoweq0  42684  hashscontpow1  42699  aks6d1c2lem4  42705  sticksstones6  42729  sticksstones7  42730  sticksstones10  42733  sticksstones12a  42735  sticksstones12  42736  aks6d1c6lem4  42751  aks6d1c7lem2  42759  grpods  42772  unitscyglem2  42774  unitscyglem4  42776  unitscyglem5  42777  fimgmcyc  43113  flt4lem7  43202  diophin  43314  irrapxlem4  43363  irrapxlem5  43364  pellexlem2  43368  pell14qrgapw  43414  pellfundgt1  43421  ltrmynn0  43486  jm2.27c  43545  jm3.1lem2  43556  fzisoeu  45840  fmuldfeq  46120  stoweidlem3  46538  stoweidlem20  46555  stoweidlem42  46577  stoweidlem51  46586  stoweidlem59  46594  stirlinglem8  46616  fourierdlem11  46653  fourierdlem41  46683  fourierdlem48  46689  fourierdlem79  46720  etransclem23  46792  etransclem28  46797  etransclem35  46804  etransclem38  46807  etransclem44  46813  etransc  46818  hoicvrrex  47091  iccpartlt  47991  lighneallem4a  48178  perfectALTVlem2  48305