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