Metamath Proof Explorer

Theorem divalglem0

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011)

Ref Expression
Hypotheses divalglem0.1 
|- N e. ZZ
divalglem0.2 
|- D e. ZZ
Assertion divalglem0 
|- ( ( R e. ZZ /\ K e. ZZ ) -> ( D || ( N - R ) -> D || ( N - ( R - ( K x. ( abs ` D ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 divalglem0.1 
 |-  N e. ZZ
2 divalglem0.2 
 |-  D e. ZZ
3 iddvds 
 |-  ( D e. ZZ -> D || D )
4 dvdsabsb 
 |-  ( ( D e. ZZ /\ D e. ZZ ) -> ( D || D <-> D || ( abs ` D ) ) )
5 4 anidms 
 |-  ( D e. ZZ -> ( D || D <-> D || ( abs ` D ) ) )
6 3 5 mpbid 
 |-  ( D e. ZZ -> D || ( abs ` D ) )
7 2 6 ax-mp 
 |-  D || ( abs ` D )
8 nn0abscl 
 |-  ( D e. ZZ -> ( abs ` D ) e. NN0 )
9 2 8 ax-mp 
 |-  ( abs ` D ) e. NN0
10 9 nn0zi 
 |-  ( abs ` D ) e. ZZ
11 dvdsmultr2 
 |-  ( ( D e. ZZ /\ K e. ZZ /\ ( abs ` D ) e. ZZ ) -> ( D || ( abs ` D ) -> D || ( K x. ( abs ` D ) ) ) )
12 2 10 11 mp3an13 
 |-  ( K e. ZZ -> ( D || ( abs ` D ) -> D || ( K x. ( abs ` D ) ) ) )
13 7 12 mpi 
 |-  ( K e. ZZ -> D || ( K x. ( abs ` D ) ) )
14 13 adantl 
 |-  ( ( R e. ZZ /\ K e. ZZ ) -> D || ( K x. ( abs ` D ) ) )
15 zsubcl 
 |-  ( ( N e. ZZ /\ R e. ZZ ) -> ( N - R ) e. ZZ )
16 1 15 mpan 
 |-  ( R e. ZZ -> ( N - R ) e. ZZ )
17 zmulcl 
 |-  ( ( K e. ZZ /\ ( abs ` D ) e. ZZ ) -> ( K x. ( abs ` D ) ) e. ZZ )
18 10 17 mpan2 
 |-  ( K e. ZZ -> ( K x. ( abs ` D ) ) e. ZZ )
19 dvds2add 
 |-  ( ( D e. ZZ /\ ( N - R ) e. ZZ /\ ( K x. ( abs ` D ) ) e. ZZ ) -> ( ( D || ( N - R ) /\ D || ( K x. ( abs ` D ) ) ) -> D || ( ( N - R ) + ( K x. ( abs ` D ) ) ) ) )
20 2 16 18 19 mp3an3an 
 |-  ( ( R e. ZZ /\ K e. ZZ ) -> ( ( D || ( N - R ) /\ D || ( K x. ( abs ` D ) ) ) -> D || ( ( N - R ) + ( K x. ( abs ` D ) ) ) ) )
21 14 20 mpan2d 
 |-  ( ( R e. ZZ /\ K e. ZZ ) -> ( D || ( N - R ) -> D || ( ( N - R ) + ( K x. ( abs ` D ) ) ) ) )
22 zcn 
 |-  ( N e. ZZ -> N e. CC )
23 1 22 ax-mp 
 |-  N e. CC
24 zcn 
 |-  ( R e. ZZ -> R e. CC )
25 18 zcnd 
 |-  ( K e. ZZ -> ( K x. ( abs ` D ) ) e. CC )
26 subsub 
 |-  ( ( N e. CC /\ R e. CC /\ ( K x. ( abs ` D ) ) e. CC ) -> ( N - ( R - ( K x. ( abs ` D ) ) ) ) = ( ( N - R ) + ( K x. ( abs ` D ) ) ) )
27 23 24 25 26 mp3an3an 
 |-  ( ( R e. ZZ /\ K e. ZZ ) -> ( N - ( R - ( K x. ( abs ` D ) ) ) ) = ( ( N - R ) + ( K x. ( abs ` D ) ) ) )
28 27 breq2d 
 |-  ( ( R e. ZZ /\ K e. ZZ ) -> ( D || ( N - ( R - ( K x. ( abs ` D ) ) ) ) <-> D || ( ( N - R ) + ( K x. ( abs ` D ) ) ) ) )
29 21 28 sylibrd 
 |-  ( ( R e. ZZ /\ K e. ZZ ) -> ( D || ( N - R ) -> D || ( N - ( R - ( K x. ( abs ` D ) ) ) ) ) )