Metamath Proof Explorer

Theorem dnibndlem7

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

Ref Expression
Hypothesis dnibndlem7.1 
|- ( ph -> B e. RR )
Assertion dnibndlem7 
|- ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 dnibndlem7.1 
 |-  ( ph -> B e. RR )
2 halfre 
 |-  ( 1 / 2 ) e. RR
3 2 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
4 1 3 jca 
 |-  ( ph -> ( B e. RR /\ ( 1 / 2 ) e. RR ) )
5 readdcl 
 |-  ( ( B e. RR /\ ( 1 / 2 ) e. RR ) -> ( B + ( 1 / 2 ) ) e. RR )
6 4 5 syl 
 |-  ( ph -> ( B + ( 1 / 2 ) ) e. RR )
7 reflcl 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
8 6 7 syl 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
9 8 1 jca 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR /\ B e. RR ) )
10 resubcl 
 |-  ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR /\ B e. RR ) -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) e. RR )
11 9 10 syl 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) e. RR )
12 1 dnicld1 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR )
13 11 leabsd 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) <_ ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) )
14 11 12 3 13 lesub2dd 
 |-  ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) <_ ( ( 1 / 2 ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) )
15 3 recnd 
 |-  ( ph -> ( 1 / 2 ) e. CC )
16 8 recnd 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. CC )
17 1 recnd 
 |-  ( ph -> B e. CC )
18 15 16 17 subsub3d 
 |-  ( ph -> ( ( 1 / 2 ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) = ( ( ( 1 / 2 ) + B ) - ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
19 15 17 addcomd 
 |-  ( ph -> ( ( 1 / 2 ) + B ) = ( B + ( 1 / 2 ) ) )
20 19 oveq1d 
 |-  ( ph -> ( ( ( 1 / 2 ) + B ) - ( |_ ` ( B + ( 1 / 2 ) ) ) ) = ( ( B + ( 1 / 2 ) ) - ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
21 17 16 15 subsub3d 
 |-  ( ph -> ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) = ( ( B + ( 1 / 2 ) ) - ( |_ ` ( B + ( 1 / 2 ) ) ) ) )
22 21 eqcomd 
 |-  ( ph -> ( ( B + ( 1 / 2 ) ) - ( |_ ` ( B + ( 1 / 2 ) ) ) ) = ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )
23 18 20 22 3eqtrd 
 |-  ( ph -> ( ( 1 / 2 ) - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) = ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )
24 14 23 breqtrd 
 |-  ( ph -> ( ( 1 / 2 ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )