Proof of Theorem nnm1nn0
| Step | Hyp | Ref
| Expression |
| 1 | | nn1m1nn 12287 |
. . . 4
⊢ (𝑁 ∈ ℕ → (𝑁 = 1 ∨ (𝑁 − 1) ∈
ℕ)) |
| 2 | | oveq1 7438 |
. . . . . 6
⊢ (𝑁 = 1 → (𝑁 − 1) = (1 −
1)) |
| 3 | | 1m1e0 12338 |
. . . . . 6
⊢ (1
− 1) = 0 |
| 4 | 2, 3 | eqtrdi 2793 |
. . . . 5
⊢ (𝑁 = 1 → (𝑁 − 1) = 0) |
| 5 | 4 | orim1i 910 |
. . . 4
⊢ ((𝑁 = 1 ∨ (𝑁 − 1) ∈ ℕ) → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈
ℕ)) |
| 6 | 1, 5 | syl 17 |
. . 3
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) = 0 ∨ (𝑁 − 1) ∈
ℕ)) |
| 7 | 6 | orcomd 872 |
. 2
⊢ (𝑁 ∈ ℕ → ((𝑁 − 1) ∈ ℕ ∨
(𝑁 − 1) =
0)) |
| 8 | | elnn0 12528 |
. 2
⊢ ((𝑁 − 1) ∈
ℕ0 ↔ ((𝑁 − 1) ∈ ℕ ∨ (𝑁 − 1) =
0)) |
| 9 | 7, 8 | sylibr 234 |
1
⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈
ℕ0) |