Metamath Proof Explorer

Theorem zmodfzp1

Description: An integer mod B lies in the first B + 1 nonnegative integers. (Contributed by AV, 27-Oct-2018)

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

Proof

Step Hyp Ref Expression
1 fzossfz 
 |-  ( 0 ..^ B ) C_ ( 0 ... B )
2 zmodfzo 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ..^ B ) )
3 1 2 sseldi 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ( 0 ... B ) )