Proof of Theorem fzofzp1
Step | Hyp | Ref
| Expression |
1 | | elfzoel1 13394 |
. . . 4
⊢ (𝐶 ∈ (𝐴..^𝐵) → 𝐴 ∈ ℤ) |
2 | | uzid 12606 |
. . . 4
⊢ (𝐴 ∈ ℤ → 𝐴 ∈
(ℤ≥‘𝐴)) |
3 | | peano2uz 12650 |
. . . 4
⊢ (𝐴 ∈
(ℤ≥‘𝐴) → (𝐴 + 1) ∈
(ℤ≥‘𝐴)) |
4 | | fzoss1 13423 |
. . . 4
⊢ ((𝐴 + 1) ∈
(ℤ≥‘𝐴) → ((𝐴 + 1)..^(𝐵 + 1)) ⊆ (𝐴..^(𝐵 + 1))) |
5 | 1, 2, 3, 4 | 4syl 19 |
. . 3
⊢ (𝐶 ∈ (𝐴..^𝐵) → ((𝐴 + 1)..^(𝐵 + 1)) ⊆ (𝐴..^(𝐵 + 1))) |
6 | | 1z 12359 |
. . . 4
⊢ 1 ∈
ℤ |
7 | | fzoaddel 13449 |
. . . 4
⊢ ((𝐶 ∈ (𝐴..^𝐵) ∧ 1 ∈ ℤ) → (𝐶 + 1) ∈ ((𝐴 + 1)..^(𝐵 + 1))) |
8 | 6, 7 | mpan2 688 |
. . 3
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ ((𝐴 + 1)..^(𝐵 + 1))) |
9 | 5, 8 | sseldd 3923 |
. 2
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ (𝐴..^(𝐵 + 1))) |
10 | | elfzoel2 13395 |
. . 3
⊢ (𝐶 ∈ (𝐴..^𝐵) → 𝐵 ∈ ℤ) |
11 | | fzval3 13465 |
. . 3
⊢ (𝐵 ∈ ℤ → (𝐴...𝐵) = (𝐴..^(𝐵 + 1))) |
12 | 10, 11 | syl 17 |
. 2
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐴...𝐵) = (𝐴..^(𝐵 + 1))) |
13 | 9, 12 | eleqtrrd 2843 |
1
⊢ (𝐶 ∈ (𝐴..^𝐵) → (𝐶 + 1) ∈ (𝐴...𝐵)) |