# Metamath Proof Explorer

## Theorem fzofzp1

Description: If a point is in a half-open range, the next point is in the closed range. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion fzofzp1 ${⊢}{C}\in \left({A}..^{B}\right)\to {C}+1\in \left({A}\dots {B}\right)$

### Proof

Step Hyp Ref Expression
1 elfzoel1 ${⊢}{C}\in \left({A}..^{B}\right)\to {A}\in ℤ$
2 uzid ${⊢}{A}\in ℤ\to {A}\in {ℤ}_{\ge {A}}$
3 peano2uz ${⊢}{A}\in {ℤ}_{\ge {A}}\to {A}+1\in {ℤ}_{\ge {A}}$
4 fzoss1 ${⊢}{A}+1\in {ℤ}_{\ge {A}}\to \left({A}+1..^{B}+1\right)\subseteq \left({A}..^{B}+1\right)$
5 1 2 3 4 4syl ${⊢}{C}\in \left({A}..^{B}\right)\to \left({A}+1..^{B}+1\right)\subseteq \left({A}..^{B}+1\right)$
6 1z ${⊢}1\in ℤ$
7 fzoaddel ${⊢}\left({C}\in \left({A}..^{B}\right)\wedge 1\in ℤ\right)\to {C}+1\in \left({A}+1..^{B}+1\right)$
8 6 7 mpan2 ${⊢}{C}\in \left({A}..^{B}\right)\to {C}+1\in \left({A}+1..^{B}+1\right)$
9 5 8 sseldd ${⊢}{C}\in \left({A}..^{B}\right)\to {C}+1\in \left({A}..^{B}+1\right)$
10 elfzoel2 ${⊢}{C}\in \left({A}..^{B}\right)\to {B}\in ℤ$
11 fzval3 ${⊢}{B}\in ℤ\to \left({A}\dots {B}\right)=\left({A}..^{B}+1\right)$
12 10 11 syl ${⊢}{C}\in \left({A}..^{B}\right)\to \left({A}\dots {B}\right)=\left({A}..^{B}+1\right)$
13 9 12 eleqtrrd ${⊢}{C}\in \left({A}..^{B}\right)\to {C}+1\in \left({A}\dots {B}\right)$