Proof of Theorem elfz2nn0
| Step | Hyp | Ref
| Expression |
| 1 | | elnn0uz 12923 |
. . . 4
⊢ (𝐾 ∈ ℕ0
↔ 𝐾 ∈
(ℤ≥‘0)) |
| 2 | 1 | anbi1i 624 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝐾)) ↔ (𝐾 ∈ (ℤ≥‘0)
∧ 𝑁 ∈
(ℤ≥‘𝐾))) |
| 3 | | eluznn0 12959 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝑁 ∈
ℕ0) |
| 4 | | eluzle 12891 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → 𝐾 ≤ 𝑁) |
| 5 | 4 | adantl 481 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝐾)) → 𝐾 ≤ 𝑁) |
| 6 | 3, 5 | jca 511 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝐾)) → (𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁)) |
| 7 | | nn0z 12638 |
. . . . . . . 8
⊢ (𝐾 ∈ ℕ0
→ 𝐾 ∈
ℤ) |
| 8 | | nn0z 12638 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
| 9 | | eluz 12892 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝐾) ↔ 𝐾 ≤ 𝑁)) |
| 10 | 7, 8, 9 | syl2an 596 |
. . . . . . 7
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝑁 ∈ (ℤ≥‘𝐾) ↔ 𝐾 ≤ 𝑁)) |
| 11 | 10 | biimprd 248 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0) → (𝐾 ≤ 𝑁 → 𝑁 ∈ (ℤ≥‘𝐾))) |
| 12 | 11 | impr 454 |
. . . . 5
⊢ ((𝐾 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ 𝐾
≤ 𝑁)) → 𝑁 ∈
(ℤ≥‘𝐾)) |
| 13 | 6, 12 | impbida 801 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ (𝑁 ∈
(ℤ≥‘𝐾) ↔ (𝑁 ∈ ℕ0 ∧ 𝐾 ≤ 𝑁))) |
| 14 | 13 | pm5.32i 574 |
. . 3
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
(ℤ≥‘𝐾)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁))) |
| 15 | 2, 14 | bitr3i 277 |
. 2
⊢ ((𝐾 ∈
(ℤ≥‘0) ∧ 𝑁 ∈ (ℤ≥‘𝐾)) ↔ (𝐾 ∈ ℕ0 ∧ (𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁))) |
| 16 | | elfzuzb 13558 |
. 2
⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ (ℤ≥‘0)
∧ 𝑁 ∈
(ℤ≥‘𝐾))) |
| 17 | | 3anass 1095 |
. 2
⊢ ((𝐾 ∈ ℕ0
∧ 𝑁 ∈
ℕ0 ∧ 𝐾
≤ 𝑁) ↔ (𝐾 ∈ ℕ0
∧ (𝑁 ∈
ℕ0 ∧ 𝐾
≤ 𝑁))) |
| 18 | 15, 16, 17 | 3bitr4i 303 |
1
⊢ (𝐾 ∈ (0...𝑁) ↔ (𝐾 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝐾 ≤ 𝑁)) |