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 
|- ( ph -> A e. RR )
itgioocnicc.b 
|- ( ph -> B e. RR )
itgioocnicc.f 
|- ( ph -> F : dom F --> CC )
itgioocnicc.fcn 
|- ( ph -> ( F |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
itgioocnicc.fdom 
|- ( ph -> ( A [,] B ) C_ dom F )
itgioocnicc.r 
|- ( ph -> R e. ( ( F |` ( A (,) B ) ) limCC A ) )
itgioocnicc.l 
|- ( ph -> L e. ( ( F |` ( A (,) B ) ) limCC B ) )
itgioocnicc.g 
|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
Assertion itgioocnicc 
|- ( ph -> ( G e. L^1 /\ S. ( A [,] B ) ( G ` x ) _d x = S. ( A [,] B ) ( F ` x ) _d x ) )

Proof

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