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 ∈ ℝ ⟼ x + 1 2 − x
dnizeq0.1 ⊢ φ → A ∈ ℤ
Assertion dnizeq0 ⊢ φ → T ⁡ A = 0

Proof

Step Hyp Ref Expression
1 dnizeq0.t ⊢ T = x ∈ ℝ ⟼ x + 1 2 − x
2 dnizeq0.1 ⊢ φ → A ∈ ℤ
3 2 zred ⊢ φ → A ∈ ℝ
4 1 dnival ⊢ A ∈ ℝ → T ⁡ A = A + 1 2 − A
5 3 4 syl ⊢ φ → T ⁡ A = A + 1 2 − A
6 halfre ⊢ 1 2 ∈ ℝ
7 6 a1i ⊢ φ → 1 2 ∈ ℝ
8 2 7 jca ⊢ φ → A ∈ ℤ ∧ 1 2 ∈ ℝ
9 flzadd ⊢ A ∈ ℤ ∧ 1 2 ∈ ℝ → A + 1 2 = A + 1 2
10 8 9 syl ⊢ φ → A + 1 2 = A + 1 2
11 6 rexri ⊢ 1 2 ∈ ℝ *
12 0re ⊢ 0 ∈ ℝ
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 ∈ ℝ * ∧ 0 ≤ 1 2 ∧ 1 2 < 1
17 0xr ⊢ 0 ∈ ℝ *
18 1xr ⊢ 1 ∈ ℝ *
19 17 18 pm3.2i ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ *
20 elico1 ⊢ 0 ∈ ℝ * ∧ 1 ∈ ℝ * → 1 2 ∈ 0 1 ↔ 1 2 ∈ ℝ * ∧ 0 ≤ 1 2 ∧ 1 2 < 1
21 19 20 ax-mp ⊢ 1 2 ∈ 0 1 ↔ 1 2 ∈ ℝ * ∧ 0 ≤ 1 2 ∧ 1 2 < 1
22 16 21 mpbir ⊢ 1 2 ∈ 0 1
23 22 a1i ⊢ φ → 1 2 ∈ 0 1
24 ico01fl0 ⊢ 1 2 ∈ 0 1 → 1 2 = 0
25 23 24 syl ⊢ φ → 1 2 = 0
26 25 oveq2d ⊢ φ → A + 1 2 = A + 0
27 3 recnd ⊢ φ → A ∈ ℂ
28 27 addridd ⊢ φ → A + 0 = A
29 26 28 eqtrd ⊢ φ → A + 1 2 = A
30 10 29 eqtrd ⊢ φ → A + 1 2 = A
31 30 oveq1d ⊢ φ → A + 1 2 − A = A − A
32 27 subidd ⊢ φ → A − A = 0
33 31 32 eqtrd ⊢ φ → A + 1 2 − A = 0
34 33 fveq2d ⊢ φ → A + 1 2 − A = 0
35 abs0 ⊢ 0 = 0
36 35 a1i ⊢ φ → 0 = 0
37 34 36 eqtrd ⊢ φ → A + 1 2 − A = 0
38 5 37 eqtrd ⊢ φ → T ⁡ A = 0