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 ( 𝜑𝐴 < 𝐵 )