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 2thalfe1 ⊢ 2 ⁢ 1 2 = 1
4 2 3 eqtr3i ⊢ 1 2 + 1 2 = 1
5 4 oveq2i ⊢ A − 1 2 + 1 2 + 1 2 = A - 1 2 + 1
6 recn ⊢ A ∈ ℝ → A ∈ ℂ
7 1 a1i ⊢ A ∈ ℝ → 1 2 ∈ ℂ
8 6 7 7 nppcan3d ⊢ A ∈ ℝ → A − 1 2 + 1 2 + 1 2 = A + 1 2
9 5 8 eqtr3id ⊢ A ∈ ℝ → A - 1 2 + 1 = A + 1 2
10 halfre ⊢ 1 2 ∈ ℝ
11 readdcl ⊢ A ∈ ℝ ∧ 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
12 10 11 mpan2 ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ
13 fllep1 ⊢ A + 1 2 ∈ ℝ → A + 1 2 ≤ A + 1 2 + 1
14 12 13 syl ⊢ A ∈ ℝ → A + 1 2 ≤ A + 1 2 + 1
15 9 14 eqbrtrd ⊢ A ∈ ℝ → A - 1 2 + 1 ≤ A + 1 2 + 1
16 resubcl ⊢ A ∈ ℝ ∧ 1 2 ∈ ℝ → A − 1 2 ∈ ℝ
17 10 16 mpan2 ⊢ A ∈ ℝ → A − 1 2 ∈ ℝ
18 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
19 12 18 syl ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ
20 1red ⊢ A ∈ ℝ → 1 ∈ ℝ
21 17 19 20 leadd1d ⊢ A ∈ ℝ → A − 1 2 ≤ A + 1 2 ↔ A - 1 2 + 1 ≤ A + 1 2 + 1
22 15 21 mpbird ⊢ A ∈ ℝ → A − 1 2 ≤ A + 1 2
23 flle ⊢ A + 1 2 ∈ ℝ → A + 1 2 ≤ A + 1 2
24 12 23 syl ⊢ A ∈ ℝ → A + 1 2 ≤ A + 1 2
25 id ⊢ A ∈ ℝ → A ∈ ℝ
26 10 a1i ⊢ A ∈ ℝ → 1 2 ∈ ℝ
27 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
28 19 25 26 27 syl3anc ⊢ A ∈ ℝ → A + 1 2 − A ≤ 1 2 ↔ A − 1 2 ≤ A + 1 2 ∧ A + 1 2 ≤ A + 1 2
29 22 24 28 mpbir2and ⊢ A ∈ ℝ → A + 1 2 − A ≤ 1 2