Metamath Proof Explorer

Theorem peano2fzr

Description: A Peano-postulate-like theorem for downward closure of a finite set of sequential integers. (Contributed by Mario Carneiro, 27-May-2014)

		Ref	Expression
	Assertion	peano2fzr	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M \dots N)) \to K \in (M \dots N)$

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M \dots N)) \to K \in ℤ_{\geq M}$
2		eluzelz	$⊢ K \in ℤ_{\geq M} \to K \in ℤ$
3		elfzuz3	$⊢ K + 1 \in (M \dots N) \to N \in ℤ_{\geq (K + 1)}$
4		peano2uzr	$⊢ (K \in ℤ \land N \in ℤ_{\geq (K + 1)}) \to N \in ℤ_{\geq K}$
5	2 3 4	syl2an	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M \dots N)) \to N \in ℤ_{\geq K}$
6		elfzuzb	$⊢ K \in (M \dots N) \leftrightarrow (K \in ℤ_{\geq M} \land N \in ℤ_{\geq K})$
7	1 5 6	sylanbrc	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M \dots N)) \to K \in (M \dots N)$