Metamath Proof Explorer

Theorem dnibndlem9

Description: Lemma for dnibnd . (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypotheses dnibndlem9.1 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
dnibndlem9.2 
|- ( ph -> A e. RR )
dnibndlem9.3 
|- ( ph -> B e. RR )
dnibndlem9.4 
|- ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
Assertion dnibndlem9 
|- ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )

Proof

Step Hyp Ref Expression
1 dnibndlem9.1 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 dnibndlem9.2 
 |-  ( ph -> A e. RR )
3 dnibndlem9.3 
 |-  ( ph -> B e. RR )
4 dnibndlem9.4 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
5 3 dnicld1 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR )
6 5 recnd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. CC )
7 2 dnicld1 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )
8 7 recnd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. CC )
9 6 8 subcld 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. CC )
10 9 abscld 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) e. RR )
11 halfre 
 |-  ( 1 / 2 ) e. RR
12 11 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
13 12 5 jca 
 |-  ( ph -> ( ( 1 / 2 ) e. RR /\ ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR ) )
14 resubcl 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR ) -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) e. RR )
15 13 14 syl 
 |-  ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) e. RR )
16 12 7 jca 
 |-  ( ph -> ( ( 1 / 2 ) e. RR /\ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR ) )
17 resubcl 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR ) -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. RR )
18 16 17 syl 
 |-  ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. RR )
19 15 18 readdcld 
 |-  ( ph -> ( ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) + ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) e. RR )
20 3 recnd 
 |-  ( ph -> B e. CC )
21 3 12 readdcld 
 |-  ( ph -> ( B + ( 1 / 2 ) ) e. RR )
22 reflcl 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
23 21 22 syl 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
24 23 recnd 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. CC )
25 12 recnd 
 |-  ( ph -> ( 1 / 2 ) e. CC )
26 24 25 subcld 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. CC )
27 20 26 subcld 
 |-  ( ph -> ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) e. CC )
28 2 12 readdcld 
 |-  ( ph -> ( A + ( 1 / 2 ) ) e. RR )
29 reflcl 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
30 28 29 syl 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
31 30 recnd 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC )
32 31 25 addcld 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) e. CC )
33 2 recnd 
 |-  ( ph -> A e. CC )
34 32 33 subcld 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) e. CC )
35 27 34 addcld 
 |-  ( ph -> ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) e. CC )
36 35 abscld 
 |-  ( ph -> ( abs ` ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) ) e. RR )
37 2 3 dnibndlem6 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) + ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) )
38 23 12 jca 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR /\ ( 1 / 2 ) e. RR ) )
39 resubcl 
 |-  ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR )
40 38 39 syl 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR )
41 3 40 jca 
 |-  ( ph -> ( B e. RR /\ ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR ) )
42 resubcl 
 |-  ( ( B e. RR /\ ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR ) -> ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) e. RR )
43 41 42 syl 
 |-  ( ph -> ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) e. RR )
44 30 12 readdcld 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) e. RR )
45 44 2 jca 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) e. RR /\ A e. RR ) )
46 resubcl 
 |-  ( ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) e. RR /\ A e. RR ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) e. RR )
47 45 46 syl 
 |-  ( ph -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) e. RR )
48 3 dnibndlem7 
 |-  ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )
49 2 dnibndlem8 
 |-  ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) <_ ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) )
50 15 18 43 47 48 49 le2addd 
 |-  ( ph -> ( ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) + ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) )
51 43 47 readdcld 
 |-  ( ph -> ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) e. RR )
52 dnibndlem4 
 |-  ( B e. RR -> 0 <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )
53 3 52 syl 
 |-  ( ph -> 0 <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )
54 0red 
 |-  ( ph -> 0 e. RR )
55 dnibndlem5 
 |-  ( A e. RR -> 0 < ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) )
56 2 55 syl 
 |-  ( ph -> 0 < ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) )
57 54 47 56 ltled 
 |-  ( ph -> 0 <_ ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) )
58 43 47 53 57 addge0d 
 |-  ( ph -> 0 <_ ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) )
59 51 58 absidd 
 |-  ( ph -> ( abs ` ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) ) = ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) )
60 59 eqcomd 
 |-  ( ph -> ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) = ( abs ` ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) ) )
61 50 60 breqtrd 
 |-  ( ph -> ( ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) + ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( abs ` ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) ) )
62 10 19 36 37 61 letrd 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( abs ` ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) ) )
63 1 2 3 4 dnibndlem3 
 |-  ( ph -> ( abs ` ( B - A ) ) = ( abs ` ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) ) )
64 63 eqcomd 
 |-  ( ph -> ( abs ` ( ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) + ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) ) = ( abs ` ( B - A ) ) )
65 62 64 breqtrd 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( abs ` ( B - A ) ) )
66 1 2 3 dnibndlem1 
 |-  ( ph -> ( ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) <-> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( abs ` ( B - A ) ) ) )
67 65 66 mpbird 
 |-  ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )