dnibndlem8

		Ref	Expression
	Hypothesis	dnibndlem8.1	$⊢ φ \to A \in ℝ$
	Assertion	dnibndlem8	$⊢ φ \to (\frac{1}{2}) - \|⌊A + (\frac{1}{2})⌋ - A\| \leq ⌊A + (\frac{1}{2})⌋ + (\frac{1}{2}) - A$

Proof

Step	Hyp	Ref	Expression
1		dnibndlem8.1	$⊢ φ \to A \in ℝ$
2		halfre	$⊢ \frac{1}{2} \in ℝ$
3	2	a1i	$⊢ φ \to \frac{1}{2} \in ℝ$
4	1 3	jca	$⊢ φ \to (A \in ℝ \land \frac{1}{2} \in ℝ)$
5		simpl	$⊢ (A \in ℝ \land \frac{1}{2} \in ℝ) \to A \in ℝ$
6	2	a1i	$⊢ (A \in ℝ \land \frac{1}{2} \in ℝ) \to \frac{1}{2} \in ℝ$
7	5 6	readdcld	$⊢ (A \in ℝ \land \frac{1}{2} \in ℝ) \to A + (\frac{1}{2}) \in ℝ$
8	4 7	syl	$⊢ φ \to A + (\frac{1}{2}) \in ℝ$
9		reflcl	$⊢ A + (\frac{1}{2}) \in ℝ \to ⌊A + (\frac{1}{2})⌋ \in ℝ$
10	8 9	syl	$⊢ φ \to ⌊A + (\frac{1}{2})⌋ \in ℝ$
11	1 10	resubcld	$⊢ φ \to A - ⌊A + (\frac{1}{2})⌋ \in ℝ$
12	1	dnicld1	$⊢ φ \to \|⌊A + (\frac{1}{2})⌋ - A\| \in ℝ$
13	11	leabsd	$⊢ φ \to A - ⌊A + (\frac{1}{2})⌋ \leq \|A - ⌊A + (\frac{1}{2})⌋\|$
14	1	recnd	$⊢ φ \to A \in ℂ$
15	10	recnd	$⊢ φ \to ⌊A + (\frac{1}{2})⌋ \in ℂ$
16	14 15	abssubd	$⊢ φ \to \|A - ⌊A + (\frac{1}{2})⌋\| = \|⌊A + (\frac{1}{2})⌋ - A\|$
17	13 16	breqtrd	$⊢ φ \to A - ⌊A + (\frac{1}{2})⌋ \leq \|⌊A + (\frac{1}{2})⌋ - A\|$
18	11 12 3 17	lesub2dd	$⊢ φ \to (\frac{1}{2}) - \|⌊A + (\frac{1}{2})⌋ - A\| \leq (\frac{1}{2}) - (A - ⌊A + (\frac{1}{2})⌋)$
19	3	recnd	$⊢ φ \to \frac{1}{2} \in ℂ$
20	19 14 15	subsub3d	$⊢ φ \to (\frac{1}{2}) - (A - ⌊A + (\frac{1}{2})⌋) = (\frac{1}{2}) + ⌊A + (\frac{1}{2})⌋ - A$
21	19 15	addcomd	$⊢ φ \to (\frac{1}{2}) + ⌊A + (\frac{1}{2})⌋ = ⌊A + (\frac{1}{2})⌋ + (\frac{1}{2})$
22	21	oveq1d	$⊢ φ \to (\frac{1}{2}) + ⌊A + (\frac{1}{2})⌋ - A = ⌊A + (\frac{1}{2})⌋ + (\frac{1}{2}) - A$
23	20 22	eqtrd	$⊢ φ \to (\frac{1}{2}) - (A - ⌊A + (\frac{1}{2})⌋) = ⌊A + (\frac{1}{2})⌋ + (\frac{1}{2}) - A$
24	18 23	breqtrd	$⊢ φ \to (\frac{1}{2}) - \|⌊A + (\frac{1}{2})⌋ - A\| \leq ⌊A + (\frac{1}{2})⌋ + (\frac{1}{2}) - A$

Metamath Proof Explorer

Theorem dnibndlem8

Proof