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

Metamath Proof Explorer

Theorem xrleneltd

Description: 'Less than or equal to' and 'not equals' implies 'less than', for extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses xrleneltd.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
xrleneltd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
xrleneltd.alb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
xrleneltd.anb ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
Assertion xrleneltd ( 𝜑 → 𝐴 < 𝐵 )

Proof

Step Hyp Ref Expression
1 xrleneltd.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 xrleneltd.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 xrleneltd.alb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
4 xrleneltd.anb ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
5 4 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
6 xrleltne ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → ( 𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴 ) )
7 1 2 3 6 syl3anc ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴 ) )
8 5 7 mpbird ⊢ ( 𝜑 → 𝐴 < 𝐵 )