Metamath Proof Explorer

Theorem dnizeq0

Description: The distance to nearest integer is zero for integers. (Contributed by Asger C. Ipsen, 15-Jun-2021)

Ref Expression
Hypotheses dnizeq0.t 
|- T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
dnizeq0.1 
|- ( ph -> A e. ZZ )
Assertion dnizeq0 
|- ( ph -> ( T ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 dnizeq0.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 dnizeq0.1 
 |-  ( ph -> A e. ZZ )
3 2 zred 
 |-  ( ph -> A e. RR )
4 1 dnival 
 |-  ( A e. RR -> ( T ` A ) = ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
5 3 4 syl 
 |-  ( ph -> ( T ` A ) = ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) )
6 halfre 
 |-  ( 1 / 2 ) e. RR
7 6 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
8 2 7 jca 
 |-  ( ph -> ( A e. ZZ /\ ( 1 / 2 ) e. RR ) )
9 flzadd 
 |-  ( ( A e. ZZ /\ ( 1 / 2 ) e. RR ) -> ( |_ ` ( A + ( 1 / 2 ) ) ) = ( A + ( |_ ` ( 1 / 2 ) ) ) )
10 8 9 syl 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) = ( A + ( |_ ` ( 1 / 2 ) ) ) )
11 6 rexri 
 |-  ( 1 / 2 ) e. RR*
12 0re 
 |-  0 e. RR
13 halfgt0 
 |-  0 < ( 1 / 2 )
14 12 6 13 ltleii 
 |-  0 <_ ( 1 / 2 )
15 halflt1 
 |-  ( 1 / 2 ) < 1
16 11 14 15 3pm3.2i 
 |-  ( ( 1 / 2 ) e. RR* /\ 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) < 1 )
17 0xr 
 |-  0 e. RR*
18 1xr 
 |-  1 e. RR*
19 17 18 pm3.2i 
 |-  ( 0 e. RR* /\ 1 e. RR* )
20 elico1 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( ( 1 / 2 ) e. ( 0 [,) 1 ) <-> ( ( 1 / 2 ) e. RR* /\ 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) < 1 ) ) )
21 19 20 ax-mp 
 |-  ( ( 1 / 2 ) e. ( 0 [,) 1 ) <-> ( ( 1 / 2 ) e. RR* /\ 0 <_ ( 1 / 2 ) /\ ( 1 / 2 ) < 1 ) )
22 16 21 mpbir 
 |-  ( 1 / 2 ) e. ( 0 [,) 1 )
23 22 a1i 
 |-  ( ph -> ( 1 / 2 ) e. ( 0 [,) 1 ) )
24 ico01fl0 
 |-  ( ( 1 / 2 ) e. ( 0 [,) 1 ) -> ( |_ ` ( 1 / 2 ) ) = 0 )
25 23 24 syl 
 |-  ( ph -> ( |_ ` ( 1 / 2 ) ) = 0 )
26 25 oveq2d 
 |-  ( ph -> ( A + ( |_ ` ( 1 / 2 ) ) ) = ( A + 0 ) )
27 3 recnd 
 |-  ( ph -> A e. CC )
28 27 addridd 
 |-  ( ph -> ( A + 0 ) = A )
29 26 28 eqtrd 
 |-  ( ph -> ( A + ( |_ ` ( 1 / 2 ) ) ) = A )
30 10 29 eqtrd 
 |-  ( ph -> ( |_ ` ( A + ( 1 / 2 ) ) ) = A )
31 30 oveq1d 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) = ( A - A ) )
32 27 subidd 
 |-  ( ph -> ( A - A ) = 0 )
33 31 32 eqtrd 
 |-  ( ph -> ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) = 0 )
34 33 fveq2d 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) = ( abs ` 0 ) )
35 abs0 
 |-  ( abs ` 0 ) = 0
36 35 a1i 
 |-  ( ph -> ( abs ` 0 ) = 0 )
37 34 36 eqtrd 
 |-  ( ph -> ( abs ` ( ( |_ ` ( A + ( 1 / 2 ) ) ) - A ) ) = 0 )
38 5 37 eqtrd 
 |-  ( ph -> ( T ` A ) = 0 )