Theorem 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	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ )

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 < 𝑁 )
2		elfzoelz	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝐾 ∈ ℤ )
3		elfzoel2	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → 𝑁 ∈ ℤ )
4		znnsub	⊢ ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 < 𝑁 ↔ ( 𝑁 − 𝐾 ) ∈ ℕ ) )
5	2 3 4	syl2anc	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝐾 < 𝑁 ↔ ( 𝑁 − 𝐾 ) ∈ ℕ ) )
6	1 5	mpbid	⊢ ( 𝐾 ∈ ( 𝑀 ..^ 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ )