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 ) )