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 ⊢ φ → A ∈ ℝ
lt4addmuld.b ⊢ φ → B ∈ ℝ
lt4addmuld.c ⊢ φ → C ∈ ℝ
lt4addmuld.d ⊢ φ → D ∈ ℝ
lt4addmuld.e ⊢ φ → E ∈ ℝ
lt4addmuld.alte ⊢ φ → A < E
lt4addmuld.blte ⊢ φ → B < E
lt4addmuld.clte ⊢ φ → C < E
lt4addmuld.dlte ⊢ φ → D < E
Assertion lt4addmuld ⊢ φ → A + B + C + D < 4 ⁢ E

Proof

Step Hyp Ref Expression
1 lt4addmuld.a ⊢ φ → A ∈ ℝ
2 lt4addmuld.b ⊢ φ → B ∈ ℝ
3 lt4addmuld.c ⊢ φ → C ∈ ℝ
4 lt4addmuld.d ⊢ φ → D ∈ ℝ
5 lt4addmuld.e ⊢ φ → E ∈ ℝ
6 lt4addmuld.alte ⊢ φ → A < E
7 lt4addmuld.blte ⊢ φ → B < E
8 lt4addmuld.clte ⊢ φ → C < E
9 lt4addmuld.dlte ⊢ φ → D < E
10 1 2 readdcld ⊢ φ → A + B ∈ ℝ
11 10 3 readdcld ⊢ φ → A + B + C ∈ ℝ
12 3re ⊢ 3 ∈ ℝ
13 12 a1i ⊢ φ → 3 ∈ ℝ
14 13 5 remulcld ⊢ φ → 3 ⁢ E ∈ ℝ
15 1 2 3 5 6 7 8 lt3addmuld ⊢ φ → A + B + C < 3 ⁢ E
16 11 4 14 5 15 9 lt2addd ⊢ φ → A + B + C + D < 3 ⁢ E + E
17 df-4 ⊢ 4 = 3 + 1
18 17 a1i ⊢ φ → 4 = 3 + 1
19 18 oveq1d ⊢ φ → 4 ⁢ E = 3 + 1 ⁢ E
20 13 recnd ⊢ φ → 3 ∈ ℂ
21 5 recnd ⊢ φ → E ∈ ℂ
22 20 21 adddirp1d ⊢ φ → 3 + 1 ⁢ E = 3 ⁢ E + E
23 19 22 eqtr2d ⊢ φ → 3 ⁢ E + E = 4 ⁢ E
24 16 23 breqtrd ⊢ φ → A + B + C + D < 4 ⁢ E