Metamath Proof Explorer

Theorem dnibndlem6

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

Ref Expression
Hypotheses dnibndlem6.1 
|- ( ph -> A e. RR )
dnibndlem6.2 
|- ( ph -> B e. RR )
Assertion 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dnibndlem6.1 
 |-  ( ph -> A e. RR )
2 dnibndlem6.2 
 |-  ( ph -> B e. RR )
3 2 dnicld1 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR )
4 3 recnd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. CC )
5 1 dnicld1 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )
6 5 recnd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. CC )
7 4 6 subcld 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. CC )
8 7 abscld 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) e. RR )
9 halfcn 
 |-  ( 1 / 2 ) e. CC
10 9 a1i 
 |-  ( ph -> ( 1 / 2 ) e. CC )
11 4 10 subcld 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( 1 / 2 ) ) e. CC )
12 11 abscld 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( 1 / 2 ) ) ) e. RR )
13 10 6 subcld 
 |-  ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. CC )
14 13 abscld 
 |-  ( ph -> ( abs ` ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) e. RR )
15 12 14 readdcld 
 |-  ( ph -> ( ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( 1 / 2 ) ) ) + ( abs ` ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) ) e. RR )
16 halfre 
 |-  ( 1 / 2 ) e. RR
17 16 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
18 17 3 jca 
 |-  ( ph -> ( ( 1 / 2 ) e. RR /\ ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR ) )
19 resubcl 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR ) -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) e. RR )
20 18 19 syl 
 |-  ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) e. RR )
21 17 5 jca 
 |-  ( ph -> ( ( 1 / 2 ) e. RR /\ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR ) )
22 resubcl 
 |-  ( ( ( 1 / 2 ) e. RR /\ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR ) -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. RR )
23 21 22 syl 
 |-  ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. RR )
24 20 23 readdcld 
 |-  ( ph -> ( ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) + ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) e. RR )
25 4 6 10 3jca 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. CC /\ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. CC /\ ( 1 / 2 ) e. CC ) )
26 abs3dif 
 |-  ( ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. CC /\ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. CC /\ ( 1 / 2 ) e. CC ) -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( 1 / 2 ) ) ) + ( abs ` ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) ) )
27 25 26 syl 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( 1 / 2 ) ) ) + ( abs ` ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) ) )
28 4 10 abssubd 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( 1 / 2 ) ) ) = ( abs ` ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) ) )
29 rddif2 
 |-  ( B e. RR -> 0 <_ ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) )
30 2 29 syl 
 |-  ( ph -> 0 <_ ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) )
31 20 30 absidd 
 |-  ( ph -> ( abs ` ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) ) = ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) )
32 28 31 eqtrd 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( 1 / 2 ) ) ) = ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) )
33 rddif2 
 |-  ( A e. RR -> 0 <_ ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) )
34 1 33 syl 
 |-  ( ph -> 0 <_ ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) )
35 23 34 absidd 
 |-  ( ph -> ( abs ` ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) = ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) )
36 32 35 oveq12d 
 |-  ( ph -> ( ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( 1 / 2 ) ) ) + ( abs ` ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) ) = ( ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) + ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) )
37 15 36 eqled 
 |-  ( ph -> ( ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( 1 / 2 ) ) ) + ( abs ` ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) ) <_ ( ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) + ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) )
38 8 15 24 27 37 letrd 
 |-  ( 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 ) ) ) ) )