Metamath Proof Explorer


Theorem lenlteq

Description: 'less than or equal to' but not 'less than' implies 'equal' . (Contributed by Glauco Siliprandi, 3-Mar-2021)

Ref Expression
Hypotheses lenlteq.1
|- ( ph -> A e. RR )
lenlteq.2
|- ( ph -> B e. RR )
lenlteq.3
|- ( ph -> A <_ B )
lenlteq.4
|- ( ph -> -. A < B )
Assertion lenlteq
|- ( ph -> A = B )

Proof

Step Hyp Ref Expression
1 lenlteq.1
 |-  ( ph -> A e. RR )
2 lenlteq.2
 |-  ( ph -> B e. RR )
3 lenlteq.3
 |-  ( ph -> A <_ B )
4 lenlteq.4
 |-  ( ph -> -. A < B )
5 3 4 jca
 |-  ( ph -> ( A <_ B /\ -. A < B ) )
6 eqlelt
 |-  ( ( A e. RR /\ B e. RR ) -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )
7 1 2 6 syl2anc
 |-  ( ph -> ( A = B <-> ( A <_ B /\ -. A < B ) ) )
8 5 7 mpbird
 |-  ( ph -> A = B )