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 ⊢ φ → A ∈ ℝ
lt2halvesd.2 ⊢ φ → B ∈ ℝ
lt2halvesd.3 ⊢ φ → C ∈ ℝ
lt2halvesd.4 ⊢ φ → A < C 2
lt2halvesd.5 ⊢ φ → B < C 2
Assertion lt2halvesd ⊢ φ → A + B < C

Proof

Step Hyp Ref Expression
1 rehalfcld.1 ⊢ φ → A ∈ ℝ
2 lt2halvesd.2 ⊢ φ → B ∈ ℝ
3 lt2halvesd.3 ⊢ φ → C ∈ ℝ
4 lt2halvesd.4 ⊢ φ → A < C 2
5 lt2halvesd.5 ⊢ φ → B < C 2
6 lt2halves ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C 2 ∧ B < C 2 → A + B < C
7 1 2 3 6 syl3anc ⊢ φ → A < C 2 ∧ B < C 2 → A + B < C
8 4 5 7 mp2and ⊢ φ → A + B < C