Metamath Proof Explorer


Theorem fourierdlem4

Description: E is a function that maps any point to a periodic corresponding point in ( A , B ] . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem4.a ( 𝜑𝐴 ∈ ℝ )
fourierdlem4.b ( 𝜑𝐵 ∈ ℝ )
fourierdlem4.altb ( 𝜑𝐴 < 𝐵 )
fourierdlem4.t 𝑇 = ( 𝐵𝐴 )
fourierdlem4.e 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
Assertion fourierdlem4 ( 𝜑𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem4.a ( 𝜑𝐴 ∈ ℝ )
2 fourierdlem4.b ( 𝜑𝐵 ∈ ℝ )
3 fourierdlem4.altb ( 𝜑𝐴 < 𝐵 )
4 fourierdlem4.t 𝑇 = ( 𝐵𝐴 )
5 fourierdlem4.e 𝐸 = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
6 simpr ( ( 𝜑𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
7 2 adantr ( ( 𝜑𝑥 ∈ ℝ ) → 𝐵 ∈ ℝ )
8 7 6 resubcld ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐵𝑥 ) ∈ ℝ )
9 2 1 resubcld ( 𝜑 → ( 𝐵𝐴 ) ∈ ℝ )
10 4 9 eqeltrid ( 𝜑𝑇 ∈ ℝ )
11 10 adantr ( ( 𝜑𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
12 4 a1i ( 𝜑𝑇 = ( 𝐵𝐴 ) )
13 2 recnd ( 𝜑𝐵 ∈ ℂ )
14 1 recnd ( 𝜑𝐴 ∈ ℂ )
15 1 3 gtned ( 𝜑𝐵𝐴 )
16 13 14 15 subne0d ( 𝜑 → ( 𝐵𝐴 ) ≠ 0 )
17 12 16 eqnetrd ( 𝜑𝑇 ≠ 0 )
18 17 adantr ( ( 𝜑𝑥 ∈ ℝ ) → 𝑇 ≠ 0 )
19 8 11 18 redivcld ( ( 𝜑𝑥 ∈ ℝ ) → ( ( 𝐵𝑥 ) / 𝑇 ) ∈ ℝ )
20 19 flcld ( ( 𝜑𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) ∈ ℤ )
21 20 zred ( ( 𝜑𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) ∈ ℝ )
22 21 11 remulcld ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ∈ ℝ )
23 6 22 readdcld ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ )
24 1 adantr ( ( 𝜑𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
25 24 6 resubcld ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐴𝑥 ) ∈ ℝ )
26 25 11 18 redivcld ( ( 𝜑𝑥 ∈ ℝ ) → ( ( 𝐴𝑥 ) / 𝑇 ) ∈ ℝ )
27 26 11 remulcld ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ( 𝐴𝑥 ) / 𝑇 ) · 𝑇 ) ∈ ℝ )
28 13 addid1d ( 𝜑 → ( 𝐵 + 0 ) = 𝐵 )
29 28 eqcomd ( 𝜑𝐵 = ( 𝐵 + 0 ) )
30 13 14 subcld ( 𝜑 → ( 𝐵𝐴 ) ∈ ℂ )
31 30 subidd ( 𝜑 → ( ( 𝐵𝐴 ) − ( 𝐵𝐴 ) ) = 0 )
32 31 eqcomd ( 𝜑 → 0 = ( ( 𝐵𝐴 ) − ( 𝐵𝐴 ) ) )
33 32 oveq2d ( 𝜑 → ( 𝐵 + 0 ) = ( 𝐵 + ( ( 𝐵𝐴 ) − ( 𝐵𝐴 ) ) ) )
34 13 30 30 addsub12d ( 𝜑 → ( 𝐵 + ( ( 𝐵𝐴 ) − ( 𝐵𝐴 ) ) ) = ( ( 𝐵𝐴 ) + ( 𝐵 − ( 𝐵𝐴 ) ) ) )
35 13 14 nncand ( 𝜑 → ( 𝐵 − ( 𝐵𝐴 ) ) = 𝐴 )
36 35 oveq2d ( 𝜑 → ( ( 𝐵𝐴 ) + ( 𝐵 − ( 𝐵𝐴 ) ) ) = ( ( 𝐵𝐴 ) + 𝐴 ) )
37 30 14 addcomd ( 𝜑 → ( ( 𝐵𝐴 ) + 𝐴 ) = ( 𝐴 + ( 𝐵𝐴 ) ) )
38 12 eqcomd ( 𝜑 → ( 𝐵𝐴 ) = 𝑇 )
39 38 oveq2d ( 𝜑 → ( 𝐴 + ( 𝐵𝐴 ) ) = ( 𝐴 + 𝑇 ) )
40 37 39 eqtrd ( 𝜑 → ( ( 𝐵𝐴 ) + 𝐴 ) = ( 𝐴 + 𝑇 ) )
41 34 36 40 3eqtrd ( 𝜑 → ( 𝐵 + ( ( 𝐵𝐴 ) − ( 𝐵𝐴 ) ) ) = ( 𝐴 + 𝑇 ) )
42 29 33 41 3eqtrd ( 𝜑𝐵 = ( 𝐴 + 𝑇 ) )
43 42 adantr ( ( 𝜑𝑥 ∈ ℝ ) → 𝐵 = ( 𝐴 + 𝑇 ) )
44 43 oveq1d ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐵𝑥 ) = ( ( 𝐴 + 𝑇 ) − 𝑥 ) )
45 14 adantr ( ( 𝜑𝑥 ∈ ℝ ) → 𝐴 ∈ ℂ )
46 11 recnd ( ( 𝜑𝑥 ∈ ℝ ) → 𝑇 ∈ ℂ )
47 6 recnd ( ( 𝜑𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
48 45 46 47 addsubd ( ( 𝜑𝑥 ∈ ℝ ) → ( ( 𝐴 + 𝑇 ) − 𝑥 ) = ( ( 𝐴𝑥 ) + 𝑇 ) )
49 44 48 eqtrd ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐵𝑥 ) = ( ( 𝐴𝑥 ) + 𝑇 ) )
50 49 oveq1d ( ( 𝜑𝑥 ∈ ℝ ) → ( ( 𝐵𝑥 ) / 𝑇 ) = ( ( ( 𝐴𝑥 ) + 𝑇 ) / 𝑇 ) )
51 45 47 subcld ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐴𝑥 ) ∈ ℂ )
52 51 46 46 18 divdird ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ( 𝐴𝑥 ) + 𝑇 ) / 𝑇 ) = ( ( ( 𝐴𝑥 ) / 𝑇 ) + ( 𝑇 / 𝑇 ) ) )
53 4 30 eqeltrid ( 𝜑𝑇 ∈ ℂ )
54 53 17 dividd ( 𝜑 → ( 𝑇 / 𝑇 ) = 1 )
55 54 adantr ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑇 / 𝑇 ) = 1 )
56 55 oveq2d ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ( 𝐴𝑥 ) / 𝑇 ) + ( 𝑇 / 𝑇 ) ) = ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) )
57 50 52 56 3eqtrd ( ( 𝜑𝑥 ∈ ℝ ) → ( ( 𝐵𝑥 ) / 𝑇 ) = ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) )
58 57 fveq2d ( ( 𝜑𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) )
59 58 oveq1d ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) )
60 59 22 eqeltrrd ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) ∈ ℝ )
61 peano2re ( ( ( 𝐴𝑥 ) / 𝑇 ) ∈ ℝ → ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ∈ ℝ )
62 26 61 syl ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ∈ ℝ )
63 reflcl ( ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ∈ ℝ → ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) ∈ ℝ )
64 62 63 syl ( ( 𝜑𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) ∈ ℝ )
65 1 2 posdifd ( 𝜑 → ( 𝐴 < 𝐵 ↔ 0 < ( 𝐵𝐴 ) ) )
66 3 65 mpbid ( 𝜑 → 0 < ( 𝐵𝐴 ) )
67 66 12 breqtrrd ( 𝜑 → 0 < 𝑇 )
68 10 67 elrpd ( 𝜑𝑇 ∈ ℝ+ )
69 68 adantr ( ( 𝜑𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ+ )
70 flltp1 ( ( ( 𝐴𝑥 ) / 𝑇 ) ∈ ℝ → ( ( 𝐴𝑥 ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐴𝑥 ) / 𝑇 ) ) + 1 ) )
71 26 70 syl ( ( 𝜑𝑥 ∈ ℝ ) → ( ( 𝐴𝑥 ) / 𝑇 ) < ( ( ⌊ ‘ ( ( 𝐴𝑥 ) / 𝑇 ) ) + 1 ) )
72 1zzd ( ( 𝜑𝑥 ∈ ℝ ) → 1 ∈ ℤ )
73 fladdz ( ( ( ( 𝐴𝑥 ) / 𝑇 ) ∈ ℝ ∧ 1 ∈ ℤ ) → ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) = ( ( ⌊ ‘ ( ( 𝐴𝑥 ) / 𝑇 ) ) + 1 ) )
74 26 72 73 syl2anc ( ( 𝜑𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) = ( ( ⌊ ‘ ( ( 𝐴𝑥 ) / 𝑇 ) ) + 1 ) )
75 71 74 breqtrrd ( ( 𝜑𝑥 ∈ ℝ ) → ( ( 𝐴𝑥 ) / 𝑇 ) < ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) )
76 26 64 69 75 ltmul1dd ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ( 𝐴𝑥 ) / 𝑇 ) · 𝑇 ) < ( ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) )
77 27 60 6 76 ltadd2dd ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐴𝑥 ) / 𝑇 ) · 𝑇 ) ) < ( 𝑥 + ( ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) ) )
78 51 46 18 divcan1d ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ( 𝐴𝑥 ) / 𝑇 ) · 𝑇 ) = ( 𝐴𝑥 ) )
79 78 oveq2d ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐴𝑥 ) / 𝑇 ) · 𝑇 ) ) = ( 𝑥 + ( 𝐴𝑥 ) ) )
80 47 45 pncan3d ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( 𝐴𝑥 ) ) = 𝐴 )
81 79 80 eqtrd ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐴𝑥 ) / 𝑇 ) · 𝑇 ) ) = 𝐴 )
82 59 oveq2d ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) ) )
83 82 eqcomd ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( ( 𝐴𝑥 ) / 𝑇 ) + 1 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
84 77 81 83 3brtr3d ( ( 𝜑𝑥 ∈ ℝ ) → 𝐴 < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
85 19 11 remulcld ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ( 𝐵𝑥 ) / 𝑇 ) · 𝑇 ) ∈ ℝ )
86 flle ( ( ( 𝐵𝑥 ) / 𝑇 ) ∈ ℝ → ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) ≤ ( ( 𝐵𝑥 ) / 𝑇 ) )
87 19 86 syl ( ( 𝜑𝑥 ∈ ℝ ) → ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) ≤ ( ( 𝐵𝑥 ) / 𝑇 ) )
88 21 19 69 lemul1d ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) ≤ ( ( 𝐵𝑥 ) / 𝑇 ) ↔ ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ≤ ( ( ( 𝐵𝑥 ) / 𝑇 ) · 𝑇 ) ) )
89 87 88 mpbid ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ≤ ( ( ( 𝐵𝑥 ) / 𝑇 ) · 𝑇 ) )
90 22 85 6 89 leadd2dd ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ≤ ( 𝑥 + ( ( ( 𝐵𝑥 ) / 𝑇 ) · 𝑇 ) ) )
91 8 recnd ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝐵𝑥 ) ∈ ℂ )
92 91 46 18 divcan1d ( ( 𝜑𝑥 ∈ ℝ ) → ( ( ( 𝐵𝑥 ) / 𝑇 ) · 𝑇 ) = ( 𝐵𝑥 ) )
93 92 oveq2d ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐵𝑥 ) / 𝑇 ) · 𝑇 ) ) = ( 𝑥 + ( 𝐵𝑥 ) ) )
94 13 adantr ( ( 𝜑𝑥 ∈ ℝ ) → 𝐵 ∈ ℂ )
95 47 94 pncan3d ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( 𝐵𝑥 ) ) = 𝐵 )
96 93 95 eqtrd ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ( 𝐵𝑥 ) / 𝑇 ) · 𝑇 ) ) = 𝐵 )
97 90 96 breqtrd ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ≤ 𝐵 )
98 24 rexrd ( ( 𝜑𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ* )
99 elioc2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ ) → ( ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ ∧ 𝐴 < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ≤ 𝐵 ) ) )
100 98 7 99 syl2anc ( ( 𝜑𝑥 ∈ ℝ ) → ( ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) ↔ ( ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ℝ ∧ 𝐴 < ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∧ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ≤ 𝐵 ) ) )
101 23 84 97 100 mpbir3and ( ( 𝜑𝑥 ∈ ℝ ) → ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵𝑥 ) / 𝑇 ) ) · 𝑇 ) ) ∈ ( 𝐴 (,] 𝐵 ) )
102 101 5 fmptd ( 𝜑𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )