# Metamath Proof Explorer

## Theorem itgioocnicc

Description: The integral of a piecewise continuous function F on an open interval is equal to the integral of the continuous function G , in the corresponding closed interval. G is equal to F on the open interval, but it is continuous at the two boundaries, also. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses itgioocnicc.a ${⊢}{\phi }\to {A}\in ℝ$
itgioocnicc.b ${⊢}{\phi }\to {B}\in ℝ$
itgioocnicc.f ${⊢}{\phi }\to {F}:\mathrm{dom}{F}⟶ℂ$
itgioocnicc.fcn ${⊢}{\phi }\to \left({{F}↾}_{\left({A},{B}\right)}\right):\left({A},{B}\right)\underset{cn}{⟶}ℂ$
itgioocnicc.fdom ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq \mathrm{dom}{F}$
itgioocnicc.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({A},{B}\right)}\right){lim}_{ℂ}{A}\right)$
itgioocnicc.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left({A},{B}\right)}\right){lim}_{ℂ}{B}\right)$
itgioocnicc.g ${⊢}{G}=\left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\right)$
Assertion itgioocnicc ${⊢}{\phi }\to \left({G}\in {𝐿}^{1}\wedge {\int }_{\left[{A},{B}\right]}{G}\left({x}\right)d{x}={\int }_{\left[{A},{B}\right]}{F}\left({x}\right)d{x}\right)$

### Proof

Step Hyp Ref Expression
1 itgioocnicc.a ${⊢}{\phi }\to {A}\in ℝ$
2 itgioocnicc.b ${⊢}{\phi }\to {B}\in ℝ$
3 itgioocnicc.f ${⊢}{\phi }\to {F}:\mathrm{dom}{F}⟶ℂ$
4 itgioocnicc.fcn ${⊢}{\phi }\to \left({{F}↾}_{\left({A},{B}\right)}\right):\left({A},{B}\right)\underset{cn}{⟶}ℂ$
5 itgioocnicc.fdom ${⊢}{\phi }\to \left[{A},{B}\right]\subseteq \mathrm{dom}{F}$
6 itgioocnicc.r ${⊢}{\phi }\to {R}\in \left(\left({{F}↾}_{\left({A},{B}\right)}\right){lim}_{ℂ}{A}\right)$
7 itgioocnicc.l ${⊢}{\phi }\to {L}\in \left(\left({{F}↾}_{\left({A},{B}\right)}\right){lim}_{ℂ}{B}\right)$
8 itgioocnicc.g ${⊢}{G}=\left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\right)$
9 iftrue ${⊢}{x}={A}\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)={R}$
10 iftrue ${⊢}{x}={A}\to if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)={R}$
11 9 10 eqtr4d ${⊢}{x}={A}\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)$
12 11 adantl ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge {x}={A}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)$
13 iftrue ${⊢}{x}={B}\to if\left({x}={B},{L},{F}\left({x}\right)\right)={L}$
14 iftrue ${⊢}{x}={B}\to if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)={L}$
15 13 14 eqtr4d ${⊢}{x}={B}\to if\left({x}={B},{L},{F}\left({x}\right)\right)=if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)$
16 15 adantl ${⊢}\left(¬{x}={A}\wedge {x}={B}\right)\to if\left({x}={B},{L},{F}\left({x}\right)\right)=if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)$
17 16 ifeq2d ${⊢}\left(¬{x}={A}\wedge {x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)$
18 17 adantll ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge {x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)$
19 iffalse ${⊢}¬{x}={A}\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={B},{L},{F}\left({x}\right)\right)$
20 19 ad2antlr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={B},{L},{F}\left({x}\right)\right)$
21 iffalse ${⊢}¬{x}={B}\to if\left({x}={B},{L},{F}\left({x}\right)\right)={F}\left({x}\right)$
22 21 adantl ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to if\left({x}={B},{L},{F}\left({x}\right)\right)={F}\left({x}\right)$
23 iffalse ${⊢}¬{x}={A}\to if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)=if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)$
24 23 ad2antlr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)=if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)$
25 iffalse ${⊢}¬{x}={B}\to if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)=\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)$
26 25 adantl ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)=\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)$
27 1 adantr ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {A}\in ℝ$
28 27 rexrd ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {A}\in {ℝ}^{*}$
29 28 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to {A}\in {ℝ}^{*}$
30 2 rexrd ${⊢}{\phi }\to {B}\in {ℝ}^{*}$
31 30 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to {B}\in {ℝ}^{*}$
32 2 adantr ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {B}\in ℝ$
33 simpr ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {x}\in \left[{A},{B}\right]$
34 eliccre ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {x}\in \left[{A},{B}\right]\right)\to {x}\in ℝ$
35 27 32 33 34 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {x}\in ℝ$
36 35 ad2antrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to {x}\in ℝ$
37 1 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\to {A}\in ℝ$
38 35 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\to {x}\in ℝ$
39 30 adantr ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {B}\in {ℝ}^{*}$
40 iccgelb ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {x}\in \left[{A},{B}\right]\right)\to {A}\le {x}$
41 28 39 33 40 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {A}\le {x}$
42 41 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\to {A}\le {x}$
43 neqne ${⊢}¬{x}={A}\to {x}\ne {A}$
44 43 adantl ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\to {x}\ne {A}$
45 37 38 42 44 leneltd ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\to {A}<{x}$
46 45 adantr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to {A}<{x}$
47 35 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={B}\right)\to {x}\in ℝ$
48 2 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={B}\right)\to {B}\in ℝ$
49 iccleub ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {x}\in \left[{A},{B}\right]\right)\to {x}\le {B}$
50 28 39 33 49 syl3anc ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {x}\le {B}$
51 50 adantr ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={B}\right)\to {x}\le {B}$
52 eqcom ${⊢}{x}={B}↔{B}={x}$
53 52 notbii ${⊢}¬{x}={B}↔¬{B}={x}$
54 53 biimpi ${⊢}¬{x}={B}\to ¬{B}={x}$
55 54 neqned ${⊢}¬{x}={B}\to {B}\ne {x}$
56 55 adantl ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={B}\right)\to {B}\ne {x}$
57 47 48 51 56 leneltd ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={B}\right)\to {x}<{B}$
58 57 adantlr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to {x}<{B}$
59 29 31 36 46 58 eliood ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to {x}\in \left({A},{B}\right)$
60 fvres ${⊢}{x}\in \left({A},{B}\right)\to \left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)={F}\left({x}\right)$
61 59 60 syl ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to \left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)={F}\left({x}\right)$
62 24 26 61 3eqtrrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to {F}\left({x}\right)=if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)$
63 20 22 62 3eqtrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)$
64 18 63 pm2.61dan ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)$
65 12 64 pm2.61dan ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)$
66 65 mpteq2dva ${⊢}{\phi }\to \left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\right)=\left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)\right)$
67 8 66 syl5eq ${⊢}{\phi }\to {G}=\left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)\right)$
68 nfv ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
69 eqid ${⊢}\left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)\right)=\left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)\right)$
70 68 69 1 2 4 7 6 cncfiooicc ${⊢}{\phi }\to \left({x}\in \left[{A},{B}\right]⟼if\left({x}={A},{R},if\left({x}={B},{L},\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\right)\right)\right):\left[{A},{B}\right]\underset{cn}{⟶}ℂ$
71 67 70 eqeltrd ${⊢}{\phi }\to {G}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ$
72 cniccibl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\wedge {G}:\left[{A},{B}\right]\underset{cn}{⟶}ℂ\right)\to {G}\in {𝐿}^{1}$
73 1 2 71 72 syl3anc ${⊢}{\phi }\to {G}\in {𝐿}^{1}$
74 9 adantl ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge {x}={A}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)={R}$
75 limccl ${⊢}\left({{F}↾}_{\left({A},{B}\right)}\right){lim}_{ℂ}{A}\subseteq ℂ$
76 75 6 sseldi ${⊢}{\phi }\to {R}\in ℂ$
77 76 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge {x}={A}\right)\to {R}\in ℂ$
78 74 77 eqeltrd ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge {x}={A}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\in ℂ$
79 19 13 sylan9eq ${⊢}\left(¬{x}={A}\wedge {x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)={L}$
80 79 adantll ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge {x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)={L}$
81 limccl ${⊢}\left({{F}↾}_{\left({A},{B}\right)}\right){lim}_{ℂ}{B}\subseteq ℂ$
82 81 7 sseldi ${⊢}{\phi }\to {L}\in ℂ$
83 82 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge {x}={B}\right)\to {L}\in ℂ$
84 80 83 eqeltrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge {x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\in ℂ$
85 19 21 sylan9eq ${⊢}\left(¬{x}={A}\wedge ¬{x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)={F}\left({x}\right)$
86 85 adantll ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)={F}\left({x}\right)$
87 61 eqcomd ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to {F}\left({x}\right)=\left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)$
88 cncff ${⊢}\left({{F}↾}_{\left({A},{B}\right)}\right):\left({A},{B}\right)\underset{cn}{⟶}ℂ\to \left({{F}↾}_{\left({A},{B}\right)}\right):\left({A},{B}\right)⟶ℂ$
89 4 88 syl ${⊢}{\phi }\to \left({{F}↾}_{\left({A},{B}\right)}\right):\left({A},{B}\right)⟶ℂ$
90 89 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to \left({{F}↾}_{\left({A},{B}\right)}\right):\left({A},{B}\right)⟶ℂ$
91 90 59 ffvelrnd ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to \left({{F}↾}_{\left({A},{B}\right)}\right)\left({x}\right)\in ℂ$
92 87 91 eqeltrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to {F}\left({x}\right)\in ℂ$
93 86 92 eqeltrd ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\wedge ¬{x}={B}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\in ℂ$
94 84 93 pm2.61dan ${⊢}\left(\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\wedge ¬{x}={A}\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\in ℂ$
95 78 94 pm2.61dan ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\in ℂ$
96 8 fvmpt2 ${⊢}\left({x}\in \left[{A},{B}\right]\wedge if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)\in ℂ\right)\to {G}\left({x}\right)=if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)$
97 33 95 96 syl2anc ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {G}\left({x}\right)=if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)$
98 97 95 eqeltrd ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {G}\left({x}\right)\in ℂ$
99 1 2 98 itgioo ${⊢}{\phi }\to {\int }_{\left({A},{B}\right)}{G}\left({x}\right)d{x}={\int }_{\left[{A},{B}\right]}{G}\left({x}\right)d{x}$
100 99 eqcomd ${⊢}{\phi }\to {\int }_{\left[{A},{B}\right]}{G}\left({x}\right)d{x}={\int }_{\left({A},{B}\right)}{G}\left({x}\right)d{x}$
101 ioossicc ${⊢}\left({A},{B}\right)\subseteq \left[{A},{B}\right]$
102 101 sseli ${⊢}{x}\in \left({A},{B}\right)\to {x}\in \left[{A},{B}\right]$
103 102 97 sylan2 ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {G}\left({x}\right)=if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)$
104 1 adantr ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {A}\in ℝ$
105 eliooord ${⊢}{x}\in \left({A},{B}\right)\to \left({A}<{x}\wedge {x}<{B}\right)$
106 105 simpld ${⊢}{x}\in \left({A},{B}\right)\to {A}<{x}$
107 106 adantl ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {A}<{x}$
108 104 107 gtned ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}\ne {A}$
109 108 neneqd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to ¬{x}={A}$
110 109 19 syl ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to if\left({x}={A},{R},if\left({x}={B},{L},{F}\left({x}\right)\right)\right)=if\left({x}={B},{L},{F}\left({x}\right)\right)$
111 102 35 sylan2 ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}\in ℝ$
112 105 simprd ${⊢}{x}\in \left({A},{B}\right)\to {x}<{B}$
113 112 adantl ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}<{B}$
114 111 113 ltned ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {x}\ne {B}$
115 114 neneqd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to ¬{x}={B}$
116 115 21 syl ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to if\left({x}={B},{L},{F}\left({x}\right)\right)={F}\left({x}\right)$
117 103 110 116 3eqtrd ${⊢}\left({\phi }\wedge {x}\in \left({A},{B}\right)\right)\to {G}\left({x}\right)={F}\left({x}\right)$
118 117 itgeq2dv ${⊢}{\phi }\to {\int }_{\left({A},{B}\right)}{G}\left({x}\right)d{x}={\int }_{\left({A},{B}\right)}{F}\left({x}\right)d{x}$
119 3 adantr ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {F}:\mathrm{dom}{F}⟶ℂ$
120 5 sselda ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {x}\in \mathrm{dom}{F}$
121 119 120 ffvelrnd ${⊢}\left({\phi }\wedge {x}\in \left[{A},{B}\right]\right)\to {F}\left({x}\right)\in ℂ$
122 1 2 121 itgioo ${⊢}{\phi }\to {\int }_{\left({A},{B}\right)}{F}\left({x}\right)d{x}={\int }_{\left[{A},{B}\right]}{F}\left({x}\right)d{x}$
123 100 118 122 3eqtrd ${⊢}{\phi }\to {\int }_{\left[{A},{B}\right]}{G}\left({x}\right)d{x}={\int }_{\left[{A},{B}\right]}{F}\left({x}\right)d{x}$
124 73 123 jca ${⊢}{\phi }\to \left({G}\in {𝐿}^{1}\wedge {\int }_{\left[{A},{B}\right]}{G}\left({x}\right)d{x}={\int }_{\left[{A},{B}\right]}{F}\left({x}\right)d{x}\right)$