Metamath Proof Explorer

Theorem divalglem4

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

Ref Expression
Hypotheses divalglem0.1 
|- N e. ZZ
divalglem0.2 
|- D e. ZZ
divalglem1.3 
|- D =/= 0
divalglem2.4 
|- S = { r e. NN0 | D || ( N - r ) }
Assertion divalglem4 
|- S = { r e. NN0 | E. q e. ZZ N = ( ( q x. D ) + r ) }

Proof

Step Hyp Ref Expression
1 divalglem0.1 
 |-  N e. ZZ
2 divalglem0.2 
 |-  D e. ZZ
3 divalglem1.3 
 |-  D =/= 0
4 divalglem2.4 
 |-  S = { r e. NN0 | D || ( N - r ) }
5 nn0z 
 |-  ( z e. NN0 -> z e. ZZ )
6 zsubcl 
 |-  ( ( N e. ZZ /\ z e. ZZ ) -> ( N - z ) e. ZZ )
7 1 5 6 sylancr 
 |-  ( z e. NN0 -> ( N - z ) e. ZZ )
8 divides 
 |-  ( ( D e. ZZ /\ ( N - z ) e. ZZ ) -> ( D || ( N - z ) <-> E. q e. ZZ ( q x. D ) = ( N - z ) ) )
9 2 7 8 sylancr 
 |-  ( z e. NN0 -> ( D || ( N - z ) <-> E. q e. ZZ ( q x. D ) = ( N - z ) ) )
10 nn0cn 
 |-  ( z e. NN0 -> z e. CC )
11 zmulcl 
 |-  ( ( q e. ZZ /\ D e. ZZ ) -> ( q x. D ) e. ZZ )
12 2 11 mpan2 
 |-  ( q e. ZZ -> ( q x. D ) e. ZZ )
13 12 zcnd 
 |-  ( q e. ZZ -> ( q x. D ) e. CC )
14 zcn 
 |-  ( N e. ZZ -> N e. CC )
15 1 14 ax-mp 
 |-  N e. CC
16 subadd 
 |-  ( ( N e. CC /\ z e. CC /\ ( q x. D ) e. CC ) -> ( ( N - z ) = ( q x. D ) <-> ( z + ( q x. D ) ) = N ) )
17 15 16 mp3an1 
 |-  ( ( z e. CC /\ ( q x. D ) e. CC ) -> ( ( N - z ) = ( q x. D ) <-> ( z + ( q x. D ) ) = N ) )
18 addcom 
 |-  ( ( z e. CC /\ ( q x. D ) e. CC ) -> ( z + ( q x. D ) ) = ( ( q x. D ) + z ) )
19 18 eqeq1d 
 |-  ( ( z e. CC /\ ( q x. D ) e. CC ) -> ( ( z + ( q x. D ) ) = N <-> ( ( q x. D ) + z ) = N ) )
20 17 19 bitrd 
 |-  ( ( z e. CC /\ ( q x. D ) e. CC ) -> ( ( N - z ) = ( q x. D ) <-> ( ( q x. D ) + z ) = N ) )
21 10 13 20 syl2an 
 |-  ( ( z e. NN0 /\ q e. ZZ ) -> ( ( N - z ) = ( q x. D ) <-> ( ( q x. D ) + z ) = N ) )
22 eqcom 
 |-  ( ( N - z ) = ( q x. D ) <-> ( q x. D ) = ( N - z ) )
23 eqcom 
 |-  ( ( ( q x. D ) + z ) = N <-> N = ( ( q x. D ) + z ) )
24 21 22 23 3bitr3g 
 |-  ( ( z e. NN0 /\ q e. ZZ ) -> ( ( q x. D ) = ( N - z ) <-> N = ( ( q x. D ) + z ) ) )
25 24 rexbidva 
 |-  ( z e. NN0 -> ( E. q e. ZZ ( q x. D ) = ( N - z ) <-> E. q e. ZZ N = ( ( q x. D ) + z ) ) )
26 9 25 bitrd 
 |-  ( z e. NN0 -> ( D || ( N - z ) <-> E. q e. ZZ N = ( ( q x. D ) + z ) ) )
27 26 pm5.32i 
 |-  ( ( z e. NN0 /\ D || ( N - z ) ) <-> ( z e. NN0 /\ E. q e. ZZ N = ( ( q x. D ) + z ) ) )
28 oveq2 
 |-  ( r = z -> ( N - r ) = ( N - z ) )
29 28 breq2d 
 |-  ( r = z -> ( D || ( N - r ) <-> D || ( N - z ) ) )
30 29 4 elrab2 
 |-  ( z e. S <-> ( z e. NN0 /\ D || ( N - z ) ) )
31 oveq2 
 |-  ( r = z -> ( ( q x. D ) + r ) = ( ( q x. D ) + z ) )
32 31 eqeq2d 
 |-  ( r = z -> ( N = ( ( q x. D ) + r ) <-> N = ( ( q x. D ) + z ) ) )
33 32 rexbidv 
 |-  ( r = z -> ( E. q e. ZZ N = ( ( q x. D ) + r ) <-> E. q e. ZZ N = ( ( q x. D ) + z ) ) )
34 33 elrab 
 |-  ( z e. { r e. NN0 | E. q e. ZZ N = ( ( q x. D ) + r ) } <-> ( z e. NN0 /\ E. q e. ZZ N = ( ( q x. D ) + z ) ) )
35 27 30 34 3bitr4i 
 |-  ( z e. S <-> z e. { r e. NN0 | E. q e. ZZ N = ( ( q x. D ) + r ) } )
36 35 eqriv 
 |-  S = { r e. NN0 | E. q e. ZZ N = ( ( q x. D ) + r ) }