Metamath Proof Explorer


Theorem xnn0gt0

Description: Nonzero extended nonnegative integers are strictly greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023)

Ref Expression
Assertion xnn0gt0 N 0 * N 0 0 < N

Proof

Step Hyp Ref Expression
1 elxnn0 N 0 * N 0 N = +∞
2 elnnne0 N N 0 N 0
3 nngt0 N 0 < N
4 2 3 sylbir N 0 N 0 0 < N
5 4 ancoms N 0 N 0 0 < N
6 5 adantll N 0 N = +∞ N 0 N 0 0 < N
7 0ltpnf 0 < +∞
8 breq2 N = +∞ 0 < N 0 < +∞
9 7 8 mpbiri N = +∞ 0 < N
10 9 adantl N 0 N = +∞ N 0 N = +∞ 0 < N
11 simpl N 0 N = +∞ N 0 N 0 N = +∞
12 6 10 11 mpjaodan N 0 N = +∞ N 0 0 < N
13 1 12 sylanb N 0 * N 0 0 < N