Description: 'Not less than or equal to' implies 'grater than'. (Contributed by Glauco Siliprandi, 2-Jan-2022)
Ref | Expression | ||
---|---|---|---|
Hypotheses | nleltd.1 | |- ( ph -> A e. RR ) |
|
nleltd.2 | |- ( ph -> B e. RR ) |
||
nleltd.3 | |- ( ph -> -. B <_ A ) |
||
Assertion | nleltd | |- ( ph -> A < B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nleltd.1 | |- ( ph -> A e. RR ) |
|
2 | nleltd.2 | |- ( ph -> B e. RR ) |
|
3 | nleltd.3 | |- ( ph -> -. B <_ A ) |
|
4 | 1 2 | ltnled | |- ( ph -> ( A < B <-> -. B <_ A ) ) |
5 | 3 4 | mpbird | |- ( ph -> A < B ) |