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

Metamath Proof Explorer

Theorem lt4addmuld

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

Ref Expression
Hypotheses lt4addmuld.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
lt4addmuld.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
lt4addmuld.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
lt4addmuld.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
lt4addmuld.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
lt4addmuld.alte ⊢ ( 𝜑 → 𝐴 < 𝐸 )
lt4addmuld.blte ⊢ ( 𝜑 → 𝐵 < 𝐸 )
lt4addmuld.clte ⊢ ( 𝜑 → 𝐶 < 𝐸 )
lt4addmuld.dlte ⊢ ( 𝜑 → 𝐷 < 𝐸 )
Assertion lt4addmuld ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) + 𝐷 ) < ( 4 · 𝐸 ) )

Proof

Step Hyp Ref Expression
1 lt4addmuld.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 lt4addmuld.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 lt4addmuld.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4 lt4addmuld.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5 lt4addmuld.e ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
6 lt4addmuld.alte ⊢ ( 𝜑 → 𝐴 < 𝐸 )
7 lt4addmuld.blte ⊢ ( 𝜑 → 𝐵 < 𝐸 )
8 lt4addmuld.clte ⊢ ( 𝜑 → 𝐶 < 𝐸 )
9 lt4addmuld.dlte ⊢ ( 𝜑 → 𝐷 < 𝐸 )
10 1 2 readdcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
11 10 3 readdcld ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) + 𝐶 ) ∈ ℝ )
12 3re ⊢ 3 ∈ ℝ
13 12 a1i ⊢ ( 𝜑 → 3 ∈ ℝ )
14 13 5 remulcld ⊢ ( 𝜑 → ( 3 · 𝐸 ) ∈ ℝ )
15 1 2 3 5 6 7 8 lt3addmuld ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) + 𝐶 ) < ( 3 · 𝐸 ) )
16 11 4 14 5 15 9 lt2addd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) + 𝐷 ) < ( ( 3 · 𝐸 ) + 𝐸 ) )
17 df-4 ⊢ 4 = ( 3 + 1 )
18 17 a1i ⊢ ( 𝜑 → 4 = ( 3 + 1 ) )
19 18 oveq1d ⊢ ( 𝜑 → ( 4 · 𝐸 ) = ( ( 3 + 1 ) · 𝐸 ) )
20 13 recnd ⊢ ( 𝜑 → 3 ∈ ℂ )
21 5 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
22 20 21 adddirp1d ⊢ ( 𝜑 → ( ( 3 + 1 ) · 𝐸 ) = ( ( 3 · 𝐸 ) + 𝐸 ) )
23 19 22 eqtr2d ⊢ ( 𝜑 → ( ( 3 · 𝐸 ) + 𝐸 ) = ( 4 · 𝐸 ) )
24 16 23 breqtrd ⊢ ( 𝜑 → ( ( ( 𝐴 + 𝐵 ) + 𝐶 ) + 𝐷 ) < ( 4 · 𝐸 ) )