Theorem fzonnsub2

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

	Ref	Expression
Assertion	fzonnsub2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		elfzolt3b	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) )
2		fzonnsub	⊢ ( 𝑀 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ )
3	1 2	syl	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁 − 𝑀 ) ∈ ℕ )