Metamath Proof Explorer


Theorem itgperiod

Description: The integral of a periodic function, with period T stays the same if the domain of integration is shifted. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgperiod.a φ A
itgperiod.b φ B
itgperiod.aleb φ A B
itgperiod.t φ T +
itgperiod.f φ F :
itgperiod.fper φ x A B F x + T = F x
itgperiod.fcn φ F A B : A B cn
Assertion itgperiod φ A + T B + T F x dx = A B F x dx

Proof

Step Hyp Ref Expression
1 itgperiod.a φ A
2 itgperiod.b φ B
3 itgperiod.aleb φ A B
4 itgperiod.t φ T +
5 itgperiod.f φ F :
6 itgperiod.fper φ x A B F x + T = F x
7 itgperiod.fcn φ F A B : A B cn
8 4 rpred φ T
9 1 2 8 3 leadd1dd φ A + T B + T
10 9 ditgpos φ A + T B + T F x dx = A + T B + T F x dx
11 1 8 readdcld φ A + T
12 2 8 readdcld φ B + T
13 5 adantr φ x A + T B + T F :
14 11 adantr φ x A + T B + T A + T
15 12 adantr φ x A + T B + T B + T
16 simpr φ x A + T B + T x A + T B + T
17 eliccre A + T B + T x A + T B + T x
18 14 15 16 17 syl3anc φ x A + T B + T x
19 13 18 ffvelrnd φ x A + T B + T F x
20 11 12 19 itgioo φ A + T B + T F x dx = A + T B + T F x dx
21 10 20 eqtr2d φ A + T B + T F x dx = A + T B + T F x dx
22 eqid y y + T = y y + T
23 8 recnd φ T
24 22 addccncf T y y + T : cn
25 23 24 syl φ y y + T : cn
26 1 2 iccssred φ A B
27 ax-resscn
28 26 27 sstrdi φ A B
29 11 12 iccssred φ A + T B + T
30 29 27 sstrdi φ A + T B + T
31 11 adantr φ y A B A + T
32 12 adantr φ y A B B + T
33 26 sselda φ y A B y
34 8 adantr φ y A B T
35 33 34 readdcld φ y A B y + T
36 1 adantr φ y A B A
37 simpr φ y A B y A B
38 2 adantr φ y A B B
39 elicc2 A B y A B y A y y B
40 36 38 39 syl2anc φ y A B y A B y A y y B
41 37 40 mpbid φ y A B y A y y B
42 41 simp2d φ y A B A y
43 36 33 34 42 leadd1dd φ y A B A + T y + T
44 41 simp3d φ y A B y B
45 33 38 34 44 leadd1dd φ y A B y + T B + T
46 31 32 35 43 45 eliccd φ y A B y + T A + T B + T
47 22 25 28 30 46 cncfmptssg φ y A B y + T : A B cn A + T B + T
48 eqeq1 w = x w = z + T x = z + T
49 48 rexbidv w = x z A B w = z + T z A B x = z + T
50 oveq1 z = y z + T = y + T
51 50 eqeq2d z = y x = z + T x = y + T
52 51 cbvrexvw z A B x = z + T y A B x = y + T
53 49 52 bitrdi w = x z A B w = z + T y A B x = y + T
54 53 cbvrabv w | z A B w = z + T = x | y A B x = y + T
55 5 ffdmd φ F : dom F
56 simp3 φ z A B w = z + T w = z + T
57 26 sselda φ z A B z
58 8 adantr φ z A B T
59 57 58 readdcld φ z A B z + T
60 59 3adant3 φ z A B w = z + T z + T
61 56 60 eqeltrd φ z A B w = z + T w
62 61 rexlimdv3a φ z A B w = z + T w
63 62 ralrimivw φ w z A B w = z + T w
64 rabss w | z A B w = z + T w z A B w = z + T w
65 63 64 sylibr φ w | z A B w = z + T
66 5 fdmd φ dom F =
67 65 66 sseqtrrd φ w | z A B w = z + T dom F
68 28 8 54 55 67 6 7 cncfperiod φ F w | z A B w = z + T : w | z A B w = z + T cn
69 49 elrab x w | z A B w = z + T x z A B x = z + T
70 simprr φ x z A B x = z + T z A B x = z + T
71 nfv z φ
72 nfv z x
73 nfre1 z z A B x = z + T
74 72 73 nfan z x z A B x = z + T
75 71 74 nfan z φ x z A B x = z + T
76 nfv z x A + T B + T
77 simp3 φ z A B x = z + T x = z + T
78 1 adantr φ z A B A
79 simpr φ z A B z A B
80 2 adantr φ z A B B
81 elicc2 A B z A B z A z z B
82 78 80 81 syl2anc φ z A B z A B z A z z B
83 79 82 mpbid φ z A B z A z z B
84 83 simp2d φ z A B A z
85 78 57 58 84 leadd1dd φ z A B A + T z + T
86 83 simp3d φ z A B z B
87 57 80 58 86 leadd1dd φ z A B z + T B + T
88 59 85 87 3jca φ z A B z + T A + T z + T z + T B + T
89 88 3adant3 φ z A B x = z + T z + T A + T z + T z + T B + T
90 11 3ad2ant1 φ z A B x = z + T A + T
91 12 3ad2ant1 φ z A B x = z + T B + T
92 elicc2 A + T B + T z + T A + T B + T z + T A + T z + T z + T B + T
93 90 91 92 syl2anc φ z A B x = z + T z + T A + T B + T z + T A + T z + T z + T B + T
94 89 93 mpbird φ z A B x = z + T z + T A + T B + T
95 77 94 eqeltrd φ z A B x = z + T x A + T B + T
96 95 3exp φ z A B x = z + T x A + T B + T
97 96 adantr φ x z A B x = z + T z A B x = z + T x A + T B + T
98 75 76 97 rexlimd φ x z A B x = z + T z A B x = z + T x A + T B + T
99 70 98 mpd φ x z A B x = z + T x A + T B + T
100 69 99 sylan2b φ x w | z A B w = z + T x A + T B + T
101 18 recnd φ x A + T B + T x
102 1 adantr φ x A + T B + T A
103 2 adantr φ x A + T B + T B
104 8 adantr φ x A + T B + T T
105 18 104 resubcld φ x A + T B + T x T
106 1 recnd φ A
107 106 23 pncand φ A + T - T = A
108 107 eqcomd φ A = A + T - T
109 108 adantr φ x A + T B + T A = A + T - T
110 elicc2 A + T B + T x A + T B + T x A + T x x B + T
111 14 15 110 syl2anc φ x A + T B + T x A + T B + T x A + T x x B + T
112 16 111 mpbid φ x A + T B + T x A + T x x B + T
113 112 simp2d φ x A + T B + T A + T x
114 14 18 104 113 lesub1dd φ x A + T B + T A + T - T x T
115 109 114 eqbrtrd φ x A + T B + T A x T
116 112 simp3d φ x A + T B + T x B + T
117 18 15 104 116 lesub1dd φ x A + T B + T x T B + T - T
118 2 recnd φ B
119 118 23 pncand φ B + T - T = B
120 119 adantr φ x A + T B + T B + T - T = B
121 117 120 breqtrd φ x A + T B + T x T B
122 102 103 105 115 121 eliccd φ x A + T B + T x T A B
123 23 adantr φ x A + T B + T T
124 101 123 npcand φ x A + T B + T x - T + T = x
125 124 eqcomd φ x A + T B + T x = x - T + T
126 oveq1 z = x T z + T = x - T + T
127 126 rspceeqv x T A B x = x - T + T z A B x = z + T
128 122 125 127 syl2anc φ x A + T B + T z A B x = z + T
129 101 128 69 sylanbrc φ x A + T B + T x w | z A B w = z + T
130 100 129 impbida φ x w | z A B w = z + T x A + T B + T
131 130 eqrdv φ w | z A B w = z + T = A + T B + T
132 131 reseq2d φ F w | z A B w = z + T = F A + T B + T
133 131 67 eqsstrrd φ A + T B + T dom F
134 55 133 feqresmpt φ F A + T B + T = x A + T B + T F x
135 132 134 eqtr2d φ x A + T B + T F x = F w | z A B w = z + T
136 1 2 8 iccshift φ A + T B + T = w | z A B w = z + T
137 136 oveq1d φ A + T B + T cn = w | z A B w = z + T cn
138 68 135 137 3eltr4d φ x A + T B + T F x : A + T B + T cn
139 ioosscn A B
140 139 a1i φ A B
141 1cnd φ 1
142 ssid
143 142 a1i φ
144 140 141 143 constcncfg φ y A B 1 : A B cn
145 fconstmpt A B × 1 = y A B 1
146 ioombl A B dom vol
147 146 a1i φ A B dom vol
148 ioovolcl A B vol A B
149 1 2 148 syl2anc φ vol A B
150 iblconst A B dom vol vol A B 1 A B × 1 𝐿 1
151 147 149 141 150 syl3anc φ A B × 1 𝐿 1
152 145 151 eqeltrrid φ y A B 1 𝐿 1
153 144 152 elind φ y A B 1 A B cn 𝐿 1
154 26 resmptd φ y y + T A B = y A B y + T
155 154 eqcomd φ y A B y + T = y y + T A B
156 155 oveq2d φ dy A B y + T d y = D y y + T A B
157 27 a1i φ
158 157 sselda φ y y
159 23 adantr φ y T
160 158 159 addcld φ y y + T
161 160 fmpttd φ y y + T :
162 ssid
163 162 a1i φ
164 eqid TopOpen fld = TopOpen fld
165 164 tgioo2 topGen ran . = TopOpen fld 𝑡
166 164 165 dvres y y + T : A B D y y + T A B = dy y + T d y int topGen ran . A B
167 157 161 163 26 166 syl22anc φ D y y + T A B = dy y + T d y int topGen ran . A B
168 156 167 eqtrd φ dy A B y + T d y = dy y + T d y int topGen ran . A B
169 iccntr A B int topGen ran . A B = A B
170 1 2 169 syl2anc φ int topGen ran . A B = A B
171 170 reseq2d φ dy y + T d y int topGen ran . A B = dy y + T d y A B
172 reelprrecn
173 172 a1i φ
174 1cnd φ y 1
175 173 dvmptid φ dy y d y = y 1
176 0cnd φ y 0
177 173 23 dvmptc φ dy T d y = y 0
178 173 158 174 175 159 176 177 dvmptadd φ dy y + T d y = y 1 + 0
179 178 reseq1d φ dy y + T d y A B = y 1 + 0 A B
180 ioossre A B
181 180 a1i φ A B
182 181 resmptd φ y 1 + 0 A B = y A B 1 + 0
183 1p0e1 1 + 0 = 1
184 183 mpteq2i y A B 1 + 0 = y A B 1
185 184 a1i φ y A B 1 + 0 = y A B 1
186 179 182 185 3eqtrd φ dy y + T d y A B = y A B 1
187 168 171 186 3eqtrd φ dy A B y + T d y = y A B 1
188 fveq2 x = y + T F x = F y + T
189 oveq1 y = A y + T = A + T
190 oveq1 y = B y + T = B + T
191 1 2 3 47 138 153 187 188 189 190 11 12 itgsubsticc φ A + T B + T F x dx = A B F y + T 1 dy
192 3 ditgpos φ A B F y + T 1 dy = A B F y + T 1 dy
193 5 adantr φ y A B F :
194 193 35 ffvelrnd φ y A B F y + T
195 1cnd φ y A B 1
196 194 195 mulcld φ y A B F y + T 1
197 1 2 196 itgioo φ A B F y + T 1 dy = A B F y + T 1 dy
198 fvoveq1 y = x F y + T = F x + T
199 198 oveq1d y = x F y + T 1 = F x + T 1
200 199 cbvitgv A B F y + T 1 dy = A B F x + T 1 dx
201 5 adantr φ x A B F :
202 26 sselda φ x A B x
203 8 adantr φ x A B T
204 202 203 readdcld φ x A B x + T
205 201 204 ffvelrnd φ x A B F x + T
206 205 mulid1d φ x A B F x + T 1 = F x + T
207 206 6 eqtrd φ x A B F x + T 1 = F x
208 207 itgeq2dv φ A B F x + T 1 dx = A B F x dx
209 200 208 syl5eq φ A B F y + T 1 dy = A B F x dx
210 192 197 209 3eqtrd φ A B F y + T 1 dy = A B F x dx
211 21 191 210 3eqtrd φ A + T B + T F x dx = A B F x dx