Theorem 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 · 𝐶 ) )