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

Theorem 1lt2 10805
Description: 1 is less than 2. (Contributed by NM, 24-Feb-2005.)
Assertion
Ref Expression
1lt2  |-  1  <  2

Proof of Theorem 1lt2
StepHypRef Expression
1 1re 9668 . . 3  |-  1  e.  RR
21ltp1i 10538 . 2  |-  1  <  ( 1  +  1 )
3 df-2 10696 . 2  |-  2  =  ( 1  +  1 )
42, 3breqtrri 4442 1  |-  1  <  2
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4416  (class class class)co 6315   1c1 9566    + caddc 9568    < clt 9701   2c2 10687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-2 10696
This theorem is referenced by:  1lt3  10807  1lt4  10810  1lt6  10819  1lt7  10825  1lt8  10832  1lt9  10840  1lt10  10849  1ne2  10851  1le2  10852  halflt1  10860  nn0n0n1ge2b  10962  nn0ge2m1nn  10963  halfnz  11043  fztpval  11886  ige2m2fzo  12008  faclbnd5  12515  hashfun  12642  hashge2el2dif  12670  wrdlenge2n0  12739  ccat2s1p2  12799  s3fv1  13023  wwlktovf  13080  sqrt2gt1lt2  13387  ege2le3  14193  ene1  14311  n2dvds1  14403  bits0o  14452  bitsfzolem  14456  bitsfzolemOLD  14457  bitsfzo  14458  bitsfi  14460  2prm  14689  3prm  14690  iserodd  14834  dec2dvds  15084  dec5nprm  15087  dec2nprm  15088  2expltfac  15112  4nprm  15125  5prm  15129  6nprm  15130  7prm  15131  8nprm  15132  10nprm  15134  11prm  15135  13prm  15136  17prm  15137  19prm  15138  37prm  15141  83prm  15143  317prm  15146  631prm  15147  grpstr  15285  grpbase  15286  grpplusg  15287  ressplusg  15288  rngstr  15293  lmodstr  15310  topgrpstr  15335  psgnunilem2  17185  isnzr2hash  18537  dyadss  22601  opnmbllem  22608  lhop1lem  23014  aaliou3lem8  23350  logblog  23778  dcubic1lem  23818  dcubic2  23819  mcubic  23822  zetacvg  23989  lgamgulmlem4  24006  ppi1  24140  cht1  24141  chtrpcl  24151  ppiltx  24153  chtub  24189  chpval2  24195  mersenne  24204  perfectlem1  24206  perfectlem2  24207  bpos1  24260  bposlem1  24261  bposlem6  24266  bposlem7  24267  bposlem8  24268  lgseisenlem1  24326  2sqblem  24354  chebbnd1lem1  24356  chebbnd1lem3  24358  chebbnd1  24359  chtppilimlem1  24360  chtppilimlem2  24361  chtppilim  24362  chto1ub  24363  chebbnd2  24364  chto1lb  24365  mulog2sumlem2  24422  pntrmax  24451  pntrlog2bndlem2  24465  pntrlog2bndlem4  24467  pntpbnd1a  24472  pntibndlem3  24479  pntibnd  24480  pntlemb  24484  pntlemk  24493  pnt  24501  axlowdim  25040  cusgrasizeindb1  25248  usgrcyclnl2  25418  constr3trllem3  25429  clwlkisclwwlklem2fv2  25560  clwwlkext2edg  25579  usg2cwwkdifex  25598  eupath2lem3  25756  konigsberg  25764  frgrareg  25894  frgraregord013  25895  fib1  29282  ballotlem2  29370  subfacp1lem1  29951  subfacp1lem5  29956  relowlpssretop  31812  tan2h  31982  opnmbllem0  32021  heiborlem7  32194  pellfundgt1  35776  stoweidlem13  37911  stoweidlem26  37924  wallispilem4  37968  wallispi  37970  wallispi2lem1  37971  wallispi2lem2  37972  wallispi2  37973  stirlinglem1  37974  dirkertrigeqlem1  37998  dirkercncflem1  38003  fouriersw  38133  etransclem23  38160  salexct2  38236  mod2eq1n2dvds  38763  dfodd4  38826  perfectALTVlem1  38881  perfectALTVlem2  38882  nnsum4primesevenALTV  38934  pfx2  38993  nbusgrvtxm1  39503  cusgrsizeindb1  39561  lfgrwlkprop  39722  uspgrn2crct  39826  usgra2pthlem1  39940  cznnring  40231  pw2m1lepw2m1  40591  difmodm1lt  40598  rege1logbzge0  40643  logbpw2m1  40651  fllog2  40652  blenpw2m1  40663  nnpw2blen  40664  dignn0flhalflem1  40699
  Copyright terms: Public domain W3C validator