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

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 ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) < 𝐶 )