lt3addmuld

Description: If three real numbers are less than a fourth real number, the sum of the three real numbers is less than three times the third real number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	lt3addmuld.a	$⊢ φ \to A \in ℝ$
	lt3addmuld.b	$⊢ φ \to B \in ℝ$
	lt3addmuld.c	$⊢ φ \to C \in ℝ$
	lt3addmuld.d	$⊢ φ \to D \in ℝ$
	lt3addmuld.altd	$⊢ φ \to A < D$
	lt3addmuld.bltd	$⊢ φ \to B < D$
	lt3addmuld.cltd	$⊢ φ \to C < D$
Assertion	lt3addmuld	$⊢ φ \to A + B + C < 3 D$

Proof

Step	Hyp	Ref	Expression
1		lt3addmuld.a	$⊢ φ \to A \in ℝ$
2		lt3addmuld.b	$⊢ φ \to B \in ℝ$
3		lt3addmuld.c	$⊢ φ \to C \in ℝ$
4		lt3addmuld.d	$⊢ φ \to D \in ℝ$
5		lt3addmuld.altd	$⊢ φ \to A < D$
6		lt3addmuld.bltd	$⊢ φ \to B < D$
7		lt3addmuld.cltd	$⊢ φ \to C < D$
8	1 2	readdcld	$⊢ φ \to A + B \in ℝ$
9		2re	$⊢ 2 \in ℝ$
10	9	a1i	$⊢ φ \to 2 \in ℝ$
11	10 4	remulcld	$⊢ φ \to 2 D \in ℝ$
12	1 2 4 5 6	lt2addmuld	$⊢ φ \to A + B < 2 D$
13	8 3 11 4 12 7	lt2addd	$⊢ φ \to A + B + C < 2 D + D$
14	10	recnd	$⊢ φ \to 2 \in ℂ$
15	4	recnd	$⊢ φ \to D \in ℂ$
16	14 15	adddirp1d	$⊢ φ \to (2 + 1) D = 2 D + D$
17		2p1e3	$⊢ 2 + 1 = 3$
18	17	a1i	$⊢ φ \to 2 + 1 = 3$
19	18	oveq1d	$⊢ φ \to (2 + 1) D = 3 D$
20	16 19	eqtr3d	$⊢ φ \to 2 D + D = 3 D$
21	13 20	breqtrd	$⊢ φ \to A + B + C < 3 D$

Metamath Proof Explorer

Theorem lt3addmuld

Proof