This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Proof

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