Metamath Proof Explorer

Theorem rddif

Description: The difference between a real number and its nearest integer is less than or equal to one half. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Sep-2015)

Ref Expression
Assertion rddif ⊢ A ∈ ℝ → A + 1 2 − A ≤ 1 2

Proof

Step Hyp Ref Expression
1 halfcn ⊢ 1 2 ∈ ℂ
2 1 2timesi ⊢ 2 ⁢ 1 2 = 1 2 + 1 2
3 2cn ⊢ 2 ∈ ℂ
4 2ne0 ⊢ 2 ≠ 0
5 3 4 recidi ⊢ 2 ⁢ 1 2 = 1
6 2 5 eqtr3i ⊢ 1 2 + 1 2 = 1
7 6 oveq2i ⊢ A − 1 2 + 1 2 + 1 2 = A - 1 2 + 1
8 recn ⊢ A ∈ ℝ → A ∈ ℂ
9 1 a1i ⊢ A ∈ ℝ → 1 2 ∈ ℂ
10 8 9 9 nppcan3d ⊢ A ∈ ℝ → A − 1 2 + 1 2 + 1 2 = A + 1 2
11 7 10 eqtr3id ⊢ A ∈ ℝ → A - 1 2 + 1 = A + 1 2
12 halfre ⊢ 1 2 ∈ ℝ
13 readdcl ⊢ A ∈ ℝ ∧ 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
14 12 13 mpan2 ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ
15 fllep1 ⊢ A + 1 2 ∈ ℝ → A + 1 2 ≤ A + 1 2 + 1
16 14 15 syl ⊢ A ∈ ℝ → A + 1 2 ≤ A + 1 2 + 1
17 11 16 eqbrtrd ⊢ A ∈ ℝ → A - 1 2 + 1 ≤ A + 1 2 + 1
18 resubcl ⊢ A ∈ ℝ ∧ 1 2 ∈ ℝ → A − 1 2 ∈ ℝ
19 12 18 mpan2 ⊢ A ∈ ℝ → A − 1 2 ∈ ℝ
20 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
21 14 20 syl ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ
22 1red ⊢ A ∈ ℝ → 1 ∈ ℝ
23 19 21 22 leadd1d ⊢ A ∈ ℝ → A − 1 2 ≤ A + 1 2 ↔ A - 1 2 + 1 ≤ A + 1 2 + 1
24 17 23 mpbird ⊢ A ∈ ℝ → A − 1 2 ≤ A + 1 2
25 flle ⊢ A + 1 2 ∈ ℝ → A + 1 2 ≤ A + 1 2
26 14 25 syl ⊢ A ∈ ℝ → A + 1 2 ≤ A + 1 2
27 id ⊢ A ∈ ℝ → A ∈ ℝ
28 12 a1i ⊢ A ∈ ℝ → 1 2 ∈ ℝ
29 absdifle ⊢ A + 1 2 ∈ ℝ ∧ A ∈ ℝ ∧ 1 2 ∈ ℝ → A + 1 2 − A ≤ 1 2 ↔ A − 1 2 ≤ A + 1 2 ∧ A + 1 2 ≤ A + 1 2
30 21 27 28 29 syl3anc ⊢ A ∈ ℝ → A + 1 2 − A ≤ 1 2 ↔ A − 1 2 ≤ A + 1 2 ∧ A + 1 2 ≤ A + 1 2
31 24 26 30 mpbir2and ⊢ A ∈ ℝ → A + 1 2 − A ≤ 1 2