Theorem 1lt2 11845

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 10679	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 11582	. 2 ⊢ 1 < (1 + 1)
3		df-2 11737	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5059	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5032  (class class class)co 7150  1c1 10576   + caddc 10578   < clt 10713  2c2 11729

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-po 5443  df-so 5444  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-er 8299  df-en 8528  df-dom 8529  df-sdom 8530  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-2 11737

This theorem is referenced by:  1lt3  11847  1lt4  11850  1lt6  11859  1lt7  11865  1lt8  11872  1lt9  11880  1ne2  11882  1le2  11883  halflt1  11892  nn0n0n1ge2b  12002  nn0ge2m1nn  12003  halfnz  12099  1lt10  12276  fztpval  13018  ige2m2fzo  13149  faclbnd5  13708  hashgt23el  13835  hashfun  13848  hashge2el2dif  13890  wrdlenge2n0  13951  ccat2s1p2  14033  ccat2s1p2OLD  14035  s3fv1  14301  pfx2  14356  wwlktovf  14367  sqrt2gt1lt2  14682  ege2le3  15491  ene1  15611  mod2eq1n2dvds  15748  bits0o  15829  bitsfzolem  15833  bitsfzo  15834  bitsfi  15836  2prm  16088  4nprm  16091  iserodd  16227  dec2dvds  16454  dec5nprm  16457  dec2nprm  16458  2expltfac  16484  5prm  16500  6nprm  16501  7prm  16502  8nprm  16503  10nprm  16505  11prm  16506  13prm  16507  17prm  16508  19prm  16509  37prm  16512  83prm  16514  317prm  16517  631prm  16518  grpstr  16667  grpbase  16668  grpplusg  16669  ressplusg  16670  rngstr  16677  lmodstr  16694  topgrpstr  16719  psgnunilem2  18690  isnzr2hash  20105  dyadss  24294  opnmbllem  24301  lhop1lem  24712  aaliou3lem8  25040  zetacvg  25699  lgamgulmlem4  25716  ppi1  25848  cht1  25849  chtrpcl  25859  ppiltx  25861  chtub  25895  chpval2  25901  mersenne  25910  perfectlem1  25912  perfectlem2  25913  bpos1  25966  bposlem1  25967  bposlem6  25972  bposlem7  25973  bposlem8  25974  lgseisenlem1  26058  2sqblem  26114  chebbnd1lem1  26152  chebbnd1lem3  26154  chebbnd1  26155  chtppilimlem1  26156  chtppilimlem2  26157  chtppilim  26158  chto1ub  26159  chebbnd2  26160  chto1lb  26161  mulog2sumlem2  26218  pntrmax  26247  pntrlog2bndlem2  26261  pntrlog2bndlem4  26263  pntpbnd1a  26268  pntibndlem3  26275  pntibnd  26276  pntlemb  26280  pntlemk  26289  pnt  26297  axlowdim  26854  lfgrnloop  27017  lfuhgr1v0e  27143  nbusgrvtxm1  27268  cusgrsizeindb1  27339  lfgrwlkprop  27576  usgr2pthlem  27651  uspgrn2crct  27693  clwlkclwwlklem2fv2  27880  clwwlkext2edg  27940  eupth2lem3lem4  28115  ex-mod  28333  9p10ne21  28354  cshw1s2  30756  fib1  31886  ballotlem2  31974  chtvalz  32128  hgt750lemd  32147  hgt750lem  32150  hgt750leme  32157  lfuhgr2  32596  subfacp1lem1  32657  subfacp1lem5  32662  knoppndvlem12  34252  knoppndvlem18  34258  relowlpssretop  35061  tan2h  35329  opnmbllem0  35373  heiborlem7  35535  lcmineqlem22  39617  3lexlogpow5ineq2  39622  3lexlogpow5ineq4  39623  3lexlogpow5ineq3  39624  3lexlogpow2ineq1  39625  3lexlogpow2ineq2  39626  3lexlogpow5ineq5  39627  dvrelog2b  39632  dvrelogpow2b  39634  aks4d1p1p3  39635  aks4d1p1p2  39636  aks4d1p1p4  39637  aks4d1p1p6  39639  aks4d1p1p7  39640  aks4d1p1p5  39641  aks4d1p1  39642  flt4lem7  39988  pellfundgt1  40197  stoweidlem13  43021  stoweidlem26  43034  wallispilem4  43076  wallispi  43078  wallispi2lem1  43079  wallispi2lem2  43080  wallispi2  43081  stirlinglem1  43082  dirkertrigeqlem1  43106  dirkercncflem1  43111  fouriersw  43239  etransclem23  43265  salexct2  43345  fmtnoge3  44415  fmtnof1  44420  fmtno4prm  44460  2pwp1prm  44474  127prm  44484  sfprmdvdsmersenne  44488  lighneallem2  44491  dfodd4  44544  perfectALTVlem1  44606  perfectALTVlem2  44607  nnsum4primesevenALTV  44686  cznnring  44947  pw2m1lepw2m1  45294  difmodm1lt  45301  rege1logbzge0  45338  logbpw2m1  45346  fllog2  45347  blenpw2m1  45358  nnpw2blen  45359  dignn0flhalflem1  45394