Metamath Proof Explorer

Theorem ltsubsubb

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

		Ref	Expression
	Assertion	ltsubsubb	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A - C < B - D \leftrightarrow A - B < C - D)$

Proof

Step	Hyp	Ref	Expression
1		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C \in ℝ$
2	1	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C \in ℂ$
3		simprr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to D \in ℝ$
4	3	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to D \in ℂ$
5		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B \in ℝ$
6	5	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B \in ℂ$
7		subadd23	$⊢ (C \in ℂ \land D \in ℂ \land B \in ℂ) \to C - D + B = C + B - D$
8	7	eqcomd	$⊢ (C \in ℂ \land D \in ℂ \land B \in ℂ) \to C + B - D = C - D + B$
9	2 4 6 8	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C + B - D = C - D + B$
10	9	breq2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A < C + B - D \leftrightarrow A < C - D + B)$
11		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A \in ℝ$
12		resubcl	$⊢ (B \in ℝ \land D \in ℝ) \to B - D \in ℝ$
13	12	ad2ant2l	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B - D \in ℝ$
14	11 1 13	ltsubadd2d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A - C < B - D \leftrightarrow A < C + B - D)$
15		resubcl	$⊢ (C \in ℝ \land D \in ℝ) \to C - D \in ℝ$
16	15	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C - D \in ℝ$
17	11 5 16	ltsubaddd	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A - B < C - D \leftrightarrow A < C - D + B)$
18	10 14 17	3bitr4d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A - C < B - D \leftrightarrow A - B < C - D)$