Theorem fourierdlem7

Description: The difference between the periodic sawtooth function and the identity function is decreasing. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	fourierdlem7.a	$$⊢\phi \to A\in ℝ$$
	fourierdlem7.b	$$⊢\phi \to B\in ℝ$$
	fourierdlem7.altb	$$⊢\phi \to A<B$$
	fourierdlem7.t	$$⊢T=B-A$$
	fourierdlem7.e	$$⊢E=\left(x\in ℝ⟼x+⌊\frac{B-x}{T}⌋T\right)$$
	fourierdlem7.x	$$⊢\phi \to X\in ℝ$$
	fourierdlem7.y	$$⊢\phi \to Y\in ℝ$$
	fourierdlem7.xlty	$$⊢\phi \to X\le Y$$
Assertion	fourierdlem7	$$⊢\phi \to E\left(Y\right)-Y\le E\left(X\right)-X$$

Proof

Step	Hyp	Ref	Expression
1		fourierdlem7.a	$$⊢\phi \to A\in ℝ$$
2		fourierdlem7.b	$$⊢\phi \to B\in ℝ$$
3		fourierdlem7.altb	$$⊢\phi \to A<B$$
4		fourierdlem7.t	$$⊢T=B-A$$
5		fourierdlem7.e	$$⊢E=\left(x\in ℝ⟼x+⌊\frac{B-x}{T}⌋T\right)$$
6		fourierdlem7.x	$$⊢\phi \to X\in ℝ$$
7		fourierdlem7.y	$$⊢\phi \to Y\in ℝ$$
8		fourierdlem7.xlty	$$⊢\phi \to X\le Y$$
9	2 7	resubcld	$$⊢\phi \to B-Y\in ℝ$$
10	2 1	resubcld	$$⊢\phi \to B-A\in ℝ$$
11	4 10	eqeltrid	$$⊢\phi \to T\in ℝ$$
12	1 2	posdifd	$$⊢\phi \to \left(A<B\leftrightarrow 0<B-A\right)$$
13	3 12	mpbid	$$⊢\phi \to 0<B-A$$
14	13 4	breqtrrdi	$$⊢\phi \to 0<T$$
15	14	gt0ne0d	$$⊢\phi \to T\ne 0$$
16	9 11 15	redivcld	$$⊢\phi \to \frac{B-Y}{T}\in ℝ$$
17	2 6	resubcld	$$⊢\phi \to B-X\in ℝ$$
18	17 11 15	redivcld	$$⊢\phi \to \frac{B-X}{T}\in ℝ$$
19	11 14	elrpd	$$⊢\phi \to T\in {ℝ}^{+}$$
20	6 7 2 8	lesub2dd	$$⊢\phi \to B-Y\le B-X$$
21	9 17 19 20	lediv1dd	$$⊢\phi \to \frac{B-Y}{T}\le \frac{B-X}{T}$$
22		flwordi	$$⊢\left(\frac{B-Y}{T}\in ℝ\wedge \frac{B-X}{T}\in ℝ\wedge \frac{B-Y}{T}\le \frac{B-X}{T}\right)\to ⌊\frac{B-Y}{T}⌋\le ⌊\frac{B-X}{T}⌋$$
23	16 18 21 22	syl3anc	$$⊢\phi \to ⌊\frac{B-Y}{T}⌋\le ⌊\frac{B-X}{T}⌋$$
24	16	flcld	$$⊢\phi \to ⌊\frac{B-Y}{T}⌋\in \mathbb{Z}$$
25	24	zred	$$⊢\phi \to ⌊\frac{B-Y}{T}⌋\in ℝ$$
26	18	flcld	$$⊢\phi \to ⌊\frac{B-X}{T}⌋\in \mathbb{Z}$$
27	26	zred	$$⊢\phi \to ⌊\frac{B-X}{T}⌋\in ℝ$$
28	25 27 19	lemul1d	$$⊢\phi \to \left(⌊\frac{B-Y}{T}⌋\le ⌊\frac{B-X}{T}⌋\leftrightarrow ⌊\frac{B-Y}{T}⌋T\le ⌊\frac{B-X}{T}⌋T\right)$$
29	23 28	mpbid	$$⊢\phi \to ⌊\frac{B-Y}{T}⌋T\le ⌊\frac{B-X}{T}⌋T$$
30	5	a1i	$$⊢\phi \to E=\left(x\in ℝ⟼x+⌊\frac{B-x}{T}⌋T\right)$$
31		id	$$⊢x=Y\to x=Y$$
32		oveq2	$$⊢x=Y\to B-x=B-Y$$
33	32	oveq1d	$$⊢x=Y\to \frac{B-x}{T}=\frac{B-Y}{T}$$
34	33	fveq2d	$$⊢x=Y\to ⌊\frac{B-x}{T}⌋=⌊\frac{B-Y}{T}⌋$$
35	34	oveq1d	$$⊢x=Y\to ⌊\frac{B-x}{T}⌋T=⌊\frac{B-Y}{T}⌋T$$
36	31 35	oveq12d	$$⊢x=Y\to x+⌊\frac{B-x}{T}⌋T=Y+⌊\frac{B-Y}{T}⌋T$$
37	36	adantl	$$⊢\left(\phi \wedge x=Y\right)\to x+⌊\frac{B-x}{T}⌋T=Y+⌊\frac{B-Y}{T}⌋T$$
38	25 11	remulcld	$$⊢\phi \to ⌊\frac{B-Y}{T}⌋T\in ℝ$$
39	7 38	readdcld	$$⊢\phi \to Y+⌊\frac{B-Y}{T}⌋T\in ℝ$$
40	30 37 7 39	fvmptd	$$⊢\phi \to E\left(Y\right)=Y+⌊\frac{B-Y}{T}⌋T$$
41	40	oveq1d	$$⊢\phi \to E\left(Y\right)-Y=Y+⌊\frac{B-Y}{T}⌋T-Y$$
42	7	recnd	$$⊢\phi \to Y\in ℂ$$
43	38	recnd	$$⊢\phi \to ⌊\frac{B-Y}{T}⌋T\in ℂ$$
44	42 43	pncan2d	$$⊢\phi \to Y+⌊\frac{B-Y}{T}⌋T-Y=⌊\frac{B-Y}{T}⌋T$$
45	41 44	eqtrd	$$⊢\phi \to E\left(Y\right)-Y=⌊\frac{B-Y}{T}⌋T$$
46		id	$$⊢x=X\to x=X$$
47		oveq2	$$⊢x=X\to B-x=B-X$$
48	47	oveq1d	$$⊢x=X\to \frac{B-x}{T}=\frac{B-X}{T}$$
49	48	fveq2d	$$⊢x=X\to ⌊\frac{B-x}{T}⌋=⌊\frac{B-X}{T}⌋$$
50	49	oveq1d	$$⊢x=X\to ⌊\frac{B-x}{T}⌋T=⌊\frac{B-X}{T}⌋T$$
51	46 50	oveq12d	$$⊢x=X\to x+⌊\frac{B-x}{T}⌋T=X+⌊\frac{B-X}{T}⌋T$$
52	51	adantl	$$⊢\left(\phi \wedge x=X\right)\to x+⌊\frac{B-x}{T}⌋T=X+⌊\frac{B-X}{T}⌋T$$
53	27 11	remulcld	$$⊢\phi \to ⌊\frac{B-X}{T}⌋T\in ℝ$$
54	6 53	readdcld	$$⊢\phi \to X+⌊\frac{B-X}{T}⌋T\in ℝ$$
55	30 52 6 54	fvmptd	$$⊢\phi \to E\left(X\right)=X+⌊\frac{B-X}{T}⌋T$$
56	55	oveq1d	$$⊢\phi \to E\left(X\right)-X=X+⌊\frac{B-X}{T}⌋T-X$$
57	6	recnd	$$⊢\phi \to X\in ℂ$$
58	53	recnd	$$⊢\phi \to ⌊\frac{B-X}{T}⌋T\in ℂ$$
59	57 58	pncan2d	$$⊢\phi \to X+⌊\frac{B-X}{T}⌋T-X=⌊\frac{B-X}{T}⌋T$$
60	56 59	eqtrd	$$⊢\phi \to E\left(X\right)-X=⌊\frac{B-X}{T}⌋T$$
61	29 45 60	3brtr4d	$$⊢\phi \to E\left(Y\right)-Y\le E\left(X\right)-X$$