Metamath Proof Explorer

Theorem dnibndlem5

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

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

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A e. RR -> A e. RR )
2 halfre 
 |-  ( 1 / 2 ) e. RR
3 2 a1i 
 |-  ( A e. RR -> ( 1 / 2 ) e. RR )
4 readdcl 
 |-  ( ( A e. RR /\ ( 1 / 2 ) e. RR ) -> ( A + ( 1 / 2 ) ) e. RR )
5 1 3 4 syl2anc2 
 |-  ( A e. RR -> ( A + ( 1 / 2 ) ) e. RR )
6 flltp1 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( A + ( 1 / 2 ) ) < ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
7 5 6 syl 
 |-  ( A e. RR -> ( A + ( 1 / 2 ) ) < ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) )
8 ax-1cn 
 |-  1 e. CC
9 2halves 
 |-  ( 1 e. CC -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
10 8 9 ax-mp 
 |-  ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1
11 10 eqcomi 
 |-  1 = ( ( 1 / 2 ) + ( 1 / 2 ) )
12 11 a1i 
 |-  ( A e. RR -> 1 = ( ( 1 / 2 ) + ( 1 / 2 ) ) )
13 12 oveq2d 
 |-  ( A e. RR -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
14 reflcl 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
15 5 14 syl 
 |-  ( A e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR )
16 15 recnd 
 |-  ( A e. RR -> ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC )
17 3 recnd 
 |-  ( A e. RR -> ( 1 / 2 ) e. CC )
18 16 17 17 3jca 
 |-  ( A e. RR -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC /\ ( 1 / 2 ) e. CC /\ ( 1 / 2 ) e. CC ) )
19 addass 
 |-  ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. CC /\ ( 1 / 2 ) e. CC /\ ( 1 / 2 ) e. CC ) -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
20 18 19 syl 
 |-  ( A e. RR -> ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
21 20 eqcomd 
 |-  ( A e. RR -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
22 13 21 eqtrd 
 |-  ( A e. RR -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + 1 ) = ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
23 7 22 breqtrd 
 |-  ( A e. RR -> ( A + ( 1 / 2 ) ) < ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
24 15 3 jca 
 |-  ( A e. RR -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR /\ ( 1 / 2 ) e. RR ) )
25 readdcl 
 |-  ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) e. RR /\ ( 1 / 2 ) e. RR ) -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) e. RR )
26 24 25 syl 
 |-  ( A e. RR -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) e. RR )
27 1 26 3 ltadd1d 
 |-  ( A e. RR -> ( A < ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) <-> ( A + ( 1 / 2 ) ) < ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) )
28 23 27 mpbird 
 |-  ( A e. RR -> A < ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) )
29 1 26 posdifd 
 |-  ( A e. RR -> ( A < ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) <-> 0 < ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) ) )
30 28 29 mpbid 
 |-  ( A e. RR -> 0 < ( ( ( |_ ` ( A + ( 1 / 2 ) ) ) + ( 1 / 2 ) ) - A ) )