This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝐸 ‘ 𝑌 ) − 𝑌 ) ≤ ( ( 𝐸 ‘ 𝑋 ) − 𝑋 ) )