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