Theorem nnge1d 12285

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

Syntax hints:   → wi 4   ∈ wcel 2099   class class class wbr 5143  1c1 11134   ≤ cle 11274  ℕcn 12237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5294  ax-nul 5301  ax-pow 5360  ax-pr 5424  ax-un 7735  ax-resscn 11190  ax-1cn 11191  ax-icn 11192  ax-addcl 11193  ax-addrcl 11194  ax-mulcl 11195  ax-mulrcl 11196  ax-mulcom 11197  ax-addass 11198  ax-mulass 11199  ax-distr 11200  ax-i2m1 11201  ax-1ne0 11202  ax-1rid 11203  ax-rnegex 11204  ax-rrecex 11205  ax-cnre 11206  ax-pre-lttri 11207  ax-pre-lttrn 11208  ax-pre-ltadd 11209  ax-pre-mulgt0 11210

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-nel 3043  df-ral 3058  df-rex 3067  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5571  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7371  df-ov 7418  df-oprab 7419  df-mpo 7420  df-om 7866  df-2nd 7989  df-frecs 8281  df-wrecs 8312  df-recs 8386  df-rdg 8425  df-er 8719  df-en 8959  df-dom 8960  df-sdom 8961  df-pnf 11275  df-mnf 11276  df-xr 11277  df-ltxr 11278  df-le 11279  df-sub 11471  df-neg 11472  df-nn 12238

This theorem is referenced by:  bernneq3  14220  facwordi  14275  faclbnd  14276  faclbnd3  14278  faclbnd4lem3  14281  facavg  14287  hashge1  14375  seqcoll  14452  wrdind  14699  wrd2ind  14700  eftlub  16080  eflegeo  16092  eirrlem  16175  divdenle  16715  eulerthlem2  16745  infpnlem2  16874  4sqlem11  16918  4sqlem12  16919  prmolefac  17009  2expltfac  17056  cshwshash  17068  fislw  19574  gzrngunitlem  21359  psdmul  22084  ovoliunlem1  25425  aalioulem2  26262  aalioulem4  26264  aalioulem5  26265  aaliou2b  26270  aaliou3lem2  26272  aaliou3lem8  26274  lgamgulmlem5  26959  vmage0  27047  chpge0  27052  vma1  27092  sqff1o  27108  fsumfldivdiaglem  27115  vmalelog  27132  chtublem  27138  fsumvma2  27141  chpchtsum  27146  logfacubnd  27148  perfectlem2  27157  dchrelbas4  27170  bposlem1  27211  bposlem2  27212  bposlem5  27215  lgsdir  27259  lgsdilem2  27260  lgseisenlem1  27302  2sqlem8  27353  chebbnd1lem1  27396  chebbnd1lem2  27397  chebbnd1lem3  27398  dchrisumlem3  27418  dchrisum0flblem1  27435  dchrisum0lem1b  27442  dirith2  27455  selbergb  27476  selberg3lem2  27485  pntrlog2bndlem1  27504  pntrlog2bndlem3  27506  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntrlog2bnd  27511  pntpbnd1a  27512  pntlemj  27530  pntlemk  27533  submateqlem2  33404  nexple  33623  plymulx0  34174  hgt750lemb  34283  poimirlem7  37095  poimirlem19  37107  poimirlem28  37116  lcmineqlem10  41504  lcmineqlem11  41505  lcmineqlem13  41507  lcmineqlem19  41513  lcmineqlem20  41514  aks4d1p1p2  41536  aks4d1p3  41544  aks4d1p5  41546  aks4d1p6  41547  aks4d1p8  41553  aks4d1p9  41554  posbezout  41566  primrootspoweq0  41572  hashscontpow1  41587  aks6d1c2lem4  41593  sticksstones6  41618  sticksstones7  41619  sticksstones10  41622  sticksstones12a  41624  sticksstones12  41625  aks6d1c6lem4  41640  metakunt1  41648  metakunt2  41649  metakunt5  41652  metakunt10  41657  metakunt16  41663  metakunt21  41668  metakunt24  41671  metakunt26  41673  metakunt28  41675  metakunt29  41676  flt4lem7  42074  diophin  42183  irrapxlem4  42236  irrapxlem5  42237  pellexlem2  42241  pell14qrgapw  42287  pellfundgt1  42294  ltrmynn0  42360  jm2.27c  42419  jm3.1lem2  42430  fzisoeu  44673  fmuldfeq  44962  stoweidlem3  45382  stoweidlem20  45399  stoweidlem42  45421  stoweidlem51  45430  stoweidlem59  45438  stirlinglem8  45460  fourierdlem11  45497  fourierdlem41  45527  fourierdlem48  45533  fourierdlem79  45564  etransclem23  45636  etransclem28  45641  etransclem35  45648  etransclem38  45651  etransclem44  45657  etransc  45662  hoicvrrex  45935  iccpartlt  46755  lighneallem4a  46939  perfectALTVlem2  47053