# 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 ${⊢}{\phi }\to {A}\in ℝ$
itgperiod.b ${⊢}{\phi }\to {B}\in ℝ$
itgperiod.aleb ${⊢}{\phi }\to {A}\le {B}$
itgperiod.t ${⊢}{\phi }\to {T}\in {ℝ}^{+}$
itgperiod.f ${⊢}{\phi }\to {F}:ℝ⟶ℂ$
itgperiod.fper ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {F}\left({x}+{T}\right)={F}\left({x}\right)$
itgperiod.fcn ${⊢}{\phi }\to \left({{F}↾}_{\left[{A},{B}\right]}\right):\left[{A},{B}\right]\underset{cn}{⟶}ℂ$
Assertion itgperiod ${⊢}{\phi }\to {\int }_{\left[{A}+{T},{B}+{T}\right]}{F}\left({x}\right)d{x}={\int }_{\left[{A},{B}\right]}{F}\left({x}\right)d{x}$

### Proof

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