Metamath Proof Explorer

Theorem zmodfz

Description: An integer mod B lies in the first B nonnegative integers. (Contributed by Jeff Madsen, 17-Jun-2010)

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

Proof

Step Hyp Ref Expression
1 zmodcl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. NN0 )
2 1 nn0zd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ZZ )
3 1 nn0ge0d 
 |-  ( ( A e. ZZ /\ B e. NN ) -> 0 <_ ( A mod B ) )
4 zre 
 |-  ( A e. ZZ -> A e. RR )
5 nnrp 
 |-  ( B e. NN -> B e. RR+ )
6 modlt 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) < B )
7 4 5 6 syl2an 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) < B )
8 0z 
 |-  0 e. ZZ
9 nnz 
 |-  ( B e. NN -> B e. ZZ )
10 9 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. ZZ )
11 elfzm11 
 |-  ( ( 0 e. ZZ /\ B e. ZZ ) -> ( ( A mod B ) e. ( 0 ... ( B - 1 ) ) <-> ( ( A mod B ) e. ZZ /\ 0 <_ ( A mod B ) /\ ( A mod B ) < B ) ) )
12 8 10 11 sylancr 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( ( A mod B ) e. ( 0 ... ( B - 1 ) ) <-> ( ( A mod B ) e. ZZ /\ 0 <_ ( A mod B ) /\ ( A mod B ) < B ) ) )
13 2 3 7 12 mpbir3and 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ... ( B - 1 ) ) )