Step |
Hyp |
Ref |
Expression |
1 |
|
elxnn0 |
⊢ ( 𝑁 ∈ ℕ0* ↔ ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ) |
2 |
|
elnnne0 |
⊢ ( 𝑁 ∈ ℕ ↔ ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) ) |
3 |
|
nngt0 |
⊢ ( 𝑁 ∈ ℕ → 0 < 𝑁 ) |
4 |
2 3
|
sylbir |
⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑁 ≠ 0 ) → 0 < 𝑁 ) |
5 |
4
|
ancoms |
⊢ ( ( 𝑁 ≠ 0 ∧ 𝑁 ∈ ℕ0 ) → 0 < 𝑁 ) |
6 |
5
|
adantll |
⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ∧ 𝑁 ≠ 0 ) ∧ 𝑁 ∈ ℕ0 ) → 0 < 𝑁 ) |
7 |
|
0ltpnf |
⊢ 0 < +∞ |
8 |
|
breq2 |
⊢ ( 𝑁 = +∞ → ( 0 < 𝑁 ↔ 0 < +∞ ) ) |
9 |
7 8
|
mpbiri |
⊢ ( 𝑁 = +∞ → 0 < 𝑁 ) |
10 |
9
|
adantl |
⊢ ( ( ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ∧ 𝑁 ≠ 0 ) ∧ 𝑁 = +∞ ) → 0 < 𝑁 ) |
11 |
|
simpl |
⊢ ( ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ∧ 𝑁 ≠ 0 ) → ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ) |
12 |
6 10 11
|
mpjaodan |
⊢ ( ( ( 𝑁 ∈ ℕ0 ∨ 𝑁 = +∞ ) ∧ 𝑁 ≠ 0 ) → 0 < 𝑁 ) |
13 |
1 12
|
sylanb |
⊢ ( ( 𝑁 ∈ ℕ0* ∧ 𝑁 ≠ 0 ) → 0 < 𝑁 ) |