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

Metamath Proof Explorer

Theorem xrlttri5d

Description: Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses xrlttri5d.a ⊢ φ → A ∈ ℝ *
xrlttri5d.b ⊢ φ → B ∈ ℝ *
xrlttri5d.aneb ⊢ φ → A ≠ B
xrlttri5d.nlt ⊢ φ → ¬ B < A
Assertion xrlttri5d ⊢ φ → A < B

Proof

Step Hyp Ref Expression
1 xrlttri5d.a ⊢ φ → A ∈ ℝ *
2 xrlttri5d.b ⊢ φ → B ∈ ℝ *
3 xrlttri5d.aneb ⊢ φ → A ≠ B
4 xrlttri5d.nlt ⊢ φ → ¬ B < A
5 3 neneqd ⊢ φ → ¬ A = B
6 xrlttri3 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → A = B ↔ ¬ A < B ∧ ¬ B < A
7 1 2 6 syl2anc ⊢ φ → A = B ↔ ¬ A < B ∧ ¬ B < A
8 5 7 mtbid ⊢ φ → ¬ ¬ A < B ∧ ¬ B < A
9 oran ⊢ A < B ∨ B < A ↔ ¬ ¬ A < B ∧ ¬ B < A
10 8 9 sylibr ⊢ φ → A < B ∨ B < A
11 10 4 jca ⊢ φ → A < B ∨ B < A ∧ ¬ B < A
12 pm5.61 ⊢ A < B ∨ B < A ∧ ¬ B < A ↔ A < B ∧ ¬ B < A
13 11 12 sylib ⊢ φ → A < B ∧ ¬ B < A
14 13 simpld ⊢ φ → A < B