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 ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
dnizphlfeqhlf.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
Assertion dnizphlfeqhlf ( 𝜑 → ( 𝑇 ‘ ( 𝐴 + ( 1 / 2 ) ) ) = ( 1 / 2 ) )

Proof

Step Hyp Ref Expression
1 dnizphlfeqhlf.t ⊢ 𝑇 = ( 𝑥 ∈ ℝ ↦ ( abs ‘ ( ( ⌊ ‘ ( 𝑥 + ( 1 / 2 ) ) ) − 𝑥 ) ) )
2 dnizphlfeqhlf.1 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
3 2 zred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
4 halfre ⊢ ( 1 / 2 ) ∈ ℝ
5 4 a1i ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℝ )
6 3 5 readdcld ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
7 1 dnival ⊢ ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( 𝑇 ‘ ( 𝐴 + ( 1 / 2 ) ) ) = ( abs ‘ ( ( ⌊ ‘ ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) − ( 𝐴 + ( 1 / 2 ) ) ) ) )
8 6 7 syl ⊢ ( 𝜑 → ( 𝑇 ‘ ( 𝐴 + ( 1 / 2 ) ) ) = ( abs ‘ ( ( ⌊ ‘ ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) − ( 𝐴 + ( 1 / 2 ) ) ) ) )
9 3 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
10 5 recnd ⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
11 9 10 addcld ⊢ ( 𝜑 → ( 𝐴 + ( 1 / 2 ) ) ∈ ℂ )
12 9 10 10 addassd ⊢ ( 𝜑 → ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( 𝐴 + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) )
13 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
14 13 2halvesd ⊢ ( 𝜑 → ( ( 1 / 2 ) + ( 1 / 2 ) ) = 1 )
15 14 oveq2d ⊢ ( 𝜑 → ( 𝐴 + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( 𝐴 + 1 ) )
16 12 15 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) = ( 𝐴 + 1 ) )
17 2 peano2zd ⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℤ )
18 16 17 eqeltrd ⊢ ( 𝜑 → ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) ∈ ℤ )
19 flid ⊢ ( ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) ∈ ℤ → ( ⌊ ‘ ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) = ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
20 18 19 syl ⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) = ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) )
21 11 10 20 mvrladdd ⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) − ( 𝐴 + ( 1 / 2 ) ) ) = ( 1 / 2 ) )
22 21 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( ⌊ ‘ ( ( 𝐴 + ( 1 / 2 ) ) + ( 1 / 2 ) ) ) − ( 𝐴 + ( 1 / 2 ) ) ) ) = ( abs ‘ ( 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 ⊢ ( 𝜑 → ( abs ‘ ( 1 / 2 ) ) = ( 1 / 2 ) )
29 8 22 28 3eqtrd ⊢ ( 𝜑 → ( 𝑇 ‘ ( 𝐴 + ( 1 / 2 ) ) ) = ( 1 / 2 ) )