peano2fzor

Description: A Peano-postulate-like theorem for downward closure of a half-open integer range. (Contributed by Mario Carneiro, 1-Oct-2015)

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

Step	Hyp	Ref	Expression
1		simpr	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M ..^N)) \to K + 1 \in (M ..^N)$
2		elfzoel2	$⊢ K + 1 \in (M ..^N) \to N \in ℤ$
3	2	adantl	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M ..^N)) \to N \in ℤ$
4		fzoval	$⊢ N \in ℤ \to (M ..^N) = (M \dots N - 1)$
5	3 4	syl	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M ..^N)) \to (M ..^N) = (M \dots N - 1)$
6	1 5	eleqtrd	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M ..^N)) \to K + 1 \in (M \dots N - 1)$
7		peano2fzr	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M \dots N - 1)) \to K \in (M \dots N - 1)$
8	6 7	syldan	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M ..^N)) \to K \in (M \dots N - 1)$
9	8 5	eleqtrrd	$⊢ (K \in ℤ_{\geq M} \land K + 1 \in (M ..^N)) \to K \in (M ..^N)$

Metamath Proof Explorer