Metamath Proof Explorer

Theorem dnibndlem8

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

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

Proof

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