Step | Hyp | Ref
| Expression |
1 | | elfzuz 13108 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (ℤ≥‘𝑀)) |
2 | 1 | adantl 485 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (ℤ≥‘𝑀)) |
3 | | elfzuz3 13109 |
. . . . 5
⊢ (𝑘 ∈ (𝑀...𝐾) → 𝐾 ∈ (ℤ≥‘𝑘)) |
4 | | uztrn 12456 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘𝐾) ∧ 𝐾 ∈ (ℤ≥‘𝑘)) → 𝑁 ∈ (ℤ≥‘𝑘)) |
5 | 3, 4 | sylan2 596 |
. . . 4
⊢ ((𝑁 ∈
(ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑁 ∈ (ℤ≥‘𝑘)) |
6 | | elfzuzb 13106 |
. . . 4
⊢ (𝑘 ∈ (𝑀...𝑁) ↔ (𝑘 ∈ (ℤ≥‘𝑀) ∧ 𝑁 ∈ (ℤ≥‘𝑘))) |
7 | 2, 5, 6 | sylanbrc 586 |
. . 3
⊢ ((𝑁 ∈
(ℤ≥‘𝐾) ∧ 𝑘 ∈ (𝑀...𝐾)) → 𝑘 ∈ (𝑀...𝑁)) |
8 | 7 | ex 416 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝑘 ∈ (𝑀...𝐾) → 𝑘 ∈ (𝑀...𝑁))) |
9 | 8 | ssrdv 3907 |
1
⊢ (𝑁 ∈
(ℤ≥‘𝐾) → (𝑀...𝐾) ⊆ (𝑀...𝑁)) |