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

Theorem 1lt2 10589
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 9486 . . 3  |-  1  e.  RR
21ltp1i 10337 . 2  |-  1  <  ( 1  +  1 )
3 df-2 10481 . 2  |-  2  =  ( 1  +  1 )
42, 3breqtrri 4415 1  |-  1  <  2
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4390  (class class class)co 6190   1c1 9384    + caddc 9386    < clt 9519   2c2 10472
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4511  ax-nul 4519  ax-pow 4568  ax-pr 4629  ax-un 6472  ax-resscn 9440  ax-1cn 9441  ax-icn 9442  ax-addcl 9443  ax-addrcl 9444  ax-mulcl 9445  ax-mulrcl 9446  ax-mulcom 9447  ax-addass 9448  ax-mulass 9449  ax-distr 9450  ax-i2m1 9451  ax-1ne0 9452  ax-1rid 9453  ax-rnegex 9454  ax-rrecex 9455  ax-cnre 9456  ax-pre-lttri 9457  ax-pre-lttrn 9458  ax-pre-ltadd 9459  ax-pre-mulgt0 9460
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-nel 2647  df-ral 2800  df-rex 2801  df-reu 2802  df-rab 2804  df-v 3070  df-sbc 3285  df-csb 3387  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-opab 4449  df-mpt 4450  df-id 4734  df-po 4739  df-so 4740  df-xp 4944  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-rn 4949  df-res 4950  df-ima 4951  df-iota 5479  df-fun 5518  df-fn 5519  df-f 5520  df-f1 5521  df-fo 5522  df-f1o 5523  df-fv 5524  df-riota 6151  df-ov 6193  df-oprab 6194  df-mpt2 6195  df-er 7201  df-en 7411  df-dom 7412  df-sdom 7413  df-pnf 9521  df-mnf 9522  df-xr 9523  df-ltxr 9524  df-le 9525  df-sub 9698  df-neg 9699  df-2 10481
This theorem is referenced by:  1lt3  10591  1lt4  10594  1lt6  10603  1lt7  10609  1lt8  10616  1lt9  10624  1lt10  10633  1ne2  10635  1le2  10636  halflt1  10644  nn0n0n1ge2b  10745  halfnz  10821  2eluzge1  11002  fztpval  11619  faclbnd5  12175  hashge2el2dif  12286  hashfun  12301  wrdlenge2n0  12363  s3fv1  12618  sqr2gt1lt2  12866  ege2le3  13477  n2dvds1  13684  bits0o  13728  bitsfzolem  13732  bitsfzo  13733  bitsfi  13735  2prm  13881  3prm  13882  iserodd  14004  dec2dvds  14194  dec5nprm  14197  dec2nprm  14198  2expltfac  14221  4nprm  14234  5prm  14238  6nprm  14239  7prm  14240  8nprm  14241  10nprm  14243  11prm  14244  13prm  14245  17prm  14246  19prm  14247  37prm  14250  83prm  14252  317prm  14255  631prm  14256  grpstr  14379  grpbase  14380  grpplusg  14381  ressplusg  14382  rngstr  14387  lmodstr  14404  topgrpstr  14429  psgnunilem2  16103  dyadss  21190  opnmbllem  21197  lhop1lem  21601  aaliou3lem8  21927  dcubic1lem  22354  dcubic2  22355  mcubic  22358  ppi1  22618  cht1  22619  chtrpcl  22629  ppiltx  22631  chtub  22667  chpval2  22673  mersenne  22682  perfectlem1  22684  perfectlem2  22685  bpos1  22738  bposlem1  22739  bposlem6  22744  bposlem7  22745  bposlem8  22746  lgseisenlem1  22804  2sqblem  22832  chebbnd1lem1  22834  chebbnd1lem3  22836  chebbnd1  22837  chtppilimlem1  22838  chtppilimlem2  22839  chtppilim  22840  chto1ub  22841  chebbnd2  22842  chto1lb  22843  mulog2sumlem2  22900  pntrmax  22929  pntrlog2bndlem2  22943  pntrlog2bndlem4  22945  pntpbnd1a  22950  pntibndlem3  22957  pntibnd  22958  pntlemb  22962  pntlemk  22971  pnt  22979  axlowdim  23342  cusgrasizeindb1  23514  usgrcyclnl2  23662  constr3trllem3  23673  eupath2lem3  23735  konigsberg  23743  fib1  26917  ballotlem2  27005  signswbase  27089  signswplusg  27090  zetacvg  27135  lgamgulmlem4  27152  subfacp1lem1  27201  subfacp1lem5  27206  tan2h  28562  opnmbllem0  28565  nn0prpwlem  28655  heiborlem7  28854  pellfundgt1  29362  stoweidlem13  29946  stoweidlem26  29959  wallispilem4  30001  wallispi  30003  wallispi2lem1  30004  wallispi2lem2  30005  wallispi2  30006  stirlinglem1  30007  ige2m2fzo  30358  wwlktovf  30389  ccat2s1p2  30404  usgra2pthlem1  30438  clwlkisclwwlklem2fv2  30583  clwwlkext2edg  30602  usg2cwwkdifex  30633  extwwlkfablem1  30805  frgrareg  30848  frgraregord013  30849  isnzr2hash  30912  ene1  31405
  Copyright terms: Public domain W3C validator