fzonnsub

Description: If K < N then N - K is a positive integer. (Contributed by Mario Carneiro, 29-Sep-2015) (Revised by Mario Carneiro, 1-Jan-2017)

		Ref	Expression
	Assertion	fzonnsub	$⊢ K \in (M ..^N) \to N - K \in ℕ$

Step	Hyp	Ref	Expression
1		elfzolt2	$⊢ K \in (M ..^N) \to K < N$
2		elfzoelz	$⊢ K \in (M ..^N) \to K \in ℤ$
3		elfzoel2	$⊢ K \in (M ..^N) \to N \in ℤ$
4		znnsub	$⊢ (K \in ℤ \land N \in ℤ) \to (K < N \leftrightarrow N - K \in ℕ)$
5	2 3 4	syl2anc	$⊢ K \in (M ..^N) \to (K < N \leftrightarrow N - K \in ℕ)$
6	1 5	mpbid	$⊢ K \in (M ..^N) \to N - K \in ℕ$

Metamath Proof Explorer