# Metamath Proof Explorer

## Theorem leltne

Description: 'Less than or equal to' implies 'less than' is not 'equals'. (Contributed by NM, 27-Jul-1999)

Ref Expression
Assertion leltne ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to \left({A}<{B}↔{B}\ne {A}\right)$

### Proof

Step Hyp Ref Expression
1 lttri3 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}={B}↔\left(¬{A}<{B}\wedge ¬{B}<{A}\right)\right)$
2 simpl ${⊢}\left(¬{A}<{B}\wedge ¬{B}<{A}\right)\to ¬{A}<{B}$
3 1 2 syl6bi ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}={B}\to ¬{A}<{B}\right)$
4 3 adantr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\le {B}\right)\to \left({A}={B}\to ¬{A}<{B}\right)$
5 leloe ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({A}\le {B}↔\left({A}<{B}\vee {A}={B}\right)\right)$
6 5 biimpa ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\le {B}\right)\to \left({A}<{B}\vee {A}={B}\right)$
7 6 ord ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\le {B}\right)\to \left(¬{A}<{B}\to {A}={B}\right)$
8 4 7 impbid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\le {B}\right)\to \left({A}={B}↔¬{A}<{B}\right)$
9 8 necon2abid ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\le {B}\right)\to \left({A}<{B}↔{A}\ne {B}\right)$
10 necom ${⊢}{B}\ne {A}↔{A}\ne {B}$
11 9 10 syl6bbr ${⊢}\left(\left({A}\in ℝ\wedge {B}\in ℝ\right)\wedge {A}\le {B}\right)\to \left({A}<{B}↔{B}\ne {A}\right)$
12 11 3impa ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to \left({A}<{B}↔{B}\ne {A}\right)$