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 x + 1 2 x
dnizphlfeqhlf.1 φ A
Assertion dnizphlfeqhlf φ T A + 1 2 = 1 2

Proof

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