This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )