This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zmodcl

Description: Closure law for the modulo operation restricted to integers. (Contributed by NM, 27-Nov-2008)

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

Proof

Step Hyp Ref Expression
1 zre 
 |-  ( A e. ZZ -> A e. RR )
2 nnrp 
 |-  ( B e. NN -> B e. RR+ )
3 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
4 1 2 3 syl2an 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
5 nnz 
 |-  ( B e. NN -> B e. ZZ )
6 5 adantl 
 |-  ( ( A e. ZZ /\ B e. NN ) -> B e. ZZ )
7 nndivre 
 |-  ( ( A e. RR /\ B e. NN ) -> ( A / B ) e. RR )
8 1 7 sylan 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A / B ) e. RR )
9 8 flcld 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( |_ ` ( A / B ) ) e. ZZ )
10 6 9 zmulcld 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( B x. ( |_ ` ( A / B ) ) ) e. ZZ )
11 zsubcl 
 |-  ( ( A e. ZZ /\ ( B x. ( |_ ` ( A / B ) ) ) e. ZZ ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) e. ZZ )
12 10 11 syldan 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) e. ZZ )
13 4 12 eqeltrd 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. ZZ )
14 modge0 
 |-  ( ( A e. RR /\ B e. RR+ ) -> 0 <_ ( A mod B ) )
15 1 2 14 syl2an 
 |-  ( ( A e. ZZ /\ B e. NN ) -> 0 <_ ( A mod B ) )
16 elnn0z 
 |-  ( ( A mod B ) e. NN0 <-> ( ( A mod B ) e. ZZ /\ 0 <_ ( A mod B ) ) )
17 13 15 16 sylanbrc 
 |-  ( ( A e. ZZ /\ B e. NN ) -> ( A mod B ) e. NN0 )