Metamath Proof Explorer

Theorem lt2sub

Description: Subtracting both sides of two 'less than' relations. (Contributed by Mario Carneiro, 14-Apr-2016)

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

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A \in ℝ$
2		simprl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C \in ℝ$
3		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to B \in ℝ$
4		ltsub1	$⊢ (A \in ℝ \land C \in ℝ \land B \in ℝ) \to (A < C \leftrightarrow A - B < C - B)$
5	1 2 3 4	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (A < C \leftrightarrow A - B < C - B)$
6		simprr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to D \in ℝ$
7		ltsub2	$⊢ (D \in ℝ \land B \in ℝ \land C \in ℝ) \to (D < B \leftrightarrow C - B < C - D)$
8	6 3 2 7	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to (D < B \leftrightarrow C - B < C - D)$
9	5 8	anbi12d	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ((A < C \land D < B) \leftrightarrow (A - B < C - B \land C - B < C - D))$
10		resubcl	$⊢ (A \in ℝ \land B \in ℝ) \to A - B \in ℝ$
11	10	adantr	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to A - B \in ℝ$
12	2 3	resubcld	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C - B \in ℝ$
13		resubcl	$⊢ (C \in ℝ \land D \in ℝ) \to C - D \in ℝ$
14	13	adantl	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to C - D \in ℝ$
15		lttr	$⊢ (A - B \in ℝ \land C - B \in ℝ \land C - D \in ℝ) \to ((A - B < C - B \land C - B < C - D) \to A - B < C - D)$
16	11 12 14 15	syl3anc	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ((A - B < C - B \land C - B < C - D) \to A - B < C - D)$
17	9 16	sylbid	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in ℝ \land D \in ℝ)) \to ((A < C \land D < B) \to A - B < C - D)$