Theorem 1lt2 12074

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 10906	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 11809	. 2 ⊢ 1 < (1 + 1)
3		df-2 11966	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5097	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5070  (class class class)co 7255  1c1 10803   + caddc 10805   < clt 10940  2c2 11958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-po 5494  df-so 5495  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-2 11966

This theorem is referenced by:  1lt3  12076  1lt4  12079  1lt6  12088  1lt7  12094  1lt8  12101  1lt9  12109  1ne2  12111  1le2  12112  halflt1  12121  nn0n0n1ge2b  12231  nn0ge2m1nn  12232  halfnz  12328  1lt10  12505  fztpval  13247  ige2m2fzo  13378  faclbnd5  13940  hashgt23el  14067  hashfun  14080  hashge2el2dif  14122  wrdlenge2n0  14183  ccat2s1p2  14265  ccat2s1p2OLD  14267  s3fv1  14533  pfx2  14588  wwlktovf  14599  sqrt2gt1lt2  14914  ege2le3  15727  ene1  15847  mod2eq1n2dvds  15984  bits0o  16065  bitsfzolem  16069  bitsfzo  16070  bitsfi  16072  2prm  16325  4nprm  16328  iserodd  16464  dec2dvds  16692  dec5nprm  16695  dec2nprm  16696  2expltfac  16722  5prm  16738  6nprm  16739  7prm  16740  8nprm  16741  10nprm  16743  11prm  16744  13prm  16745  17prm  16746  19prm  16747  37prm  16750  83prm  16752  317prm  16755  631prm  16756  basendxltplusgndx  16917  grpstr  16920  grpbaseOLD  16923  grpplusgOLD  16925  rngstr  16934  lmodstr  16961  topgrpstr  16995  psgnunilem2  19018  isnzr2hash  20448  dyadss  24663  opnmbllem  24670  lhop1lem  25082  aaliou3lem8  25410  zetacvg  26069  lgamgulmlem4  26086  ppi1  26218  cht1  26219  chtrpcl  26229  ppiltx  26231  chtub  26265  chpval2  26271  mersenne  26280  perfectlem1  26282  perfectlem2  26283  bpos1  26336  bposlem1  26337  bposlem6  26342  bposlem7  26343  bposlem8  26344  lgseisenlem1  26428  2sqblem  26484  chebbnd1lem1  26522  chebbnd1lem3  26524  chebbnd1  26525  chtppilimlem1  26526  chtppilimlem2  26527  chtppilim  26528  chto1ub  26529  chebbnd2  26530  chto1lb  26531  mulog2sumlem2  26588  pntrmax  26617  pntrlog2bndlem2  26631  pntrlog2bndlem4  26633  pntpbnd1a  26638  pntibndlem3  26645  pntibnd  26646  pntlemb  26650  pntlemk  26659  pnt  26667  axlowdim  27232  lfgrnloop  27398  lfuhgr1v0e  27524  nbusgrvtxm1  27649  cusgrsizeindb1  27720  lfgrwlkprop  27957  usgr2pthlem  28032  uspgrn2crct  28074  clwlkclwwlklem2fv2  28261  clwwlkext2edg  28321  eupth2lem3lem4  28496  ex-mod  28714  9p10ne21  28735  cshw1s2  31134  fib1  32267  ballotlem2  32355  chtvalz  32509  hgt750lemd  32528  hgt750lem  32531  hgt750leme  32538  lfuhgr2  32980  subfacp1lem1  33041  subfacp1lem5  33046  knoppndvlem12  34630  knoppndvlem18  34636  relowlpssretop  35462  tan2h  35696  opnmbllem0  35740  heiborlem7  35902  lcmineqlem22  39986  3lexlogpow5ineq2  39991  3lexlogpow5ineq4  39992  3lexlogpow5ineq3  39993  3lexlogpow2ineq1  39994  3lexlogpow2ineq2  39995  3lexlogpow5ineq5  39996  aks4d1lem1  39998  dvrelog2b  40002  dvrelogpow2b  40004  aks4d1p1p3  40005  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p6  40009  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  aks4d1p9  40024  flt4lem7  40412  pellfundgt1  40621  stoweidlem13  43444  stoweidlem26  43457  wallispilem4  43499  wallispi  43501  wallispi2lem1  43502  wallispi2lem2  43503  wallispi2  43504  stirlinglem1  43505  dirkertrigeqlem1  43529  dirkercncflem1  43534  fouriersw  43662  etransclem23  43688  salexct2  43768  fmtnoge3  44870  fmtnof1  44875  fmtno4prm  44915  2pwp1prm  44929  127prm  44939  sfprmdvdsmersenne  44943  lighneallem2  44946  dfodd4  44999  perfectALTVlem1  45061  perfectALTVlem2  45062  nnsum4primesevenALTV  45141  cznnring  45402  pw2m1lepw2m1  45749  difmodm1lt  45756  rege1logbzge0  45793  logbpw2m1  45801  fllog2  45802  blenpw2m1  45813  nnpw2blen  45814  dignn0flhalflem1  45849