Metamath Proof Explorer

Theorem lt2halves

Description: A sum is less than the whole if each term is less than half. (Contributed by NM, 13-Dec-2006)

Ref Expression
Assertion lt2halves ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C 2 ∧ B < C 2 → A + B < C

Proof

Step Hyp Ref Expression
1 3simpa ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A ∈ ℝ ∧ B ∈ ℝ
2 rehalfcl ⊢ C ∈ ℝ → C 2 ∈ ℝ
3 2 2 jca ⊢ C ∈ ℝ → C 2 ∈ ℝ ∧ C 2 ∈ ℝ
4 3 3ad2ant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → C 2 ∈ ℝ ∧ C 2 ∈ ℝ
5 lt2add ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C 2 ∈ ℝ ∧ C 2 ∈ ℝ → A < C 2 ∧ B < C 2 → A + B < C 2 + C 2
6 1 4 5 syl2anc ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C 2 ∧ B < C 2 → A + B < C 2 + C 2
7 recn ⊢ C ∈ ℝ → C ∈ ℂ
8 2halves ⊢ C ∈ ℂ → C 2 + C 2 = C
9 7 8 syl ⊢ C ∈ ℝ → C 2 + C 2 = C
10 9 breq2d ⊢ C ∈ ℝ → A + B < C 2 + C 2 ↔ A + B < C
11 10 3ad2ant3 ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A + B < C 2 + C 2 ↔ A + B < C
12 6 11 sylibd ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ C ∈ ℝ → A < C 2 ∧ B < C 2 → A + B < C