Metamath Proof Explorer

Theorem dnibndlem4

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

Ref Expression
Assertion dnibndlem4 
|- ( B e. RR -> 0 <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( B e. RR -> B e. RR )
2 halfre 
 |-  ( 1 / 2 ) e. RR
3 2 a1i 
 |-  ( B e. RR -> ( 1 / 2 ) e. RR )
4 1 3 readdcld 
 |-  ( B e. RR -> ( B + ( 1 / 2 ) ) e. RR )
5 flle 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( B + ( 1 / 2 ) ) )
6 4 5 syl 
 |-  ( B e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( B + ( 1 / 2 ) ) )
7 reflcl 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
8 4 7 syl 
 |-  ( B e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
9 8 3 1 lesubaddd 
 |-  ( B e. RR -> ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) <_ B <-> ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( B + ( 1 / 2 ) ) ) )
10 6 9 mpbird 
 |-  ( B e. RR -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) <_ B )
11 8 3 jca 
 |-  ( B e. RR -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR /\ ( 1 / 2 ) e. RR ) )
12 resubcl 
 |-  ( ( ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR )
13 11 12 syl 
 |-  ( B e. RR -> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) e. RR )
14 1 13 subge0d 
 |-  ( B e. RR -> ( 0 <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) <-> ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) <_ B ) )
15 10 14 mpbird 
 |-  ( B e. RR -> 0 <_ ( B - ( ( |_ ` ( B + ( 1 / 2 ) ) ) - ( 1 / 2 ) ) ) )