Theorem ltsubaddb

Description: Equivalence for the "less than" relation between differences and sums. (Contributed by AV, 6-Jun-2020)

	Ref	Expression
Assertion	ltsubaddb	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 − 𝐶 ) < ( 𝐵 − 𝐷 ) ↔ ( 𝐴 + 𝐷 ) < ( 𝐵 + 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℝ )
2	1	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐵 ∈ ℂ )
3		simprl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℝ )
4	3	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
5		simprr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℝ )
6	5	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐷 ∈ ℂ )
7	2 4 6	addsubd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐵 + 𝐶 ) − 𝐷 ) = ( ( 𝐵 − 𝐷 ) + 𝐶 ) )
8	7	eqcomd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐵 − 𝐷 ) + 𝐶 ) = ( ( 𝐵 + 𝐶 ) − 𝐷 ) )
9	8	breq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐴 < ( ( 𝐵 − 𝐷 ) + 𝐶 ) ↔ 𝐴 < ( ( 𝐵 + 𝐶 ) − 𝐷 ) ) )
10		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → 𝐴 ∈ ℝ )
11		resubcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐵 − 𝐷 ) ∈ ℝ )
12	11	ad2ant2l	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 − 𝐷 ) ∈ ℝ )
13	10 3 12	ltsubaddd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 − 𝐶 ) < ( 𝐵 − 𝐷 ) ↔ 𝐴 < ( ( 𝐵 − 𝐷 ) + 𝐶 ) ) )
14		readdcl	⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
15	14	ad2ant2lr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( 𝐵 + 𝐶 ) ∈ ℝ )
16	10 5 15	ltaddsubd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 + 𝐷 ) < ( 𝐵 + 𝐶 ) ↔ 𝐴 < ( ( 𝐵 + 𝐶 ) − 𝐷 ) ) )
17	9 13 16	3bitr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( 𝐴 − 𝐶 ) < ( 𝐵 − 𝐷 ) ↔ ( 𝐴 + 𝐷 ) < ( 𝐵 + 𝐶 ) ) )