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	$$⊢\phi \to A\in ℝ$$
	lt2addmuld.b	$$⊢\phi \to B\in ℝ$$
	lt2addmuld.c	$$⊢\phi \to C\in ℝ$$
	lt2addmuld.altc	$$⊢\phi \to A<C$$
	lt2addmuld.bltc	$$⊢\phi \to B<C$$
Assertion	lt2addmuld	$$⊢\phi \to A+B<2C$$

Proof

Step	Hyp	Ref	Expression
1		lt2addmuld.a	$$⊢\phi \to A\in ℝ$$
2		lt2addmuld.b	$$⊢\phi \to B\in ℝ$$
3		lt2addmuld.c	$$⊢\phi \to C\in ℝ$$
4		lt2addmuld.altc	$$⊢\phi \to A<C$$
5		lt2addmuld.bltc	$$⊢\phi \to B<C$$
6	1 2 3 3 4 5	lt2addd	$$⊢\phi \to A+B<C+C$$
7	3	recnd	$$⊢\phi \to C\in ℂ$$
8	7	2timesd	$$⊢\phi \to 2C=C+C$$
9	6 8	breqtrrd	$$⊢\phi \to A+B<2C$$