This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database REAL AND COMPLEX NUMBERS Integer sets Simple number properties lt2addmuld
Description: If two real numbers are less than a third real number, the sum of the
two real numbers is less than twice the third real number. (Contributed by Glauco Siliprandi , 11-Dec-2019)
Ref
Expression
Hypotheses
lt2addmuld.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
lt2addmuld.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
lt2addmuld.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
lt2addmuld.altc ⊢ ( 𝜑 → 𝐴 < 𝐶 )
lt2addmuld.bltc ⊢ ( 𝜑 → 𝐵 < 𝐶 )
Assertion
lt2addmuld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) < ( 2 · 𝐶 ) )
Proof
Step
Hyp
Ref
Expression
1
lt2addmuld.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2
lt2addmuld.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3
lt2addmuld.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4
lt2addmuld.altc ⊢ ( 𝜑 → 𝐴 < 𝐶 )
5
lt2addmuld.bltc ⊢ ( 𝜑 → 𝐵 < 𝐶 )
6
1 2 3 3 4 5
lt2addd ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐶 ) )
7
3
recnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
8
7
2timesd ⊢ ( 𝜑 → ( 2 · 𝐶 ) = ( 𝐶 + 𝐶 ) )
9
6 8
breqtrrd ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) < ( 2 · 𝐶 ) )