Metamath Proof Explorer


Theorem nnnle0

Description: A positive integer is not less than or equal to zero. (Contributed by AV, 13-May-2020)

Ref Expression
Assertion nnnle0 A ¬ A 0

Proof

Step Hyp Ref Expression
1 nngt0 A 0 < A
2 0re 0
3 nnre A A
4 ltnle 0 A 0 < A ¬ A 0
5 4 bicomd 0 A ¬ A 0 0 < A
6 2 3 5 sylancr A ¬ A 0 0 < A
7 1 6 mpbird A ¬ A 0