Proof of Theorem fzofzp1
| Step | Hyp | Ref
| Expression |
| 1 | | elfzoel1 13697 |
. . . 4
⊢ (𝐶 ∈ (𝐴..^𝐵) → 𝐴 ∈ ℤ) |
| 2 | | uzid 12893 |
. . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) |
| 3 | | peano2uz 12943 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘𝐴) → (𝐴 + 1) ∈
(ℤ≥‘𝐴)) |
| 4 | | fzoss1 13726 |
. . . 4
⊢ ((𝐴 + 1) ∈
(ℤ≥‘𝐴) → ((𝐴 + 1)..^(𝐵 + 1)) ⊆ (𝐴..^(𝐵 + 1))) |
| 5 | 1, 2, 3, 4 | 4syl 19 |
. . 3
⊢ (𝐶 ∈ (𝐴..^𝐵) → ((𝐴 + 1)..^(𝐵 + 1)) ⊆ (𝐴..^(𝐵 + 1))) |
| 6 | | 1z 12647 |
. . . 4
⊢ 1 ∈
ℤ |
| 7 | | fzoaddel 13756 |
. . . 4
⊢ ((𝐶 ∈ (𝐴..^𝐵) ∧ 1 ∈ ℤ) → (𝐶 + 1) ∈ ((𝐴 + 1)..^(𝐵 + 1))) |
| 8 | 6, 7 | mpan2 691 |
. . 3
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ ((𝐴 + 1)..^(𝐵 + 1))) |
| 9 | 5, 8 | sseldd 3984 |
. 2
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ (𝐴..^(𝐵 + 1))) |
| 10 | | elfzoel2 13698 |
. . 3
⊢ (𝐶 ∈ (𝐴..^𝐵) → 𝐵 ∈ ℤ) |
| 11 | | fzval3 13773 |
. . 3
⊢ (𝐵 ∈ ℤ → (𝐴...𝐵) = (𝐴..^(𝐵 + 1))) |
| 12 | 10, 11 | syl 17 |
. 2
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐴...𝐵) = (𝐴..^(𝐵 + 1))) |
| 13 | 9, 12 | eleqtrrd 2844 |
1
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ (𝐴...𝐵)) |