Theorem ltsubsubb

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

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

Proof

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