# Metamath Proof Explorer

Description: Integral substitution, adding a constant to the function's argument. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgsbtaddcnst.a ${⊢}{\phi }\to {A}\in ℝ$
itgsbtaddcnst.b ${⊢}{\phi }\to {B}\in ℝ$
itgsbtaddcnst.aleb ${⊢}{\phi }\to {A}\le {B}$
itgsbtaddcnst.x ${⊢}{\phi }\to {X}\in ℝ$
itgsbtaddcnst.f ${⊢}{\phi }\to {F}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ$
Assertion itgsbtaddcnst ${⊢}{\phi }\to {\int }_{\left({A}-{X}\right)}^{\left({B}-{X}\right)}{F}\left({X}+{s}\right)d{s}={\int }_{{A}}^{{B}}{F}\left({t}\right)d{t}$

### Proof

Step Hyp Ref Expression
1 itgsbtaddcnst.a ${⊢}{\phi }\to {A}\in ℝ$
2 itgsbtaddcnst.b ${⊢}{\phi }\to {B}\in ℝ$
3 itgsbtaddcnst.aleb ${⊢}{\phi }\to {A}\le {B}$
4 itgsbtaddcnst.x ${⊢}{\phi }\to {X}\in ℝ$
5 itgsbtaddcnst.f ${⊢}{\phi }\to {F}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ$
6 1 2 iccssred ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq ℝ$
7 6 sselda ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}\in ℝ$
8 7 recnd ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}\in ℂ$
9 4 recnd ${⊢}{\phi }\to {X}\in ℂ$
10 9 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {X}\in ℂ$
11 8 10 negsubd ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}+\left(-{X}\right)={t}-{X}$
12 11 eqcomd ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}-{X}={t}+\left(-{X}\right)$
13 12 mpteq2dva ${⊢}{\phi }\to \left({t}\in \left[{A},{B}\right]⟼{t}-{X}\right)=\left({t}\in \left[{A},{B}\right]⟼{t}+\left(-{X}\right)\right)$
14 1 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {A}\in ℝ$
15 4 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {X}\in ℝ$
16 14 15 resubcld ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {A}-{X}\in ℝ$
17 2 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {B}\in ℝ$
18 17 15 resubcld ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {B}-{X}\in ℝ$
19 7 15 resubcld ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}-{X}\in ℝ$
20 simpr ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}\in \left[{A},{B}\right]$
21 1 2 jca ${⊢}{\phi }\to \left({A}\in ℝ\wedge {B}\in ℝ\right)$
22 21 adantr ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to \left({A}\in ℝ\wedge {B}\in ℝ\right)$
23 elicc2 ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to \left({t}\in \left[{A},{B}\right]↔\left({t}\in ℝ\wedge {A}\le {t}\wedge {t}\le {B}\right)\right)$
24 22 23 syl ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to \left({t}\in \left[{A},{B}\right]↔\left({t}\in ℝ\wedge {A}\le {t}\wedge {t}\le {B}\right)\right)$
25 20 24 mpbid ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to \left({t}\in ℝ\wedge {A}\le {t}\wedge {t}\le {B}\right)$
26 25 simp2d ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {A}\le {t}$
27 14 7 15 26 lesub1dd ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {A}-{X}\le {t}-{X}$
28 25 simp3d ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}\le {B}$
29 7 17 15 28 lesub1dd ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}-{X}\le {B}-{X}$
30 16 18 19 27 29 eliccd ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}-{X}\in \left[{A}-{X},{B}-{X}\right]$
31 30 fmpttd ${⊢}{\phi }\to \left({t}\in \left[{A},{B}\right]⟼{t}-{X}\right):\left[{A},{B}\right]⟶\left[{A}-{X},{B}-{X}\right]$
32 13 31 feq1dd ${⊢}{\phi }\to \left({t}\in \left[{A},{B}\right]⟼{t}+\left(-{X}\right)\right):\left[{A},{B}\right]⟶\left[{A}-{X},{B}-{X}\right]$
33 1 4 resubcld ${⊢}{\phi }\to {A}-{X}\in ℝ$
34 2 4 resubcld ${⊢}{\phi }\to {B}-{X}\in ℝ$
35 33 34 iccssred ${⊢}{\phi }\to \left[{A}-{X},{B}-{X}\right]\subseteq ℝ$
36 ax-resscn ${⊢}ℝ\subseteq ℂ$
37 35 36 sstrdi ${⊢}{\phi }\to \left[{A}-{X},{B}-{X}\right]\subseteq ℂ$
38 6 36 sstrdi ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq ℂ$
39 38 resmptd ${⊢}{\phi }\to {\left({t}\in ℂ⟼{t}-{X}\right)↾}_{\left[{A},{B}\right]}=\left({t}\in \left[{A},{B}\right]⟼{t}-{X}\right)$
40 ssid ${⊢}ℂ\subseteq ℂ$
41 cncfmptid ${⊢}\left(ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left({t}\in ℂ⟼{t}\right):ℂ\underset{cn}{⟶}ℂ$
42 40 40 41 mp2an ${⊢}\left({t}\in ℂ⟼{t}\right):ℂ\underset{cn}{⟶}ℂ$
43 42 a1i ${⊢}{X}\in ℂ\to \left({t}\in ℂ⟼{t}\right):ℂ\underset{cn}{⟶}ℂ$
44 40 a1i ${⊢}{X}\in ℂ\to ℂ\subseteq ℂ$
45 id ${⊢}{X}\in ℂ\to {X}\in ℂ$
46 44 45 44 constcncfg ${⊢}{X}\in ℂ\to \left({t}\in ℂ⟼{X}\right):ℂ\underset{cn}{⟶}ℂ$
47 43 46 subcncf ${⊢}{X}\in ℂ\to \left({t}\in ℂ⟼{t}-{X}\right):ℂ\underset{cn}{⟶}ℂ$
48 9 47 syl ${⊢}{\phi }\to \left({t}\in ℂ⟼{t}-{X}\right):ℂ\underset{cn}{⟶}ℂ$
49 rescncf ${⊢}\left[{A},{B}\right]\subseteq ℂ\to \left(\left({t}\in ℂ⟼{t}-{X}\right):ℂ\underset{cn}{⟶}ℂ\to \left({\left({t}\in ℂ⟼{t}-{X}\right)↾}_{\left[{A},{B}\right]}\right):\left[{A},{B}\right]\underset{cn}{⟶}ℂ\right)$
50 38 48 49 sylc ${⊢}{\phi }\to \left({\left({t}\in ℂ⟼{t}-{X}\right)↾}_{\left[{A},{B}\right]}\right):\left[{A},{B}\right]\underset{cn}{⟶}ℂ$
51 39 50 eqeltrrd ${⊢}{\phi }\to \left({t}\in \left[{A},{B}\right]⟼{t}-{X}\right):\left[{A},{B}\right]\underset{cn}{⟶}ℂ$
52 13 51 eqeltrrd ${⊢}{\phi }\to \left({t}\in \left[{A},{B}\right]⟼{t}+\left(-{X}\right)\right):\left[{A},{B}\right]\underset{cn}{⟶}ℂ$
53 cncffvrn ${⊢}\left(\left[{A}-{X},{B}-{X}\right]\subseteq ℂ\wedge \left({t}\in \left[{A},{B}\right]⟼{t}+\left(-{X}\right)\right):\left[{A},{B}\right]\underset{cn}{⟶}ℂ\right)\to \left(\left({t}\in \left[{A},{B}\right]⟼{t}+\left(-{X}\right)\right):\left[{A},{B}\right]\underset{cn}{⟶}\left[{A}-{X},{B}-{X}\right]↔\left({t}\in \left[{A},{B}\right]⟼{t}+\left(-{X}\right)\right):\left[{A},{B}\right]⟶\left[{A}-{X},{B}-{X}\right]\right)$
54 37 52 53 syl2anc ${⊢}{\phi }\to \left(\left({t}\in \left[{A},{B}\right]⟼{t}+\left(-{X}\right)\right):\left[{A},{B}\right]\underset{cn}{⟶}\left[{A}-{X},{B}-{X}\right]↔\left({t}\in \left[{A},{B}\right]⟼{t}+\left(-{X}\right)\right):\left[{A},{B}\right]⟶\left[{A}-{X},{B}-{X}\right]\right)$
55 32 54 mpbird ${⊢}{\phi }\to \left({t}\in \left[{A},{B}\right]⟼{t}+\left(-{X}\right)\right):\left[{A},{B}\right]\underset{cn}{⟶}\left[{A}-{X},{B}-{X}\right]$
56 13 55 eqeltrd ${⊢}{\phi }\to \left({t}\in \left[{A},{B}\right]⟼{t}-{X}\right):\left[{A},{B}\right]\underset{cn}{⟶}\left[{A}-{X},{B}-{X}\right]$
57 eqid ${⊢}\left({s}\in ℂ⟼{X}+{s}\right)=\left({s}\in ℂ⟼{X}+{s}\right)$
58 9 adantr ${⊢}\left({\phi }\wedge {s}\in ℂ\right)\to {X}\in ℂ$
59 simpr ${⊢}\left({\phi }\wedge {s}\in ℂ\right)\to {s}\in ℂ$
60 58 59 addcomd ${⊢}\left({\phi }\wedge {s}\in ℂ\right)\to {X}+{s}={s}+{X}$
61 60 mpteq2dva ${⊢}{\phi }\to \left({s}\in ℂ⟼{X}+{s}\right)=\left({s}\in ℂ⟼{s}+{X}\right)$
62 eqid ${⊢}\left({s}\in ℂ⟼{s}+{X}\right)=\left({s}\in ℂ⟼{s}+{X}\right)$
63 62 addccncf ${⊢}{X}\in ℂ\to \left({s}\in ℂ⟼{s}+{X}\right):ℂ\underset{cn}{⟶}ℂ$
64 9 63 syl ${⊢}{\phi }\to \left({s}\in ℂ⟼{s}+{X}\right):ℂ\underset{cn}{⟶}ℂ$
65 61 64 eqeltrd ${⊢}{\phi }\to \left({s}\in ℂ⟼{X}+{s}\right):ℂ\underset{cn}{⟶}ℂ$
66 1 adantr ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {A}\in ℝ$
67 2 adantr ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {B}\in ℝ$
68 4 adantr ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {X}\in ℝ$
69 35 sselda ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {s}\in ℝ$
70 68 69 readdcld ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {X}+{s}\in ℝ$
71 simpr ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {s}\in \left[{A}-{X},{B}-{X}\right]$
72 33 adantr ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {A}-{X}\in ℝ$
73 34 adantr ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {B}-{X}\in ℝ$
74 elicc2 ${⊢}\left({A}-{X}\in ℝ\wedge {B}-{X}\in ℝ\right)\to \left({s}\in \left[{A}-{X},{B}-{X}\right]↔\left({s}\in ℝ\wedge {A}-{X}\le {s}\wedge {s}\le {B}-{X}\right)\right)$
75 72 73 74 syl2anc ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to \left({s}\in \left[{A}-{X},{B}-{X}\right]↔\left({s}\in ℝ\wedge {A}-{X}\le {s}\wedge {s}\le {B}-{X}\right)\right)$
76 71 75 mpbid ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to \left({s}\in ℝ\wedge {A}-{X}\le {s}\wedge {s}\le {B}-{X}\right)$
77 76 simp2d ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {A}-{X}\le {s}$
78 66 68 69 lesubadd2d ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to \left({A}-{X}\le {s}↔{A}\le {X}+{s}\right)$
79 77 78 mpbid ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {A}\le {X}+{s}$
80 76 simp3d ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {s}\le {B}-{X}$
81 68 69 67 leaddsub2d ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to \left({X}+{s}\le {B}↔{s}\le {B}-{X}\right)$
82 80 81 mpbird ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {X}+{s}\le {B}$
83 66 67 70 79 82 eliccd ${⊢}\left({\phi }\wedge {s}\in \left[{A}-{X},{B}-{X}\right]\right)\to {X}+{s}\in \left[{A},{B}\right]$
84 57 65 37 38 83 cncfmptssg ${⊢}{\phi }\to \left({s}\in \left[{A}-{X},{B}-{X}\right]⟼{X}+{s}\right):\left[{A}-{X},{B}-{X}\right]\underset{cn}{⟶}\left[{A},{B}\right]$
85 84 5 cncfcompt ${⊢}{\phi }\to \left({s}\in \left[{A}-{X},{B}-{X}\right]⟼{F}\left({X}+{s}\right)\right):\left[{A}-{X},{B}-{X}\right]\underset{cn}{⟶}ℂ$
86 ax-1cn ${⊢}1\in ℂ$
87 ioosscn ${⊢}\left({A},{B}\right)\subseteq ℂ$
88 cncfmptc ${⊢}\left(1\in ℂ\wedge \left({A},{B}\right)\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left({t}\in \left({A},{B}\right)⟼1\right):\left({A},{B}\right)\underset{cn}{⟶}ℂ$
89 86 87 40 88 mp3an ${⊢}\left({t}\in \left({A},{B}\right)⟼1\right):\left({A},{B}\right)\underset{cn}{⟶}ℂ$
90 89 a1i ${⊢}{\phi }\to \left({t}\in \left({A},{B}\right)⟼1\right):\left({A},{B}\right)\underset{cn}{⟶}ℂ$
91 fconstmpt ${⊢}\left({A},{B}\right)×\left\{1\right\}=\left({t}\in \left({A},{B}\right)⟼1\right)$
92 ioombl ${⊢}\left({A},{B}\right)\in \mathrm{dom}vol$
93 92 a1i ${⊢}{\phi }\to \left({A},{B}\right)\in \mathrm{dom}vol$
94 volioo ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {A}\le {B}\right)\to vol\left(\left({A},{B}\right)\right)={B}-{A}$
95 1 2 3 94 syl3anc ${⊢}{\phi }\to vol\left(\left({A},{B}\right)\right)={B}-{A}$
96 2 1 resubcld ${⊢}{\phi }\to {B}-{A}\in ℝ$
97 95 96 eqeltrd ${⊢}{\phi }\to vol\left(\left({A},{B}\right)\right)\in ℝ$
98 1cnd ${⊢}{\phi }\to 1\in ℂ$
99 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}$
100 93 97 98 99 syl3anc ${⊢}{\phi }\to \left({A},{B}\right)×\left\{1\right\}\in {𝐿}^{1}$
101 91 100 eqeltrrid ${⊢}{\phi }\to \left({t}\in \left({A},{B}\right)⟼1\right)\in {𝐿}^{1}$
102 90 101 elind
103 36 a1i ${⊢}{\phi }\to ℝ\subseteq ℂ$
104 19 recnd ${⊢}\left({\phi }\wedge {t}\in \left[{A},{B}\right]\right)\to {t}-{X}\in ℂ$
105 eqid ${⊢}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$
106 105 tgioo2 ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){↾}_{𝑡}ℝ$
107 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)$
108 21 107 syl ${⊢}{\phi }\to \mathrm{int}\left(\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\right)\left(\left[{A},{B}\right]\right)=\left({A},{B}\right)$
109 103 6 104 106 105 108 dvmptntr ${⊢}{\phi }\to \frac{d\left({t}\in \left[{A},{B}\right]⟼{t}-{X}\right)}{{d}_{ℝ}{t}}=\frac{d\left({t}\in \left({A},{B}\right)⟼{t}-{X}\right)}{{d}_{ℝ}{t}}$
110 reelprrecn ${⊢}ℝ\in \left\{ℝ,ℂ\right\}$
111 110 a1i ${⊢}{\phi }\to ℝ\in \left\{ℝ,ℂ\right\}$
112 ioossre ${⊢}\left({A},{B}\right)\subseteq ℝ$
113 112 sseli ${⊢}{t}\in \left({A},{B}\right)\to {t}\in ℝ$
114 113 adantl ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {t}\in ℝ$
115 114 recnd ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {t}\in ℂ$
116 1cnd ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to 1\in ℂ$
117 103 sselda ${⊢}\left({\phi }\wedge {t}\in ℝ\right)\to {t}\in ℂ$
118 1cnd ${⊢}\left({\phi }\wedge {t}\in ℝ\right)\to 1\in ℂ$
119 111 dvmptid ${⊢}{\phi }\to \frac{d\left({t}\in ℝ⟼{t}\right)}{{d}_{ℝ}{t}}=\left({t}\in ℝ⟼1\right)$
120 112 a1i ${⊢}{\phi }\to \left({A},{B}\right)\subseteq ℝ$
121 iooretop ${⊢}\left({A},{B}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
122 121 a1i ${⊢}{\phi }\to \left({A},{B}\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
123 111 117 118 119 120 106 105 122 dvmptres ${⊢}{\phi }\to \frac{d\left({t}\in \left({A},{B}\right)⟼{t}\right)}{{d}_{ℝ}{t}}=\left({t}\in \left({A},{B}\right)⟼1\right)$
124 9 adantr ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {X}\in ℂ$
125 0cnd ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to 0\in ℂ$
126 9 adantr ${⊢}\left({\phi }\wedge {t}\in ℝ\right)\to {X}\in ℂ$
127 0cnd ${⊢}\left({\phi }\wedge {t}\in ℝ\right)\to 0\in ℂ$
128 111 9 dvmptc ${⊢}{\phi }\to \frac{d\left({t}\in ℝ⟼{X}\right)}{{d}_{ℝ}{t}}=\left({t}\in ℝ⟼0\right)$
129 111 126 127 128 120 106 105 122 dvmptres ${⊢}{\phi }\to \frac{d\left({t}\in \left({A},{B}\right)⟼{X}\right)}{{d}_{ℝ}{t}}=\left({t}\in \left({A},{B}\right)⟼0\right)$
130 111 115 116 123 124 125 129 dvmptsub ${⊢}{\phi }\to \frac{d\left({t}\in \left({A},{B}\right)⟼{t}-{X}\right)}{{d}_{ℝ}{t}}=\left({t}\in \left({A},{B}\right)⟼1-0\right)$
131 116 subid1d ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to 1-0=1$
132 131 mpteq2dva ${⊢}{\phi }\to \left({t}\in \left({A},{B}\right)⟼1-0\right)=\left({t}\in \left({A},{B}\right)⟼1\right)$
133 109 130 132 3eqtrd ${⊢}{\phi }\to \frac{d\left({t}\in \left[{A},{B}\right]⟼{t}-{X}\right)}{{d}_{ℝ}{t}}=\left({t}\in \left({A},{B}\right)⟼1\right)$
134 oveq2 ${⊢}{s}={t}-{X}\to {X}+{s}={X}+{t}-{X}$
135 134 fveq2d ${⊢}{s}={t}-{X}\to {F}\left({X}+{s}\right)={F}\left({X}+{t}-{X}\right)$
136 oveq1 ${⊢}{t}={A}\to {t}-{X}={A}-{X}$
137 oveq1 ${⊢}{t}={B}\to {t}-{X}={B}-{X}$
138 1 2 3 56 85 102 133 135 136 137 33 34 itgsubsticc ${⊢}{\phi }\to {\int }_{\left({A}-{X}\right)}^{\left({B}-{X}\right)}{F}\left({X}+{s}\right)d{s}={\int }_{{A}}^{{B}}{F}\left({X}+{t}-{X}\right)\cdot 1d{t}$
139 124 115 pncan3d ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {X}+{t}-{X}={t}$
140 139 fveq2d ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {F}\left({X}+{t}-{X}\right)={F}\left({t}\right)$
141 140 oveq1d ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {F}\left({X}+{t}-{X}\right)\cdot 1={F}\left({t}\right)\cdot 1$
142 cncff ${⊢}{F}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ\to {F}:\left[{A},{B}\right]⟶ℂ$
143 5 142 syl ${⊢}{\phi }\to {F}:\left[{A},{B}\right]⟶ℂ$
144 143 adantr ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {F}:\left[{A},{B}\right]⟶ℂ$
145 ioossicc ${⊢}\left({A},{B}\right)\subseteq \left[{A},{B}\right]$
146 145 sseli ${⊢}{t}\in \left({A},{B}\right)\to {t}\in \left[{A},{B}\right]$
147 146 adantl ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {t}\in \left[{A},{B}\right]$
148 144 147 ffvelrnd ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {F}\left({t}\right)\in ℂ$
149 148 mulid1d ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {F}\left({t}\right)\cdot 1={F}\left({t}\right)$
150 141 149 eqtrd ${⊢}\left({\phi }\wedge {t}\in \left({A},{B}\right)\right)\to {F}\left({X}+{t}-{X}\right)\cdot 1={F}\left({t}\right)$
151 3 150 ditgeq3d ${⊢}{\phi }\to {\int }_{{A}}^{{B}}{F}\left({X}+{t}-{X}\right)\cdot 1d{t}={\int }_{{A}}^{{B}}{F}\left({t}\right)d{t}$
152 138 151 eqtrd ${⊢}{\phi }\to {\int }_{\left({A}-{X}\right)}^{\left({B}-{X}\right)}{F}\left({X}+{s}\right)d{s}={\int }_{{A}}^{{B}}{F}\left({t}\right)d{t}$