Theorem 1lt2 12291

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 11112	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12026	. 2 ⊢ 1 < (1 + 1)
3		df-2 12188	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5118	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5091  (class class class)co 7346  1c1 11007   + caddc 11009   < clt 11146  2c2 12180

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pow 5303  ax-pr 5370  ax-un 7668  ax-resscn 11063  ax-1cn 11064  ax-icn 11065  ax-addcl 11066  ax-addrcl 11067  ax-mulcl 11068  ax-mulrcl 11069  ax-mulcom 11070  ax-addass 11071  ax-mulass 11072  ax-distr 11073  ax-i2m1 11074  ax-1ne0 11075  ax-1rid 11076  ax-rnegex 11077  ax-rrecex 11078  ax-cnre 11079  ax-pre-lttri 11080  ax-pre-lttrn 11081  ax-pre-ltadd 11082  ax-pre-mulgt0 11083

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-nel 3033  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-pw 4552  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5092  df-opab 5154  df-mpt 5173  df-id 5511  df-po 5524  df-so 5525  df-xp 5622  df-rel 5623  df-cnv 5624  df-co 5625  df-dm 5626  df-rn 5627  df-res 5628  df-ima 5629  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-riota 7303  df-ov 7349  df-oprab 7350  df-mpo 7351  df-er 8622  df-en 8870  df-dom 8871  df-sdom 8872  df-pnf 11148  df-mnf 11149  df-xr 11150  df-ltxr 11151  df-le 11152  df-sub 11346  df-neg 11347  df-2 12188

This theorem is referenced by:  1lt3  12293  1lt4  12296  1lt6  12305  1lt7  12311  1lt8  12318  1lt9  12326  1ne2  12328  1le2  12329  halflt1  12338  nn0n0n1ge2b  12450  nn0ge2m1nn  12451  halfnz  12551  1lt10  12727  fztpval  13486  ige2m2fzo  13628  faclbnd5  14205  hashgt23el  14331  hashfun  14344  hashge2el2dif  14387  tpf1ofv2  14405  wrdlenge2n0  14459  ccat2s1p2  14538  s3fv1  14799  pfx2  14854  wwlktovf  14863  sqrt2gt1lt2  15181  ege2le3  15997  ene1  16119  mod2eq1n2dvds  16258  bits0o  16341  bitsfzolem  16345  bitsfzo  16346  bitsfi  16348  2prm  16603  4nprm  16606  iserodd  16747  dec2dvds  16975  dec5nprm  16978  dec2nprm  16979  2expltfac  17004  5prm  17020  6nprm  17021  7prm  17022  8nprm  17023  10nprm  17025  11prm  17026  13prm  17027  17prm  17028  19prm  17029  37prm  17032  83prm  17034  317prm  17037  631prm  17038  basendxltplusgndx  17190  rngstr  17202  lmodstr  17229  topgrpstr  17265  psgnunilem2  19408  isnzr2hash  20435  dyadss  25523  opnmbllem  25530  lhop1lem  25946  aaliou3lem8  26281  zetacvg  26953  lgamgulmlem4  26970  ppi1  27102  cht1  27103  chtrpcl  27113  ppiltx  27115  chtub  27151  chpval2  27157  mersenne  27166  perfectlem1  27168  perfectlem2  27169  bpos1  27222  bposlem1  27223  bposlem6  27228  bposlem7  27229  bposlem8  27230  lgseisenlem1  27314  2sqblem  27370  chebbnd1lem1  27408  chebbnd1lem3  27410  chebbnd1  27411  chtppilimlem1  27412  chtppilimlem2  27413  chtppilim  27414  chto1ub  27415  chebbnd2  27416  chto1lb  27417  mulog2sumlem2  27474  pntrmax  27503  pntrlog2bndlem2  27517  pntrlog2bndlem4  27519  pntpbnd1a  27524  pntibndlem3  27531  pntibnd  27532  pntlemb  27536  pntlemk  27545  pnt  27553  axlowdim  28940  lfgrnloop  29104  lfuhgr1v0e  29233  nbusgrvtxm1  29358  cusgrsizeindb1  29430  lfgrwlkprop  29665  usgr2pthlem  29742  uspgrn2crct  29787  clwlkclwwlklem2fv2  29974  clwwlkext2edg  30034  eupth2lem3lem4  30209  ex-mod  30427  9p10ne21  30448  cshw1s2  32939  drngidlhash  33397  rtelextdg2lem  33737  fib1  34411  ballotlem2  34500  chtvalz  34640  hgt750lemd  34659  hgt750lem  34662  hgt750leme  34669  lfuhgr2  35161  subfacp1lem1  35221  subfacp1lem5  35226  knoppndvlem12  36563  knoppndvlem18  36569  relowlpssretop  37404  tan2h  37658  opnmbllem0  37702  heiborlem7  37863  lcmineqlem22  42089  3lexlogpow5ineq2  42094  3lexlogpow5ineq4  42095  3lexlogpow5ineq3  42096  3lexlogpow2ineq1  42097  3lexlogpow2ineq2  42098  3lexlogpow5ineq5  42099  aks4d1lem1  42101  dvrelog2b  42105  dvrelogpow2b  42107  aks4d1p1p3  42108  aks4d1p1p2  42109  aks4d1p1p4  42110  aks4d1p1p6  42112  aks4d1p1p7  42113  aks4d1p1p5  42114  aks4d1p1  42115  aks4d1p2  42116  aks4d1p3  42117  aks4d1p5  42119  aks4d1p6  42120  aks4d1p7d1  42121  aks4d1p7  42122  aks4d1p8  42126  aks4d1p9  42127  aks6d1c3  42162  aks6d1c6lem4  42212  aks6d1c7lem2  42220  flt4lem7  42698  pellfundgt1  42922  stoweidlem13  46057  stoweidlem26  46070  wallispilem4  46112  wallispi  46114  wallispi2lem1  46115  wallispi2lem2  46116  wallispi2  46117  stirlinglem1  46118  dirkertrigeqlem1  46142  dirkercncflem1  46147  fouriersw  46275  etransclem23  46301  salexct2  46383  ceilhalfgt1  47366  ceil5half3  47377  difmodm1lt  47396  fmtnoge3  47567  fmtnof1  47572  fmtno4prm  47612  2pwp1prm  47626  127prm  47636  sfprmdvdsmersenne  47640  lighneallem2  47643  dfodd4  47696  perfectALTVlem1  47758  perfectALTVlem2  47759  nnsum4primesevenALTV  47838  gpgprismgrusgra  48095  cznnring  48299  pw2m1lepw2m1  48558  rege1logbzge0  48597  logbpw2m1  48605  fllog2  48606  blenpw2m1  48617  nnpw2blen  48618  dignn0flhalflem1  48653