Theorem 1lt2 12282

Description: 1 is less than 2. (Contributed by NM, 24-Feb-2005.)

Assertion

Ref	Expression
1lt2	⊢ 1 < 2

Proof of Theorem 1lt2

Step	Hyp	Ref	Expression
1		1re 11103	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12017	. 2 ⊢ 1 < (1 + 1)
3		df-2 12179	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5115	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5088  (class class class)co 7340  1c1 10998   + caddc 11000   < clt 11137  2c2 12171

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5231  ax-nul 5241  ax-pow 5300  ax-pr 5367  ax-un 7662  ax-resscn 11054  ax-1cn 11055  ax-icn 11056  ax-addcl 11057  ax-addrcl 11058  ax-mulcl 11059  ax-mulrcl 11060  ax-mulcom 11061  ax-addass 11062  ax-mulass 11063  ax-distr 11064  ax-i2m1 11065  ax-1ne0 11066  ax-1rid 11067  ax-rnegex 11068  ax-rrecex 11069  ax-cnre 11070  ax-pre-lttri 11071  ax-pre-lttrn 11072  ax-pre-ltadd 11073  ax-pre-mulgt0 11074

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3344  df-rab 3393  df-v 3435  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-mpt 5170  df-id 5508  df-po 5521  df-so 5522  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-riota 7297  df-ov 7343  df-oprab 7344  df-mpo 7345  df-er 8616  df-en 8864  df-dom 8865  df-sdom 8866  df-pnf 11139  df-mnf 11140  df-xr 11141  df-ltxr 11142  df-le 11143  df-sub 11337  df-neg 11338  df-2 12179

This theorem is referenced by:  1lt3  12284  1lt4  12287  1lt6  12296  1lt7  12302  1lt8  12309  1lt9  12317  1ne2  12319  1le2  12320  halflt1  12329  nn0n0n1ge2b  12441  nn0ge2m1nn  12442  halfnz  12542  1lt10  12718  fztpval  13477  ige2m2fzo  13619  faclbnd5  14193  hashgt23el  14319  hashfun  14332  hashge2el2dif  14375  tpf1ofv2  14393  wrdlenge2n0  14447  ccat2s1p2  14525  s3fv1  14786  pfx2  14841  wwlktovf  14850  sqrt2gt1lt2  15168  ege2le3  15984  ene1  16106  mod2eq1n2dvds  16245  bits0o  16328  bitsfzolem  16332  bitsfzo  16333  bitsfi  16335  2prm  16590  4nprm  16593  iserodd  16734  dec2dvds  16962  dec5nprm  16965  dec2nprm  16966  2expltfac  16991  5prm  17007  6nprm  17008  7prm  17009  8nprm  17010  10nprm  17012  11prm  17013  13prm  17014  17prm  17015  19prm  17016  37prm  17019  83prm  17021  317prm  17024  631prm  17025  basendxltplusgndx  17177  rngstr  17189  lmodstr  17216  topgrpstr  17252  psgnunilem2  19361  isnzr2hash  20388  dyadss  25476  opnmbllem  25483  lhop1lem  25899  aaliou3lem8  26234  zetacvg  26906  lgamgulmlem4  26923  ppi1  27055  cht1  27056  chtrpcl  27066  ppiltx  27068  chtub  27104  chpval2  27110  mersenne  27119  perfectlem1  27121  perfectlem2  27122  bpos1  27175  bposlem1  27176  bposlem6  27181  bposlem7  27182  bposlem8  27183  lgseisenlem1  27267  2sqblem  27323  chebbnd1lem1  27361  chebbnd1lem3  27363  chebbnd1  27364  chtppilimlem1  27365  chtppilimlem2  27366  chtppilim  27367  chto1ub  27368  chebbnd2  27369  chto1lb  27370  mulog2sumlem2  27427  pntrmax  27456  pntrlog2bndlem2  27470  pntrlog2bndlem4  27472  pntpbnd1a  27477  pntibndlem3  27484  pntibnd  27485  pntlemb  27489  pntlemk  27498  pnt  27506  axlowdim  28893  lfgrnloop  29057  lfuhgr1v0e  29186  nbusgrvtxm1  29311  cusgrsizeindb1  29383  lfgrwlkprop  29618  usgr2pthlem  29695  uspgrn2crct  29740  clwlkclwwlklem2fv2  29927  clwwlkext2edg  29987  eupth2lem3lem4  30162  ex-mod  30380  9p10ne21  30401  cshw1s2  32897  drngidlhash  33367  rtelextdg2lem  33707  fib1  34381  ballotlem2  34470  chtvalz  34610  hgt750lemd  34629  hgt750lem  34632  hgt750leme  34639  lfuhgr2  35109  subfacp1lem1  35169  subfacp1lem5  35174  knoppndvlem12  36514  knoppndvlem18  36520  relowlpssretop  37355  tan2h  37609  opnmbllem0  37653  heiborlem7  37814  lcmineqlem22  42040  3lexlogpow5ineq2  42045  3lexlogpow5ineq4  42046  3lexlogpow5ineq3  42047  3lexlogpow2ineq1  42048  3lexlogpow2ineq2  42049  3lexlogpow5ineq5  42050  aks4d1lem1  42052  dvrelog2b  42056  dvrelogpow2b  42058  aks4d1p1p3  42059  aks4d1p1p2  42060  aks4d1p1p4  42061  aks4d1p1p6  42063  aks4d1p1p7  42064  aks4d1p1p5  42065  aks4d1p1  42066  aks4d1p2  42067  aks4d1p3  42068  aks4d1p5  42070  aks4d1p6  42071  aks4d1p7d1  42072  aks4d1p7  42073  aks4d1p8  42077  aks4d1p9  42078  aks6d1c3  42113  aks6d1c6lem4  42163  aks6d1c7lem2  42171  flt4lem7  42649  pellfundgt1  42873  stoweidlem13  46008  stoweidlem26  46021  wallispilem4  46063  wallispi  46065  wallispi2lem1  46066  wallispi2lem2  46067  wallispi2  46068  stirlinglem1  46069  dirkertrigeqlem1  46093  dirkercncflem1  46098  fouriersw  46226  etransclem23  46252  salexct2  46334  ceilhalfgt1  47327  ceil5half3  47338  difmodm1lt  47357  fmtnoge3  47528  fmtnof1  47533  fmtno4prm  47573  2pwp1prm  47587  127prm  47597  sfprmdvdsmersenne  47601  lighneallem2  47604  dfodd4  47657  perfectALTVlem1  47719  perfectALTVlem2  47720  nnsum4primesevenALTV  47799  gpgprismgrusgra  48056  cznnring  48260  pw2m1lepw2m1  48519  rege1logbzge0  48558  logbpw2m1  48566  fllog2  48567  blenpw2m1  48578  nnpw2blen  48579  dignn0flhalflem1  48614