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

Theorem 1lt2 12257
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 11088 . . 3 1 ∈ ℝ
21ltp1i 11992 . 2 1 < (1 + 1)
3 df-2 12149 . 2 2 = (1 + 1)
42, 3breqtrri 5130 1 1 < 2
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 5103  (class class class)co 7349  1c1 10985   + caddc 10987   < clt 11122  2c2 12141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2708  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7662  ax-resscn 11041  ax-1cn 11042  ax-icn 11043  ax-addcl 11044  ax-addrcl 11045  ax-mulcl 11046  ax-mulrcl 11047  ax-mulcom 11048  ax-addass 11049  ax-mulass 11050  ax-distr 11051  ax-i2m1 11052  ax-1ne0 11053  ax-1rid 11054  ax-rnegex 11055  ax-rrecex 11056  ax-cnre 11057  ax-pre-lttri 11058  ax-pre-lttrn 11059  ax-pre-ltadd 11060  ax-pre-mulgt0 11061
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3352  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5528  df-po 5542  df-so 5543  df-xp 5636  df-rel 5637  df-cnv 5638  df-co 5639  df-dm 5640  df-rn 5641  df-res 5642  df-ima 5643  df-iota 6443  df-fun 6493  df-fn 6494  df-f 6495  df-f1 6496  df-fo 6497  df-f1o 6498  df-fv 6499  df-riota 7305  df-ov 7352  df-oprab 7353  df-mpo 7354  df-er 8581  df-en 8817  df-dom 8818  df-sdom 8819  df-pnf 11124  df-mnf 11125  df-xr 11126  df-ltxr 11127  df-le 11128  df-sub 11320  df-neg 11321  df-2 12149
This theorem is referenced by:  1lt3  12259  1lt4  12262  1lt6  12271  1lt7  12277  1lt8  12284  1lt9  12292  1ne2  12294  1le2  12295  halflt1  12304  nn0n0n1ge2b  12414  nn0ge2m1nn  12415  halfnz  12511  1lt10  12689  fztpval  13431  ige2m2fzo  13563  faclbnd5  14125  hashgt23el  14251  hashfun  14264  hashge2el2dif  14306  wrdlenge2n0  14367  ccat2s1p2  14445  s3fv1  14712  pfx2  14767  wwlktovf  14778  sqrt2gt1lt2  15093  ege2le3  15906  ene1  16026  mod2eq1n2dvds  16163  bits0o  16244  bitsfzolem  16248  bitsfzo  16249  bitsfi  16251  2prm  16502  4nprm  16505  iserodd  16641  dec2dvds  16869  dec5nprm  16872  dec2nprm  16873  2expltfac  16899  5prm  16915  6nprm  16916  7prm  16917  8nprm  16918  10nprm  16920  11prm  16921  13prm  16922  17prm  16923  19prm  16924  37prm  16927  83prm  16929  317prm  16932  631prm  16933  basendxltplusgndx  17096  grpstr  17099  grpbaseOLD  17102  grpplusgOLD  17104  rngstr  17113  lmodstr  17140  topgrpstr  17176  psgnunilem2  19209  isnzr2hash  20657  dyadss  24880  opnmbllem  24887  lhop1lem  25299  aaliou3lem8  25627  zetacvg  26286  lgamgulmlem4  26303  ppi1  26435  cht1  26436  chtrpcl  26446  ppiltx  26448  chtub  26482  chpval2  26488  mersenne  26497  perfectlem1  26499  perfectlem2  26500  bpos1  26553  bposlem1  26554  bposlem6  26559  bposlem7  26560  bposlem8  26561  lgseisenlem1  26645  2sqblem  26701  chebbnd1lem1  26739  chebbnd1lem3  26741  chebbnd1  26742  chtppilimlem1  26743  chtppilimlem2  26744  chtppilim  26745  chto1ub  26746  chebbnd2  26747  chto1lb  26748  mulog2sumlem2  26805  pntrmax  26834  pntrlog2bndlem2  26848  pntrlog2bndlem4  26850  pntpbnd1a  26855  pntibndlem3  26862  pntibnd  26863  pntlemb  26867  pntlemk  26876  pnt  26884  axlowdim  27708  lfgrnloop  27874  lfuhgr1v0e  28000  nbusgrvtxm1  28125  cusgrsizeindb1  28196  lfgrwlkprop  28433  usgr2pthlem  28509  uspgrn2crct  28551  clwlkclwwlklem2fv2  28738  clwwlkext2edg  28798  eupth2lem3lem4  28973  ex-mod  29191  9p10ne21  29212  cshw1s2  31608  fib1  32773  ballotlem2  32861  chtvalz  33015  hgt750lemd  33034  hgt750lem  33037  hgt750leme  33044  lfuhgr2  33485  subfacp1lem1  33546  subfacp1lem5  33551  knoppndvlem12  34881  knoppndvlem18  34887  relowlpssretop  35730  tan2h  35965  opnmbllem0  36009  heiborlem7  36171  lcmineqlem22  40402  3lexlogpow5ineq2  40407  3lexlogpow5ineq4  40408  3lexlogpow5ineq3  40409  3lexlogpow2ineq1  40410  3lexlogpow2ineq2  40411  3lexlogpow5ineq5  40412  aks4d1lem1  40414  dvrelog2b  40418  dvrelogpow2b  40420  aks4d1p1p3  40421  aks4d1p1p2  40422  aks4d1p1p4  40423  aks4d1p1p6  40425  aks4d1p1p7  40426  aks4d1p1p5  40427  aks4d1p1  40428  aks4d1p2  40429  aks4d1p3  40430  aks4d1p5  40432  aks4d1p6  40433  aks4d1p7d1  40434  aks4d1p7  40435  aks4d1p8  40439  aks4d1p9  40440  flt4lem7  40862  pellfundgt1  41071  stoweidlem13  44007  stoweidlem26  44020  wallispilem4  44062  wallispi  44064  wallispi2lem1  44065  wallispi2lem2  44066  wallispi2  44067  stirlinglem1  44068  dirkertrigeqlem1  44092  dirkercncflem1  44097  fouriersw  44225  etransclem23  44251  salexct2  44333  fmtnoge3  45471  fmtnof1  45476  fmtno4prm  45516  2pwp1prm  45530  127prm  45540  sfprmdvdsmersenne  45544  lighneallem2  45547  dfodd4  45600  perfectALTVlem1  45662  perfectALTVlem2  45663  nnsum4primesevenALTV  45742  cznnring  46003  pw2m1lepw2m1  46350  difmodm1lt  46357  rege1logbzge0  46394  logbpw2m1  46402  fllog2  46403  blenpw2m1  46414  nnpw2blen  46415  dignn0flhalflem1  46450
  Copyright terms: Public domain W3C validator