Theorem 1lt2 12153

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 10984	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 11888	. 2 ⊢ 1 < (1 + 1)
3		df-2 12045	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5102	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5075  (class class class)co 7284  1c1 10881   + caddc 10883   < clt 11018  2c2 12037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-1cn 10938  ax-icn 10939  ax-addcl 10940  ax-addrcl 10941  ax-mulcl 10942  ax-mulrcl 10943  ax-mulcom 10944  ax-addass 10945  ax-mulass 10946  ax-distr 10947  ax-i2m1 10948  ax-1ne0 10949  ax-1rid 10950  ax-rnegex 10951  ax-rrecex 10952  ax-cnre 10953  ax-pre-lttri 10954  ax-pre-lttrn 10955  ax-pre-ltadd 10956  ax-pre-mulgt0 10957

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3070  df-rex 3071  df-reu 3073  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-po 5504  df-so 5505  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-riota 7241  df-ov 7287  df-oprab 7288  df-mpo 7289  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024  df-sub 11216  df-neg 11217  df-2 12045

This theorem is referenced by:  1lt3  12155  1lt4  12158  1lt6  12167  1lt7  12173  1lt8  12180  1lt9  12188  1ne2  12190  1le2  12191  halflt1  12200  nn0n0n1ge2b  12310  nn0ge2m1nn  12311  halfnz  12407  1lt10  12585  fztpval  13327  ige2m2fzo  13459  faclbnd5  14021  hashgt23el  14148  hashfun  14161  hashge2el2dif  14203  wrdlenge2n0  14264  ccat2s1p2  14346  ccat2s1p2OLD  14348  s3fv1  14614  pfx2  14669  wwlktovf  14680  sqrt2gt1lt2  14995  ege2le3  15808  ene1  15928  mod2eq1n2dvds  16065  bits0o  16146  bitsfzolem  16150  bitsfzo  16151  bitsfi  16153  2prm  16406  4nprm  16409  iserodd  16545  dec2dvds  16773  dec5nprm  16776  dec2nprm  16777  2expltfac  16803  5prm  16819  6nprm  16820  7prm  16821  8nprm  16822  10nprm  16824  11prm  16825  13prm  16826  17prm  16827  19prm  16828  37prm  16831  83prm  16833  317prm  16836  631prm  16837  basendxltplusgndx  17000  grpstr  17003  grpbaseOLD  17006  grpplusgOLD  17008  rngstr  17017  lmodstr  17044  topgrpstr  17080  psgnunilem2  19112  isnzr2hash  20544  dyadss  24767  opnmbllem  24774  lhop1lem  25186  aaliou3lem8  25514  zetacvg  26173  lgamgulmlem4  26190  ppi1  26322  cht1  26323  chtrpcl  26333  ppiltx  26335  chtub  26369  chpval2  26375  mersenne  26384  perfectlem1  26386  perfectlem2  26387  bpos1  26440  bposlem1  26441  bposlem6  26446  bposlem7  26447  bposlem8  26448  lgseisenlem1  26532  2sqblem  26588  chebbnd1lem1  26626  chebbnd1lem3  26628  chebbnd1  26629  chtppilimlem1  26630  chtppilimlem2  26631  chtppilim  26632  chto1ub  26633  chebbnd2  26634  chto1lb  26635  mulog2sumlem2  26692  pntrmax  26721  pntrlog2bndlem2  26735  pntrlog2bndlem4  26737  pntpbnd1a  26742  pntibndlem3  26749  pntibnd  26750  pntlemb  26754  pntlemk  26763  pnt  26771  axlowdim  27338  lfgrnloop  27504  lfuhgr1v0e  27630  nbusgrvtxm1  27755  cusgrsizeindb1  27826  lfgrwlkprop  28064  usgr2pthlem  28140  uspgrn2crct  28182  clwlkclwwlklem2fv2  28369  clwwlkext2edg  28429  eupth2lem3lem4  28604  ex-mod  28822  9p10ne21  28843  cshw1s2  31241  fib1  32376  ballotlem2  32464  chtvalz  32618  hgt750lemd  32637  hgt750lem  32640  hgt750leme  32647  lfuhgr2  33089  subfacp1lem1  33150  subfacp1lem5  33155  knoppndvlem12  34712  knoppndvlem18  34718  relowlpssretop  35544  tan2h  35778  opnmbllem0  35822  heiborlem7  35984  lcmineqlem22  40065  3lexlogpow5ineq2  40070  3lexlogpow5ineq4  40071  3lexlogpow5ineq3  40072  3lexlogpow2ineq1  40073  3lexlogpow2ineq2  40074  3lexlogpow5ineq5  40075  aks4d1lem1  40077  dvrelog2b  40081  dvrelogpow2b  40083  aks4d1p1p3  40084  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1p6  40088  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p2  40092  aks4d1p3  40093  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8  40102  aks4d1p9  40103  flt4lem7  40503  pellfundgt1  40712  stoweidlem13  43561  stoweidlem26  43574  wallispilem4  43616  wallispi  43618  wallispi2lem1  43619  wallispi2lem2  43620  wallispi2  43621  stirlinglem1  43622  dirkertrigeqlem1  43646  dirkercncflem1  43651  fouriersw  43779  etransclem23  43805  salexct2  43885  fmtnoge3  44993  fmtnof1  44998  fmtno4prm  45038  2pwp1prm  45052  127prm  45062  sfprmdvdsmersenne  45066  lighneallem2  45069  dfodd4  45122  perfectALTVlem1  45184  perfectALTVlem2  45185  nnsum4primesevenALTV  45264  cznnring  45525  pw2m1lepw2m1  45872  difmodm1lt  45879  rege1logbzge0  45916  logbpw2m1  45924  fllog2  45925  blenpw2m1  45936  nnpw2blen  45937  dignn0flhalflem1  45972