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

Theorem 1lt2 12258
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 11089 . . 3 1 ∈ ℝ
21ltp1i 11993 . 2 1 < (1 + 1)
3 df-2 12150 . 2 2 = (1 + 1)
42, 3breqtrri 5131 1 1 < 2
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 5104  (class class class)co 7350  1c1 10986   + caddc 10988   < clt 11123  2c2 12142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4865  df-br 5105  df-opab 5167  df-mpt 5188  df-id 5529  df-po 5543  df-so 5544  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-er 8582  df-en 8818  df-dom 8819  df-sdom 8820  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-2 12150
This theorem is referenced by:  1lt3  12260  1lt4  12263  1lt6  12272  1lt7  12278  1lt8  12285  1lt9  12293  1ne2  12295  1le2  12296  halflt1  12305  nn0n0n1ge2b  12415  nn0ge2m1nn  12416  halfnz  12512  1lt10  12690  fztpval  13432  ige2m2fzo  13564  faclbnd5  14126  hashgt23el  14252  hashfun  14265  hashge2el2dif  14307  wrdlenge2n0  14368  ccat2s1p2  14446  s3fv1  14713  pfx2  14768  wwlktovf  14779  sqrt2gt1lt2  15094  ege2le3  15907  ene1  16027  mod2eq1n2dvds  16164  bits0o  16245  bitsfzolem  16249  bitsfzo  16250  bitsfi  16252  2prm  16503  4nprm  16506  iserodd  16642  dec2dvds  16870  dec5nprm  16873  dec2nprm  16874  2expltfac  16900  5prm  16916  6nprm  16917  7prm  16918  8nprm  16919  10nprm  16921  11prm  16922  13prm  16923  17prm  16924  19prm  16925  37prm  16928  83prm  16930  317prm  16933  631prm  16934  basendxltplusgndx  17097  grpstr  17100  grpbaseOLD  17103  grpplusgOLD  17105  rngstr  17114  lmodstr  17141  topgrpstr  17177  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  27696  lfgrnloop  27862  lfuhgr1v0e  27988  nbusgrvtxm1  28113  cusgrsizeindb1  28184  lfgrwlkprop  28421  usgr2pthlem  28497  uspgrn2crct  28539  clwlkclwwlklem2fv2  28726  clwwlkext2edg  28786  eupth2lem3lem4  28961  ex-mod  29179  9p10ne21  29200  cshw1s2  31596  fib1  32761  ballotlem2  32849  chtvalz  33003  hgt750lemd  33022  hgt750lem  33025  hgt750leme  33032  lfuhgr2  33473  subfacp1lem1  33534  subfacp1lem5  33539  knoppndvlem12  34872  knoppndvlem18  34878  relowlpssretop  35721  tan2h  35956  opnmbllem0  36000  heiborlem7  36162  lcmineqlem22  40393  3lexlogpow5ineq2  40398  3lexlogpow5ineq4  40399  3lexlogpow5ineq3  40400  3lexlogpow2ineq1  40401  3lexlogpow2ineq2  40402  3lexlogpow5ineq5  40403  aks4d1lem1  40405  dvrelog2b  40409  dvrelogpow2b  40411  aks4d1p1p3  40412  aks4d1p1p2  40413  aks4d1p1p4  40414  aks4d1p1p6  40416  aks4d1p1p7  40417  aks4d1p1p5  40418  aks4d1p1  40419  aks4d1p2  40420  aks4d1p3  40421  aks4d1p5  40423  aks4d1p6  40424  aks4d1p7d1  40425  aks4d1p7  40426  aks4d1p8  40430  aks4d1p9  40431  flt4lem7  40831  pellfundgt1  41040  stoweidlem13  43964  stoweidlem26  43977  wallispilem4  44019  wallispi  44021  wallispi2lem1  44022  wallispi2lem2  44023  wallispi2  44024  stirlinglem1  44025  dirkertrigeqlem1  44049  dirkercncflem1  44054  fouriersw  44182  etransclem23  44208  salexct2  44288  fmtnoge3  45422  fmtnof1  45427  fmtno4prm  45467  2pwp1prm  45481  127prm  45491  sfprmdvdsmersenne  45495  lighneallem2  45498  dfodd4  45551  perfectALTVlem1  45613  perfectALTVlem2  45614  nnsum4primesevenALTV  45693  cznnring  45954  pw2m1lepw2m1  46301  difmodm1lt  46308  rege1logbzge0  46345  logbpw2m1  46353  fllog2  46354  blenpw2m1  46365  nnpw2blen  46366  dignn0flhalflem1  46401
  Copyright terms: Public domain W3C validator