Theorem 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	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,) 𝐵 ) ) ) → ( abs ‘ ( 𝐶 − 𝐷 ) ) < ( 𝐵 − 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ* )
2		elico2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ) )
3		elico2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( 𝐷 ∈ ( 𝐴 [,) 𝐵 ) ↔ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) )
4	2 3	anbi12d	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,) 𝐵 ) ) ↔ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) )
5	4	biimpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) )
6	1 5	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,) 𝐵 ) ) → ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) )
7		simplr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐵 ∈ ℝ )
8	7	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐵 ∈ ℂ )
9		simpll	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐴 ∈ ℝ )
10	9	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐴 ∈ ℂ )
11	8 10	negsubdi2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → - ( 𝐵 − 𝐴 ) = ( 𝐴 − 𝐵 ) )
12	9 7	resubcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐴 − 𝐵 ) ∈ ℝ )
13		simprl1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐶 ∈ ℝ )
14	13 7	resubcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐶 − 𝐵 ) ∈ ℝ )
15		simprr1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐷 ∈ ℝ )
16	13 15	resubcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐶 − 𝐷 ) ∈ ℝ )
17		simprl2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐴 ≤ 𝐶 )
18	9 13 7 17	lesub1dd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐴 − 𝐵 ) ≤ ( 𝐶 − 𝐵 ) )
19		simprr3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐷 < 𝐵 )
20	15 7 13 19	ltsub2dd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐶 − 𝐵 ) < ( 𝐶 − 𝐷 ) )
21	12 14 16 18 20	lelttrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐴 − 𝐵 ) < ( 𝐶 − 𝐷 ) )
22	11 21	eqbrtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → - ( 𝐵 − 𝐴 ) < ( 𝐶 − 𝐷 ) )
23	7 15	resubcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐵 − 𝐷 ) ∈ ℝ )
24	7 9	resubcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
25		simprl3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐶 < 𝐵 )
26	13 7 15 25	ltsub1dd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐶 − 𝐷 ) < ( 𝐵 − 𝐷 ) )
27		simprr2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → 𝐴 ≤ 𝐷 )
28	9 15 7 27	lesub2dd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐵 − 𝐷 ) ≤ ( 𝐵 − 𝐴 ) )
29	16 23 24 26 28	ltletrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( 𝐶 − 𝐷 ) < ( 𝐵 − 𝐴 ) )
30	16 24	absltd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( ( abs ‘ ( 𝐶 − 𝐷 ) ) < ( 𝐵 − 𝐴 ) ↔ ( - ( 𝐵 − 𝐴 ) < ( 𝐶 − 𝐷 ) ∧ ( 𝐶 − 𝐷 ) < ( 𝐵 − 𝐴 ) ) ) )
31	22 29 30	mpbir2and	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) ) → ( abs ‘ ( 𝐶 − 𝐷 ) ) < ( 𝐵 − 𝐴 ) )
32	31	ex	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( ( 𝐶 ∈ ℝ ∧ 𝐴 ≤ 𝐶 ∧ 𝐶 < 𝐵 ) ∧ ( 𝐷 ∈ ℝ ∧ 𝐴 ≤ 𝐷 ∧ 𝐷 < 𝐵 ) ) → ( abs ‘ ( 𝐶 − 𝐷 ) ) < ( 𝐵 − 𝐴 ) ) )
33	6 32	syld	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,) 𝐵 ) ) → ( abs ‘ ( 𝐶 − 𝐷 ) ) < ( 𝐵 − 𝐴 ) ) )
34	33	imp	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ( 𝐴 [,) 𝐵 ) ∧ 𝐷 ∈ ( 𝐴 [,) 𝐵 ) ) ) → ( abs ‘ ( 𝐶 − 𝐷 ) ) < ( 𝐵 − 𝐴 ) )