Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	lt3addmuld.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	lt3addmuld.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	lt3addmuld.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
	lt3addmuld.altd	⊢ ( 𝜑 → 𝐴 < 𝐷 )
	lt3addmuld.bltd	⊢ ( 𝜑 → 𝐵 < 𝐷 )
	lt3addmuld.cltd	⊢ ( 𝜑 → 𝐶 < 𝐷 )
Assertion	lt3addmuld	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) + 𝐶 ) < ( 3 · 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		lt3addmuld.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		lt3addmuld.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		lt3addmuld.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		lt3addmuld.d	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5		lt3addmuld.altd	⊢ ( 𝜑 → 𝐴 < 𝐷 )
6		lt3addmuld.bltd	⊢ ( 𝜑 → 𝐵 < 𝐷 )
7		lt3addmuld.cltd	⊢ ( 𝜑 → 𝐶 < 𝐷 )
8	1 2	readdcld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
9		2re	⊢ 2 ∈ ℝ
10	9	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
11	10 4	remulcld	⊢ ( 𝜑 → ( 2 · 𝐷 ) ∈ ℝ )
12	1 2 4 5 6	lt2addmuld	⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) < ( 2 · 𝐷 ) )
13	8 3 11 4 12 7	lt2addd	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) + 𝐶 ) < ( ( 2 · 𝐷 ) + 𝐷 ) )
14	10	recnd	⊢ ( 𝜑 → 2 ∈ ℂ )
15	4	recnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
16	14 15	adddirp1d	⊢ ( 𝜑 → ( ( 2 + 1 ) · 𝐷 ) = ( ( 2 · 𝐷 ) + 𝐷 ) )
17		2p1e3	⊢ ( 2 + 1 ) = 3
18	17	a1i	⊢ ( 𝜑 → ( 2 + 1 ) = 3 )
19	18	oveq1d	⊢ ( 𝜑 → ( ( 2 + 1 ) · 𝐷 ) = ( 3 · 𝐷 ) )
20	16 19	eqtr3d	⊢ ( 𝜑 → ( ( 2 · 𝐷 ) + 𝐷 ) = ( 3 · 𝐷 ) )
21	13 20	breqtrd	⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) + 𝐶 ) < ( 3 · 𝐷 ) )