Theorem ltleadd

Description: Adding both sides of two orderings. (Contributed by NM, 23-Dec-2007)

	Ref	Expression
Assertion	ltleadd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷 ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltadd1	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐶 ↔ ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐵 ) ) )
2	1	3com23	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐶 ↔ ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐵 ) ) )
3	2	3expa	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ 𝐶 ∈ ℝ ) → ( 𝐴 < 𝐶 ↔ ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐵 ) ) )
4	3	adantrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 < 𝐶 ↔ ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐵 ) ) )
5		leadd2	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 ≤ 𝐷 ↔ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )
6	5	3com23	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐵 ≤ 𝐷 ↔ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )
7	6	3expb	⊢ ( ( 𝐵 ∈ ℝ ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 ≤ 𝐷 ↔ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )
8	7	adantll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 ≤ 𝐷 ↔ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) )
9	4 8	anbi12d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷 ) ↔ ( ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐵 ) ∧ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) ) )
10		readdcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
11	10	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 + 𝐵 ) ∈ ℝ )
12		readdcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
13	12	ancoms	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
14	13	ad2ant2lr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐶 + 𝐵 ) ∈ ℝ )
15		readdcl	⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 + 𝐷 ) ∈ ℝ )
16	15	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐶 + 𝐷 ) ∈ ℝ )
17		ltletr	⊢ ( ( ( 𝐴 + 𝐵 ) ∈ ℝ ∧ ( 𝐶 + 𝐵 ) ∈ ℝ ∧ ( 𝐶 + 𝐷 ) ∈ ℝ ) → ( ( ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐵 ) ∧ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) )
18	11 14 16 17	syl3anc	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐵 ) ∧ ( 𝐶 + 𝐵 ) ≤ ( 𝐶 + 𝐷 ) ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) )
19	9 18	sylbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 < 𝐶 ∧ 𝐵 ≤ 𝐷 ) → ( 𝐴 + 𝐵 ) < ( 𝐶 + 𝐷 ) ) )