Metamath Proof Explorer


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 ) )