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