Theorem 3lt4 11397

Description: 3 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)

Assertion

Ref	Expression
3lt4	⊢ 3 < 4

Proof of Theorem 3lt4

Step	Hyp	Ref	Expression
1		3re 11294	. . 3 ⊢ 3 ∈ ℝ
2	1	ltp1i 11127	. 2 ⊢ 3 < (3 + 1)
3		df-4 11281	. 2 ⊢ 4 = (3 + 1)
4	2, 3	breqtrri 4813	1 ⊢ 3 < 4

Syntax hints:   class class class wbr 4786  (class class class)co 6791  1c1 10137   + caddc 10139   < clt 10274  3c3 11271  4c4 11272

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7094  ax-resscn 10193  ax-1cn 10194  ax-icn 10195  ax-addcl 10196  ax-addrcl 10197  ax-mulcl 10198  ax-mulrcl 10199  ax-mulcom 10200  ax-addass 10201  ax-mulass 10202  ax-distr 10203  ax-i2m1 10204  ax-1ne0 10205  ax-1rid 10206  ax-rnegex 10207  ax-rrecex 10208  ax-cnre 10209  ax-pre-lttri 10210  ax-pre-lttrn 10211  ax-pre-ltadd 10212  ax-pre-mulgt0 10213

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-mpt 4864  df-id 5157  df-po 5170  df-so 5171  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-iota 5992  df-fun 6031  df-fn 6032  df-f 6033  df-f1 6034  df-fo 6035  df-f1o 6036  df-fv 6037  df-riota 6752  df-ov 6794  df-oprab 6795  df-mpt2 6796  df-er 7894  df-en 8108  df-dom 8109  df-sdom 8110  df-pnf 10276  df-mnf 10277  df-xr 10278  df-ltxr 10279  df-le 10280  df-sub 10468  df-neg 10469  df-2 11279  df-3 11280  df-4 11281

This theorem is referenced by:  2lt4  11398  3lt5  11401  3lt6  11406  3lt7  11412  3lt8  11419  3lt9  11427  3lt10OLD  11436  3halfnz  11656  3lt10  11878  fz0to4untppr  12643  fldiv4p1lem1div2  12837  bpoly4  14989  ef01bndlem  15113  sin01bnd  15114  flodddiv4  15338  srngfn  16209  cnfldfun  19966  dveflem  23955  tangtx  24471  ppiublem1  25141  bpos1  25222  bposlem2  25224  gausslemma2dlem4  25308  2lgslem3b  25336  2lgslem3d  25338  chebbnd1lem2  25373  chebbnd1lem3  25374  chebbnd1  25375  pntlemb  25500  usgrexmplef  26367  upgr4cycl4dv4e  27358  ex-fl  27639  hlhilsmul  37744  stoweidlem26  40753  stoweid  40790  mod42tp1mod8  42040  nnsum4primes4  42198  nnsum4primesprm  42200  nnsum4primesgbe  42202  nnsum4primesle9  42204  nnsum4primeseven  42209  nnsum4primesevenALTV  42210  wtgoldbnnsum4prm  42211