Metamath Proof Explorer

Theorem fzofzp1b

Description: If a point is in a half-open range, the next point is in the closed range. (Contributed by Mario Carneiro, 27-Sep-2015)

Ref Expression
Assertion fzofzp1b ⊢ C ∈ ℤ ≥ A → C ∈ A ..^ B ↔ C + 1 ∈ A … B

Proof

Step Hyp Ref Expression
1 fzofzp1 ⊢ C ∈ A ..^ B → C + 1 ∈ A … B
2 simpl ⊢ C ∈ ℤ ≥ A ∧ C + 1 ∈ A … B → C ∈ ℤ ≥ A
3 eluzelz ⊢ C ∈ ℤ ≥ A → C ∈ ℤ
4 elfzuz3 ⊢ C + 1 ∈ A … B → B ∈ ℤ ≥ C + 1
5 eluzp1m1 ⊢ C ∈ ℤ ∧ B ∈ ℤ ≥ C + 1 → B − 1 ∈ ℤ ≥ C
6 3 4 5 syl2an ⊢ C ∈ ℤ ≥ A ∧ C + 1 ∈ A … B → B − 1 ∈ ℤ ≥ C
7 elfzuzb ⊢ C ∈ A … B − 1 ↔ C ∈ ℤ ≥ A ∧ B − 1 ∈ ℤ ≥ C
8 2 6 7 sylanbrc ⊢ C ∈ ℤ ≥ A ∧ C + 1 ∈ A … B → C ∈ A … B − 1
9 elfzel2 ⊢ C + 1 ∈ A … B → B ∈ ℤ
10 9 adantl ⊢ C ∈ ℤ ≥ A ∧ C + 1 ∈ A … B → B ∈ ℤ
11 fzoval ⊢ B ∈ ℤ → A ..^ B = A … B − 1
12 10 11 syl ⊢ C ∈ ℤ ≥ A ∧ C + 1 ∈ A … B → A ..^ B = A … B − 1
13 8 12 eleqtrrd ⊢ C ∈ ℤ ≥ A ∧ C + 1 ∈ A … B → C ∈ A ..^ B
14 13 ex ⊢ C ∈ ℤ ≥ A → C + 1 ∈ A … B → C ∈ A ..^ B
15 1 14 impbid2 ⊢ C ∈ ℤ ≥ A → C ∈ A ..^ B ↔ C + 1 ∈ A … B