Theorem 1lt2 12434

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 11258	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12169	. 2 ⊢ 1 < (1 + 1)
3		df-2 12326	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5174	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5147  (class class class)co 7430  1c1 11153   + caddc 11155   < clt 11292  2c2 12318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-2 12326

This theorem is referenced by:  1lt3  12436  1lt4  12439  1lt6  12448  1lt7  12454  1lt8  12461  1lt9  12469  1ne2  12471  1le2  12472  halflt1  12481  nn0n0n1ge2b  12592  nn0ge2m1nn  12593  halfnz  12693  1lt10  12869  fztpval  13622  ige2m2fzo  13763  faclbnd5  14333  hashgt23el  14459  hashfun  14472  hashge2el2dif  14515  tpf1ofv2  14533  wrdlenge2n0  14586  ccat2s1p2  14664  s3fv1  14927  pfx2  14982  wwlktovf  14991  sqrt2gt1lt2  15309  ege2le3  16122  ene1  16242  mod2eq1n2dvds  16380  bits0o  16463  bitsfzolem  16467  bitsfzo  16468  bitsfi  16470  2prm  16725  4nprm  16728  iserodd  16868  dec2dvds  17096  dec5nprm  17099  dec2nprm  17100  2expltfac  17126  5prm  17142  6nprm  17143  7prm  17144  8nprm  17145  10nprm  17147  11prm  17148  13prm  17149  17prm  17150  19prm  17151  37prm  17154  83prm  17156  317prm  17159  631prm  17160  basendxltplusgndx  17326  grpstr  17329  grpbaseOLD  17332  grpplusgOLD  17334  rngstr  17343  lmodstr  17370  topgrpstr  17406  psgnunilem2  19527  isnzr2hash  20535  dyadss  25642  opnmbllem  25649  lhop1lem  26066  aaliou3lem8  26401  zetacvg  27072  lgamgulmlem4  27089  ppi1  27221  cht1  27222  chtrpcl  27232  ppiltx  27234  chtub  27270  chpval2  27276  mersenne  27285  perfectlem1  27287  perfectlem2  27288  bpos1  27341  bposlem1  27342  bposlem6  27347  bposlem7  27348  bposlem8  27349  lgseisenlem1  27433  2sqblem  27489  chebbnd1lem1  27527  chebbnd1lem3  27529  chebbnd1  27530  chtppilimlem1  27531  chtppilimlem2  27532  chtppilim  27533  chto1ub  27534  chebbnd2  27535  chto1lb  27536  mulog2sumlem2  27593  pntrmax  27622  pntrlog2bndlem2  27636  pntrlog2bndlem4  27638  pntpbnd1a  27643  pntibndlem3  27650  pntibnd  27651  pntlemb  27655  pntlemk  27664  pnt  27672  axlowdim  28990  lfgrnloop  29156  lfuhgr1v0e  29285  nbusgrvtxm1  29410  cusgrsizeindb1  29482  lfgrwlkprop  29719  usgr2pthlem  29795  uspgrn2crct  29837  clwlkclwwlklem2fv2  30024  clwwlkext2edg  30084  eupth2lem3lem4  30259  ex-mod  30477  9p10ne21  30498  cshw1s2  32929  drngidlhash  33441  rtelextdg2lem  33731  fib1  34381  ballotlem2  34469  chtvalz  34622  hgt750lemd  34641  hgt750lem  34644  hgt750leme  34651  lfuhgr2  35102  subfacp1lem1  35163  subfacp1lem5  35168  knoppndvlem12  36505  knoppndvlem18  36511  relowlpssretop  37346  tan2h  37598  opnmbllem0  37642  heiborlem7  37803  lcmineqlem22  42031  3lexlogpow5ineq2  42036  3lexlogpow5ineq4  42037  3lexlogpow5ineq3  42038  3lexlogpow2ineq1  42039  3lexlogpow2ineq2  42040  3lexlogpow5ineq5  42041  aks4d1lem1  42043  dvrelog2b  42047  dvrelogpow2b  42049  aks4d1p1p3  42050  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p6  42054  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  aks4d1p9  42069  aks6d1c3  42104  aks6d1c6lem4  42154  aks6d1c7lem2  42162  flt4lem7  42645  pellfundgt1  42870  stoweidlem13  45968  stoweidlem26  45981  wallispilem4  46023  wallispi  46025  wallispi2lem1  46026  wallispi2lem2  46027  wallispi2  46028  stirlinglem1  46029  dirkertrigeqlem1  46053  dirkercncflem1  46058  fouriersw  46186  etransclem23  46212  salexct2  46294  ceil5half3  47279  fmtnoge3  47454  fmtnof1  47459  fmtno4prm  47499  2pwp1prm  47513  127prm  47523  sfprmdvdsmersenne  47527  lighneallem2  47530  dfodd4  47583  perfectALTVlem1  47645  perfectALTVlem2  47646  nnsum4primesevenALTV  47725  cznnring  48105  pw2m1lepw2m1  48365  difmodm1lt  48371  rege1logbzge0  48408  logbpw2m1  48416  fllog2  48417  blenpw2m1  48428  nnpw2blen  48429  dignn0flhalflem1  48464