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 ) |
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 ) |