Theorem dnibndlem1

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

	Ref	Expression
Hypotheses	dnibndlem1.1	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
	dnibndlem1.2	$$⊢\phi \to A\in ℝ$$
	dnibndlem1.3	$$⊢\phi \to B\in ℝ$$
Assertion	dnibndlem1	$$⊢\phi \to \left(\left|T\left(B\right)-T\left(A\right)\right|\le S\leftrightarrow \left|\left|⌊B+\left(\frac{1}{2}\right)⌋-B\right|-\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\right|\le S\right)$$

Proof

Step	Hyp	Ref	Expression
1		dnibndlem1.1	$$⊢T=\left(x\in ℝ⟼\left|⌊x+\left(\frac{1}{2}\right)⌋-x\right|\right)$$
2		dnibndlem1.2	$$⊢\phi \to A\in ℝ$$
3		dnibndlem1.3	$$⊢\phi \to B\in ℝ$$
4	1	dnival	$$⊢B\in ℝ\to T\left(B\right)=\left|⌊B+\left(\frac{1}{2}\right)⌋-B\right|$$
5	3 4	syl	$$⊢\phi \to T\left(B\right)=\left|⌊B+\left(\frac{1}{2}\right)⌋-B\right|$$
6	1	dnival	$$⊢A\in ℝ\to T\left(A\right)=\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$
7	2 6	syl	$$⊢\phi \to T\left(A\right)=\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$
8	5 7	oveq12d	$$⊢\phi \to T\left(B\right)-T\left(A\right)=\left|⌊B+\left(\frac{1}{2}\right)⌋-B\right|-\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|$$
9	8	fveq2d	$$⊢\phi \to \left|T\left(B\right)-T\left(A\right)\right|=\left|\left|⌊B+\left(\frac{1}{2}\right)⌋-B\right|-\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\right|$$
10	9	breq1d	$$⊢\phi \to \left(\left|T\left(B\right)-T\left(A\right)\right|\le S\leftrightarrow \left|\left|⌊B+\left(\frac{1}{2}\right)⌋-B\right|-\left|⌊A+\left(\frac{1}{2}\right)⌋-A\right|\right|\le S\right)$$