Theorem fzp1elp1

Description: Add one to an element of a finite set of integers. (Contributed by Jeff Madsen, 6-Jun-2010) (Revised by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	fzp1elp1	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) )
2		peano2uz	⊢ ( 𝐾 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
3	1 2	syl	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) )
4		elfzuz3	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) )
5		eluzp1p1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝐾 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
6	4 5	syl	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) )
7		elfzuzb	⊢ ( ( 𝐾 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) ↔ ( ( 𝐾 + 1 ) ∈ ( ℤ≥ ‘ 𝑀 ) ∧ ( 𝑁 + 1 ) ∈ ( ℤ≥ ‘ ( 𝐾 + 1 ) ) ) )
8	3 6 7	sylanbrc	⊢ ( 𝐾 ∈ ( 𝑀 ... 𝑁 ) → ( 𝐾 + 1 ) ∈ ( 𝑀 ... ( 𝑁 + 1 ) ) )