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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	fourierdlem7.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	fourierdlem7.altb	⊢ ( 𝜑 → 𝐴 < 𝐵 )
	fourierdlem7.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
	fourierdlem7.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
	fourierdlem7.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
	fourierdlem7.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
	fourierdlem7.xlty	⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
Assertion	fourierdlem7	⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ≤ ( ( 𝐸 ‘ 𝑋 ) − 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fourierdlem7.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		fourierdlem7.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		fourierdlem7.altb	⊢ ( 𝜑 → 𝐴 < 𝐵 )
4		fourierdlem7.t	⊢ 𝑇 = ( 𝐵 − 𝐴 )
5		fourierdlem7.e	⊢ 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
6		fourierdlem7.x	⊢ ( 𝜑 → 𝑋 ∈ ℝ )
7		fourierdlem7.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
8		fourierdlem7.xlty	⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
9	2 7	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ∈ ℝ )
10	2 1	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
11	4 10	eqeltrid	⊢ ( 𝜑 → 𝑇 ∈ ℝ )
12	1 2	posdifd	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵 − 𝐴 ) ) )
13	3 12	mpbid	⊢ ( 𝜑 → 0 < ( 𝐵 − 𝐴 ) )
14	13 4	breqtrrdi	⊢ ( 𝜑 → 0 < 𝑇 )
15	14	gt0ne0d	⊢ ( 𝜑 → 𝑇 ≠ 0 )
16	9 11 15	redivcld	⊢ ( 𝜑 → ( ( 𝐵 − 𝑌 ) / 𝑇 ) ∈ ℝ )
17	2 6	resubcld	⊢ ( 𝜑 → ( 𝐵 − 𝑋 ) ∈ ℝ )
18	17 11 15	redivcld	⊢ ( 𝜑 → ( ( 𝐵 − 𝑋 ) / 𝑇 ) ∈ ℝ )
19	11 14	elrpd	⊢ ( 𝜑 → 𝑇 ∈ ℝ+ )
20	6 7 2 8	lesub2dd	⊢ ( 𝜑 → ( 𝐵 − 𝑌 ) ≤ ( 𝐵 − 𝑋 ) )
21	9 17 19 20	lediv1dd	⊢ ( 𝜑 → ( ( 𝐵 − 𝑌 ) / 𝑇 ) ≤ ( ( 𝐵 − 𝑋 ) / 𝑇 ) )
22		flwordi	⊢ ( ( ( ( 𝐵 − 𝑌 ) / 𝑇 ) ∈ ℝ ∧ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ∈ ℝ ∧ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ≤ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ≤ ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) )
23	16 18 21 22	syl3anc	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ≤ ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) )
24	16	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ∈ ℤ )
25	24	zred	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ∈ ℝ )
26	18	flcld	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℤ )
27	26	zred	⊢ ( 𝜑 → ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ∈ ℝ )
28	25 27 19	lemul1d	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) ≤ ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) ↔ ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ≤ ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
29	23 28	mpbid	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ≤ ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
30	5	a1i	⊢ ( 𝜑 → 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ) )
31		id	⊢ ( 𝑥 = 𝑌 → 𝑥 = 𝑌 )
32		oveq2	⊢ ( 𝑥 = 𝑌 → ( 𝐵 − 𝑥 ) = ( 𝐵 − 𝑌 ) )
33	32	oveq1d	⊢ ( 𝑥 = 𝑌 → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − 𝑌 ) / 𝑇 ) )
34	33	fveq2d	⊢ ( 𝑥 = 𝑌 → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) )
35	34	oveq1d	⊢ ( 𝑥 = 𝑌 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) )
36	31 35	oveq12d	⊢ ( 𝑥 = 𝑌 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) )
37	36	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) )
38	25 11	remulcld	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
39	7 38	readdcld	⊢ ( 𝜑 → ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
40	30 37 7 39	fvmptd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑌 ) = ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) )
41	40	oveq1d	⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) = ( ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑌 ) )
42	7	recnd	⊢ ( 𝜑 → 𝑌 ∈ ℂ )
43	38	recnd	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
44	42 43	pncan2d	⊢ ( 𝜑 → ( ( 𝑌 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑌 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) )
45	41 44	eqtrd	⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑌 ) / 𝑇 ) ) · 𝑇 ) )
46		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
47		oveq2	⊢ ( 𝑥 = 𝑋 → ( 𝐵 − 𝑥 ) = ( 𝐵 − 𝑋 ) )
48	47	oveq1d	⊢ ( 𝑥 = 𝑋 → ( ( 𝐵 − 𝑥 ) / 𝑇 ) = ( ( 𝐵 − 𝑋 ) / 𝑇 ) )
49	48	fveq2d	⊢ ( 𝑥 = 𝑋 → ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) )
50	49	oveq1d	⊢ ( 𝑥 = 𝑋 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
51	46 50	oveq12d	⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
52	51	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
53	27 11	remulcld	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
54	6 53	readdcld	⊢ ( 𝜑 → ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
55	30 52 6 54	fvmptd	⊢ ( 𝜑 → ( 𝐸 ‘ 𝑋 ) = ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) )
56	55	oveq1d	⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑋 ) − 𝑋 ) = ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑋 ) )
57	6	recnd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
58	53	recnd	⊢ ( 𝜑 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ∈ ℂ )
59	57 58	pncan2d	⊢ ( 𝜑 → ( ( 𝑋 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) ) − 𝑋 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
60	56 59	eqtrd	⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑋 ) − 𝑋 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑋 ) / 𝑇 ) ) · 𝑇 ) )
61	29 45 60	3brtr4d	⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ≤ ( ( 𝐸 ‘ 𝑋 ) − 𝑋 ) )