Metamath Proof Explorer

Theorem divalglem8

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

Ref Expression
Hypotheses divalglem8.1 
|- N e. ZZ
divalglem8.2 
|- D e. ZZ
divalglem8.3 
|- D =/= 0
divalglem8.4 
|- S = { r e. NN0 | D || ( N - r ) }
Assertion divalglem8 
|- ( ( ( X e. S /\ Y e. S ) /\ ( X < ( abs ` D ) /\ Y < ( abs ` D ) ) ) -> ( K e. ZZ -> ( ( K x. ( abs ` D ) ) = ( Y - X ) -> X = Y ) ) )

Proof

Step Hyp Ref Expression
1 divalglem8.1 
 |-  N e. ZZ
2 divalglem8.2 
 |-  D e. ZZ
3 divalglem8.3 
 |-  D =/= 0
4 divalglem8.4 
 |-  S = { r e. NN0 | D || ( N - r ) }
5 4 ssrab3 
 |-  S C_ NN0
6 nn0sscn 
 |-  NN0 C_ CC
7 5 6 sstri 
 |-  S C_ CC
8 7 sseli 
 |-  ( Y e. S -> Y e. CC )
9 7 sseli 
 |-  ( X e. S -> X e. CC )
10 nnabscl 
 |-  ( ( D e. ZZ /\ D =/= 0 ) -> ( abs ` D ) e. NN )
11 2 3 10 mp2an 
 |-  ( abs ` D ) e. NN
12 11 nnzi 
 |-  ( abs ` D ) e. ZZ
13 zmulcl 
 |-  ( ( K e. ZZ /\ ( abs ` D ) e. ZZ ) -> ( K x. ( abs ` D ) ) e. ZZ )
14 12 13 mpan2 
 |-  ( K e. ZZ -> ( K x. ( abs ` D ) ) e. ZZ )
15 14 zcnd 
 |-  ( K e. ZZ -> ( K x. ( abs ` D ) ) e. CC )
16 subadd 
 |-  ( ( Y e. CC /\ X e. CC /\ ( K x. ( abs ` D ) ) e. CC ) -> ( ( Y - X ) = ( K x. ( abs ` D ) ) <-> ( X + ( K x. ( abs ` D ) ) ) = Y ) )
17 8 9 15 16 syl3an 
 |-  ( ( Y e. S /\ X e. S /\ K e. ZZ ) -> ( ( Y - X ) = ( K x. ( abs ` D ) ) <-> ( X + ( K x. ( abs ` D ) ) ) = Y ) )
18 17 3com12 
 |-  ( ( X e. S /\ Y e. S /\ K e. ZZ ) -> ( ( Y - X ) = ( K x. ( abs ` D ) ) <-> ( X + ( K x. ( abs ` D ) ) ) = Y ) )
19 eqcom 
 |-  ( ( Y - X ) = ( K x. ( abs ` D ) ) <-> ( K x. ( abs ` D ) ) = ( Y - X ) )
20 eqcom 
 |-  ( ( X + ( K x. ( abs ` D ) ) ) = Y <-> Y = ( X + ( K x. ( abs ` D ) ) ) )
21 18 19 20 3bitr3g 
 |-  ( ( X e. S /\ Y e. S /\ K e. ZZ ) -> ( ( K x. ( abs ` D ) ) = ( Y - X ) <-> Y = ( X + ( K x. ( abs ` D ) ) ) ) )
22 21 3adant1r 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ Y e. S /\ K e. ZZ ) -> ( ( K x. ( abs ` D ) ) = ( Y - X ) <-> Y = ( X + ( K x. ( abs ` D ) ) ) ) )
23 22 3adant2r 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( ( K x. ( abs ` D ) ) = ( Y - X ) <-> Y = ( X + ( K x. ( abs ` D ) ) ) ) )
24 breq1 
 |-  ( z = Y -> ( z < ( abs ` D ) <-> Y < ( abs ` D ) ) )
25 eleq1 
 |-  ( z = Y -> ( z e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> Y e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
26 24 25 imbi12d 
 |-  ( z = Y -> ( ( z < ( abs ` D ) -> z e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) <-> ( Y < ( abs ` D ) -> Y e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) ) )
27 5 sseli 
 |-  ( z e. S -> z e. NN0 )
28 elnn0z 
 |-  ( z e. NN0 <-> ( z e. ZZ /\ 0 <_ z ) )
29 27 28 sylib 
 |-  ( z e. S -> ( z e. ZZ /\ 0 <_ z ) )
30 29 anim1i 
 |-  ( ( z e. S /\ z < ( abs ` D ) ) -> ( ( z e. ZZ /\ 0 <_ z ) /\ z < ( abs ` D ) ) )
31 df-3an 
 |-  ( ( z e. ZZ /\ 0 <_ z /\ z < ( abs ` D ) ) <-> ( ( z e. ZZ /\ 0 <_ z ) /\ z < ( abs ` D ) ) )
32 30 31 sylibr 
 |-  ( ( z e. S /\ z < ( abs ` D ) ) -> ( z e. ZZ /\ 0 <_ z /\ z < ( abs ` D ) ) )
33 0z 
 |-  0 e. ZZ
34 elfzm11 
 |-  ( ( 0 e. ZZ /\ ( abs ` D ) e. ZZ ) -> ( z e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> ( z e. ZZ /\ 0 <_ z /\ z < ( abs ` D ) ) ) )
35 33 12 34 mp2an 
 |-  ( z e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> ( z e. ZZ /\ 0 <_ z /\ z < ( abs ` D ) ) )
36 32 35 sylibr 
 |-  ( ( z e. S /\ z < ( abs ` D ) ) -> z e. ( 0 ... ( ( abs ` D ) - 1 ) ) )
37 36 ex 
 |-  ( z e. S -> ( z < ( abs ` D ) -> z e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
38 26 37 vtoclga 
 |-  ( Y e. S -> ( Y < ( abs ` D ) -> Y e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
39 eleq1 
 |-  ( Y = ( X + ( K x. ( abs ` D ) ) ) -> ( Y e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
40 39 biimpd 
 |-  ( Y = ( X + ( K x. ( abs ` D ) ) ) -> ( Y e. ( 0 ... ( ( abs ` D ) - 1 ) ) -> ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
41 38 40 sylan9 
 |-  ( ( Y e. S /\ Y = ( X + ( K x. ( abs ` D ) ) ) ) -> ( Y < ( abs ` D ) -> ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
42 41 impancom 
 |-  ( ( Y e. S /\ Y < ( abs ` D ) ) -> ( Y = ( X + ( K x. ( abs ` D ) ) ) -> ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
43 42 3ad2ant2 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( Y = ( X + ( K x. ( abs ` D ) ) ) -> ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
44 breq1 
 |-  ( z = X -> ( z < ( abs ` D ) <-> X < ( abs ` D ) ) )
45 eleq1 
 |-  ( z = X -> ( z e. ( 0 ... ( ( abs ` D ) - 1 ) ) <-> X e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
46 44 45 imbi12d 
 |-  ( z = X -> ( ( z < ( abs ` D ) -> z e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) <-> ( X < ( abs ` D ) -> X e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) ) )
47 46 37 vtoclga 
 |-  ( X e. S -> ( X < ( abs ` D ) -> X e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
48 47 imp 
 |-  ( ( X e. S /\ X < ( abs ` D ) ) -> X e. ( 0 ... ( ( abs ` D ) - 1 ) ) )
49 2 3 divalglem7 
 |-  ( ( X e. ( 0 ... ( ( abs ` D ) - 1 ) ) /\ K e. ZZ ) -> ( K =/= 0 -> -. ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
50 48 49 sylan 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ K e. ZZ ) -> ( K =/= 0 -> -. ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
51 50 3adant2 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( K =/= 0 -> -. ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) ) )
52 51 con2d 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( ( X + ( K x. ( abs ` D ) ) ) e. ( 0 ... ( ( abs ` D ) - 1 ) ) -> -. K =/= 0 ) )
53 43 52 syld 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( Y = ( X + ( K x. ( abs ` D ) ) ) -> -. K =/= 0 ) )
54 df-ne 
 |-  ( K =/= 0 <-> -. K = 0 )
55 54 con2bii 
 |-  ( K = 0 <-> -. K =/= 0 )
56 53 55 syl6ibr 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( Y = ( X + ( K x. ( abs ` D ) ) ) -> K = 0 ) )
57 23 56 sylbid 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( ( K x. ( abs ` D ) ) = ( Y - X ) -> K = 0 ) )
58 oveq1 
 |-  ( K = 0 -> ( K x. ( abs ` D ) ) = ( 0 x. ( abs ` D ) ) )
59 11 nncni 
 |-  ( abs ` D ) e. CC
60 59 mul02i 
 |-  ( 0 x. ( abs ` D ) ) = 0
61 58 60 eqtrdi 
 |-  ( K = 0 -> ( K x. ( abs ` D ) ) = 0 )
62 61 eqeq1d 
 |-  ( K = 0 -> ( ( K x. ( abs ` D ) ) = ( Y - X ) <-> 0 = ( Y - X ) ) )
63 62 biimpac 
 |-  ( ( ( K x. ( abs ` D ) ) = ( Y - X ) /\ K = 0 ) -> 0 = ( Y - X ) )
64 subeq0 
 |-  ( ( Y e. CC /\ X e. CC ) -> ( ( Y - X ) = 0 <-> Y = X ) )
65 8 9 64 syl2anr 
 |-  ( ( X e. S /\ Y e. S ) -> ( ( Y - X ) = 0 <-> Y = X ) )
66 eqcom 
 |-  ( ( Y - X ) = 0 <-> 0 = ( Y - X ) )
67 eqcom 
 |-  ( Y = X <-> X = Y )
68 65 66 67 3bitr3g 
 |-  ( ( X e. S /\ Y e. S ) -> ( 0 = ( Y - X ) <-> X = Y ) )
69 63 68 syl5ib 
 |-  ( ( X e. S /\ Y e. S ) -> ( ( ( K x. ( abs ` D ) ) = ( Y - X ) /\ K = 0 ) -> X = Y ) )
70 69 ad2ant2r 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) ) -> ( ( ( K x. ( abs ` D ) ) = ( Y - X ) /\ K = 0 ) -> X = Y ) )
71 70 3adant3 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( ( ( K x. ( abs ` D ) ) = ( Y - X ) /\ K = 0 ) -> X = Y ) )
72 71 expd 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( ( K x. ( abs ` D ) ) = ( Y - X ) -> ( K = 0 -> X = Y ) ) )
73 57 72 mpdd 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) /\ K e. ZZ ) -> ( ( K x. ( abs ` D ) ) = ( Y - X ) -> X = Y ) )
74 73 3expia 
 |-  ( ( ( X e. S /\ X < ( abs ` D ) ) /\ ( Y e. S /\ Y < ( abs ` D ) ) ) -> ( K e. ZZ -> ( ( K x. ( abs ` D ) ) = ( Y - X ) -> X = Y ) ) )
75 74 an4s 
 |-  ( ( ( X e. S /\ Y e. S ) /\ ( X < ( abs ` D ) /\ Y < ( abs ` D ) ) ) -> ( K e. ZZ -> ( ( K x. ( abs ` D ) ) = ( Y - X ) -> X = Y ) ) )