Metamath Proof Explorer

Theorem modabsdifz

Description: Divisibility in terms of modular reduction by the absolute value of the base. (Contributed by Stefan O'Rear, 26-Sep-2014)

Ref Expression
Assertion modabsdifz 
|- ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( N - ( N mod ( abs ` M ) ) ) / M ) e. ZZ )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> N e. RR )
2 simp2 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> M e. RR )
3 2 recnd 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> M e. CC )
4 simp3 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> M =/= 0 )
5 3 4 absrpcld 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( abs ` M ) e. RR+ )
6 moddifz 
 |-  ( ( N e. RR /\ ( abs ` M ) e. RR+ ) -> ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) e. ZZ )
7 1 5 6 syl2anc 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) e. ZZ )
8 absidm 
 |-  ( M e. CC -> ( abs ` ( abs ` M ) ) = ( abs ` M ) )
9 3 8 syl 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( abs ` ( abs ` M ) ) = ( abs ` M ) )
10 9 oveq2d 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( abs ` ( N - ( N mod ( abs ` M ) ) ) ) / ( abs ` ( abs ` M ) ) ) = ( ( abs ` ( N - ( N mod ( abs ` M ) ) ) ) / ( abs ` M ) ) )
11 1 5 modcld 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( N mod ( abs ` M ) ) e. RR )
12 1 11 resubcld 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( N - ( N mod ( abs ` M ) ) ) e. RR )
13 12 recnd 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( N - ( N mod ( abs ` M ) ) ) e. CC )
14 3 abscld 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( abs ` M ) e. RR )
15 14 recnd 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( abs ` M ) e. CC )
16 5 rpne0d 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( abs ` M ) =/= 0 )
17 13 15 16 absdivd 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) ) = ( ( abs ` ( N - ( N mod ( abs ` M ) ) ) ) / ( abs ` ( abs ` M ) ) ) )
18 13 3 4 absdivd 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / M ) ) = ( ( abs ` ( N - ( N mod ( abs ` M ) ) ) ) / ( abs ` M ) ) )
19 10 17 18 3eqtr4d 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) ) = ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / M ) ) )
20 19 eleq1d 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) ) e. ZZ <-> ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / M ) ) e. ZZ ) )
21 12 14 16 redivcld 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) e. RR )
22 absz 
 |-  ( ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) e. RR -> ( ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) e. ZZ <-> ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) ) e. ZZ ) )
23 21 22 syl 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) e. ZZ <-> ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) ) e. ZZ ) )
24 12 2 4 redivcld 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( N - ( N mod ( abs ` M ) ) ) / M ) e. RR )
25 absz 
 |-  ( ( ( N - ( N mod ( abs ` M ) ) ) / M ) e. RR -> ( ( ( N - ( N mod ( abs ` M ) ) ) / M ) e. ZZ <-> ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / M ) ) e. ZZ ) )
26 24 25 syl 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( ( N - ( N mod ( abs ` M ) ) ) / M ) e. ZZ <-> ( abs ` ( ( N - ( N mod ( abs ` M ) ) ) / M ) ) e. ZZ ) )
27 20 23 26 3bitr4d 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( ( N - ( N mod ( abs ` M ) ) ) / ( abs ` M ) ) e. ZZ <-> ( ( N - ( N mod ( abs ` M ) ) ) / M ) e. ZZ ) )
28 7 27 mpbid 
 |-  ( ( N e. RR /\ M e. RR /\ M =/= 0 ) -> ( ( N - ( N mod ( abs ` M ) ) ) / M ) e. ZZ )