# Metamath Proof Explorer

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 ${⊢}{\phi }\to {A}\in ℝ$
lt4addmuld.b ${⊢}{\phi }\to {B}\in ℝ$
lt4addmuld.c ${⊢}{\phi }\to {C}\in ℝ$
lt4addmuld.d ${⊢}{\phi }\to {D}\in ℝ$
lt4addmuld.e ${⊢}{\phi }\to {E}\in ℝ$
lt4addmuld.alte ${⊢}{\phi }\to {A}<{E}$
lt4addmuld.blte ${⊢}{\phi }\to {B}<{E}$
lt4addmuld.clte ${⊢}{\phi }\to {C}<{E}$
lt4addmuld.dlte ${⊢}{\phi }\to {D}<{E}$
Assertion lt4addmuld ${⊢}{\phi }\to \left({A}+{B}\right)+{C}+{D}<4{E}$

### Proof

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