Proof of Theorem nn0ge0
Step | Hyp | Ref
| Expression |
1 | | elnn0 11171 |
. . 3
⊢ (𝑁 ∈ ℕ0
↔ (𝑁 ∈ ℕ
∨ 𝑁 =
0)) |
2 | | nngt0 10926 |
. . . 4
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
3 | | id 22 |
. . . . 5
⊢ (𝑁 = 0 → 𝑁 = 0) |
4 | 3 | eqcomd 2616 |
. . . 4
⊢ (𝑁 = 0 → 0 = 𝑁) |
5 | 2, 4 | orim12i 537 |
. . 3
⊢ ((𝑁 ∈ ℕ ∨ 𝑁 = 0) → (0 < 𝑁 ∨ 0 = 𝑁)) |
6 | 1, 5 | sylbi 206 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (0 < 𝑁 ∨ 0 =
𝑁)) |
7 | | 0re 9919 |
. . 3
⊢ 0 ∈
ℝ |
8 | | nn0re 11178 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
9 | | leloe 10003 |
. . 3
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℝ) → (0 ≤ 𝑁 ↔ (0 < 𝑁 ∨ 0 = 𝑁))) |
10 | 7, 8, 9 | sylancr 694 |
. 2
⊢ (𝑁 ∈ ℕ0
→ (0 ≤ 𝑁 ↔ (0
< 𝑁 ∨ 0 = 𝑁))) |
11 | 6, 10 | mpbird 246 |
1
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |