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 ) |