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	|- ( K e. ( M ..^ N ) -> ( N - K ) e. NN )

Proof

Step	Hyp	Ref	Expression
1		elfzolt2	|- ( K e. ( M ..^ N ) -> K < N )
2		elfzoelz	|- ( K e. ( M ..^ N ) -> K e. ZZ )
3		elfzoel2	|- ( K e. ( M ..^ N ) -> N e. ZZ )
4		znnsub	|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K < N <-> ( N - K ) e. NN ) )
5	2 3 4	syl2anc	|- ( K e. ( M ..^ N ) -> ( K < N <-> ( N - K ) e. NN ) )
6	1 5	mpbid	|- ( K e. ( M ..^ N ) -> ( N - K ) e. NN )