MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nnge1d Structured version   Unicode version

Theorem nnge1d 10354
Description: A positive integer is one or greater. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
nnge1d.1  |-  ( ph  ->  A  e.  NN )
Assertion
Ref Expression
nnge1d  |-  ( ph  ->  1  <_  A )

Proof of Theorem nnge1d
StepHypRef Expression
1 nnge1d.1 . 2  |-  ( ph  ->  A  e.  NN )
2 nnge1 10338 . 2  |-  ( A  e.  NN  ->  1  <_  A )
31, 2syl 16 1  |-  ( ph  ->  1  <_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1757   class class class wbr 4282   1c1 9273    <_ cle 9409   NNcn 10312
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363  ax-resscn 9329  ax-1cn 9330  ax-icn 9331  ax-addcl 9332  ax-addrcl 9333  ax-mulcl 9334  ax-mulrcl 9335  ax-mulcom 9336  ax-addass 9337  ax-mulass 9338  ax-distr 9339  ax-i2m1 9340  ax-1ne0 9341  ax-1rid 9342  ax-rnegex 9343  ax-rrecex 9344  ax-cnre 9345  ax-pre-lttri 9346  ax-pre-lttrn 9347  ax-pre-ltadd 9348  ax-pre-mulgt0 9349
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2966  df-sbc 3178  df-csb 3279  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-pss 3334  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-tp 3872  df-op 3874  df-uni 4082  df-iun 4163  df-br 4283  df-opab 4341  df-mpt 4342  df-tr 4376  df-eprel 4621  df-id 4625  df-po 4630  df-so 4631  df-fr 4668  df-we 4670  df-ord 4711  df-on 4712  df-lim 4713  df-suc 4714  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-f1 5413  df-fo 5414  df-f1o 5415  df-fv 5416  df-riota 6041  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-om 6468  df-recs 6820  df-rdg 6854  df-er 7091  df-en 7301  df-dom 7302  df-sdom 7303  df-pnf 9410  df-mnf 9411  df-xr 9412  df-ltxr 9413  df-le 9414  df-sub 9587  df-neg 9588  df-nn 10313
This theorem is referenced by:  bernneq3  11978  facwordi  12051  faclbnd  12052  faclbnd3  12054  faclbnd4lem3  12057  facavg  12063  hashge1  12138  seqcoll  12202  eftlub  13378  eflegeo  13390  eirrlem  13471  divdenle  13812  eulerthlem2  13842  infpnlem2  13957  4sqlem11  14001  4sqlem12  14002  2expltfac  14104  cshwshash  14116  fislw  16106  gzrngunitlem  17723  ovoliunlem1  20829  aalioulem2  21686  aalioulem4  21688  aalioulem5  21689  aaliou2b  21694  aaliou3lem2  21696  aaliou3lem8  21698  vmage0  22346  chpge0  22351  vma1  22391  sqff1o  22407  fsumfldivdiaglem  22416  vmalelog  22431  chtublem  22437  fsumvma2  22440  chpchtsum  22445  logfacubnd  22447  perfectlem2  22456  dchrelbas4  22469  bposlem1  22510  bposlem2  22511  bposlem5  22514  lgsdir  22556  lgsdilem2  22557  lgseisenlem1  22575  2sqlem8  22598  chebbnd1lem1  22605  chebbnd1lem2  22606  chebbnd1lem3  22607  dchrisumlem3  22627  dchrisum0flblem1  22644  dchrisum0lem1b  22651  dirith2  22664  selbergb  22685  selberg3lem2  22694  pntrlog2bndlem1  22713  pntrlog2bndlem3  22715  pntrlog2bndlem4  22716  pntrlog2bndlem5  22717  pntrlog2bnd  22720  pntpbnd1a  22721  pntlemj  22739  pntlemk  22742  lgamgulmlem5  26869  diophin  28958  irrapxlem4  29013  irrapxlem5  29014  pellexlem2  29018  pell14qrgapw  29064  pellfundgt1  29071  ltrmynn0  29138  jm2.27c  29203  jm3.1lem2  29214  fmuldfeq  29611  stoweidlem3  29646  stoweidlem20  29663  stoweidlem42  29685  stoweidlem51  29694  stoweidlem59  29702  stirlinglem8  29724  clwlkfoclwwlk  30366
  Copyright terms: Public domain W3C validator