Theorem 3lt4 11798

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 11704	. . 3 ⊢ 3 ∈ ℝ
2	1	ltp1i 11530	. 2 ⊢ 3 < (3 + 1)
3		df-4 11689	. 2 ⊢ 4 = (3 + 1)
4	2, 3	breqtrri 5079	1 ⊢ 3 < 4

Syntax hints:   class class class wbr 5052  (class class class)co 7142  1c1 10524   + caddc 10526   < clt 10661  3c3 11680  4c4 11681

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447  ax-resscn 10580  ax-1cn 10581  ax-icn 10582  ax-addcl 10583  ax-addrcl 10584  ax-mulcl 10585  ax-mulrcl 10586  ax-mulcom 10587  ax-addass 10588  ax-mulass 10589  ax-distr 10590  ax-i2m1 10591  ax-1ne0 10592  ax-1rid 10593  ax-rnegex 10594  ax-rrecex 10595  ax-cnre 10596  ax-pre-lttri 10597  ax-pre-lttrn 10598  ax-pre-ltadd 10599  ax-pre-mulgt0 10600

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-po 5460  df-so 5461  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-mpo 7147  df-er 8275  df-en 8496  df-dom 8497  df-sdom 8498  df-pnf 10663  df-mnf 10664  df-xr 10665  df-ltxr 10666  df-le 10667  df-sub 10858  df-neg 10859  df-2 11687  df-3 11688  df-4 11689

This theorem is referenced by:  2lt4  11799  3lt5  11802  3lt6  11807  3lt7  11813  3lt8  11820  3lt9  11828  3halfnz  12048  3lt10  12222  fz0to4untppr  13000  fldiv4p1lem1div2  13195  bpoly4  15398  ef01bndlem  15522  sin01bnd  15523  flodddiv4  15747  srngstr  16610  cnfldfun  20540  dveflem  24561  tangtx  25077  ppiublem1  25764  bpos1  25845  bposlem2  25847  gausslemma2dlem4  25931  2lgslem3b  25959  2lgslem3d  25961  chebbnd1lem2  26032  chebbnd1lem3  26033  chebbnd1  26034  pntlemb  26159  usgrexmplef  27027  upgr4cycl4dv4e  27948  ex-fl  28210  hlhilsmul  39109  stoweidlem26  42401  stoweid  42438  mod42tp1mod8  43852  nnsum4primes4  44039  nnsum4primesprm  44041  nnsum4primesgbe  44043  nnsum4primesle9  44045  nnsum4primeseven  44050  nnsum4primesevenALTV  44051  wtgoldbnnsum4prm  44052