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

Metamath Proof Explorer

Theorem xrltlen

Description: 'Less than' expressed in terms of 'less than or equal to'. (Contributed by Mario Carneiro, 6-Nov-2015)

Ref Expression
Assertion xrltlen ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ A ≤ B ∧ B ≠ A

Proof

Step Hyp Ref Expression
1 xrlttri ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ ¬ A = B ∨ B < A
2 ioran ⊢ ¬ A = B ∨ B < A ↔ ¬ A = B ∧ ¬ B < A
3 2 biancomi ⊢ ¬ A = B ∨ B < A ↔ ¬ B < A ∧ ¬ A = B
4 1 3 bitrdi ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ ¬ B < A ∧ ¬ A = B
5 xrlenlt ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ↔ ¬ B < A
6 nesym ⊢ B ≠ A ↔ ¬ A = B
7 6 a1i ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → B ≠ A ↔ ¬ A = B
8 5 7 anbi12d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A ≤ B ∧ B ≠ A ↔ ¬ B < A ∧ ¬ A = B
9 4 8 bitr4d ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A < B ↔ A ≤ B ∧ B ≠ A