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

Metamath Proof Explorer

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 · 𝐷 ) )