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 e. NN0* /\ N =/= 0 ) -> 0 < N )

Proof

Step Hyp Ref Expression
1 elxnn0
 |-  ( N e. NN0* <-> ( N e. NN0 \/ N = +oo ) )
2 elnnne0
 |-  ( N e. NN <-> ( N e. NN0 /\ N =/= 0 ) )
3 nngt0
 |-  ( N e. NN -> 0 < N )
4 2 3 sylbir
 |-  ( ( N e. NN0 /\ N =/= 0 ) -> 0 < N )
5 4 ancoms
 |-  ( ( N =/= 0 /\ N e. NN0 ) -> 0 < N )
6 5 adantll
 |-  ( ( ( ( N e. NN0 \/ N = +oo ) /\ N =/= 0 ) /\ N e. NN0 ) -> 0 < N )
7 0ltpnf
 |-  0 < +oo
8 breq2
 |-  ( N = +oo -> ( 0 < N <-> 0 < +oo ) )
9 7 8 mpbiri
 |-  ( N = +oo -> 0 < N )
10 9 adantl
 |-  ( ( ( ( N e. NN0 \/ N = +oo ) /\ N =/= 0 ) /\ N = +oo ) -> 0 < N )
11 simpl
 |-  ( ( ( N e. NN0 \/ N = +oo ) /\ N =/= 0 ) -> ( N e. NN0 \/ N = +oo ) )
12 6 10 11 mpjaodan
 |-  ( ( ( N e. NN0 \/ N = +oo ) /\ N =/= 0 ) -> 0 < N )
13 1 12 sylanb
 |-  ( ( N e. NN0* /\ N =/= 0 ) -> 0 < N )