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 ∈ A ..^ B → C + 1 ∈ A … B

Proof

Step Hyp Ref Expression
1 elfzoel1 ⊢ C ∈ A ..^ B → A ∈ ℤ
2 uzid ⊢ A ∈ ℤ → A ∈ ℤ ≥ A
3 peano2uz ⊢ A ∈ ℤ ≥ A → A + 1 ∈ ℤ ≥ A
4 fzoss1 ⊢ A + 1 ∈ ℤ ≥ A → A + 1 ..^ B + 1 ⊆ A ..^ B + 1
5 1 2 3 4 4syl ⊢ C ∈ A ..^ B → A + 1 ..^ B + 1 ⊆ A ..^ B + 1
6 1z ⊢ 1 ∈ ℤ
7 fzoaddel ⊢ C ∈ A ..^ B ∧ 1 ∈ ℤ → C + 1 ∈ A + 1 ..^ B + 1
8 6 7 mpan2 ⊢ C ∈ A ..^ B → C + 1 ∈ A + 1 ..^ B + 1
9 5 8 sseldd ⊢ C ∈ A ..^ B → C + 1 ∈ A ..^ B + 1
10 elfzoel2 ⊢ C ∈ A ..^ B → B ∈ ℤ
11 fzval3 ⊢ B ∈ ℤ → A … B = A ..^ B + 1
12 10 11 syl ⊢ C ∈ A ..^ B → A … B = A ..^ B + 1
13 9 12 eleqtrrd ⊢ C ∈ A ..^ B → C + 1 ∈ A … B