Metamath Proof Explorer


Theorem lt2add

Description: Adding both sides of two 'less than' relations. Theorem I.25 of Apostol p. 20. (Contributed by NM, 15-Aug-1999) (Proof shortened by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion lt2add ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 < 𝐶𝐵 < 𝐷 ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 ltle ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐶𝐴𝐶 ) )
2 1 ad2ant2r ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 < 𝐶𝐴𝐶 ) )
3 leltadd ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴𝐶𝐵 < 𝐷 ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) )
4 2 3 syland ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 < 𝐶𝐵 < 𝐷 ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) )