Metamath Proof Explorer

Theorem dnicn

Description: The "distance to nearest integer" function is continuous. (Contributed by Asger C. Ipsen, 4-Apr-2021)

Ref Expression
Hypothesis dnicn.1 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
Assertion dnicn 
|- T e. ( RR -cn-> RR )

Proof

Step Hyp Ref Expression
1 dnicn.1 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 1 dnif 
 |-  T : RR --> RR
3 simpr 
 |-  ( ( y e. RR /\ e e. RR+ ) -> e e. RR+ )
4 simplr 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> z e. RR )
5 1 4 dnicld2 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( T ` z ) e. RR )
6 simplll 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> y e. RR )
7 1 6 dnicld2 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( T ` y ) e. RR )
8 5 7 resubcld 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( ( T ` z ) - ( T ` y ) ) e. RR )
9 8 recnd 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( ( T ` z ) - ( T ` y ) ) e. CC )
10 9 abscld 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) e. RR )
11 4 6 resubcld 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( z - y ) e. RR )
12 11 recnd 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( z - y ) e. CC )
13 12 abscld 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( abs ` ( z - y ) ) e. RR )
14 3 ad2antrr 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> e e. RR+ )
15 14 rpred 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> e e. RR )
16 1 6 4 dnibnd 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) <_ ( abs ` ( z - y ) ) )
17 simpr 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( abs ` ( z - y ) ) < e )
18 10 13 15 16 17 lelttrd 
 |-  ( ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) /\ ( abs ` ( z - y ) ) < e ) -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) < e )
19 18 ex 
 |-  ( ( ( y e. RR /\ e e. RR+ ) /\ z e. RR ) -> ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) < e ) )
20 19 ralrimiva 
 |-  ( ( y e. RR /\ e e. RR+ ) -> A. z e. RR ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) < e ) )
21 breq2 
 |-  ( d = e -> ( ( abs ` ( z - y ) ) < d <-> ( abs ` ( z - y ) ) < e ) )
22 21 rspceaimv 
 |-  ( ( e e. RR+ /\ A. z e. RR ( ( abs ` ( z - y ) ) < e -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) < e ) ) -> E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) < e ) )
23 3 20 22 syl2anc 
 |-  ( ( y e. RR /\ e e. RR+ ) -> E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) < e ) )
24 23 rgen2 
 |-  A. y e. RR A. e e. RR+ E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) < e )
25 ax-resscn 
 |-  RR C_ CC
26 elcncf2 
 |-  ( ( RR C_ CC /\ RR C_ CC ) -> ( T e. ( RR -cn-> RR ) <-> ( T : RR --> RR /\ A. y e. RR A. e e. RR+ E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) < e ) ) ) )
27 25 25 26 mp2an 
 |-  ( T e. ( RR -cn-> RR ) <-> ( T : RR --> RR /\ A. y e. RR A. e e. RR+ E. d e. RR+ A. z e. RR ( ( abs ` ( z - y ) ) < d -> ( abs ` ( ( T ` z ) - ( T ` y ) ) ) < e ) ) )
28 2 24 27 mpbir2an 
 |-  T e. ( RR -cn-> RR )