Metamath Proof Explorer

Theorem fznn0sub2

Description: Subtraction closure for a member of a finite set of sequential nonnegative integers. (Contributed by NM, 26-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

		Ref	Expression
	Assertion	fznn0sub2	$⊢ K \in (0 \dots N) \to N - K \in (0 \dots N)$

Proof

Step	Hyp	Ref	Expression
1		elfzle1	$⊢ K \in (0 \dots N) \to 0 \leq K$
2		elfzel2	$⊢ K \in (0 \dots N) \to N \in ℤ$
3		elfzelz	$⊢ K \in (0 \dots N) \to K \in ℤ$
4		zre	$⊢ N \in ℤ \to N \in ℝ$
5		zre	$⊢ K \in ℤ \to K \in ℝ$
6		subge02	$⊢ (N \in ℝ \land K \in ℝ) \to (0 \leq K \leftrightarrow N - K \leq N)$
7	4 5 6	syl2an	$⊢ (N \in ℤ \land K \in ℤ) \to (0 \leq K \leftrightarrow N - K \leq N)$
8	2 3 7	syl2anc	$⊢ K \in (0 \dots N) \to (0 \leq K \leftrightarrow N - K \leq N)$
9	1 8	mpbid	$⊢ K \in (0 \dots N) \to N - K \leq N$
10		fznn0sub	$⊢ K \in (0 \dots N) \to N - K \in ℕ_{0}$
11		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
12	10 11	eleqtrdi	$⊢ K \in (0 \dots N) \to N - K \in ℤ_{\geq 0}$
13		elfz5	$⊢ (N - K \in ℤ_{\geq 0} \land N \in ℤ) \to (N - K \in (0 \dots N) \leftrightarrow N - K \leq N)$
14	12 2 13	syl2anc	$⊢ K \in (0 \dots N) \to (N - K \in (0 \dots N) \leftrightarrow N - K \leq N)$
15	9 14	mpbird	$⊢ K \in (0 \dots N) \to N - K \in (0 \dots N)$