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

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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( ( 𝐴 < ( 𝐶 / 2 ) ∧ 𝐵 < ( 𝐶 / 2 ) ) → ( 𝐴 + 𝐵 ) < 𝐶 ) )

Proof

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