Proof of Theorem 0nn0m1nnn0
| Step | Hyp | Ref
| Expression |
| 1 | | 0nn0 12541 |
. . . 4
⊢ 0 ∈
ℕ0 |
| 2 | | eleq1 2829 |
. . . 4
⊢ (𝑁 = 0 → (𝑁 ∈ ℕ0 ↔ 0 ∈
ℕ0)) |
| 3 | 1, 2 | mpbiri 258 |
. . 3
⊢ (𝑁 = 0 → 𝑁 ∈
ℕ0) |
| 4 | | 1nn 12277 |
. . . . . 6
⊢ 1 ∈
ℕ |
| 5 | | 0mnnnnn0 12558 |
. . . . . 6
⊢ (1 ∈
ℕ → (0 − 1) ∉ ℕ0) |
| 6 | 4, 5 | ax-mp 5 |
. . . . 5
⊢ (0
− 1) ∉ ℕ0 |
| 7 | | oveq1 7438 |
. . . . . 6
⊢ (𝑁 = 0 → (𝑁 − 1) = (0 −
1)) |
| 8 | | neleq1 3052 |
. . . . . 6
⊢ ((𝑁 − 1) = (0 − 1)
→ ((𝑁 − 1)
∉ ℕ0 ↔ (0 − 1) ∉
ℕ0)) |
| 9 | 7, 8 | syl 17 |
. . . . 5
⊢ (𝑁 = 0 → ((𝑁 − 1) ∉ ℕ0
↔ (0 − 1) ∉ ℕ0)) |
| 10 | 6, 9 | mpbiri 258 |
. . . 4
⊢ (𝑁 = 0 → (𝑁 − 1) ∉
ℕ0) |
| 11 | | df-nel 3047 |
. . . 4
⊢ ((𝑁 − 1) ∉
ℕ0 ↔ ¬ (𝑁 − 1) ∈
ℕ0) |
| 12 | 10, 11 | sylib 218 |
. . 3
⊢ (𝑁 = 0 → ¬ (𝑁 − 1) ∈
ℕ0) |
| 13 | 3, 12 | jca 511 |
. 2
⊢ (𝑁 = 0 → (𝑁 ∈ ℕ0 ∧ ¬
(𝑁 − 1) ∈
ℕ0)) |
| 14 | | nn0z 12638 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 15 | | peano2zm 12660 |
. . . . . . 7
⊢ (𝑁 ∈ ℤ → (𝑁 − 1) ∈
ℤ) |
| 16 | 14, 15 | syl 17 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ∈
ℤ) |
| 17 | | elnn0z 12626 |
. . . . . . . 8
⊢ ((𝑁 − 1) ∈
ℕ0 ↔ ((𝑁 − 1) ∈ ℤ ∧ 0 ≤
(𝑁 −
1))) |
| 18 | 17 | notbii 320 |
. . . . . . 7
⊢ (¬
(𝑁 − 1) ∈
ℕ0 ↔ ¬ ((𝑁 − 1) ∈ ℤ ∧ 0 ≤
(𝑁 −
1))) |
| 19 | 18 | biimpi 216 |
. . . . . 6
⊢ (¬
(𝑁 − 1) ∈
ℕ0 → ¬ ((𝑁 − 1) ∈ ℤ ∧ 0 ≤
(𝑁 −
1))) |
| 20 | | annotanannot 835 |
. . . . . . 7
⊢ (((𝑁 − 1) ∈ ℤ ∧
¬ ((𝑁 − 1) ∈
ℤ ∧ 0 ≤ (𝑁
− 1))) ↔ ((𝑁
− 1) ∈ ℤ ∧ ¬ 0 ≤ (𝑁 − 1))) |
| 21 | 20 | simprbi 496 |
. . . . . 6
⊢ (((𝑁 − 1) ∈ ℤ ∧
¬ ((𝑁 − 1) ∈
ℤ ∧ 0 ≤ (𝑁
− 1))) → ¬ 0 ≤ (𝑁 − 1)) |
| 22 | 16, 19, 21 | syl2an 596 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ¬ (𝑁 − 1)
∈ ℕ0) → ¬ 0 ≤ (𝑁 − 1)) |
| 23 | | zre 12617 |
. . . . . . . . 9
⊢ ((𝑁 − 1) ∈ ℤ
→ (𝑁 − 1) ∈
ℝ) |
| 24 | 14, 15, 23 | 3syl 18 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (𝑁 − 1) ∈
ℝ) |
| 25 | | 0red 11264 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 0 ∈ ℝ) |
| 26 | 24, 25 | ltnled 11408 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1) <
0 ↔ ¬ 0 ≤ (𝑁
− 1))) |
| 27 | 26 | biimprd 248 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (¬ 0 ≤ (𝑁
− 1) → (𝑁
− 1) < 0)) |
| 28 | 27 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ ¬ (𝑁 − 1)
∈ ℕ0) → (¬ 0 ≤ (𝑁 − 1) → (𝑁 − 1) < 0)) |
| 29 | 22, 28 | mpd 15 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ¬ (𝑁 − 1)
∈ ℕ0) → (𝑁 − 1) < 0) |
| 30 | | 0z 12624 |
. . . . . . 7
⊢ 0 ∈
ℤ |
| 31 | | zlem1lt 12669 |
. . . . . . 7
⊢ ((𝑁 ∈ ℤ ∧ 0 ∈
ℤ) → (𝑁 ≤ 0
↔ (𝑁 − 1) <
0)) |
| 32 | 14, 30, 31 | sylancl 586 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 ≤ 0 ↔
(𝑁 − 1) <
0)) |
| 33 | 32 | biimprd 248 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 − 1) <
0 → 𝑁 ≤
0)) |
| 34 | 33 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ ¬ (𝑁 − 1)
∈ ℕ0) → ((𝑁 − 1) < 0 → 𝑁 ≤ 0)) |
| 35 | 29, 34 | mpd 15 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ¬ (𝑁 − 1)
∈ ℕ0) → 𝑁 ≤ 0) |
| 36 | | nn0ge0 12551 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 0 ≤ 𝑁) |
| 37 | 36 | adantr 480 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ¬ (𝑁 − 1)
∈ ℕ0) → 0 ≤ 𝑁) |
| 38 | | nn0re 12535 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
| 39 | 38, 25 | letri3d 11403 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑁 = 0 ↔ (𝑁 ≤ 0 ∧ 0 ≤ 𝑁))) |
| 40 | 39 | biimprd 248 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ ((𝑁 ≤ 0 ∧ 0
≤ 𝑁) → 𝑁 = 0)) |
| 41 | 40 | adantr 480 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ ¬ (𝑁 − 1)
∈ ℕ0) → ((𝑁 ≤ 0 ∧ 0 ≤ 𝑁) → 𝑁 = 0)) |
| 42 | 35, 37, 41 | mp2and 699 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ ¬ (𝑁 − 1)
∈ ℕ0) → 𝑁 = 0) |
| 43 | 13, 42 | impbii 209 |
1
⊢ (𝑁 = 0 ↔ (𝑁 ∈ ℕ0 ∧ ¬
(𝑁 − 1) ∈
ℕ0)) |