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

Theorem nnge1d 10640
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 10623 . 2  |-  ( A  e.  NN  ->  1  <_  A )
31, 2syl 17 1  |-  ( ph  ->  1  <_  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1890   class class class wbr 4373   1c1 9526    <_ cle 9662   NNcn 10597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-8 1892  ax-9 1899  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431  ax-sep 4496  ax-nul 4505  ax-pow 4553  ax-pr 4611  ax-un 6570  ax-resscn 9582  ax-1cn 9583  ax-icn 9584  ax-addcl 9585  ax-addrcl 9586  ax-mulcl 9587  ax-mulrcl 9588  ax-mulcom 9589  ax-addass 9590  ax-mulass 9591  ax-distr 9592  ax-i2m1 9593  ax-1ne0 9594  ax-1rid 9595  ax-rnegex 9596  ax-rrecex 9597  ax-cnre 9598  ax-pre-lttri 9599  ax-pre-lttrn 9600  ax-pre-ltadd 9601  ax-pre-mulgt0 9602
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 3014  df-sbc 3235  df-csb 3331  df-dif 3374  df-un 3376  df-in 3378  df-ss 3385  df-pss 3387  df-nul 3699  df-if 3849  df-pw 3920  df-sn 3936  df-pr 3938  df-tp 3940  df-op 3942  df-uni 4168  df-iun 4249  df-br 4374  df-opab 4433  df-mpt 4434  df-tr 4469  df-eprel 4722  df-id 4726  df-po 4732  df-so 4733  df-fr 4770  df-we 4772  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-pred 5358  df-ord 5404  df-on 5405  df-lim 5406  df-suc 5407  df-iota 5524  df-fun 5562  df-fn 5563  df-f 5564  df-f1 5565  df-fo 5566  df-f1o 5567  df-fv 5568  df-riota 6237  df-ov 6278  df-oprab 6279  df-mpt2 6280  df-om 6680  df-wrecs 7014  df-recs 7076  df-rdg 7114  df-er 7349  df-en 7556  df-dom 7557  df-sdom 7558  df-pnf 9663  df-mnf 9664  df-xr 9665  df-ltxr 9666  df-le 9667  df-sub 9848  df-neg 9849  df-nn 10598
This theorem is referenced by:  bernneq3  12393  facwordi  12467  faclbnd  12468  faclbnd3  12470  faclbnd4lem3  12473  facavg  12479  hashge1  12561  seqcoll  12621  wrdind  12831  wrd2ind  12832  eftlub  14173  eflegeo  14185  eirrlem  14266  divdenle  14708  eulerthlem2  14740  infpnlem2  14865  4sqlem11  14909  4sqlem12  14910  prmolefac  15014  prmorlefacOLD  15028  2expltfac  15073  cshwshash  15085  fislw  17287  gzrngunitlem  19042  ovoliunlem1  22465  aalioulem2  23300  aalioulem4  23302  aalioulem5  23303  aaliou2b  23308  aaliou3lem2  23310  aaliou3lem8  23312  lgamgulmlem5  23969  vmage0  24059  chpge0  24064  vma1  24104  sqff1o  24120  fsumfldivdiaglem  24129  vmalelog  24144  chtublem  24150  fsumvma2  24153  chpchtsum  24158  logfacubnd  24160  perfectlem2  24169  dchrelbas4  24182  bposlem1  24223  bposlem2  24224  bposlem5  24227  lgsdir  24269  lgsdilem2  24270  lgseisenlem1  24288  2sqlem8  24311  chebbnd1lem1  24318  chebbnd1lem2  24319  chebbnd1lem3  24320  dchrisumlem3  24340  dchrisum0flblem1  24357  dchrisum0lem1b  24364  dirith2  24377  selbergb  24398  selberg3lem2  24407  pntrlog2bndlem1  24426  pntrlog2bndlem3  24428  pntrlog2bndlem4  24429  pntrlog2bndlem5  24430  pntrlog2bnd  24433  pntpbnd1a  24434  pntlemj  24452  pntlemk  24455  clwlkfoclwwlk  25584  submateqlem2  28640  nexple  28837  plymulx0  29441  poimirlem7  31948  poimirlem19  31960  poimirlem28  31969  diophin  35616  irrapxlem4  35670  irrapxlem5  35671  pellexlem2  35675  pell14qrgapw  35723  pellfundgt1  35732  ltrmynn0  35799  jm2.27c  35863  jm3.1lem2  35874  fzisoeu  37548  fmuldfeq  37702  stoweidlem3  37919  stoweidlem20  37936  stoweidlem42  37959  stoweidlem51  37968  stoweidlem59  37976  stirlinglem8  37999  fourierdlem11  38036  fourierdlem41  38067  fourierdlem48  38074  fourierdlem79  38105  etransclem23  38178  etransclem28  38183  etransclem35  38190  etransclem38  38193  etransclem44  38199  etransc  38205  hoicvrrex  38440  iccpartlt  38828  perfectALTVlem2  38934
  Copyright terms: Public domain W3C validator