This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )