Metamath Proof Explorer


Theorem lt2halvesd

Description: A sum is less than the whole if each term is less than half. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses rehalfcld.1 ( 𝜑𝐴 ∈ ℝ )
lt2halvesd.2 ( 𝜑𝐵 ∈ ℝ )
lt2halvesd.3 ( 𝜑𝐶 ∈ ℝ )
lt2halvesd.4 ( 𝜑𝐴 < ( 𝐶 / 2 ) )
lt2halvesd.5 ( 𝜑𝐵 < ( 𝐶 / 2 ) )
Assertion lt2halvesd ( 𝜑 → ( 𝐴 + 𝐵 ) < 𝐶 )

Proof

Step Hyp Ref Expression
1 rehalfcld.1 ( 𝜑𝐴 ∈ ℝ )
2 lt2halvesd.2 ( 𝜑𝐵 ∈ ℝ )
3 lt2halvesd.3 ( 𝜑𝐶 ∈ ℝ )
4 lt2halvesd.4 ( 𝜑𝐴 < ( 𝐶 / 2 ) )
5 lt2halvesd.5 ( 𝜑𝐵 < ( 𝐶 / 2 ) )
6 lt2halves ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < ( 𝐶 / 2 ) ∧ 𝐵 < ( 𝐶 / 2 ) ) → ( 𝐴 + 𝐵 ) < 𝐶 ) )
7 1 2 3 6 syl3anc ( 𝜑 → ( ( 𝐴 < ( 𝐶 / 2 ) ∧ 𝐵 < ( 𝐶 / 2 ) ) → ( 𝐴 + 𝐵 ) < 𝐶 ) )
8 4 5 7 mp2and ( 𝜑 → ( 𝐴 + 𝐵 ) < 𝐶 )