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 addid1d
 |-  ( 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 )