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

Theorem 1lt2 10480
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 9377 . . 3  |-  1  e.  RR
21ltp1i 10228 . 2  |-  1  <  ( 1  +  1 )
3 df-2 10372 . 2  |-  2  =  ( 1  +  1 )
42, 3breqtrri 4312 1  |-  1  <  2
Colors of variables: wff setvar class
Syntax hints:   class class class wbr 4287  (class class class)co 6086   1c1 9275    + caddc 9277    < clt 9410   2c2 10363
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-mpt 4347  df-id 4631  df-po 4636  df-so 4637  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-2 10372
This theorem is referenced by:  1lt3  10482  1lt4  10485  1lt6  10494  1lt7  10500  1lt8  10507  1lt9  10515  1lt10  10524  1ne2  10526  1le2  10527  halflt1  10535  nn0n0n1ge2b  10636  halfnz  10712  2eluzge1  10893  fztpval  11510  faclbnd5  12066  hashge2el2dif  12176  hashfun  12191  wrdlenge2n0  12253  s3fv1  12508  sqr2gt1lt2  12756  ege2le3  13367  n2dvds1  13574  bits0o  13618  bitsfzolem  13622  bitsfzo  13623  bitsfi  13625  2prm  13771  3prm  13772  iserodd  13894  dec2dvds  14084  dec5nprm  14087  dec2nprm  14088  2expltfac  14111  4nprm  14124  5prm  14128  6nprm  14129  7prm  14130  8nprm  14131  10nprm  14133  11prm  14134  13prm  14135  17prm  14136  19prm  14137  37prm  14140  83prm  14142  317prm  14145  631prm  14146  grpstr  14269  grpbase  14270  grpplusg  14271  ressplusg  14272  rngstr  14277  lmodstr  14294  topgrpstr  14319  psgnunilem2  15992  dyadss  21054  opnmbllem  21061  lhop1lem  21465  aaliou3lem8  21791  dcubic1lem  22218  dcubic2  22219  mcubic  22222  ppi1  22482  cht1  22483  chtrpcl  22493  ppiltx  22495  chtub  22531  chpval2  22537  mersenne  22546  perfectlem1  22548  perfectlem2  22549  bpos1  22602  bposlem1  22603  bposlem6  22608  bposlem7  22609  bposlem8  22610  lgseisenlem1  22668  2sqblem  22696  chebbnd1lem1  22698  chebbnd1lem3  22700  chebbnd1  22701  chtppilimlem1  22702  chtppilimlem2  22703  chtppilim  22704  chto1ub  22705  chebbnd2  22706  chto1lb  22707  mulog2sumlem2  22764  pntrmax  22793  pntrlog2bndlem2  22807  pntrlog2bndlem4  22809  pntpbnd1a  22814  pntibndlem3  22821  pntibnd  22822  pntlemb  22826  pntlemk  22835  pnt  22843  axlowdim  23175  cusgrasizeindb1  23347  usgrcyclnl2  23495  constr3trllem3  23506  eupath2lem3  23568  konigsberg  23576  fib1  26752  ballotlem2  26840  signswbase  26924  signswplusg  26925  zetacvg  26970  lgamgulmlem4  26987  subfacp1lem1  27036  subfacp1lem5  27041  tan2h  28395  opnmbllem0  28398  nn0prpwlem  28488  heiborlem7  28687  pellfundgt1  29195  stoweidlem13  29779  stoweidlem26  29792  wallispilem4  29834  wallispi  29836  wallispi2lem1  29837  wallispi2lem2  29838  wallispi2  29839  stirlinglem1  29840  ige2m2fzo  30191  wwlktovf  30222  ccat2s1p2  30237  usgra2pthlem1  30271  clwlkisclwwlklem2fv2  30416  clwwlkext2edg  30435  usg2cwwkdifex  30466  extwwlkfablem1  30638  frgrareg  30681  frgraregord013  30682  isnzr2hash  30743  ene1  31040
  Copyright terms: Public domain W3C validator