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

Proof

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