Metamath Proof Explorer

Theorem divalglem9

Description: Lemma for divalg . (Contributed by Paul Chapman, 21-Mar-2011) (Revised by AV, 2-Oct-2020)

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 ) }
divalglem9.5 
|- R = inf ( S , RR , < )
Assertion divalglem9 
|- E! x e. S x < ( abs ` D )

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 divalglem9.5 
 |-  R = inf ( S , RR , < )
6 1 2 3 4 divalglem2 
 |-  inf ( S , RR , < ) e. S
7 5 6 eqeltri 
 |-  R e. S
8 1 2 3 4 5 divalglem5 
 |-  ( 0 <_ R /\ R < ( abs ` D ) )
9 8 simpri 
 |-  R < ( abs ` D )
10 breq1 
 |-  ( x = R -> ( x < ( abs ` D ) <-> R < ( abs ` D ) ) )
11 10 rspcev 
 |-  ( ( R e. S /\ R < ( abs ` D ) ) -> E. x e. S x < ( abs ` D ) )
12 7 9 11 mp2an 
 |-  E. x e. S x < ( abs ` D )
13 oveq2 
 |-  ( r = x -> ( N - r ) = ( N - x ) )
14 13 breq2d 
 |-  ( r = x -> ( D || ( N - r ) <-> D || ( N - x ) ) )
15 14 4 elrab2 
 |-  ( x e. S <-> ( x e. NN0 /\ D || ( N - x ) ) )
16 15 simplbi 
 |-  ( x e. S -> x e. NN0 )
17 16 nn0zd 
 |-  ( x e. S -> x e. ZZ )
18 oveq2 
 |-  ( r = y -> ( N - r ) = ( N - y ) )
19 18 breq2d 
 |-  ( r = y -> ( D || ( N - r ) <-> D || ( N - y ) ) )
20 19 4 elrab2 
 |-  ( y e. S <-> ( y e. NN0 /\ D || ( N - y ) ) )
21 20 simplbi 
 |-  ( y e. S -> y e. NN0 )
22 21 nn0zd 
 |-  ( y e. S -> y e. ZZ )
23 zsubcl 
 |-  ( ( N e. ZZ /\ x e. ZZ ) -> ( N - x ) e. ZZ )
24 1 23 mpan 
 |-  ( x e. ZZ -> ( N - x ) e. ZZ )
25 zsubcl 
 |-  ( ( N e. ZZ /\ y e. ZZ ) -> ( N - y ) e. ZZ )
26 1 25 mpan 
 |-  ( y e. ZZ -> ( N - y ) e. ZZ )
27 24 26 anim12i 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( N - x ) e. ZZ /\ ( N - y ) e. ZZ ) )
28 17 22 27 syl2an 
 |-  ( ( x e. S /\ y e. S ) -> ( ( N - x ) e. ZZ /\ ( N - y ) e. ZZ ) )
29 15 simprbi 
 |-  ( x e. S -> D || ( N - x ) )
30 20 simprbi 
 |-  ( y e. S -> D || ( N - y ) )
31 29 30 anim12i 
 |-  ( ( x e. S /\ y e. S ) -> ( D || ( N - x ) /\ D || ( N - y ) ) )
32 dvds2sub 
 |-  ( ( D e. ZZ /\ ( N - x ) e. ZZ /\ ( N - y ) e. ZZ ) -> ( ( D || ( N - x ) /\ D || ( N - y ) ) -> D || ( ( N - x ) - ( N - y ) ) ) )
33 2 32 mp3an1 
 |-  ( ( ( N - x ) e. ZZ /\ ( N - y ) e. ZZ ) -> ( ( D || ( N - x ) /\ D || ( N - y ) ) -> D || ( ( N - x ) - ( N - y ) ) ) )
34 28 31 33 sylc 
 |-  ( ( x e. S /\ y e. S ) -> D || ( ( N - x ) - ( N - y ) ) )
35 zcn 
 |-  ( x e. ZZ -> x e. CC )
36 zcn 
 |-  ( y e. ZZ -> y e. CC )
37 1 zrei 
 |-  N e. RR
38 37 recni 
 |-  N e. CC
39 38 subidi 
 |-  ( N - N ) = 0
40 39 oveq1i 
 |-  ( ( N - N ) - ( x - y ) ) = ( 0 - ( x - y ) )
41 0cn 
 |-  0 e. CC
42 subsub2 
 |-  ( ( 0 e. CC /\ x e. CC /\ y e. CC ) -> ( 0 - ( x - y ) ) = ( 0 + ( y - x ) ) )
43 41 42 mp3an1 
 |-  ( ( x e. CC /\ y e. CC ) -> ( 0 - ( x - y ) ) = ( 0 + ( y - x ) ) )
44 40 43 syl5eq 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( N - N ) - ( x - y ) ) = ( 0 + ( y - x ) ) )
45 sub4 
 |-  ( ( ( N e. CC /\ N e. CC ) /\ ( x e. CC /\ y e. CC ) ) -> ( ( N - N ) - ( x - y ) ) = ( ( N - x ) - ( N - y ) ) )
46 38 38 45 mpanl12 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( N - N ) - ( x - y ) ) = ( ( N - x ) - ( N - y ) ) )
47 subcl 
 |-  ( ( y e. CC /\ x e. CC ) -> ( y - x ) e. CC )
48 47 ancoms 
 |-  ( ( x e. CC /\ y e. CC ) -> ( y - x ) e. CC )
49 48 addid2d 
 |-  ( ( x e. CC /\ y e. CC ) -> ( 0 + ( y - x ) ) = ( y - x ) )
50 44 46 49 3eqtr3d 
 |-  ( ( x e. CC /\ y e. CC ) -> ( ( N - x ) - ( N - y ) ) = ( y - x ) )
51 35 36 50 syl2an 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( N - x ) - ( N - y ) ) = ( y - x ) )
52 17 22 51 syl2an 
 |-  ( ( x e. S /\ y e. S ) -> ( ( N - x ) - ( N - y ) ) = ( y - x ) )
53 52 breq2d 
 |-  ( ( x e. S /\ y e. S ) -> ( D || ( ( N - x ) - ( N - y ) ) <-> D || ( y - x ) ) )
54 34 53 mpbid 
 |-  ( ( x e. S /\ y e. S ) -> D || ( y - x ) )
55 zsubcl 
 |-  ( ( y e. ZZ /\ x e. ZZ ) -> ( y - x ) e. ZZ )
56 55 ancoms 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( y - x ) e. ZZ )
57 absdvdsb 
 |-  ( ( D e. ZZ /\ ( y - x ) e. ZZ ) -> ( D || ( y - x ) <-> ( abs ` D ) || ( y - x ) ) )
58 2 56 57 sylancr 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( D || ( y - x ) <-> ( abs ` D ) || ( y - x ) ) )
59 17 22 58 syl2an 
 |-  ( ( x e. S /\ y e. S ) -> ( D || ( y - x ) <-> ( abs ` D ) || ( y - x ) ) )
60 54 59 mpbid 
 |-  ( ( x e. S /\ y e. S ) -> ( abs ` D ) || ( y - x ) )
61 nnabscl 
 |-  ( ( D e. ZZ /\ D =/= 0 ) -> ( abs ` D ) e. NN )
62 2 3 61 mp2an 
 |-  ( abs ` D ) e. NN
63 62 nnzi 
 |-  ( abs ` D ) e. ZZ
64 divides 
 |-  ( ( ( abs ` D ) e. ZZ /\ ( y - x ) e. ZZ ) -> ( ( abs ` D ) || ( y - x ) <-> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) ) )
65 63 56 64 sylancr 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( ( abs ` D ) || ( y - x ) <-> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) ) )
66 17 22 65 syl2an 
 |-  ( ( x e. S /\ y e. S ) -> ( ( abs ` D ) || ( y - x ) <-> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) ) )
67 60 66 mpbid 
 |-  ( ( x e. S /\ y e. S ) -> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) )
68 67 adantr 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( x < ( abs ` D ) /\ y < ( abs ` D ) ) ) -> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) )
69 1 2 3 4 divalglem8 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( x < ( abs ` D ) /\ y < ( abs ` D ) ) ) -> ( k e. ZZ -> ( ( k x. ( abs ` D ) ) = ( y - x ) -> x = y ) ) )
70 69 rexlimdv 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( x < ( abs ` D ) /\ y < ( abs ` D ) ) ) -> ( E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) -> x = y ) )
71 68 70 mpd 
 |-  ( ( ( x e. S /\ y e. S ) /\ ( x < ( abs ` D ) /\ y < ( abs ` D ) ) ) -> x = y )
72 71 ex 
 |-  ( ( x e. S /\ y e. S ) -> ( ( x < ( abs ` D ) /\ y < ( abs ` D ) ) -> x = y ) )
73 72 rgen2 
 |-  A. x e. S A. y e. S ( ( x < ( abs ` D ) /\ y < ( abs ` D ) ) -> x = y )
74 breq1 
 |-  ( x = y -> ( x < ( abs ` D ) <-> y < ( abs ` D ) ) )
75 74 reu4 
 |-  ( E! x e. S x < ( abs ` D ) <-> ( E. x e. S x < ( abs ` D ) /\ A. x e. S A. y e. S ( ( x < ( abs ` D ) /\ y < ( abs ` D ) ) -> x = y ) ) )
76 12 73 75 mpbir2an 
 |-  E! x e. S x < ( abs ` D )