Metamath Proof Explorer

Theorem fourierdlem82

Description: Integral by substitution, adding a constant to the function's argument, for a function on an open interval with finite limits ad boundary points. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem82.1 
|- G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) )
fourierdlem82.2 
|- ( ph -> A e. RR )
fourierdlem82.3 
|- ( ph -> B e. RR )
fourierdlem82.4 
|- ( ph -> A < B )
fourierdlem82.5 
|- ( ph -> F : ( A [,] B ) --> CC )
fourierdlem82.6 
|- ( ph -> ( F |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
fourierdlem82.7 
|- ( ph -> L e. ( F limCC B ) )
fourierdlem82.8 
|- ( ph -> R e. ( F limCC A ) )
fourierdlem82.9 
|- ( ph -> X e. RR )
Assertion fourierdlem82 
|- ( ph -> S. ( A [,] B ) ( F ` t ) _d t = S. ( ( A - X ) [,] ( B - X ) ) ( F ` ( X + t ) ) _d t )

Proof

Step Hyp Ref Expression
1 fourierdlem82.1 
 |-  G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) )
2 fourierdlem82.2 
 |-  ( ph -> A e. RR )
3 fourierdlem82.3 
 |-  ( ph -> B e. RR )
4 fourierdlem82.4 
 |-  ( ph -> A < B )
5 fourierdlem82.5 
 |-  ( ph -> F : ( A [,] B ) --> CC )
6 fourierdlem82.6 
 |-  ( ph -> ( F |` ( A (,) B ) ) e. ( ( A (,) B ) -cn-> CC ) )
7 fourierdlem82.7 
 |-  ( ph -> L e. ( F limCC B ) )
8 fourierdlem82.8 
 |-  ( ph -> R e. ( F limCC A ) )
9 fourierdlem82.9 
 |-  ( ph -> X e. RR )
10 2 3 4 ltled 
 |-  ( ph -> A <_ B )
11 2 3 9 10 lesub1dd 
 |-  ( ph -> ( A - X ) <_ ( B - X ) )
12 11 ditgpos 
 |-  ( ph -> S_ [ ( A - X ) -> ( B - X ) ] ( G ` ( X + t ) ) _d t = S. ( ( A - X ) (,) ( B - X ) ) ( G ` ( X + t ) ) _d t )
13 iftrue 
 |-  ( x = A -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = R )
14 13 adantl 
 |-  ( ( ph /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = R )
15 iftrue 
 |-  ( x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
16 15 adantl 
 |-  ( ( ph /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = R )
17 14 16 eqtr4d 
 |-  ( ( ph /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
18 17 adantlr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ x = A ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
19 iffalse 
 |-  ( -. x = A -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) )
20 iftrue 
 |-  ( x = B -> if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) = L )
21 19 20 sylan9eq 
 |-  ( ( -. x = A /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = L )
22 21 adantll 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = L )
23 iffalse 
 |-  ( -. x = A -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( x = B , L , ( F ` x ) ) )
24 iftrue 
 |-  ( x = B -> if ( x = B , L , ( F ` x ) ) = L )
25 23 24 sylan9eq 
 |-  ( ( -. x = A /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = L )
26 25 adantll 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = L )
27 22 26 eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ x = B ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
28 iffalse 
 |-  ( -. x = B -> if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) = ( ( F |` ( A (,) B ) ) ` x ) )
29 28 adantl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) = ( ( F |` ( A (,) B ) ) ` x ) )
30 19 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 ) ) )
31 iffalse 
 |-  ( -. x = B -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
32 31 adantl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = B , L , ( F ` x ) ) = ( F ` x ) )
33 23 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 ) ) )
34 2 rexrd 
 |-  ( ph -> A e. RR* )
35 34 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A e. RR* )
36 3 rexrd 
 |-  ( ph -> B e. RR* )
37 36 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> B e. RR* )
38 2 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A e. RR )
39 3 adantr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> B e. RR )
40 simpr 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. ( A [,] B ) )
41 eliccre 
 |-  ( ( A e. RR /\ B e. RR /\ x e. ( A [,] B ) ) -> x e. RR )
42 38 39 40 41 syl3anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x e. RR )
43 42 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. RR )
44 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> A e. RR )
45 42 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> x e. RR )
46 elicc2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
47 38 39 46 syl2anc 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. ( A [,] B ) <-> ( x e. RR /\ A <_ x /\ x <_ B ) ) )
48 40 47 mpbid 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( x e. RR /\ A <_ x /\ x <_ B ) )
49 48 simp2d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> A <_ x )
50 49 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> A <_ x )
51 neqne 
 |-  ( -. x = A -> x =/= A )
52 51 adantl 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> x =/= A )
53 44 45 50 52 leneltd 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> A < x )
54 53 adantr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> A < x )
55 42 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> x e. RR )
56 3 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> B e. RR )
57 48 simp3d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> x <_ B )
58 57 adantr 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> x <_ B )
59 nesym 
 |-  ( B =/= x <-> -. x = B )
60 59 biimpri 
 |-  ( -. x = B -> B =/= x )
61 60 adantl 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> B =/= x )
62 55 56 58 61 leneltd 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = B ) -> x < B )
63 62 adantlr 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x < B )
64 35 37 43 54 63 eliood 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> x e. ( A (,) B ) )
65 fvres 
 |-  ( x e. ( A (,) B ) -> ( ( F |` ( A (,) B ) ) ` x ) = ( F ` x ) )
66 64 65 syl 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> ( ( F |` ( A (,) B ) ) ` x ) = ( F ` x ) )
67 32 33 66 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( ( F |` ( A (,) B ) ) ` x ) )
68 29 30 67 3eqtr4d 
 |-  ( ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) /\ -. x = B ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
69 27 68 pm2.61dan 
 |-  ( ( ( ph /\ x e. ( A [,] B ) ) /\ -. x = A ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
70 18 69 pm2.61dan 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) )
71 70 mpteq2dva 
 |-  ( ph -> ( 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 ` x ) ) ) ) )
72 1 71 eqtrid 
 |-  ( ph -> G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
73 72 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) ) )
74 eqeq1 
 |-  ( x = ( X + t ) -> ( x = A <-> ( X + t ) = A ) )
75 eqeq1 
 |-  ( x = ( X + t ) -> ( x = B <-> ( X + t ) = B ) )
76 fveq2 
 |-  ( x = ( X + t ) -> ( F ` x ) = ( F ` ( X + t ) ) )
77 75 76 ifbieq2d 
 |-  ( x = ( X + t ) -> if ( x = B , L , ( F ` x ) ) = if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) )
78 74 77 ifbieq2d 
 |-  ( x = ( X + t ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = if ( ( X + t ) = A , R , if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) ) )
79 2 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> A e. RR )
80 simpr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> t e. ( ( A - X ) (,) ( B - X ) ) )
81 2 9 resubcld 
 |-  ( ph -> ( A - X ) e. RR )
82 81 rexrd 
 |-  ( ph -> ( A - X ) e. RR* )
83 82 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( A - X ) e. RR* )
84 3 9 resubcld 
 |-  ( ph -> ( B - X ) e. RR )
85 84 rexrd 
 |-  ( ph -> ( B - X ) e. RR* )
86 85 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( B - X ) e. RR* )
87 elioo2 
 |-  ( ( ( A - X ) e. RR* /\ ( B - X ) e. RR* ) -> ( t e. ( ( A - X ) (,) ( B - X ) ) <-> ( t e. RR /\ ( A - X ) < t /\ t < ( B - X ) ) ) )
88 83 86 87 syl2anc 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( t e. ( ( A - X ) (,) ( B - X ) ) <-> ( t e. RR /\ ( A - X ) < t /\ t < ( B - X ) ) ) )
89 80 88 mpbid 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( t e. RR /\ ( A - X ) < t /\ t < ( B - X ) ) )
90 89 simp2d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( A - X ) < t )
91 9 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> X e. RR )
92 89 simp1d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> t e. RR )
93 79 91 92 ltsubadd2d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( ( A - X ) < t <-> A < ( X + t ) ) )
94 90 93 mpbid 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> A < ( X + t ) )
95 79 94 gtned 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) =/= A )
96 95 neneqd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> -. ( X + t ) = A )
97 96 iffalsed 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> if ( ( X + t ) = A , R , if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) ) = if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) )
98 91 92 readdcld 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) e. RR )
99 89 simp3d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> t < ( B - X ) )
100 3 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> B e. RR )
101 91 92 100 ltaddsub2d 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( ( X + t ) < B <-> t < ( B - X ) ) )
102 99 101 mpbird 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) < B )
103 98 102 ltned 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) =/= B )
104 103 neneqd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> -. ( X + t ) = B )
105 104 iffalsed 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) = ( F ` ( X + t ) ) )
106 97 105 eqtrd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> if ( ( X + t ) = A , R , if ( ( X + t ) = B , L , ( F ` ( X + t ) ) ) ) = ( F ` ( X + t ) ) )
107 78 106 sylan9eqr 
 |-  ( ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) /\ x = ( X + t ) ) -> if ( x = A , R , if ( x = B , L , ( F ` x ) ) ) = ( F ` ( X + t ) ) )
108 79 98 94 ltled 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> A <_ ( X + t ) )
109 98 100 102 ltled 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) <_ B )
110 79 100 98 108 109 eliccd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) e. ( A [,] B ) )
111 5 ffund 
 |-  ( ph -> Fun F )
112 111 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> Fun F )
113 5 fdmd 
 |-  ( ph -> dom F = ( A [,] B ) )
114 113 eqcomd 
 |-  ( ph -> ( A [,] B ) = dom F )
115 114 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( A [,] B ) = dom F )
116 110 115 eleqtrd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( X + t ) e. dom F )
117 fvelrn 
 |-  ( ( Fun F /\ ( X + t ) e. dom F ) -> ( F ` ( X + t ) ) e. ran F )
118 112 116 117 syl2anc 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( F ` ( X + t ) ) e. ran F )
119 73 107 110 118 fvmptd 
 |-  ( ( ph /\ t e. ( ( A - X ) (,) ( B - X ) ) ) -> ( G ` ( X + t ) ) = ( F ` ( X + t ) ) )
120 119 itgeq2dv 
 |-  ( ph -> S. ( ( A - X ) (,) ( B - X ) ) ( G ` ( X + t ) ) _d t = S. ( ( A - X ) (,) ( B - X ) ) ( F ` ( X + t ) ) _d t )
121 5 frnd 
 |-  ( ph -> ran F C_ CC )
122 121 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ran F C_ CC )
123 111 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> Fun F )
124 2 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> A e. RR )
125 3 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> B e. RR )
126 9 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> X e. RR )
127 81 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A - X ) e. RR )
128 84 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( B - X ) e. RR )
129 simpr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> t e. ( ( A - X ) [,] ( B - X ) ) )
130 eliccre 
 |-  ( ( ( A - X ) e. RR /\ ( B - X ) e. RR /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> t e. RR )
131 127 128 129 130 syl3anc 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> t e. RR )
132 126 131 readdcld 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + t ) e. RR )
133 elicc2 
 |-  ( ( ( A - X ) e. RR /\ ( B - X ) e. RR ) -> ( t e. ( ( A - X ) [,] ( B - X ) ) <-> ( t e. RR /\ ( A - X ) <_ t /\ t <_ ( B - X ) ) ) )
134 127 128 133 syl2anc 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( t e. ( ( A - X ) [,] ( B - X ) ) <-> ( t e. RR /\ ( A - X ) <_ t /\ t <_ ( B - X ) ) ) )
135 129 134 mpbid 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( t e. RR /\ ( A - X ) <_ t /\ t <_ ( B - X ) ) )
136 135 simp2d 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A - X ) <_ t )
137 124 126 131 lesubadd2d 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( ( A - X ) <_ t <-> A <_ ( X + t ) ) )
138 136 137 mpbid 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> A <_ ( X + t ) )
139 135 simp3d 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> t <_ ( B - X ) )
140 126 131 125 leaddsub2d 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( ( X + t ) <_ B <-> t <_ ( B - X ) ) )
141 139 140 mpbird 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + t ) <_ B )
142 124 125 132 138 141 eliccd 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + t ) e. ( A [,] B ) )
143 114 adantr 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( A [,] B ) = dom F )
144 142 143 eleqtrd 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( X + t ) e. dom F )
145 123 144 117 syl2anc 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( F ` ( X + t ) ) e. ran F )
146 122 145 sseldd 
 |-  ( ( ph /\ t e. ( ( A - X ) [,] ( B - X ) ) ) -> ( F ` ( X + t ) ) e. CC )
147 81 84 146 itgioo 
 |-  ( ph -> S. ( ( A - X ) (,) ( B - X ) ) ( F ` ( X + t ) ) _d t = S. ( ( A - X ) [,] ( B - X ) ) ( F ` ( X + t ) ) _d t )
148 12 120 147 3eqtrrd 
 |-  ( ph -> S. ( ( A - X ) [,] ( B - X ) ) ( F ` ( X + t ) ) _d t = S_ [ ( A - X ) -> ( B - X ) ] ( G ` ( X + t ) ) _d t )
149 nfv 
 |-  F/ x ph
150 2 3 4 5 limcicciooub 
 |-  ( ph -> ( ( F |` ( A (,) B ) ) limCC B ) = ( F limCC B ) )
151 7 150 eleqtrrd 
 |-  ( ph -> L e. ( ( F |` ( A (,) B ) ) limCC B ) )
152 2 3 4 5 limciccioolb 
 |-  ( ph -> ( ( F |` ( A (,) B ) ) limCC A ) = ( F limCC A ) )
153 8 152 eleqtrrd 
 |-  ( ph -> R e. ( ( F |` ( A (,) B ) ) limCC A ) )
154 149 1 2 3 6 151 153 cncfiooicc 
 |-  ( ph -> G e. ( ( A [,] B ) -cn-> CC ) )
155 2 3 10 9 154 itgsbtaddcnst 
 |-  ( ph -> S_ [ ( A - X ) -> ( B - X ) ] ( G ` ( X + t ) ) _d t = S_ [ A -> B ] ( G ` s ) _d s )
156 10 ditgpos 
 |-  ( ph -> S_ [ A -> B ] ( G ` s ) _d s = S. ( A (,) B ) ( G ` s ) _d s )
157 fveq2 
 |-  ( s = t -> ( G ` s ) = ( G ` t ) )
158 157 cbvitgv 
 |-  S. ( A (,) B ) ( G ` s ) _d s = S. ( A (,) B ) ( G ` t ) _d t
159 1 a1i 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> G = ( x e. ( A [,] B ) |-> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) ) )
160 2 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> A e. RR )
161 simplr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> t e. ( A (,) B ) )
162 34 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> A e. RR* )
163 36 ad2antrr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> B e. RR* )
164 elioo2 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( t e. ( A (,) B ) <-> ( t e. RR /\ A < t /\ t < B ) ) )
165 162 163 164 syl2anc 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( t e. ( A (,) B ) <-> ( t e. RR /\ A < t /\ t < B ) ) )
166 161 165 mpbid 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( t e. RR /\ A < t /\ t < B ) )
167 166 simp2d 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> A < t )
168 simpr 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x = t )
169 167 168 breqtrrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> A < x )
170 160 169 gtned 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x =/= A )
171 170 neneqd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> -. x = A )
172 171 iffalsed 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) )
173 166 simp1d 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> t e. RR )
174 168 173 eqeltrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x e. RR )
175 166 simp3d 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> t < B )
176 168 175 eqbrtrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x < B )
177 174 176 ltned 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x =/= B )
178 177 neneqd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> -. x = B )
179 178 iffalsed 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) = ( ( F |` ( A (,) B ) ) ` x ) )
180 168 161 eqeltrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> x e. ( A (,) B ) )
181 180 65 syl 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( ( F |` ( A (,) B ) ) ` x ) = ( F ` x ) )
182 fveq2 
 |-  ( x = t -> ( F ` x ) = ( F ` t ) )
183 182 adantl 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( F ` x ) = ( F ` t ) )
184 181 183 eqtrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> ( ( F |` ( A (,) B ) ) ` x ) = ( F ` t ) )
185 172 179 184 3eqtrd 
 |-  ( ( ( ph /\ t e. ( A (,) B ) ) /\ x = t ) -> if ( x = A , R , if ( x = B , L , ( ( F |` ( A (,) B ) ) ` x ) ) ) = ( F ` t ) )
186 ioossicc 
 |-  ( A (,) B ) C_ ( A [,] B )
187 simpr 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> t e. ( A (,) B ) )
188 186 187 sselid 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> t e. ( A [,] B ) )
189 111 adantr 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> Fun F )
190 114 adantr 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( A [,] B ) = dom F )
191 188 190 eleqtrd 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> t e. dom F )
192 fvelrn 
 |-  ( ( Fun F /\ t e. dom F ) -> ( F ` t ) e. ran F )
193 189 191 192 syl2anc 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( F ` t ) e. ran F )
194 159 185 188 193 fvmptd 
 |-  ( ( ph /\ t e. ( A (,) B ) ) -> ( G ` t ) = ( F ` t ) )
195 194 itgeq2dv 
 |-  ( ph -> S. ( A (,) B ) ( G ` t ) _d t = S. ( A (,) B ) ( F ` t ) _d t )
196 158 195 eqtrid 
 |-  ( ph -> S. ( A (,) B ) ( G ` s ) _d s = S. ( A (,) B ) ( F ` t ) _d t )
197 5 ffvelcdmda 
 |-  ( ( ph /\ t e. ( A [,] B ) ) -> ( F ` t ) e. CC )
198 2 3 197 itgioo 
 |-  ( ph -> S. ( A (,) B ) ( F ` t ) _d t = S. ( A [,] B ) ( F ` t ) _d t )
199 156 196 198 3eqtrd 
 |-  ( ph -> S_ [ A -> B ] ( G ` s ) _d s = S. ( A [,] B ) ( F ` t ) _d t )
200 148 155 199 3eqtrrd 
 |-  ( ph -> S. ( A [,] B ) ( F ` t ) _d t = S. ( ( A - X ) [,] ( B - X ) ) ( F ` ( X + t ) ) _d t )