Metamath Proof Explorer

Theorem absrdbnd

Description: Bound on the absolute value of a real number rounded to the nearest integer. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 14-Sep-2015)

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

Proof

Step Hyp Ref Expression
1 halfre ⊢ 1 2 ∈ ℝ
2 readdcl ⊢ A ∈ ℝ ∧ 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
3 1 2 mpan2 ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ
4 reflcl ⊢ A + 1 2 ∈ ℝ → A + 1 2 ∈ ℝ
5 3 4 syl ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ
6 5 recnd ⊢ A ∈ ℝ → A + 1 2 ∈ ℂ
7 abscl ⊢ A + 1 2 ∈ ℂ → A + 1 2 ∈ ℝ
8 6 7 syl ⊢ A ∈ ℝ → A + 1 2 ∈ ℝ
9 recn ⊢ A ∈ ℝ → A ∈ ℂ
10 abscl ⊢ A ∈ ℂ → A ∈ ℝ
11 9 10 syl ⊢ A ∈ ℝ → A ∈ ℝ
12 1re ⊢ 1 ∈ ℝ
13 12 a1i ⊢ A ∈ ℝ → 1 ∈ ℝ
14 8 11 resubcld ⊢ A ∈ ℝ → A + 1 2 − A ∈ ℝ
15 resubcl ⊢ A + 1 2 ∈ ℝ ∧ A ∈ ℝ → A + 1 2 − A ∈ ℝ
16 5 15 mpancom ⊢ A ∈ ℝ → A + 1 2 − A ∈ ℝ
17 16 recnd ⊢ A ∈ ℝ → A + 1 2 − A ∈ ℂ
18 abscl ⊢ A + 1 2 − A ∈ ℂ → A + 1 2 − A ∈ ℝ
19 17 18 syl ⊢ A ∈ ℝ → A + 1 2 − A ∈ ℝ
20 abs2dif ⊢ A + 1 2 ∈ ℂ ∧ A ∈ ℂ → A + 1 2 − A ≤ A + 1 2 − A
21 6 9 20 syl2anc ⊢ A ∈ ℝ → A + 1 2 − A ≤ A + 1 2 − A
22 1 a1i ⊢ A ∈ ℝ → 1 2 ∈ ℝ
23 rddif ⊢ A ∈ ℝ → A + 1 2 − A ≤ 1 2
24 halflt1 ⊢ 1 2 < 1
25 1 12 24 ltleii ⊢ 1 2 ≤ 1
26 25 a1i ⊢ A ∈ ℝ → 1 2 ≤ 1
27 19 22 13 23 26 letrd ⊢ A ∈ ℝ → A + 1 2 − A ≤ 1
28 14 19 13 21 27 letrd ⊢ A ∈ ℝ → A + 1 2 − A ≤ 1
29 8 11 13 28 subled ⊢ A ∈ ℝ → A + 1 2 − 1 ≤ A
30 3 flcld ⊢ A ∈ ℝ → A + 1 2 ∈ ℤ
31 nn0abscl ⊢ A + 1 2 ∈ ℤ → A + 1 2 ∈ ℕ 0
32 30 31 syl ⊢ A ∈ ℝ → A + 1 2 ∈ ℕ 0
33 32 nn0zd ⊢ A ∈ ℝ → A + 1 2 ∈ ℤ
34 peano2zm ⊢ A + 1 2 ∈ ℤ → A + 1 2 − 1 ∈ ℤ
35 33 34 syl ⊢ A ∈ ℝ → A + 1 2 − 1 ∈ ℤ
36 flge ⊢ A ∈ ℝ ∧ A + 1 2 − 1 ∈ ℤ → A + 1 2 − 1 ≤ A ↔ A + 1 2 − 1 ≤ A
37 11 35 36 syl2anc ⊢ A ∈ ℝ → A + 1 2 − 1 ≤ A ↔ A + 1 2 − 1 ≤ A
38 29 37 mpbid ⊢ A ∈ ℝ → A + 1 2 − 1 ≤ A
39 reflcl ⊢ A ∈ ℝ → A ∈ ℝ
40 11 39 syl ⊢ A ∈ ℝ → A ∈ ℝ
41 8 13 40 lesubaddd ⊢ A ∈ ℝ → A + 1 2 − 1 ≤ A ↔ A + 1 2 ≤ A + 1
42 38 41 mpbid ⊢ A ∈ ℝ → A + 1 2 ≤ A + 1