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	|- ( ph -> A e. RR )
	lt2addmuld.b	|- ( ph -> B e. RR )
	lt2addmuld.c	|- ( ph -> C e. RR )
	lt2addmuld.altc	|- ( ph -> A < C )
	lt2addmuld.bltc	|- ( ph -> B < C )
Assertion	lt2addmuld	|- ( ph -> ( A + B ) < ( 2 x. C ) )

Proof

Step	Hyp	Ref	Expression
1		lt2addmuld.a	|- ( ph -> A e. RR )
2		lt2addmuld.b	|- ( ph -> B e. RR )
3		lt2addmuld.c	|- ( ph -> C e. RR )
4		lt2addmuld.altc	|- ( ph -> A < C )
5		lt2addmuld.bltc	|- ( ph -> B < C )
6	1 2 3 3 4 5	lt2addd	|- ( ph -> ( A + B ) < ( C + C ) )
7	3	recnd	|- ( ph -> C e. CC )
8	7	2timesd	|- ( ph -> ( 2 x. C ) = ( C + C ) )
9	6 8	breqtrrd	|- ( ph -> ( A + B ) < ( 2 x. C ) )