Theorem 1lt2 11809

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 10641	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 11544	. 2 ⊢ 1 < (1 + 1)
3		df-2 11701	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5093	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5066  (class class class)co 7156  1c1 10538   + caddc 10540   < clt 10675  2c2 11693

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-1cn 10595  ax-icn 10596  ax-addcl 10597  ax-addrcl 10598  ax-mulcl 10599  ax-mulrcl 10600  ax-mulcom 10601  ax-addass 10602  ax-mulass 10603  ax-distr 10604  ax-i2m1 10605  ax-1ne0 10606  ax-1rid 10607  ax-rnegex 10608  ax-rrecex 10609  ax-cnre 10610  ax-pre-lttri 10611  ax-pre-lttrn 10612  ax-pre-ltadd 10613  ax-pre-mulgt0 10614

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-po 5474  df-so 5475  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681  df-sub 10872  df-neg 10873  df-2 11701

This theorem is referenced by:  1lt3  11811  1lt4  11814  1lt6  11823  1lt7  11829  1lt8  11836  1lt9  11844  1ne2  11846  1le2  11847  halflt1  11856  nn0n0n1ge2b  11964  nn0ge2m1nn  11965  halfnz  12061  1lt10  12238  fztpval  12970  ige2m2fzo  13101  faclbnd5  13659  hashgt23el  13786  hashfun  13799  hashge2el2dif  13839  wrdlenge2n0  13904  ccat2s1p2  13986  ccat2s1p2OLD  13988  s3fv1  14254  pfx2  14309  wwlktovf  14320  sqrt2gt1lt2  14634  ege2le3  15443  ene1  15563  mod2eq1n2dvds  15696  n2dvds1OLD  15718  bits0o  15779  bitsfzolem  15783  bitsfzo  15784  bitsfi  15786  2prm  16036  4nprm  16039  iserodd  16172  dec2dvds  16399  dec5nprm  16402  dec2nprm  16403  2expltfac  16426  5prm  16442  6nprm  16443  7prm  16444  8nprm  16445  10nprm  16447  11prm  16448  13prm  16449  17prm  16450  19prm  16451  37prm  16454  83prm  16456  317prm  16459  631prm  16460  grpstr  16609  grpbase  16610  grpplusg  16611  ressplusg  16612  rngstr  16619  lmodstr  16636  topgrpstr  16661  psgnunilem2  18623  isnzr2hash  20037  dyadss  24195  opnmbllem  24202  lhop1lem  24610  aaliou3lem8  24934  zetacvg  25592  lgamgulmlem4  25609  ppi1  25741  cht1  25742  chtrpcl  25752  ppiltx  25754  chtub  25788  chpval2  25794  mersenne  25803  perfectlem1  25805  perfectlem2  25806  bpos1  25859  bposlem1  25860  bposlem6  25865  bposlem7  25866  bposlem8  25867  lgseisenlem1  25951  2sqblem  26007  chebbnd1lem1  26045  chebbnd1lem3  26047  chebbnd1  26048  chtppilimlem1  26049  chtppilimlem2  26050  chtppilim  26051  chto1ub  26052  chebbnd2  26053  chto1lb  26054  mulog2sumlem2  26111  pntrmax  26140  pntrlog2bndlem2  26154  pntrlog2bndlem4  26156  pntpbnd1a  26161  pntibndlem3  26168  pntibnd  26169  pntlemb  26173  pntlemk  26182  pnt  26190  axlowdim  26747  lfgrnloop  26910  lfuhgr1v0e  27036  nbusgrvtxm1  27161  cusgrsizeindb1  27232  lfgrwlkprop  27469  usgr2pthlem  27544  uspgrn2crct  27586  clwlkclwwlklem2fv2  27774  clwwlkext2edg  27835  eupth2lem3lem4  28010  ex-mod  28228  9p10ne21  28249  cshw1s2  30634  fib1  31658  ballotlem2  31746  chtvalz  31900  hgt750lemd  31919  hgt750lem  31922  hgt750leme  31929  lfuhgr2  32365  subfacp1lem1  32426  subfacp1lem5  32431  knoppndvlem12  33862  knoppndvlem18  33868  relowlpssretop  34648  tan2h  34899  opnmbllem0  34943  heiborlem7  35110  pellfundgt1  39529  stoweidlem13  42347  stoweidlem26  42360  wallispilem4  42402  wallispi  42404  wallispi2lem1  42405  wallispi2lem2  42406  wallispi2  42407  stirlinglem1  42408  dirkertrigeqlem1  42432  dirkercncflem1  42437  fouriersw  42565  etransclem23  42591  salexct2  42671  fmtnoge3  43741  fmtnof1  43746  fmtno4prm  43786  2pwp1prm  43800  127prm  43812  sfprmdvdsmersenne  43817  lighneallem2  43820  dfodd4  43873  perfectALTVlem1  43935  perfectALTVlem2  43936  nnsum4primesevenALTV  44015  cznnring  44276  pw2m1lepw2m1  44624  difmodm1lt  44631  rege1logbzge0  44668  logbpw2m1  44676  fllog2  44677  blenpw2m1  44688  nnpw2blen  44689  dignn0flhalflem1  44724