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	$⊢ K \in (M \dots N) \to K + 1 \in (M \dots N + 1)$

Step	Hyp	Ref	Expression
1		elfzuz	$⊢ K \in (M \dots N) \to K \in ℤ_{\geq M}$
2		peano2uz	$⊢ K \in ℤ_{\geq M} \to K + 1 \in ℤ_{\geq M}$
3	1 2	syl	$⊢ K \in (M \dots N) \to K + 1 \in ℤ_{\geq M}$
4		elfzuz3	$⊢ K \in (M \dots N) \to N \in ℤ_{\geq K}$
5		eluzp1p1	$⊢ N \in ℤ_{\geq K} \to N + 1 \in ℤ_{\geq (K + 1)}$
6	4 5	syl	$⊢ K \in (M \dots N) \to N + 1 \in ℤ_{\geq (K + 1)}$
7		elfzuzb	$⊢ K + 1 \in (M \dots N + 1) \leftrightarrow (K + 1 \in ℤ_{\geq M} \land N + 1 \in ℤ_{\geq (K + 1)})$
8	3 6 7	sylanbrc	$⊢ K \in (M \dots N) \to K + 1 \in (M \dots N + 1)$

Metamath Proof Explorer