Theorem 2lt3 12339

Description: 2 is less than 3. (Contributed by NM, 26-Sep-2010.)

Assertion

Ref	Expression
2lt3	⊢ 2 < 3

Proof of Theorem 2lt3

Step	Hyp	Ref	Expression
1		2re 12246	. . 3 ⊢ 2 ∈ ℝ
2	1	ltp1i 12051	. 2 ⊢ 2 < (2 + 1)
3		df-3 12236	. 2 ⊢ 3 = (2 + 1)
4	2, 3	breqtrri 5113	1 ⊢ 2 < 3

Syntax hints:   class class class wbr 5086  (class class class)co 7360  1c1 11030   + caddc 11032   < clt 11170  2c2 12227  3c3 12228

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 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7317  df-ov 7363  df-oprab 7364  df-mpo 7365  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-2 12235  df-3 12236

This theorem is referenced by:  1lt3  12340  2lt4  12342  2lt6  12351  2lt7  12357  2lt8  12364  2lt9  12372  3halfnz  12599  2lt10  12773  uzuzle23  12825  uz3m2nn  12835  fztpval  13531  fvf1tp  13739  expnass  14161  hash3tpde  14446  tpf1ofv2  14451  tpfo  14453  s4fv2  14850  f1oun2prg  14870  caucvgrlem  15626  cos01gt0  16149  3lcm2e6  16693  5prm  17070  11prm  17076  17prm  17078  23prm  17080  83prm  17084  317prm  17087  4001lem4  17105  plusgndxnmulrndx  17251  rngstr  17252  slotsdifunifndx  17355  cnfldstr  21346  cnfldstrOLD  21361  2logb9irr  26772  2logb3irr  26774  log2le1  26927  chtub  27189  bpos1  27260  bposlem6  27266  chto1ub  27453  dchrvmasumiflem1  27478  istrkg3ld  28543  tgcgr4  28613  axlowdimlem2  29026  axlowdimlem16  29040  axlowdimlem17  29041  axlowdim  29044  usgrexmpldifpr  29341  upgr3v3e3cycl  30265  konigsbergiedgw  30333  konigsberglem1  30337  konigsberglem2  30338  konigsberglem3  30339  ex-pss  30513  ex-res  30526  ex-fv  30528  ex-fl  30532  ex-mod  30534  evl1deg3  33653  2sqr3minply  33940  2sqr3nconstr  33941  cos9thpinconstrlem2  33950  prodfzo03  34763  cnndvlem1  36813  poimirlem9  37964  3lexlogpow2ineq1  42511  aks4d1p1p6  42526  aks4d1p1p5  42528  2ap1caineq  42598  rabren3dioph  43261  jm2.20nn  43443  wallispilem4  46514  fourierdlem87  46639  smfmullem4  47240  257prm  48036  31prm  48072  9fppr8  48225  fpprel2  48229  nnsum3primes4  48276  nnsum3primesgbe  48280  nnsum3primesle9  48282  nnsum4primesodd  48284  nnsum4primesoddALTV  48285  tgoldbach  48305  cycl3grtri  48435  usgrexmpl1lem  48509  usgrexmpl2lem  48514  usgrexmpl2nb2  48521  usgrexmpl2nb3  48522  usgrexmpl2trifr  48525  gpg3nbgrvtx0  48564  gpg3kgrtriexlem1  48571  zlmodzxznm  48985  zlmodzxzldeplem  48986  sepfsepc  49415