Theorem 1lt2 12347

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 11144	. . 3 ⊢ 1 ∈ ℝ
2	1	ltp1i 12060	. 2 ⊢ 1 < (1 + 1)
3		df-2 12244	. 2 ⊢ 2 = (1 + 1)
4	2, 3	breqtrri 5112	1 ⊢ 1 < 2

Syntax hints:   class class class wbr 5085  (class class class)co 7367  1c1 11039   + caddc 11041   < clt 11179  2c2 12236

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-1cn 11096  ax-icn 11097  ax-addcl 11098  ax-addrcl 11099  ax-mulcl 11100  ax-mulrcl 11101  ax-mulcom 11102  ax-addass 11103  ax-mulass 11104  ax-distr 11105  ax-i2m1 11106  ax-1ne0 11107  ax-1rid 11108  ax-rnegex 11109  ax-rrecex 11110  ax-cnre 11111  ax-pre-lttri 11112  ax-pre-lttrn 11113  ax-pre-ltadd 11114  ax-pre-mulgt0 11115

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-mpo 7372  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185  df-sub 11379  df-neg 11380  df-2 12244

This theorem is referenced by:  1lt3  12349  1lt4  12352  1lt6  12361  1lt7  12367  1lt8  12374  1lt9  12382  1ne2  12384  1le2  12385  halflt1  12394  nn0n0n1ge2b  12506  nn0ge2m1nn  12507  halfnz  12607  1lt10  12783  fztpval  13540  ige2m2fzo  13683  faclbnd5  14260  hashgt23el  14386  hashfun  14399  hashge2el2dif  14442  tpf1ofv2  14460  wrdlenge2n0  14514  ccat2s1p2  14593  s3fv1  14854  pfx2  14909  wwlktovf  14918  sqrt2gt1lt2  15236  ege2le3  16055  ene1  16177  mod2eq1n2dvds  16316  bits0o  16399  bitsfzolem  16403  bitsfzo  16404  bitsfi  16406  2prm  16661  4nprm  16664  iserodd  16806  dec2dvds  17034  dec5nprm  17037  dec2nprm  17038  2expltfac  17063  5prm  17079  6nprm  17080  7prm  17081  8nprm  17082  10nprm  17084  11prm  17085  13prm  17086  17prm  17087  19prm  17088  37prm  17091  83prm  17093  317prm  17096  631prm  17097  basendxltplusgndx  17249  rngstr  17261  lmodstr  17288  topgrpstr  17324  psgnunilem2  19470  isnzr2hash  20496  dyadss  25561  opnmbllem  25568  lhop1lem  25980  aaliou3lem8  26311  zetacvg  26978  lgamgulmlem4  26995  ppi1  27127  cht1  27128  chtrpcl  27138  ppiltx  27140  chtub  27175  chpval2  27181  mersenne  27190  perfectlem1  27192  perfectlem2  27193  bpos1  27246  bposlem1  27247  bposlem6  27252  bposlem7  27253  bposlem8  27254  lgseisenlem1  27338  2sqblem  27394  chebbnd1lem1  27432  chebbnd1lem3  27434  chebbnd1  27435  chtppilimlem1  27436  chtppilimlem2  27437  chtppilim  27438  chto1ub  27439  chebbnd2  27440  chto1lb  27441  mulog2sumlem2  27498  pntrmax  27527  pntrlog2bndlem2  27541  pntrlog2bndlem4  27543  pntpbnd1a  27548  pntibndlem3  27555  pntibnd  27556  pntlemb  27560  pntlemk  27569  pnt  27577  axlowdim  29030  lfgrnloop  29194  lfuhgr1v0e  29323  nbusgrvtxm1  29448  cusgrsizeindb1  29519  lfgrwlkprop  29754  usgr2pthlem  29831  uspgrn2crct  29876  clwlkclwwlklem2fv2  30066  clwwlkext2edg  30126  eupth2lem3lem4  30301  ex-mod  30519  9p10ne21  30540  cshw1s2  33020  drngidlhash  33494  rtelextdg2lem  33870  fib1  34544  ballotlem2  34633  chtvalz  34773  hgt750lemd  34792  hgt750lem  34795  hgt750leme  34802  lfuhgr2  35301  subfacp1lem1  35361  subfacp1lem5  35366  knoppndvlem12  36783  knoppndvlem18  36789  relowlpssretop  37680  tan2h  37933  opnmbllem0  37977  heiborlem7  38138  lcmineqlem22  42489  3lexlogpow5ineq2  42494  3lexlogpow5ineq4  42495  3lexlogpow5ineq3  42496  3lexlogpow2ineq1  42497  3lexlogpow2ineq2  42498  3lexlogpow5ineq5  42499  aks4d1lem1  42501  dvrelog2b  42505  dvrelogpow2b  42507  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p6  42512  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p1  42515  aks4d1p2  42516  aks4d1p3  42517  aks4d1p5  42519  aks4d1p6  42520  aks4d1p7d1  42521  aks4d1p7  42522  aks4d1p8  42526  aks4d1p9  42527  aks6d1c3  42562  aks6d1c6lem4  42612  aks6d1c7lem2  42620  flt4lem7  43092  pellfundgt1  43311  stoweidlem13  46441  stoweidlem26  46454  wallispilem4  46496  wallispi  46498  wallispi2lem1  46499  wallispi2lem2  46500  wallispi2  46501  stirlinglem1  46502  dirkertrigeqlem1  46526  dirkercncflem1  46531  fouriersw  46659  etransclem23  46685  salexct2  46767  nthrucw  47316  ceilhalfgt1  47781  ceil5half3  47794  difmodm1lt  47813  2timesltsqm1  47827  fmtnoge3  47993  fmtnof1  47998  fmtno4prm  48038  2pwp1prm  48052  127prm  48062  sfprmdvdsmersenne  48066  lighneallem2  48069  nprmdvdsfacm1lem4  48086  ppivalnn  48095  dfodd4  48135  perfectALTVlem1  48197  perfectALTVlem2  48198  nnsum4primesevenALTV  48277  gpgprismgrusgra  48534  cznnring  48738  pw2m1lepw2m1  48996  rege1logbzge0  49035  logbpw2m1  49043  fllog2  49044  blenpw2m1  49055  nnpw2blen  49056  dignn0flhalflem1  49091