Metamath Proof Explorer

Theorem dnizphlfeqhlf

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

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

Proof

Step Hyp Ref Expression
1 dnizphlfeqhlf.t 
 |-  T = ( x e. RR |-> ( abs ` ( ( |_ ` ( x + ( 1 / 2 ) ) ) - x ) ) )
2 dnizphlfeqhlf.1 
 |-  ( ph -> A e. ZZ )
3 2 zred 
 |-  ( ph -> A e. RR )
4 halfre 
 |-  ( 1 / 2 ) e. RR
5 4 a1i 
 |-  ( ph -> ( 1 / 2 ) e. RR )
6 3 5 readdcld 
 |-  ( ph -> ( A + ( 1 / 2 ) ) e. RR )
7 1 dnival 
 |-  ( ( A + ( 1 / 2 ) ) e. RR -> ( T ` ( A + ( 1 / 2 ) ) ) = ( abs ` ( ( |_ ` ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) - ( A + ( 1 / 2 ) ) ) ) )
8 6 7 syl 
 |-  ( ph -> ( T ` ( A + ( 1 / 2 ) ) ) = ( abs ` ( ( |_ ` ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) - ( A + ( 1 / 2 ) ) ) ) )
9 3 recnd 
 |-  ( ph -> A e. CC )
10 5 recnd 
 |-  ( ph -> ( 1 / 2 ) e. CC )
11 9 10 addcld 
 |-  ( ph -> ( A + ( 1 / 2 ) ) e. CC )
12 9 10 10 addassd 
 |-  ( ph -> ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( A + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
13 1cnd 
 |-  ( ph -> 1 e. CC )
14 13 2halvesd 
 |-  ( ph -> ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
15 14 oveq2d 
 |-  ( ph -> ( A + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( A + 1 ) )
16 12 15 eqtrd 
 |-  ( ph -> ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( A + 1 ) )
17 2 peano2zd 
 |-  ( ph -> ( A + 1 ) e. ZZ )
18 16 17 eqeltrd 
 |-  ( ph -> ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) e. ZZ )
19 flid 
 |-  ( ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) e. ZZ -> ( |_ ` ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) = ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
20 18 19 syl 
 |-  ( ph -> ( |_ ` ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) = ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
21 11 10 20 mvrladdd 
 |-  ( ph -> ( ( |_ ` ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) - ( A + ( 1 / 2 ) ) ) = ( 1 / 2 ) )
22 21 fveq2d 
 |-  ( ph -> ( abs ` ( ( |_ ` ( ( A + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) - ( A + ( 1 / 2 ) ) ) ) = ( abs ` ( 1 / 2 ) ) )
23 halfgt0 
 |-  0 < ( 1 / 2 )
24 0re 
 |-  0 e. RR
25 24 4 ltlei 
 |-  ( 0 < ( 1 / 2 ) -> 0 <_ ( 1 / 2 ) )
26 23 25 ax-mp 
 |-  0 <_ ( 1 / 2 )
27 26 a1i 
 |-  ( ph -> 0 <_ ( 1 / 2 ) )
28 5 27 absidd 
 |-  ( ph -> ( abs ` ( 1 / 2 ) ) = ( 1 / 2 ) )
29 8 22 28 3eqtrd 
 |-  ( ph -> ( T ` ( A + ( 1 / 2 ) ) ) = ( 1 / 2 ) )