Metamath Proof Explorer


Theorem fourierdlem94

Description: For a piecewise smooth function, the left and the right limits exist at any point. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem94.f φ F :
fourierdlem94.t T = 2 π
fourierdlem94.per φ x F x + T = F x
fourierdlem94.x φ X
fourierdlem94.p P = n p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1
fourierdlem94.m φ M
fourierdlem94.q φ Q P M
fourierdlem94.dvcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
fourierdlem94.dvlb φ i 0 ..^ M F Q i Q i + 1 lim Q i
fourierdlem94.dvub φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1
Assertion fourierdlem94 φ F −∞ X lim X F X +∞ lim X

Proof

Step Hyp Ref Expression
1 fourierdlem94.f φ F :
2 fourierdlem94.t T = 2 π
3 fourierdlem94.per φ x F x + T = F x
4 fourierdlem94.x φ X
5 fourierdlem94.p P = n p 0 n | p 0 = π p n = π i 0 ..^ n p i < p i + 1
6 fourierdlem94.m φ M
7 fourierdlem94.q φ Q P M
8 fourierdlem94.dvcn φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
9 fourierdlem94.dvlb φ i 0 ..^ M F Q i Q i + 1 lim Q i
10 fourierdlem94.dvub φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1
11 pire π
12 11 renegcli π
13 12 a1i φ π
14 11 a1i φ π
15 negpilt0 π < 0
16 pipos 0 < π
17 0re 0
18 12 17 11 lttri π < 0 0 < π π < π
19 15 16 18 mp2an π < π
20 19 a1i φ π < π
21 picn π
22 21 2timesi 2 π = π + π
23 21 21 subnegi π π = π + π
24 22 2 23 3eqtr4i T = π π
25 ssid
26 25 a1i φ
27 simp2 φ x k x
28 zre k k
29 28 3ad2ant3 φ x k k
30 2re 2
31 30 11 remulcli 2 π
32 31 a1i φ 2 π
33 2 32 eqeltrid φ T
34 33 adantr φ k T
35 34 3adant2 φ x k T
36 29 35 remulcld φ x k k T
37 27 36 readdcld φ x k x + k T
38 simp1 φ x k φ
39 simp3 φ x k k
40 ax-resscn
41 40 a1i φ
42 1 41 fssd φ F :
43 42 adantr φ k F :
44 43 adantr φ k x F :
45 34 adantr φ k x T
46 simplr φ k x k
47 simpr φ k x x
48 eleq1w x = y x y
49 48 anbi2d x = y φ x φ y
50 oveq1 x = y x + T = y + T
51 50 fveq2d x = y F x + T = F y + T
52 fveq2 x = y F x = F y
53 51 52 eqeq12d x = y F x + T = F x F y + T = F y
54 49 53 imbi12d x = y φ x F x + T = F x φ y F y + T = F y
55 54 3 chvarvv φ y F y + T = F y
56 55 ad4ant14 φ k x y F y + T = F y
57 44 45 46 47 56 fperiodmul φ k x F x + k T = F x
58 38 39 27 57 syl21anc φ x k F x + k T = F x
59 40 a1i φ i 0 ..^ M
60 ioossre Q i Q i + 1
61 60 a1i φ Q i Q i + 1
62 1 61 fssresd φ F Q i Q i + 1 : Q i Q i + 1
63 62 41 fssd φ F Q i Q i + 1 : Q i Q i + 1
64 63 adantr φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1
65 60 a1i φ i 0 ..^ M Q i Q i + 1
66 42 adantr φ i 0 ..^ M F :
67 25 a1i φ i 0 ..^ M
68 eqid TopOpen fld = TopOpen fld
69 68 tgioo2 topGen ran . = TopOpen fld 𝑡
70 68 69 dvres F : Q i Q i + 1 D F Q i Q i + 1 = F int topGen ran . Q i Q i + 1
71 59 66 67 65 70 syl22anc φ i 0 ..^ M D F Q i Q i + 1 = F int topGen ran . Q i Q i + 1
72 71 dmeqd φ i 0 ..^ M dom F Q i Q i + 1 = dom F int topGen ran . Q i Q i + 1
73 ioontr int topGen ran . Q i Q i + 1 = Q i Q i + 1
74 73 reseq2i F int topGen ran . Q i Q i + 1 = F Q i Q i + 1
75 74 dmeqi dom F int topGen ran . Q i Q i + 1 = dom F Q i Q i + 1
76 75 a1i φ i 0 ..^ M dom F int topGen ran . Q i Q i + 1 = dom F Q i Q i + 1
77 cncff F Q i Q i + 1 : Q i Q i + 1 cn F Q i Q i + 1 : Q i Q i + 1
78 fdm F Q i Q i + 1 : Q i Q i + 1 dom F Q i Q i + 1 = Q i Q i + 1
79 8 77 78 3syl φ i 0 ..^ M dom F Q i Q i + 1 = Q i Q i + 1
80 72 76 79 3eqtrd φ i 0 ..^ M dom F Q i Q i + 1 = Q i Q i + 1
81 dvcn F Q i Q i + 1 : Q i Q i + 1 Q i Q i + 1 dom F Q i Q i + 1 = Q i Q i + 1 F Q i Q i + 1 : Q i Q i + 1 cn
82 59 64 65 80 81 syl31anc φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1 cn
83 65 40 sstrdi φ i 0 ..^ M Q i Q i + 1
84 5 fourierdlem2 M Q P M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
85 6 84 syl φ Q P M Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
86 7 85 mpbid φ Q 0 M Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
87 86 simpld φ Q 0 M
88 elmapi Q 0 M Q : 0 M
89 87 88 syl φ Q : 0 M
90 89 adantr φ i 0 ..^ M Q : 0 M
91 elfzofz i 0 ..^ M i 0 M
92 91 adantl φ i 0 ..^ M i 0 M
93 90 92 ffvelrnd φ i 0 ..^ M Q i
94 93 rexrd φ i 0 ..^ M Q i *
95 fzofzp1 i 0 ..^ M i + 1 0 M
96 95 adantl φ i 0 ..^ M i + 1 0 M
97 90 96 ffvelrnd φ i 0 ..^ M Q i + 1
98 86 simprrd φ i 0 ..^ M Q i < Q i + 1
99 98 r19.21bi φ i 0 ..^ M Q i < Q i + 1
100 68 94 97 99 lptioo2cn φ i 0 ..^ M Q i + 1 limPt TopOpen fld Q i Q i + 1
101 62 adantr φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1
102 41 42 26 dvbss φ dom F
103 dvfre F : F : dom F
104 1 26 103 syl2anc φ F : dom F
105 86 simprd φ Q 0 = π Q M = π i 0 ..^ M Q i < Q i + 1
106 105 simplld φ Q 0 = π
107 105 simplrd φ Q M = π
108 8 77 syl φ i 0 ..^ M F Q i Q i + 1 : Q i Q i + 1
109 97 rexrd φ i 0 ..^ M Q i + 1 *
110 68 109 93 99 lptioo1cn φ i 0 ..^ M Q i limPt TopOpen fld Q i Q i + 1
111 108 83 110 9 68 ellimciota φ i 0 ..^ M ι x | x F Q i Q i + 1 lim Q i F Q i Q i + 1 lim Q i
112 108 83 100 10 68 ellimciota φ i 0 ..^ M ι x | x F Q i Q i + 1 lim Q i + 1 F Q i Q i + 1 lim Q i + 1
113 28 adantl φ k k
114 113 34 remulcld φ k k T
115 43 adantr φ k t F :
116 34 adantr φ k t T
117 simplr φ k t k
118 simpr φ k t t
119 3 ad4ant14 φ k t x F x + T = F x
120 115 116 117 118 119 fperiodmul φ k t F t + k T = F t
121 eqid D F = D F
122 43 114 120 121 fperdvper φ k t dom F t + k T dom F F t + k T = F t
123 122 an32s φ t dom F k t + k T dom F F t + k T = F t
124 123 simpld φ t dom F k t + k T dom F
125 123 simprd φ t dom F k F t + k T = F t
126 fveq2 j = i Q j = Q i
127 oveq1 j = i j + 1 = i + 1
128 127 fveq2d j = i Q j + 1 = Q i + 1
129 126 128 oveq12d j = i Q j Q j + 1 = Q i Q i + 1
130 129 cbvmptv j 0 ..^ M Q j Q j + 1 = i 0 ..^ M Q i Q i + 1
131 eqid t t + π t T T = t t + π t T T
132 102 104 13 14 20 24 6 89 106 107 8 111 112 124 125 130 131 fourierdlem71 φ z t dom F F t z
133 132 adantr φ i 0 ..^ M z t dom F F t z
134 nfv t φ i 0 ..^ M
135 nfra1 t t dom F F t z
136 134 135 nfan t φ i 0 ..^ M t dom F F t z
137 71 74 eqtrdi φ i 0 ..^ M D F Q i Q i + 1 = F Q i Q i + 1
138 137 fveq1d φ i 0 ..^ M F Q i Q i + 1 t = F Q i Q i + 1 t
139 fvres t Q i Q i + 1 F Q i Q i + 1 t = F t
140 138 139 sylan9eq φ i 0 ..^ M t Q i Q i + 1 F Q i Q i + 1 t = F t
141 140 fveq2d φ i 0 ..^ M t Q i Q i + 1 F Q i Q i + 1 t = F t
142 141 adantlr φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t = F t
143 simplr φ i 0 ..^ M t dom F F t z t Q i Q i + 1 t dom F F t z
144 ssdmres Q i Q i + 1 dom F dom F Q i Q i + 1 = Q i Q i + 1
145 79 144 sylibr φ i 0 ..^ M Q i Q i + 1 dom F
146 145 ad2antrr φ i 0 ..^ M t dom F F t z t Q i Q i + 1 Q i Q i + 1 dom F
147 simpr φ i 0 ..^ M t dom F F t z t Q i Q i + 1 t Q i Q i + 1
148 146 147 sseldd φ i 0 ..^ M t dom F F t z t Q i Q i + 1 t dom F
149 rspa t dom F F t z t dom F F t z
150 143 148 149 syl2anc φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F t z
151 142 150 eqbrtrd φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t z
152 151 ex φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t z
153 136 152 ralrimi φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t z
154 153 ex φ i 0 ..^ M t dom F F t z t Q i Q i + 1 F Q i Q i + 1 t z
155 154 reximdv φ i 0 ..^ M z t dom F F t z z t Q i Q i + 1 F Q i Q i + 1 t z
156 133 155 mpd φ i 0 ..^ M z t Q i Q i + 1 F Q i Q i + 1 t z
157 93 97 101 80 156 ioodvbdlimc2 φ i 0 ..^ M F Q i Q i + 1 lim Q i + 1
158 64 83 100 157 68 ellimciota φ i 0 ..^ M ι y | y F Q i Q i + 1 lim Q i + 1 F Q i Q i + 1 lim Q i + 1
159 oveq2 y = x π y = π x
160 159 oveq1d y = x π y T = π x T
161 160 fveq2d y = x π y T = π x T
162 161 oveq1d y = x π y T T = π x T T
163 162 cbvmptv y π y T T = x π x T T
164 id z = x z = x
165 fveq2 z = x y π y T T z = y π y T T x
166 164 165 oveq12d z = x z + y π y T T z = x + y π y T T x
167 166 cbvmptv z z + y π y T T z = x x + y π y T T x
168 13 14 20 5 24 6 7 26 1 37 58 82 158 4 163 167 fourierdlem49 φ F −∞ X lim X
169 93 97 101 80 156 ioodvbdlimc1 φ i 0 ..^ M F Q i Q i + 1 lim Q i
170 64 83 110 169 68 ellimciota φ i 0 ..^ M ι y | y F Q i Q i + 1 lim Q i F Q i Q i + 1 lim Q i
171 biid φ i 0 ..^ M w Q i Q i + 1 k w = X + k T φ i 0 ..^ M w Q i Q i + 1 k w = X + k T
172 13 14 20 5 24 6 7 1 37 58 82 170 4 163 167 171 fourierdlem48 φ F X +∞ lim X
173 168 172 jca φ F −∞ X lim X F X +∞ lim X