Theorem zmodfzo

Description: An integer mod B lies in the first B nonnegative integers. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Assertion	zmodfzo	|- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ..^ B ) )

Proof

Step	Hyp	Ref	Expression
1		zmodfz	|- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ... ( B - 1 ) ) )
2		nnz	|- ( B e. NN -> B e. ZZ )
3		fzoval	|- ( B e. ZZ -> ( 0 ..^ B ) = ( 0 ... ( B - 1 ) ) )
4	2 3	syl	|- ( B e. NN -> ( 0 ..^ B ) = ( 0 ... ( B - 1 ) ) )
5	4	adantl	|- ( ( A e. ZZ /\ B e. NN ) -> ( 0 ..^ B ) = ( 0 ... ( B - 1 ) ) )
6	1 5	eleqtrrd	|- ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ..^ B ) )