icodiamlt

Description: Two elements in a half-open interval have separationstrictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014)

		Ref	Expression
	Assertion	icodiamlt	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in [A, B) \land D \in [A, B))) \to \|C - D\| < B - A$

Proof

Step	Hyp	Ref	Expression
1		rexr	$⊢ B \in ℝ \to B \in ℝ^{*}$
2		elico2	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to (C \in [A, B) \leftrightarrow (C \in ℝ \land A \leq C \land C < B))$
3		elico2	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to (D \in [A, B) \leftrightarrow (D \in ℝ \land A \leq D \land D < B))$
4	2 3	anbi12d	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to ((C \in [A, B) \land D \in [A, B)) \leftrightarrow ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B)))$
5	4	biimpd	$⊢ (A \in ℝ \land B \in ℝ^{*}) \to ((C \in [A, B) \land D \in [A, B)) \to ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B)))$
6	1 5	sylan2	$⊢ (A \in ℝ \land B \in ℝ) \to ((C \in [A, B) \land D \in [A, B)) \to ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B)))$
7		simplr	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to B \in ℝ$
8	7	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to B \in ℂ$
9		simpll	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to A \in ℝ$
10	9	recnd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to A \in ℂ$
11	8 10	negsubdi2d	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to - (B - A) = A - B$
12	9 7	resubcld	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to A - B \in ℝ$
13		simprl1	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to C \in ℝ$
14	13 7	resubcld	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to C - B \in ℝ$
15		simprr1	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to D \in ℝ$
16	13 15	resubcld	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to C - D \in ℝ$
17		simprl2	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to A \leq C$
18	9 13 7 17	lesub1dd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to A - B \leq C - B$
19		simprr3	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to D < B$
20	15 7 13 19	ltsub2dd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to C - B < C - D$
21	12 14 16 18 20	lelttrd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to A - B < C - D$
22	11 21	eqbrtrd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to - (B - A) < C - D$
23	7 15	resubcld	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to B - D \in ℝ$
24	7 9	resubcld	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to B - A \in ℝ$
25		simprl3	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to C < B$
26	13 7 15 25	ltsub1dd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to C - D < B - D$
27		simprr2	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to A \leq D$
28	9 15 7 27	lesub2dd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to B - D \leq B - A$
29	16 23 24 26 28	ltletrd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to C - D < B - A$
30	16 24	absltd	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to (\|C - D\| < B - A \leftrightarrow (- (B - A) < C - D \land C - D < B - A))$
31	22 29 30	mpbir2and	$⊢ ((A \in ℝ \land B \in ℝ) \land ((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B))) \to \|C - D\| < B - A$
32	31	ex	$⊢ (A \in ℝ \land B \in ℝ) \to (((C \in ℝ \land A \leq C \land C < B) \land (D \in ℝ \land A \leq D \land D < B)) \to \|C - D\| < B - A)$
33	6 32	syld	$⊢ (A \in ℝ \land B \in ℝ) \to ((C \in [A, B) \land D \in [A, B)) \to \|C - D\| < B - A)$
34	33	imp	$⊢ ((A \in ℝ \land B \in ℝ) \land (C \in [A, B) \land D \in [A, B))) \to \|C - D\| < B - A$

Metamath Proof Explorer

Theorem icodiamlt

Proof