Metamath Proof Explorer

Theorem dnibndlem12

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem12.1 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 dnibndlem12.2 
 |-  ( ph -> A e. RR )
3 dnibndlem12.3 
 |-  ( ph -> B e. RR )
4 dnibndlem12.4 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 2 ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )
5 3 dnicld1 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR )
6 2 dnicld1 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )
7 5 6 resubcld 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. RR )
8 7 recnd 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. CC )
9 8 abscld 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) e. RR )
10 1red 
 |-  ( ph -> 1 e. RR )
11 3 2 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
12 11 recnd 
 |-  ( ph -> ( B - A ) e. CC )
13 12 abscld 
 |-  ( ph -> ( abs ` ( B - A ) ) e. RR )
14 10 rehalfcld 
 |-  ( ph -> ( 1 / 2 ) e. RR )
15 2 3 dnibndlem11 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( 1 / 2 ) )
16 halflt1 
 |-  ( 1 / 2 ) < 1
17 halfre 
 |-  ( 1 / 2 ) e. RR
18 1re 
 |-  1 e. RR
19 17 18 pm3.2i 
 |-  ( ( 1 / 2 ) e. RR /\ 1 e. RR )
20 ltle 
 |-  ( ( ( 1 / 2 ) e. RR /\ 1 e. RR ) -> ( ( 1 / 2 ) < 1 -> ( 1 / 2 ) <_ 1 ) )
21 19 20 ax-mp 
 |-  ( ( 1 / 2 ) < 1 -> ( 1 / 2 ) <_ 1 )
22 16 21 ax-mp 
 |-  ( 1 / 2 ) <_ 1
23 22 a1i 
 |-  ( ph -> ( 1 / 2 ) <_ 1 )
24 9 14 10 15 23 letrd 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ 1 )
25 2 3 4 dnibndlem10 
 |-  ( ph -> 1 <_ ( B - A ) )
26 11 leabsd 
 |-  ( ph -> ( B - A ) <_ ( abs ` ( B - A ) ) )
27 10 11 13 25 26 letrd 
 |-  ( ph -> 1 <_ ( abs ` ( B - A ) ) )
28 9 10 13 24 27 letrd 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( abs ` ( B - A ) ) )
29 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 ) ) ) )
30 28 29 mpbird 
 |-  ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )