This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ ( 𝐶 − 𝐷 ) ) < ( 𝐵 − 𝐴 ) )