Metamath Proof Explorer

Theorem divalglem5

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

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 ) }
divalglem5.5 
|- R = inf ( S , RR , < )
Assertion divalglem5 
|- ( 0 <_ R /\ R < ( abs ` D ) )

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 divalglem5.5 
 |-  R = inf ( S , RR , < )
6 1 2 3 4 divalglem2 
 |-  inf ( S , RR , < ) e. S
7 5 6 eqeltri 
 |-  R e. S
8 oveq2 
 |-  ( x = R -> ( N - x ) = ( N - R ) )
9 8 breq2d 
 |-  ( x = R -> ( D || ( N - x ) <-> D || ( N - R ) ) )
10 oveq2 
 |-  ( r = x -> ( N - r ) = ( N - x ) )
11 10 breq2d 
 |-  ( r = x -> ( D || ( N - r ) <-> D || ( N - x ) ) )
12 11 cbvrabv 
 |-  { r e. NN0 | D || ( N - r ) } = { x e. NN0 | D || ( N - x ) }
13 4 12 eqtri 
 |-  S = { x e. NN0 | D || ( N - x ) }
14 9 13 elrab2 
 |-  ( R e. S <-> ( R e. NN0 /\ D || ( N - R ) ) )
15 7 14 mpbi 
 |-  ( R e. NN0 /\ D || ( N - R ) )
16 15 simpli 
 |-  R e. NN0
17 16 nn0ge0i 
 |-  0 <_ R
18 nnabscl 
 |-  ( ( D e. ZZ /\ D =/= 0 ) -> ( abs ` D ) e. NN )
19 2 3 18 mp2an 
 |-  ( abs ` D ) e. NN
20 19 nngt0i 
 |-  0 < ( abs ` D )
21 0re 
 |-  0 e. RR
22 zcn 
 |-  ( D e. ZZ -> D e. CC )
23 2 22 ax-mp 
 |-  D e. CC
24 23 abscli 
 |-  ( abs ` D ) e. RR
25 21 24 ltnlei 
 |-  ( 0 < ( abs ` D ) <-> -. ( abs ` D ) <_ 0 )
26 20 25 mpbi 
 |-  -. ( abs ` D ) <_ 0
27 4 ssrab3 
 |-  S C_ NN0
28 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
29 27 28 sseqtri 
 |-  S C_ ( ZZ>= ` 0 )
30 nn0abscl 
 |-  ( D e. ZZ -> ( abs ` D ) e. NN0 )
31 2 30 ax-mp 
 |-  ( abs ` D ) e. NN0
32 nn0sub2 
 |-  ( ( ( abs ` D ) e. NN0 /\ R e. NN0 /\ ( abs ` D ) <_ R ) -> ( R - ( abs ` D ) ) e. NN0 )
33 31 16 32 mp3an12 
 |-  ( ( abs ` D ) <_ R -> ( R - ( abs ` D ) ) e. NN0 )
34 15 a1i 
 |-  ( ( abs ` D ) <_ R -> ( R e. NN0 /\ D || ( N - R ) ) )
35 nn0z 
 |-  ( R e. NN0 -> R e. ZZ )
36 1z 
 |-  1 e. ZZ
37 1 2 divalglem0 
 |-  ( ( R e. ZZ /\ 1 e. ZZ ) -> ( D || ( N - R ) -> D || ( N - ( R - ( 1 x. ( abs ` D ) ) ) ) ) )
38 36 37 mpan2 
 |-  ( R e. ZZ -> ( D || ( N - R ) -> D || ( N - ( R - ( 1 x. ( abs ` D ) ) ) ) ) )
39 24 recni 
 |-  ( abs ` D ) e. CC
40 39 mullidi 
 |-  ( 1 x. ( abs ` D ) ) = ( abs ` D )
41 40 oveq2i 
 |-  ( R - ( 1 x. ( abs ` D ) ) ) = ( R - ( abs ` D ) )
42 41 oveq2i 
 |-  ( N - ( R - ( 1 x. ( abs ` D ) ) ) ) = ( N - ( R - ( abs ` D ) ) )
43 42 breq2i 
 |-  ( D || ( N - ( R - ( 1 x. ( abs ` D ) ) ) ) <-> D || ( N - ( R - ( abs ` D ) ) ) )
44 38 43 imbitrdi 
 |-  ( R e. ZZ -> ( D || ( N - R ) -> D || ( N - ( R - ( abs ` D ) ) ) ) )
45 35 44 syl 
 |-  ( R e. NN0 -> ( D || ( N - R ) -> D || ( N - ( R - ( abs ` D ) ) ) ) )
46 45 imp 
 |-  ( ( R e. NN0 /\ D || ( N - R ) ) -> D || ( N - ( R - ( abs ` D ) ) ) )
47 34 46 syl 
 |-  ( ( abs ` D ) <_ R -> D || ( N - ( R - ( abs ` D ) ) ) )
48 oveq2 
 |-  ( x = ( R - ( abs ` D ) ) -> ( N - x ) = ( N - ( R - ( abs ` D ) ) ) )
49 48 breq2d 
 |-  ( x = ( R - ( abs ` D ) ) -> ( D || ( N - x ) <-> D || ( N - ( R - ( abs ` D ) ) ) ) )
50 49 13 elrab2 
 |-  ( ( R - ( abs ` D ) ) e. S <-> ( ( R - ( abs ` D ) ) e. NN0 /\ D || ( N - ( R - ( abs ` D ) ) ) ) )
51 33 47 50 sylanbrc 
 |-  ( ( abs ` D ) <_ R -> ( R - ( abs ` D ) ) e. S )
52 infssuzle 
 |-  ( ( S C_ ( ZZ>= ` 0 ) /\ ( R - ( abs ` D ) ) e. S ) -> inf ( S , RR , < ) <_ ( R - ( abs ` D ) ) )
53 29 51 52 sylancr 
 |-  ( ( abs ` D ) <_ R -> inf ( S , RR , < ) <_ ( R - ( abs ` D ) ) )
54 5 53 eqbrtrid 
 |-  ( ( abs ` D ) <_ R -> R <_ ( R - ( abs ` D ) ) )
55 34 simpld 
 |-  ( ( abs ` D ) <_ R -> R e. NN0 )
56 55 nn0red 
 |-  ( ( abs ` D ) <_ R -> R e. RR )
57 lesub 
 |-  ( ( R e. RR /\ R e. RR /\ ( abs ` D ) e. RR ) -> ( R <_ ( R - ( abs ` D ) ) <-> ( abs ` D ) <_ ( R - R ) ) )
58 24 57 mp3an3 
 |-  ( ( R e. RR /\ R e. RR ) -> ( R <_ ( R - ( abs ` D ) ) <-> ( abs ` D ) <_ ( R - R ) ) )
59 56 56 58 syl2anc 
 |-  ( ( abs ` D ) <_ R -> ( R <_ ( R - ( abs ` D ) ) <-> ( abs ` D ) <_ ( R - R ) ) )
60 56 recnd 
 |-  ( ( abs ` D ) <_ R -> R e. CC )
61 60 subidd 
 |-  ( ( abs ` D ) <_ R -> ( R - R ) = 0 )
62 61 breq2d 
 |-  ( ( abs ` D ) <_ R -> ( ( abs ` D ) <_ ( R - R ) <-> ( abs ` D ) <_ 0 ) )
63 59 62 bitrd 
 |-  ( ( abs ` D ) <_ R -> ( R <_ ( R - ( abs ` D ) ) <-> ( abs ` D ) <_ 0 ) )
64 54 63 mpbid 
 |-  ( ( abs ` D ) <_ R -> ( abs ` D ) <_ 0 )
65 26 64 mto 
 |-  -. ( abs ` D ) <_ R
66 16 nn0rei 
 |-  R e. RR
67 66 24 ltnlei 
 |-  ( R < ( abs ` D ) <-> -. ( abs ` D ) <_ R )
68 65 67 mpbir 
 |-  R < ( abs ` D )
69 17 68 pm3.2i 
 |-  ( 0 <_ R /\ R < ( abs ` D ) )