Theorem fzonnsub2

Description: If M < N then N - M is a positive integer. (Contributed by Mario Carneiro, 1-Jan-2017)

	Ref	Expression
Assertion	fzonnsub2	$$⊢K\in \left(M..^N\right)\to N-M\in \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		elfzolt3b	$$⊢K\in \left(M..^N\right)\to M\in \left(M..^N\right)$$
2		fzonnsub	$$⊢M\in \left(M..^N\right)\to N-M\in \mathbb{N}$$
3	1 2	syl	$$⊢K\in \left(M..^N\right)\to N-M\in \mathbb{N}$$