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

Theorem 1lt2 12283
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 11114 . . 3 1 ∈ ℝ
21ltp1i 12018 . 2 1 < (1 + 1)
3 df-2 12175 . 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 7352  1c1 11011   + caddc 11013   < clt 11148  2c2 12167
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 7665  ax-resscn 11067  ax-1cn 11068  ax-icn 11069  ax-addcl 11070  ax-addrcl 11071  ax-mulcl 11072  ax-mulrcl 11073  ax-mulcom 11074  ax-addass 11075  ax-mulass 11076  ax-distr 11077  ax-i2m1 11078  ax-1ne0 11079  ax-1rid 11080  ax-rnegex 11081  ax-rrecex 11082  ax-cnre 11083  ax-pre-lttri 11084  ax-pre-lttrn 11085  ax-pre-ltadd 11086  ax-pre-mulgt0 11087
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 5530  df-po 5544  df-so 5545  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6446  df-fun 6496  df-fn 6497  df-f 6498  df-f1 6499  df-fo 6500  df-f1o 6501  df-fv 6502  df-riota 7308  df-ov 7355  df-oprab 7356  df-mpo 7357  df-er 8607  df-en 8843  df-dom 8844  df-sdom 8845  df-pnf 11150  df-mnf 11151  df-xr 11152  df-ltxr 11153  df-le 11154  df-sub 11346  df-neg 11347  df-2 12175
This theorem is referenced by:  1lt3  12285  1lt4  12288  1lt6  12297  1lt7  12303  1lt8  12310  1lt9  12318  1ne2  12320  1le2  12321  halflt1  12330  nn0n0n1ge2b  12440  nn0ge2m1nn  12441  halfnz  12540  1lt10  12716  fztpval  13458  ige2m2fzo  13590  faclbnd5  14152  hashgt23el  14278  hashfun  14291  hashge2el2dif  14333  wrdlenge2n0  14394  ccat2s1p2  14472  s3fv1  14739  pfx2  14794  wwlktovf  14805  sqrt2gt1lt2  15119  ege2le3  15932  ene1  16052  mod2eq1n2dvds  16189  bits0o  16270  bitsfzolem  16274  bitsfzo  16275  bitsfi  16277  2prm  16528  4nprm  16531  iserodd  16667  dec2dvds  16895  dec5nprm  16898  dec2nprm  16899  2expltfac  16925  5prm  16941  6nprm  16942  7prm  16943  8nprm  16944  10nprm  16946  11prm  16947  13prm  16948  17prm  16949  19prm  16950  37prm  16953  83prm  16955  317prm  16958  631prm  16959  basendxltplusgndx  17122  grpstr  17125  grpbaseOLD  17128  grpplusgOLD  17130  rngstr  17139  lmodstr  17166  topgrpstr  17202  psgnunilem2  19236  isnzr2hash  20687  dyadss  24910  opnmbllem  24917  lhop1lem  25329  aaliou3lem8  25657  zetacvg  26316  lgamgulmlem4  26333  ppi1  26465  cht1  26466  chtrpcl  26476  ppiltx  26478  chtub  26512  chpval2  26518  mersenne  26527  perfectlem1  26529  perfectlem2  26530  bpos1  26583  bposlem1  26584  bposlem6  26589  bposlem7  26590  bposlem8  26591  lgseisenlem1  26675  2sqblem  26731  chebbnd1lem1  26769  chebbnd1lem3  26771  chebbnd1  26772  chtppilimlem1  26773  chtppilimlem2  26774  chtppilim  26775  chto1ub  26776  chebbnd2  26777  chto1lb  26778  mulog2sumlem2  26835  pntrmax  26864  pntrlog2bndlem2  26878  pntrlog2bndlem4  26880  pntpbnd1a  26885  pntibndlem3  26892  pntibnd  26893  pntlemb  26897  pntlemk  26906  pnt  26914  axlowdim  27739  lfgrnloop  27905  lfuhgr1v0e  28031  nbusgrvtxm1  28156  cusgrsizeindb1  28227  lfgrwlkprop  28464  usgr2pthlem  28540  uspgrn2crct  28582  clwlkclwwlklem2fv2  28769  clwwlkext2edg  28829  eupth2lem3lem4  29004  ex-mod  29222  9p10ne21  29243  cshw1s2  31639  fib1  32804  ballotlem2  32892  chtvalz  33046  hgt750lemd  33065  hgt750lem  33068  hgt750leme  33075  lfuhgr2  33516  subfacp1lem1  33577  subfacp1lem5  33582  knoppndvlem12  34918  knoppndvlem18  34924  relowlpssretop  35767  tan2h  36002  opnmbllem0  36046  heiborlem7  36208  lcmineqlem22  40439  3lexlogpow5ineq2  40444  3lexlogpow5ineq4  40445  3lexlogpow5ineq3  40446  3lexlogpow2ineq1  40447  3lexlogpow2ineq2  40448  3lexlogpow5ineq5  40449  aks4d1lem1  40451  dvrelog2b  40455  dvrelogpow2b  40457  aks4d1p1p3  40458  aks4d1p1p2  40459  aks4d1p1p4  40460  aks4d1p1p6  40462  aks4d1p1p7  40463  aks4d1p1p5  40464  aks4d1p1  40465  aks4d1p2  40466  aks4d1p3  40467  aks4d1p5  40469  aks4d1p6  40470  aks4d1p7d1  40471  aks4d1p7  40472  aks4d1p8  40476  aks4d1p9  40477  flt4lem7  40900  pellfundgt1  41109  stoweidlem13  44149  stoweidlem26  44162  wallispilem4  44204  wallispi  44206  wallispi2lem1  44207  wallispi2lem2  44208  wallispi2  44209  stirlinglem1  44210  dirkertrigeqlem1  44234  dirkercncflem1  44239  fouriersw  44367  etransclem23  44393  salexct2  44475  fmtnoge3  45617  fmtnof1  45622  fmtno4prm  45662  2pwp1prm  45676  127prm  45686  sfprmdvdsmersenne  45690  lighneallem2  45693  dfodd4  45746  perfectALTVlem1  45808  perfectALTVlem2  45809  nnsum4primesevenALTV  45888  cznnring  46149  pw2m1lepw2m1  46496  difmodm1lt  46503  rege1logbzge0  46540  logbpw2m1  46548  fllog2  46549  blenpw2m1  46560  nnpw2blen  46561  dignn0flhalflem1  46596
  Copyright terms: Public domain W3C validator