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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
xrlttri5d.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
xrlttri5d.aneb ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
xrlttri5d.nlt ⊢ ( 𝜑 → ¬ 𝐵 < 𝐴 )
Assertion xrlttri5d ( 𝜑 → 𝐴 < 𝐵 )

Proof

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