ige2m1fz

		Ref	Expression
	Assertion	ige2m1fz	$⊢ (N \in ℕ_{0} \land 2 \leq N) \to N - 1 \in (0 \dots N)$

Step	Hyp	Ref	Expression
1		1eluzge0	$⊢ 1 \in ℤ_{\geq 0}$
2		fzss1	$⊢ 1 \in ℤ_{\geq 0} \to (1 \dots N) \subseteq (0 \dots N)$
3	1 2	ax-mp	$⊢ (1 \dots N) \subseteq (0 \dots N)$
4		2z	$⊢ 2 \in ℤ$
5	4	a1i	$⊢ (N \in ℕ_{0} \land 2 \leq N) \to 2 \in ℤ$
6		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
7	6	adantr	$⊢ (N \in ℕ_{0} \land 2 \leq N) \to N \in ℤ$
8		simpr	$⊢ (N \in ℕ_{0} \land 2 \leq N) \to 2 \leq N$
9		eluz2	$⊢ N \in ℤ_{\geq 2} \leftrightarrow (2 \in ℤ \land N \in ℤ \land 2 \leq N)$
10	5 7 8 9	syl3anbrc	$⊢ (N \in ℕ_{0} \land 2 \leq N) \to N \in ℤ_{\geq 2}$
11		ige2m1fz1	$⊢ N \in ℤ_{\geq 2} \to N - 1 \in (1 \dots N)$
12	10 11	syl	$⊢ (N \in ℕ_{0} \land 2 \leq N) \to N - 1 \in (1 \dots N)$
13	3 12	sselid	$⊢ (N \in ℕ_{0} \land 2 \leq N) \to N - 1 \in (0 \dots N)$

Metamath Proof Explorer