Metamath Proof Explorer

Theorem dnibndlem11

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

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

Proof

Step Hyp Ref Expression
1 dnibndlem11.1 
 |-  ( ph -> A e. RR )
2 dnibndlem11.2 
 |-  ( ph -> B e. RR )
3 2 dnicld1 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. RR )
4 1 dnicld1 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. RR )
5 3 4 resubcld 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) e. RR )
6 halfre 
 |-  ( 1 / 2 ) e. RR
7 6 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
8 3 recnd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) e. CC )
9 4 recnd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) e. CC )
10 8 9 negsubdi2d 
 |-  ( ph -> -u ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) = ( ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) )
11 4 3 resubcld 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) e. RR )
12 2 7 readdcld 
 |-  ( ph -> ( B + ( 1 / 2 ) ) e. RR )
13 reflcl 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
14 12 13 syl 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
15 14 recnd 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. CC )
16 2 recnd 
 |-  ( ph -> B e. CC )
17 15 16 subcld 
 |-  ( ph -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) e. CC )
18 17 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) )
19 4 3 subge02d 
 |-  ( ph -> ( 0 <_ ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) <-> ( ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) <_ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) )
20 18 19 mpbid 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) <_ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
21 rddif 
 |-  ( A e. RR -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ ( 1 / 2 ) )
22 1 21 syl 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <_ ( 1 / 2 ) )
23 11 4 7 20 22 letrd 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) - ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) <_ ( 1 / 2 ) )
24 10 23 eqbrtrd 
 |-  ( ph -> -u ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) <_ ( 1 / 2 ) )
25 5 7 24 lenegcon1d 
 |-  ( ph -> -u ( 1 / 2 ) <_ ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) )
26 1 7 readdcld 
 |-  ( ph -> ( A + ( 1 / 2 ) ) e. RR )
27 reflcl 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
28 26 27 syl 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
29 28 recnd 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC )
30 1 recnd 
 |-  ( ph -> A e. CC )
31 29 30 subcld 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) e. CC )
32 31 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
33 3 4 subge02d 
 |-  ( ph -> ( 0 <_ ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) <-> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) <_ ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) ) )
34 32 33 mpbid 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) <_ ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) )
35 rddif 
 |-  ( B e. RR -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) <_ ( 1 / 2 ) )
36 2 35 syl 
 |-  ( ph -> ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) <_ ( 1 / 2 ) )
37 5 3 7 34 36 letrd 
 |-  ( ph -> ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) <_ ( 1 / 2 ) )
38 25 37 jca 
 |-  ( ph -> ( -u ( 1 / 2 ) <_ ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) /\ ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) <_ ( 1 / 2 ) ) )
39 5 7 absled 
 |-  ( ph -> ( ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( 1 / 2 ) <-> ( -u ( 1 / 2 ) <_ ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) /\ ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) <_ ( 1 / 2 ) ) ) )
40 38 39 mpbird 
 |-  ( ph -> ( abs ` ( ( abs ` ( ( |_ ` ( B + ( 1 / 2 ) ) ) - B ) ) - ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) ) ) <_ ( 1 / 2 ) )