Theorem dnibndlem5

Description: Lemma for dnibnd . (Contributed by Asger C. Ipsen, 4-Apr-2021)

	Ref	Expression
Assertion	dnibndlem5	$$⊢A\in ℝ\to 0<⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)-A$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\in ℝ\to A\in ℝ$$
2		halfre	$$⊢\frac{1}{2}\in ℝ$$
3	2	a1i	$$⊢A\in ℝ\to \frac{1}{2}\in ℝ$$
4		readdcl	$$⊢\left(A\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to A+\left(\frac{1}{2}\right)\in ℝ$$
5	1 3 4	syl2anc2	$$⊢A\in ℝ\to A+\left(\frac{1}{2}\right)\in ℝ$$
6		flltp1	$$⊢A+\left(\frac{1}{2}\right)\in ℝ\to A+\left(\frac{1}{2}\right)<⌊A+\left(\frac{1}{2}\right)⌋+1$$
7	5 6	syl	$$⊢A\in ℝ\to A+\left(\frac{1}{2}\right)<⌊A+\left(\frac{1}{2}\right)⌋+1$$
8		ax-1cn	$$⊢1\in ℂ$$
9		2halves	$$⊢1\in ℂ\to \left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
10	8 9	ax-mp	$$⊢\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=1$$
11	10	eqcomi	$$⊢1=\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
12	11	a1i	$$⊢A\in ℝ\to 1=\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
13	12	oveq2d	$$⊢A\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋+1=⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
14		reflcl	$$⊢A+\left(\frac{1}{2}\right)\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋\in ℝ$$
15	5 14	syl	$$⊢A\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋\in ℝ$$
16	15	recnd	$$⊢A\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋\in ℂ$$
17	3	recnd	$$⊢A\in ℝ\to \frac{1}{2}\in ℂ$$
18	16 17 17	3jca	$$⊢A\in ℝ\to \left(⌊A+\left(\frac{1}{2}\right)⌋\in ℂ\wedge \frac{1}{2}\in ℂ\wedge \frac{1}{2}\in ℂ\right)$$
19		addass	$$⊢\left(⌊A+\left(\frac{1}{2}\right)⌋\in ℂ\wedge \frac{1}{2}\in ℂ\wedge \frac{1}{2}\in ℂ\right)\to ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
20	18 19	syl	$$⊢A\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
21	20	eqcomd	$$⊢A\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)=⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
22	13 21	eqtrd	$$⊢A\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋+1=⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
23	7 22	breqtrd	$$⊢A\in ℝ\to A+\left(\frac{1}{2}\right)<⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)$$
24	15 3	jca	$$⊢A\in ℝ\to \left(⌊A+\left(\frac{1}{2}\right)⌋\in ℝ\wedge \frac{1}{2}\in ℝ\right)$$
25		readdcl	$$⊢\left(⌊A+\left(\frac{1}{2}\right)⌋\in ℝ\wedge \frac{1}{2}\in ℝ\right)\to ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\in ℝ$$
26	24 25	syl	$$⊢A\in ℝ\to ⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\in ℝ$$
27	1 26 3	ltadd1d	$$⊢A\in ℝ\to \left(A<⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\leftrightarrow A+\left(\frac{1}{2}\right)<⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)+\left(\frac{1}{2}\right)\right)$$
28	23 27	mpbird	$$⊢A\in ℝ\to A<⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)$$
29	1 26	posdifd	$$⊢A\in ℝ\to \left(A<⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)\leftrightarrow 0<⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)-A\right)$$
30	28 29	mpbid	$$⊢A\in ℝ\to 0<⌊A+\left(\frac{1}{2}\right)⌋+\left(\frac{1}{2}\right)-A$$