Metamath Proof Explorer

Theorem dnibndlem2

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem2.1 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 dnibndlem2.2 
 |-  ( ph -> A e. RR )
3 dnibndlem2.3 
 |-  ( ph -> B e. RR )
4 dnibndlem2.4 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) = ( |_ ` ( A + ( 1 / 2 ) ) ) )
5 halfre 
 |-  ( 1 / 2 ) e. RR
6 5 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
7 3 6 jca 
 |-  ( ph -> ( B e. RR /\ ( 1 / 2 ) e. RR ) )
8 readdcl 
 |-  ( ( B e. RR /\ ( 1 / 2 ) e. RR ) -> ( B + ( 1 / 2 ) ) e. RR )
9 7 8 syl 
 |-  ( ph -> ( B + ( 1 / 2 ) ) e. RR )
10 reflcl 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
11 9 10 syl 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
12 11 recnd 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. CC )
13 3 recnd 
 |-  ( ph -> B e. CC )
14 12 13 subcld 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) e. CC )
15 14 abscld 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR )
16 15 recnd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. CC )
17 4 12 eqeltrrd 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC )
18 2 recnd 
 |-  ( ph -> A e. CC )
19 17 18 subcld 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) e. CC )
20 19 abscld 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )
21 20 recnd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. CC )
22 16 21 subcld 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. CC )
23 22 abscld 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) e. RR )
24 14 19 subcld 
 |-  ( ph -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. CC )
25 24 abscld 
 |-  ( ph -> ( abs ` ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. RR )
26 13 18 subcld 
 |-  ( ph -> ( B - A ) e. CC )
27 26 abscld 
 |-  ( ph -> ( abs ` ( B - A ) ) e. RR )
28 14 19 abs2difabsd 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( abs ` ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) )
29 12 18 13 nnncan1d 
 |-  ( ph -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - A ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) = ( B - A ) )
30 29 eqcomd 
 |-  ( ph -> ( B - A ) = ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - A ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) )
31 30 fveq2d 
 |-  ( ph -> ( abs ` ( B - A ) ) = ( abs ` ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - A ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) )
32 4 oveq1d 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - A ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) )
33 32 oveq1d 
 |-  ( ph -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - A ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) = ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) )
34 33 fveq2d 
 |-  ( ph -> ( abs ` ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - A ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) = ( abs ` ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) )
35 19 14 abssubd 
 |-  ( ph -> ( abs ` ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) = ( abs ` ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) )
36 31 34 35 3eqtrd 
 |-  ( ph -> ( abs ` ( B - A ) ) = ( abs ` ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) )
37 27 leidd 
 |-  ( ph -> ( abs ` ( B - A ) ) <_ ( abs ` ( B - A ) ) )
38 36 37 eqbrtrrd 
 |-  ( ph -> ( abs ` ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) - ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) <_ ( abs ` ( B - A ) ) )
39 23 25 27 28 38 letrd 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( abs ` ( B - A ) ) )
40 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 ) ) ) )
41 39 40 mpbird 
 |-  ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )