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 ( 𝐴 ∈ ℝ → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ≤ ( 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 ( ( 𝐴 − ( 1 / 2 ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( ( 𝐴 − ( 1 / 2 ) ) + 1 )
8 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
9 1 a1i ( 𝐴 ∈ ℝ → ( 1 / 2 ) ∈ ℂ )
10 8 9 9 nppcan3d ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( 1 / 2 ) ) + ( ( 1 / 2 ) + ( 1 / 2 ) ) ) = ( 𝐴 + ( 1 / 2 ) ) )
11 7 10 eqtr3id ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( 1 / 2 ) ) + 1 ) = ( 𝐴 + ( 1 / 2 ) ) )
12 halfre ( 1 / 2 ) ∈ ℝ
13 readdcl ( ( 𝐴 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
14 12 13 mpan2 ( 𝐴 ∈ ℝ → ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ )
15 fllep1 ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( 𝐴 + ( 1 / 2 ) ) ≤ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
16 14 15 syl ( 𝐴 ∈ ℝ → ( 𝐴 + ( 1 / 2 ) ) ≤ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
17 11 16 eqbrtrd ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( 1 / 2 ) ) + 1 ) ≤ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) )
18 resubcl ( ( 𝐴 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( 𝐴 − ( 1 / 2 ) ) ∈ ℝ )
19 12 18 mpan2 ( 𝐴 ∈ ℝ → ( 𝐴 − ( 1 / 2 ) ) ∈ ℝ )
20 reflcl ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
21 14 20 syl ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ )
22 1red ( 𝐴 ∈ ℝ → 1 ∈ ℝ )
23 19 21 22 leadd1d ( 𝐴 ∈ ℝ → ( ( 𝐴 − ( 1 / 2 ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ↔ ( ( 𝐴 − ( 1 / 2 ) ) + 1 ) ≤ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) + 1 ) ) )
24 17 23 mpbird ( 𝐴 ∈ ℝ → ( 𝐴 − ( 1 / 2 ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) )
25 flle ( ( 𝐴 + ( 1 / 2 ) ) ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( 𝐴 + ( 1 / 2 ) ) )
26 14 25 syl ( 𝐴 ∈ ℝ → ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( 𝐴 + ( 1 / 2 ) ) )
27 id ( 𝐴 ∈ ℝ → 𝐴 ∈ ℝ )
28 12 a1i ( 𝐴 ∈ ℝ → ( 1 / 2 ) ∈ ℝ )
29 absdifle ( ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ≤ ( 1 / 2 ) ↔ ( ( 𝐴 − ( 1 / 2 ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∧ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( 𝐴 + ( 1 / 2 ) ) ) ) )
30 21 27 28 29 syl3anc ( 𝐴 ∈ ℝ → ( ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ≤ ( 1 / 2 ) ↔ ( ( 𝐴 − ( 1 / 2 ) ) ≤ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ∧ ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) ≤ ( 𝐴 + ( 1 / 2 ) ) ) ) )
31 24 26 30 mpbir2and ( 𝐴 ∈ ℝ → ( abs ‘ ( ( ⌊ ‘ ( 𝐴 + ( 1 / 2 ) ) ) − 𝐴 ) ) ≤ ( 1 / 2 ) )