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	⊢ ( 𝐶 ∈ ( ℤ≥ ‘ 𝐴 ) → ( 𝐶 ∈ ( 𝐴 ..^ 𝐵 ) ↔ ( 𝐶 + 1 ) ∈ ( 𝐴 ... 𝐵 ) ) )

Proof

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