Metamath Proof Explorer

Theorem dnibnd

Description: The "distance to nearest integer" function is 1-Lipschitz continuous, i.e., is a short map. (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypotheses dnibnd.1 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
dnibnd.2 
|- ( ph -> A e. RR )
dnibnd.3 
|- ( ph -> B e. RR )
Assertion dnibnd 
|- ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )

Proof

Step Hyp Ref Expression
1 dnibnd.1 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 dnibnd.2 
 |-  ( ph -> A e. RR )
3 dnibnd.3 
 |-  ( ph -> B e. RR )
4 2 adantr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> A e. RR )
5 3 adantr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> B e. RR )
6 simpr 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) )
7 1 4 5 6 dnibndlem13 
 |-  ( ( ph /\ ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) ) -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
8 1 3 dnicld2 
 |-  ( ph -> ( T ` B ) e. RR )
9 8 recnd 
 |-  ( ph -> ( T ` B ) e. CC )
10 1 2 dnicld2 
 |-  ( ph -> ( T ` A ) e. RR )
11 10 recnd 
 |-  ( ph -> ( T ` A ) e. CC )
12 9 11 abssubd 
 |-  ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) = ( abs ` ( ( T ` A ) - ( T ` B ) ) ) )
13 12 adantr 
 |-  ( ( ph /\ ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) ) -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) = ( abs ` ( ( T ` A ) - ( T ` B ) ) ) )
14 3 adantr 
 |-  ( ( ph /\ ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) ) -> B e. RR )
15 2 adantr 
 |-  ( ( ph /\ ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) ) -> A e. RR )
16 simpr 
 |-  ( ( ph /\ ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) ) -> ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) )
17 1 14 15 16 dnibndlem13 
 |-  ( ( ph /\ ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) ) -> ( abs ` ( ( T ` A ) - ( T ` B ) ) ) <_ ( abs ` ( A - B ) ) )
18 2 recnd 
 |-  ( ph -> A e. CC )
19 3 recnd 
 |-  ( ph -> B e. CC )
20 18 19 abssubd 
 |-  ( ph -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
21 20 adantr 
 |-  ( ( ph /\ ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) ) -> ( abs ` ( A - B ) ) = ( abs ` ( B - A ) ) )
22 17 21 breqtrd 
 |-  ( ( ph /\ ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) ) -> ( abs ` ( ( T ` A ) - ( T ` B ) ) ) <_ ( abs ` ( B - A ) ) )
23 13 22 eqbrtrd 
 |-  ( ( ph /\ ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) ) -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )
24 halfre 
 |-  ( 1 / 2 ) e. RR
25 24 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
26 2 25 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 3 25 readdcld 
 |-  ( ph -> ( B + ( 1 / 2 ) ) e. RR )
30 reflcl 
 |-  ( ( B + ( 1 / 2 ) ) e. RR -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
31 29 30 syl 
 |-  ( ph -> ( |_ ` ( B + ( 1 / 2 ) ) ) e. RR )
32 28 31 letrid 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) <_ ( |_ ` ( B + ( 1 / 2 ) ) ) \/ ( |_ ` ( B + ( 1 / 2 ) ) ) <_ ( |_ ` ( A + ( 1 / 2 ) ) ) ) )
33 7 23 32 mpjaodan 
 |-  ( ph -> ( abs ` ( ( T ` B ) - ( T ` A ) ) ) <_ ( abs ` ( B - A ) ) )