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

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 addridd ⊢ ( 𝜑 → ( 𝐵 + 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 ⊢ ( 𝜑 → 𝐸 : ℝ ⟶ ( 𝐴 (,] 𝐵 ) )