Metamath Proof Explorer

Theorem areaquad

Description: The area of a quadrilateral with two sides which are parallel to the y-axis in ( RR X. RR ) is its width multiplied by the average height of its higher edge minus the average height of its lower edge. Co-author TA. (Contributed by Jon Pennant, 31-May-2019)

Ref Expression
Hypotheses areaquad.1 
|- A e. RR
areaquad.2 
|- B e. RR
areaquad.3 
|- C e. RR
areaquad.4 
|- D e. RR
areaquad.5 
|- E e. RR
areaquad.6 
|- F e. RR
areaquad.7 
|- A < B
areaquad.8 
|- C <_ E
areaquad.9 
|- D <_ F
areaquad.10 
|- U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
areaquad.11 
|- V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
areaquad.12 
|- S = { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }
Assertion areaquad 
|- ( area ` S ) = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )

Proof

Step Hyp Ref Expression
1 areaquad.1 
 |-  A e. RR
2 areaquad.2 
 |-  B e. RR
3 areaquad.3 
 |-  C e. RR
4 areaquad.4 
 |-  D e. RR
5 areaquad.5 
 |-  E e. RR
6 areaquad.6 
 |-  F e. RR
7 areaquad.7 
 |-  A < B
8 areaquad.8 
 |-  C <_ E
9 areaquad.9 
 |-  D <_ F
10 areaquad.10 
 |-  U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
11 areaquad.11 
 |-  V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
12 areaquad.12 
 |-  S = { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }
13 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
14 1 2 13 mp2an 
 |-  ( A [,] B ) C_ RR
15 14 sseli 
 |-  ( x e. ( A [,] B ) -> x e. RR )
16 15 adantr 
 |-  ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> x e. RR )
17 3 recni 
 |-  C e. CC
18 17 a1i 
 |-  ( x e. RR -> C e. CC )
19 resubcl 
 |-  ( ( x e. RR /\ A e. RR ) -> ( x - A ) e. RR )
20 1 19 mpan2 
 |-  ( x e. RR -> ( x - A ) e. RR )
21 2 1 resubcli 
 |-  ( B - A ) e. RR
22 21 a1i 
 |-  ( x e. RR -> ( B - A ) e. RR )
23 2 recni 
 |-  B e. CC
24 23 a1i 
 |-  ( A e. RR -> B e. CC )
25 recn 
 |-  ( A e. RR -> A e. CC )
26 1 7 gtneii 
 |-  B =/= A
27 26 a1i 
 |-  ( A e. RR -> B =/= A )
28 24 25 27 subne0d 
 |-  ( A e. RR -> ( B - A ) =/= 0 )
29 1 28 ax-mp 
 |-  ( B - A ) =/= 0
30 29 a1i 
 |-  ( x e. RR -> ( B - A ) =/= 0 )
31 20 22 30 redivcld 
 |-  ( x e. RR -> ( ( x - A ) / ( B - A ) ) e. RR )
32 31 recnd 
 |-  ( x e. RR -> ( ( x - A ) / ( B - A ) ) e. CC )
33 4 recni 
 |-  D e. CC
34 33 a1i 
 |-  ( x e. RR -> D e. CC )
35 32 34 mulcld 
 |-  ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. D ) e. CC )
36 32 18 mulcld 
 |-  ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. C ) e. CC )
37 18 35 36 addsub12d 
 |-  ( x e. RR -> ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
38 32 34 18 subdid 
 |-  ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) = ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
39 38 oveq2d 
 |-  ( x e. RR -> ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) = ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
40 10 39 syl5eq 
 |-  ( x e. RR -> U = ( C + ( ( ( ( x - A ) / ( B - A ) ) x. D ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
41 1cnd 
 |-  ( x e. RR -> 1 e. CC )
42 41 32 18 subdird 
 |-  ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( ( 1 x. C ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
43 17 mulid2i 
 |-  ( 1 x. C ) = C
44 43 oveq1i 
 |-  ( ( 1 x. C ) - ( ( ( x - A ) / ( B - A ) ) x. C ) ) = ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) )
45 42 44 eqtrdi 
 |-  ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) )
46 45 oveq2d 
 |-  ( x e. RR -> ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) ) = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( C - ( ( ( x - A ) / ( B - A ) ) x. C ) ) ) )
47 37 40 46 3eqtr4d 
 |-  ( x e. RR -> U = ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) ) )
48 1red 
 |-  ( x e. RR -> 1 e. RR )
49 48 31 resubcld 
 |-  ( x e. RR -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. RR )
50 49 recnd 
 |-  ( x e. RR -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. CC )
51 50 18 mulcld 
 |-  ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) e. CC )
52 35 51 addcomd 
 |-  ( x e. RR -> ( ( ( ( x - A ) / ( B - A ) ) x. D ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) ) = ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) + ( ( ( x - A ) / ( B - A ) ) x. D ) ) )
53 50 18 mulcomd 
 |-  ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) = ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
54 32 34 mulcomd 
 |-  ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. D ) = ( D x. ( ( x - A ) / ( B - A ) ) ) )
55 53 54 oveq12d 
 |-  ( x e. RR -> ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. C ) + ( ( ( x - A ) / ( B - A ) ) x. D ) ) = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) )
56 47 52 55 3eqtrd 
 |-  ( x e. RR -> U = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) )
57 3 a1i 
 |-  ( x e. RR -> C e. RR )
58 57 49 remulcld 
 |-  ( x e. RR -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
59 4 a1i 
 |-  ( x e. RR -> D e. RR )
60 59 31 remulcld 
 |-  ( x e. RR -> ( D x. ( ( x - A ) / ( B - A ) ) ) e. RR )
61 58 60 readdcld 
 |-  ( x e. RR -> ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) e. RR )
62 56 61 eqeltrd 
 |-  ( x e. RR -> U e. RR )
63 5 recni 
 |-  E e. CC
64 63 a1i 
 |-  ( x e. RR -> E e. CC )
65 6 recni 
 |-  F e. CC
66 65 a1i 
 |-  ( x e. RR -> F e. CC )
67 32 66 mulcld 
 |-  ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. F ) e. CC )
68 32 64 mulcld 
 |-  ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. E ) e. CC )
69 64 67 68 addsub12d 
 |-  ( x e. RR -> ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
70 32 66 64 subdid 
 |-  ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) = ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
71 70 oveq2d 
 |-  ( x e. RR -> ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) = ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
72 11 71 syl5eq 
 |-  ( x e. RR -> V = ( E + ( ( ( ( x - A ) / ( B - A ) ) x. F ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
73 41 32 64 subdird 
 |-  ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( ( 1 x. E ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
74 63 mulid2i 
 |-  ( 1 x. E ) = E
75 74 oveq1i 
 |-  ( ( 1 x. E ) - ( ( ( x - A ) / ( B - A ) ) x. E ) ) = ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) )
76 73 75 eqtrdi 
 |-  ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) )
77 76 oveq2d 
 |-  ( x e. RR -> ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) ) = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( E - ( ( ( x - A ) / ( B - A ) ) x. E ) ) ) )
78 69 72 77 3eqtr4d 
 |-  ( x e. RR -> V = ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) ) )
79 50 64 mulcld 
 |-  ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) e. CC )
80 67 79 addcomd 
 |-  ( x e. RR -> ( ( ( ( x - A ) / ( B - A ) ) x. F ) + ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) ) = ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) + ( ( ( x - A ) / ( B - A ) ) x. F ) ) )
81 50 64 mulcomd 
 |-  ( x e. RR -> ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) = ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
82 32 66 mulcomd 
 |-  ( x e. RR -> ( ( ( x - A ) / ( B - A ) ) x. F ) = ( F x. ( ( x - A ) / ( B - A ) ) ) )
83 81 82 oveq12d 
 |-  ( x e. RR -> ( ( ( 1 - ( ( x - A ) / ( B - A ) ) ) x. E ) + ( ( ( x - A ) / ( B - A ) ) x. F ) ) = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
84 78 80 83 3eqtrd 
 |-  ( x e. RR -> V = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
85 5 a1i 
 |-  ( x e. RR -> E e. RR )
86 85 49 remulcld 
 |-  ( x e. RR -> ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
87 6 a1i 
 |-  ( x e. RR -> F e. RR )
88 87 31 remulcld 
 |-  ( x e. RR -> ( F x. ( ( x - A ) / ( B - A ) ) ) e. RR )
89 86 88 readdcld 
 |-  ( x e. RR -> ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) e. RR )
90 84 89 eqeltrd 
 |-  ( x e. RR -> V e. RR )
91 iccssre 
 |-  ( ( U e. RR /\ V e. RR ) -> ( U [,] V ) C_ RR )
92 62 90 91 syl2anc 
 |-  ( x e. RR -> ( U [,] V ) C_ RR )
93 15 92 syl 
 |-  ( x e. ( A [,] B ) -> ( U [,] V ) C_ RR )
94 93 sselda 
 |-  ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> y e. RR )
95 16 94 jca 
 |-  ( ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) -> ( x e. RR /\ y e. RR ) )
96 95 ssopab2i 
 |-  { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) } C_ { <. x , y >. | ( x e. RR /\ y e. RR ) }
97 df-xp 
 |-  ( RR X. RR ) = { <. x , y >. | ( x e. RR /\ y e. RR ) }
98 96 12 97 3sstr4i 
 |-  S C_ ( RR X. RR )
99 iftrue 
 |-  ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( V - U ) )
100 nfv 
 |-  F/ y x e. ( A [,] B )
101 nfopab2 
 |-  F/_ y { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) }
102 12 101 nfcxfr 
 |-  F/_ y S
103 nfcv 
 |-  F/_ y { x }
104 102 103 nfima 
 |-  F/_ y ( S " { x } )
105 nfcv 
 |-  F/_ y ( U [,] V )
106 vex 
 |-  x e. _V
107 vex 
 |-  y e. _V
108 106 107 elimasn 
 |-  ( y e. ( S " { x } ) <-> <. x , y >. e. S )
109 12 eleq2i 
 |-  ( <. x , y >. e. S <-> <. x , y >. e. { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) } )
110 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) } <-> ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) )
111 108 109 110 3bitri 
 |-  ( y e. ( S " { x } ) <-> ( x e. ( A [,] B ) /\ y e. ( U [,] V ) ) )
112 111 baib 
 |-  ( x e. ( A [,] B ) -> ( y e. ( S " { x } ) <-> y e. ( U [,] V ) ) )
113 100 104 105 112 eqrd 
 |-  ( x e. ( A [,] B ) -> ( S " { x } ) = ( U [,] V ) )
114 113 fveq2d 
 |-  ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` ( U [,] V ) ) )
115 15 62 syl 
 |-  ( x e. ( A [,] B ) -> U e. RR )
116 15 90 syl 
 |-  ( x e. ( A [,] B ) -> V e. RR )
117 iccmbl 
 |-  ( ( U e. RR /\ V e. RR ) -> ( U [,] V ) e. dom vol )
118 115 116 117 syl2anc 
 |-  ( x e. ( A [,] B ) -> ( U [,] V ) e. dom vol )
119 mblvol 
 |-  ( ( U [,] V ) e. dom vol -> ( vol ` ( U [,] V ) ) = ( vol* ` ( U [,] V ) ) )
120 118 119 syl 
 |-  ( x e. ( A [,] B ) -> ( vol ` ( U [,] V ) ) = ( vol* ` ( U [,] V ) ) )
121 15 58 syl 
 |-  ( x e. ( A [,] B ) -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
122 15 60 syl 
 |-  ( x e. ( A [,] B ) -> ( D x. ( ( x - A ) / ( B - A ) ) ) e. RR )
123 15 86 syl 
 |-  ( x e. ( A [,] B ) -> ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) e. RR )
124 15 88 syl 
 |-  ( x e. ( A [,] B ) -> ( F x. ( ( x - A ) / ( B - A ) ) ) e. RR )
125 3 a1i 
 |-  ( x e. ( A [,] B ) -> C e. RR )
126 5 a1i 
 |-  ( x e. ( A [,] B ) -> E e. RR )
127 15 49 syl 
 |-  ( x e. ( A [,] B ) -> ( 1 - ( ( x - A ) / ( B - A ) ) ) e. RR )
128 15 31 syl 
 |-  ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) e. RR )
129 128 recnd 
 |-  ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) e. CC )
130 129 subidd 
 |-  ( x e. ( A [,] B ) -> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) ) = 0 )
131 1red 
 |-  ( x e. ( A [,] B ) -> 1 e. RR )
132 2 a1i 
 |-  ( x e. ( A [,] B ) -> B e. RR )
133 1 a1i 
 |-  ( x e. ( A [,] B ) -> A e. RR )
134 1 rexri 
 |-  A e. RR*
135 2 rexri 
 |-  B e. RR*
136 iccleub 
 |-  ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> x <_ B )
137 134 135 136 mp3an12 
 |-  ( x e. ( A [,] B ) -> x <_ B )
138 15 132 133 137 lesub1dd 
 |-  ( x e. ( A [,] B ) -> ( x - A ) <_ ( B - A ) )
139 15 1 19 sylancl 
 |-  ( x e. ( A [,] B ) -> ( x - A ) e. RR )
140 21 a1i 
 |-  ( x e. ( A [,] B ) -> ( B - A ) e. RR )
141 1 recni 
 |-  A e. CC
142 141 subidi 
 |-  ( A - A ) = 0
143 133 132 133 ltsub1d 
 |-  ( x e. ( A [,] B ) -> ( A < B <-> ( A - A ) < ( B - A ) ) )
144 7 143 mpbii 
 |-  ( x e. ( A [,] B ) -> ( A - A ) < ( B - A ) )
145 142 144 eqbrtrrid 
 |-  ( x e. ( A [,] B ) -> 0 < ( B - A ) )
146 lediv1 
 |-  ( ( ( x - A ) e. RR /\ ( B - A ) e. RR /\ ( ( B - A ) e. RR /\ 0 < ( B - A ) ) ) -> ( ( x - A ) <_ ( B - A ) <-> ( ( x - A ) / ( B - A ) ) <_ ( ( B - A ) / ( B - A ) ) ) )
147 139 140 140 145 146 syl112anc 
 |-  ( x e. ( A [,] B ) -> ( ( x - A ) <_ ( B - A ) <-> ( ( x - A ) / ( B - A ) ) <_ ( ( B - A ) / ( B - A ) ) ) )
148 138 147 mpbid 
 |-  ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) <_ ( ( B - A ) / ( B - A ) ) )
149 21 recni 
 |-  ( B - A ) e. CC
150 149 29 dividi 
 |-  ( ( B - A ) / ( B - A ) ) = 1
151 148 150 breqtrdi 
 |-  ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) <_ 1 )
152 128 131 128 151 lesub1dd 
 |-  ( x e. ( A [,] B ) -> ( ( ( x - A ) / ( B - A ) ) - ( ( x - A ) / ( B - A ) ) ) <_ ( 1 - ( ( x - A ) / ( B - A ) ) ) )
153 130 152 eqbrtrrd 
 |-  ( x e. ( A [,] B ) -> 0 <_ ( 1 - ( ( x - A ) / ( B - A ) ) ) )
154 8 a1i 
 |-  ( x e. ( A [,] B ) -> C <_ E )
155 125 126 127 153 154 lemul1ad 
 |-  ( x e. ( A [,] B ) -> ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) <_ ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) )
156 4 a1i 
 |-  ( x e. ( A [,] B ) -> D e. RR )
157 6 a1i 
 |-  ( x e. ( A [,] B ) -> F e. RR )
158 140 145 elrpd 
 |-  ( x e. ( A [,] B ) -> ( B - A ) e. RR+ )
159 iccgelb 
 |-  ( ( A e. RR* /\ B e. RR* /\ x e. ( A [,] B ) ) -> A <_ x )
160 134 135 159 mp3an12 
 |-  ( x e. ( A [,] B ) -> A <_ x )
161 133 15 133 160 lesub1dd 
 |-  ( x e. ( A [,] B ) -> ( A - A ) <_ ( x - A ) )
162 142 161 eqbrtrrid 
 |-  ( x e. ( A [,] B ) -> 0 <_ ( x - A ) )
163 139 158 162 divge0d 
 |-  ( x e. ( A [,] B ) -> 0 <_ ( ( x - A ) / ( B - A ) ) )
164 9 a1i 
 |-  ( x e. ( A [,] B ) -> D <_ F )
165 156 157 128 163 164 lemul1ad 
 |-  ( x e. ( A [,] B ) -> ( D x. ( ( x - A ) / ( B - A ) ) ) <_ ( F x. ( ( x - A ) / ( B - A ) ) ) )
166 121 122 123 124 155 165 le2addd 
 |-  ( x e. ( A [,] B ) -> ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) <_ ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
167 15 56 syl 
 |-  ( x e. ( A [,] B ) -> U = ( ( C x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( D x. ( ( x - A ) / ( B - A ) ) ) ) )
168 15 84 syl 
 |-  ( x e. ( A [,] B ) -> V = ( ( E x. ( 1 - ( ( x - A ) / ( B - A ) ) ) ) + ( F x. ( ( x - A ) / ( B - A ) ) ) ) )
169 166 167 168 3brtr4d 
 |-  ( x e. ( A [,] B ) -> U <_ V )
170 ovolicc 
 |-  ( ( U e. RR /\ V e. RR /\ U <_ V ) -> ( vol* ` ( U [,] V ) ) = ( V - U ) )
171 115 116 169 170 syl3anc 
 |-  ( x e. ( A [,] B ) -> ( vol* ` ( U [,] V ) ) = ( V - U ) )
172 114 120 171 3eqtrd 
 |-  ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( V - U ) )
173 99 172 eqtr4d 
 |-  ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) ) )
174 iffalse 
 |-  ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = 0 )
175 nfv 
 |-  F/ y -. x e. ( A [,] B )
176 nfcv 
 |-  F/_ y (/)
177 111 simplbi 
 |-  ( y e. ( S " { x } ) -> x e. ( A [,] B ) )
178 noel 
 |-  -. y e. (/)
179 178 pm2.21i 
 |-  ( y e. (/) -> x e. ( A [,] B ) )
180 177 179 pm5.21ni 
 |-  ( -. x e. ( A [,] B ) -> ( y e. ( S " { x } ) <-> y e. (/) ) )
181 175 104 176 180 eqrd 
 |-  ( -. x e. ( A [,] B ) -> ( S " { x } ) = (/) )
182 181 fveq2d 
 |-  ( -. x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = ( vol ` (/) ) )
183 0mbl 
 |-  (/) e. dom vol
184 mblvol 
 |-  ( (/) e. dom vol -> ( vol ` (/) ) = ( vol* ` (/) ) )
185 183 184 ax-mp 
 |-  ( vol ` (/) ) = ( vol* ` (/) )
186 ovol0 
 |-  ( vol* ` (/) ) = 0
187 185 186 eqtri 
 |-  ( vol ` (/) ) = 0
188 182 187 eqtrdi 
 |-  ( -. x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) = 0 )
189 174 188 eqtr4d 
 |-  ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) ) )
190 173 189 pm2.61i 
 |-  if ( x e. ( A [,] B ) , ( V - U ) , 0 ) = ( vol ` ( S " { x } ) )
191 190 eqcomi 
 |-  ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 )
192 90 62 resubcld 
 |-  ( x e. RR -> ( V - U ) e. RR )
193 0re 
 |-  0 e. RR
194 ifcl 
 |-  ( ( ( V - U ) e. RR /\ 0 e. RR ) -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) e. RR )
195 192 193 194 sylancl 
 |-  ( x e. RR -> if ( x e. ( A [,] B ) , ( V - U ) , 0 ) e. RR )
196 191 195 eqeltrid 
 |-  ( x e. RR -> ( vol ` ( S " { x } ) ) e. RR )
197 volf 
 |-  vol : dom vol --> ( 0 [,] +oo )
198 ffun 
 |-  ( vol : dom vol --> ( 0 [,] +oo ) -> Fun vol )
199 197 198 ax-mp 
 |-  Fun vol
200 iftrue 
 |-  ( x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) = ( U [,] V ) )
201 113 200 eqtr4d 
 |-  ( x e. ( A [,] B ) -> ( S " { x } ) = if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) )
202 iffalse 
 |-  ( -. x e. ( A [,] B ) -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) = (/) )
203 181 202 eqtr4d 
 |-  ( -. x e. ( A [,] B ) -> ( S " { x } ) = if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) )
204 201 203 pm2.61i 
 |-  ( S " { x } ) = if ( x e. ( A [,] B ) , ( U [,] V ) , (/) )
205 62 90 117 syl2anc 
 |-  ( x e. RR -> ( U [,] V ) e. dom vol )
206 183 a1i 
 |-  ( x e. RR -> (/) e. dom vol )
207 205 206 ifcld 
 |-  ( x e. RR -> if ( x e. ( A [,] B ) , ( U [,] V ) , (/) ) e. dom vol )
208 204 207 eqeltrid 
 |-  ( x e. RR -> ( S " { x } ) e. dom vol )
209 fvimacnv 
 |-  ( ( Fun vol /\ ( S " { x } ) e. dom vol ) -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) ) )
210 199 208 209 sylancr 
 |-  ( x e. RR -> ( ( vol ` ( S " { x } ) ) e. RR <-> ( S " { x } ) e. ( `' vol " RR ) ) )
211 196 210 mpbid 
 |-  ( x e. RR -> ( S " { x } ) e. ( `' vol " RR ) )
212 211 rgen 
 |-  A. x e. RR ( S " { x } ) e. ( `' vol " RR )
213 14 a1i 
 |-  ( 0 e. RR -> ( A [,] B ) C_ RR )
214 rembl 
 |-  RR e. dom vol
215 214 a1i 
 |-  ( 0 e. RR -> RR e. dom vol )
216 116 115 resubcld 
 |-  ( x e. ( A [,] B ) -> ( V - U ) e. RR )
217 172 216 eqeltrd 
 |-  ( x e. ( A [,] B ) -> ( vol ` ( S " { x } ) ) e. RR )
218 217 adantl 
 |-  ( ( 0 e. RR /\ x e. ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) e. RR )
219 eldifn 
 |-  ( x e. ( RR \ ( A [,] B ) ) -> -. x e. ( A [,] B ) )
220 219 188 syl 
 |-  ( x e. ( RR \ ( A [,] B ) ) -> ( vol ` ( S " { x } ) ) = 0 )
221 220 adantl 
 |-  ( ( 0 e. RR /\ x e. ( RR \ ( A [,] B ) ) ) -> ( vol ` ( S " { x } ) ) = 0 )
222 172 mpteq2ia 
 |-  ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) = ( x e. ( A [,] B ) |-> ( V - U ) )
223 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
224 223 subcn 
 |-  - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
225 224 a1i 
 |-  ( T. -> - e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
226 11 mpteq2i 
 |-  ( x e. ( A [,] B ) |-> V ) = ( x e. ( A [,] B ) |-> ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) )
227 223 addcn 
 |-  + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) )
228 227 a1i 
 |-  ( T. -> + e. ( ( ( TopOpen ` CCfld ) tX ( TopOpen ` CCfld ) ) Cn ( TopOpen ` CCfld ) ) )
229 ax-resscn 
 |-  RR C_ CC
230 14 229 sstri 
 |-  ( A [,] B ) C_ CC
231 ssid 
 |-  CC C_ CC
232 cncfmptc 
 |-  ( ( E e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC ) )
233 63 230 231 232 mp3an 
 |-  ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC )
234 233 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC ) )
235 230 sseli 
 |-  ( x e. ( A [,] B ) -> x e. CC )
236 141 a1i 
 |-  ( x e. ( A [,] B ) -> A e. CC )
237 149 a1i 
 |-  ( x e. ( A [,] B ) -> ( B - A ) e. CC )
238 29 a1i 
 |-  ( x e. ( A [,] B ) -> ( B - A ) =/= 0 )
239 235 236 237 238 divsubdird 
 |-  ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) = ( ( x / ( B - A ) ) - ( A / ( B - A ) ) ) )
240 239 adantl 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> ( ( x - A ) / ( B - A ) ) = ( ( x / ( B - A ) ) - ( A / ( B - A ) ) ) )
241 240 mpteq2dva 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) = ( x e. ( A [,] B ) |-> ( ( x / ( B - A ) ) - ( A / ( B - A ) ) ) ) )
242 resmpt 
 |-  ( ( A [,] B ) C_ CC -> ( ( x e. CC |-> ( x / ( B - A ) ) ) |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( x / ( B - A ) ) ) )
243 230 242 ax-mp 
 |-  ( ( x e. CC |-> ( x / ( B - A ) ) ) |` ( A [,] B ) ) = ( x e. ( A [,] B ) |-> ( x / ( B - A ) ) )
244 eqid 
 |-  ( x e. CC |-> ( x / ( B - A ) ) ) = ( x e. CC |-> ( x / ( B - A ) ) )
245 244 divccncf 
 |-  ( ( ( B - A ) e. CC /\ ( B - A ) =/= 0 ) -> ( x e. CC |-> ( x / ( B - A ) ) ) e. ( CC -cn-> CC ) )
246 149 29 245 mp2an 
 |-  ( x e. CC |-> ( x / ( B - A ) ) ) e. ( CC -cn-> CC )
247 rescncf 
 |-  ( ( A [,] B ) C_ CC -> ( ( x e. CC |-> ( x / ( B - A ) ) ) e. ( CC -cn-> CC ) -> ( ( x e. CC |-> ( x / ( B - A ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) )
248 230 246 247 mp2 
 |-  ( ( x e. CC |-> ( x / ( B - A ) ) ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC )
249 243 248 eqeltrri 
 |-  ( x e. ( A [,] B ) |-> ( x / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC )
250 249 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( x / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
251 141 149 29 divcli 
 |-  ( A / ( B - A ) ) e. CC
252 cncfmptc 
 |-  ( ( ( A / ( B - A ) ) e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> ( A / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
253 251 230 231 252 mp3an 
 |-  ( x e. ( A [,] B ) |-> ( A / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC )
254 253 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( A / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
255 223 225 250 254 cncfmpt2f 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( ( x / ( B - A ) ) - ( A / ( B - A ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
256 241 255 eqeltrd 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
257 cncfmptc 
 |-  ( ( F e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> F ) e. ( ( A [,] B ) -cn-> CC ) )
258 65 230 231 257 mp3an 
 |-  ( x e. ( A [,] B ) |-> F ) e. ( ( A [,] B ) -cn-> CC )
259 258 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> F ) e. ( ( A [,] B ) -cn-> CC ) )
260 223 225 259 234 cncfmpt2f 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( F - E ) ) e. ( ( A [,] B ) -cn-> CC ) )
261 256 260 mulcncf 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
262 223 228 234 261 cncfmpt2f 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
263 226 262 eqeltrid 
 |-  ( T. -> ( x e. ( A [,] B ) |-> V ) e. ( ( A [,] B ) -cn-> CC ) )
264 10 mpteq2i 
 |-  ( x e. ( A [,] B ) |-> U ) = ( x e. ( A [,] B ) |-> ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) )
265 cncfmptc 
 |-  ( ( C e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) )
266 17 230 231 265 mp3an 
 |-  ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC )
267 266 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) )
268 cncfmptc 
 |-  ( ( D e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> D ) e. ( ( A [,] B ) -cn-> CC ) )
269 33 230 231 268 mp3an 
 |-  ( x e. ( A [,] B ) |-> D ) e. ( ( A [,] B ) -cn-> CC )
270 269 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> D ) e. ( ( A [,] B ) -cn-> CC ) )
271 223 225 270 267 cncfmpt2f 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( D - C ) ) e. ( ( A [,] B ) -cn-> CC ) )
272 256 271 mulcncf 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
273 223 228 267 272 cncfmpt2f 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) ) e. ( ( A [,] B ) -cn-> CC ) )
274 264 273 eqeltrid 
 |-  ( T. -> ( x e. ( A [,] B ) |-> U ) e. ( ( A [,] B ) -cn-> CC ) )
275 223 225 263 274 cncfmpt2f 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) )
276 275 mptru 
 |-  ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC )
277 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( V - U ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1 )
278 1 2 276 277 mp3an 
 |-  ( x e. ( A [,] B ) |-> ( V - U ) ) e. L^1
279 222 278 eqeltri 
 |-  ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1
280 279 a1i 
 |-  ( 0 e. RR -> ( x e. ( A [,] B ) |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
281 213 215 218 221 280 iblss2 
 |-  ( 0 e. RR -> ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 )
282 193 281 ax-mp 
 |-  ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1
283 dmarea 
 |-  ( S e. dom area <-> ( S C_ ( RR X. RR ) /\ A. x e. RR ( S " { x } ) e. ( `' vol " RR ) /\ ( x e. RR |-> ( vol ` ( S " { x } ) ) ) e. L^1 ) )
284 98 212 282 283 mpbir3an 
 |-  S e. dom area
285 areaval 
 |-  ( S e. dom area -> ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x )
286 284 285 ax-mp 
 |-  ( area ` S ) = S. RR ( vol ` ( S " { x } ) ) _d x
287 itgeq2 
 |-  ( A. x e. RR ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 ) -> S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x )
288 191 a1i 
 |-  ( x e. RR -> ( vol ` ( S " { x } ) ) = if ( x e. ( A [,] B ) , ( V - U ) , 0 ) )
289 287 288 mprg 
 |-  S. RR ( vol ` ( S " { x } ) ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x
290 itgss2 
 |-  ( ( A [,] B ) C_ RR -> S. ( A [,] B ) ( V - U ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x )
291 14 290 ax-mp 
 |-  S. ( A [,] B ) ( V - U ) _d x = S. RR if ( x e. ( A [,] B ) , ( V - U ) , 0 ) _d x
292 65 63 addcli 
 |-  ( F + E ) e. CC
293 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
294 div32 
 |-  ( ( ( F + E ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC ) -> ( ( ( F + E ) / 2 ) x. ( B - A ) ) = ( ( F + E ) x. ( ( B - A ) / 2 ) ) )
295 292 293 149 294 mp3an 
 |-  ( ( ( F + E ) / 2 ) x. ( B - A ) ) = ( ( F + E ) x. ( ( B - A ) / 2 ) )
296 33 17 addcli 
 |-  ( D + C ) e. CC
297 div32 
 |-  ( ( ( D + C ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC ) -> ( ( ( D + C ) / 2 ) x. ( B - A ) ) = ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
298 296 293 149 297 mp3an 
 |-  ( ( ( D + C ) / 2 ) x. ( B - A ) ) = ( ( D + C ) x. ( ( B - A ) / 2 ) )
299 295 298 oveq12i 
 |-  ( ( ( ( F + E ) / 2 ) x. ( B - A ) ) - ( ( ( D + C ) / 2 ) x. ( B - A ) ) ) = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
300 2cn 
 |-  2 e. CC
301 2ne0 
 |-  2 =/= 0
302 292 300 301 divcli 
 |-  ( ( F + E ) / 2 ) e. CC
303 296 300 301 divcli 
 |-  ( ( D + C ) / 2 ) e. CC
304 302 303 149 subdiri 
 |-  ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) ) = ( ( ( ( F + E ) / 2 ) x. ( B - A ) ) - ( ( ( D + C ) / 2 ) x. ( B - A ) ) )
305 116 adantl 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> V e. RR )
306 263 mptru 
 |-  ( x e. ( A [,] B ) |-> V ) e. ( ( A [,] B ) -cn-> CC )
307 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> V ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> V ) e. L^1 )
308 1 2 306 307 mp3an 
 |-  ( x e. ( A [,] B ) |-> V ) e. L^1
309 308 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> V ) e. L^1 )
310 115 adantl 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> U e. RR )
311 274 mptru 
 |-  ( x e. ( A [,] B ) |-> U ) e. ( ( A [,] B ) -cn-> CC )
312 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> U ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> U ) e. L^1 )
313 1 2 311 312 mp3an 
 |-  ( x e. ( A [,] B ) |-> U ) e. L^1
314 313 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> U ) e. L^1 )
315 305 309 310 314 itgsub 
 |-  ( T. -> S. ( A [,] B ) ( V - U ) _d x = ( S. ( A [,] B ) V _d x - S. ( A [,] B ) U _d x ) )
316 315 mptru 
 |-  S. ( A [,] B ) ( V - U ) _d x = ( S. ( A [,] B ) V _d x - S. ( A [,] B ) U _d x )
317 63 300 301 divcan4i 
 |-  ( ( E x. 2 ) / 2 ) = E
318 317 oveq1i 
 |-  ( ( ( E x. 2 ) / 2 ) x. ( B - A ) ) = ( E x. ( B - A ) )
319 63 300 mulcli 
 |-  ( E x. 2 ) e. CC
320 div32 
 |-  ( ( ( E x. 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC ) -> ( ( ( E x. 2 ) / 2 ) x. ( B - A ) ) = ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) )
321 319 293 149 320 mp3an 
 |-  ( ( ( E x. 2 ) / 2 ) x. ( B - A ) ) = ( ( E x. 2 ) x. ( ( B - A ) / 2 ) )
322 318 321 eqtr3i 
 |-  ( E x. ( B - A ) ) = ( ( E x. 2 ) x. ( ( B - A ) / 2 ) )
323 322 oveq1i 
 |-  ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) ) = ( ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
324 itgeq2 
 |-  ( A. x e. ( A [,] B ) V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) -> S. ( A [,] B ) V _d x = S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x )
325 11 a1i 
 |-  ( x e. ( A [,] B ) -> V = ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) )
326 324 325 mprg 
 |-  S. ( A [,] B ) V _d x = S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x
327 5 a1i 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> E e. RR )
328 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> E ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> E ) e. L^1 )
329 1 2 233 328 mp3an 
 |-  ( x e. ( A [,] B ) |-> E ) e. L^1
330 329 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> E ) e. L^1 )
331 128 adantl 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> ( ( x - A ) / ( B - A ) ) e. RR )
332 6 a1i 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> F e. RR )
333 332 327 resubcld 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> ( F - E ) e. RR )
334 331 333 remulcld 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) e. RR )
335 261 mptru 
 |-  ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. ( ( A [,] B ) -cn-> CC )
336 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. L^1 )
337 1 2 335 336 mp3an 
 |-  ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. L^1
338 337 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) e. L^1 )
339 327 330 334 338 itgadd 
 |-  ( T. -> S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x = ( S. ( A [,] B ) E _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x ) )
340 339 mptru 
 |-  S. ( A [,] B ) ( E + ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) ) _d x = ( S. ( A [,] B ) E _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x )
341 iccmbl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) e. dom vol )
342 1 2 341 mp2an 
 |-  ( A [,] B ) e. dom vol
343 mblvol 
 |-  ( ( A [,] B ) e. dom vol -> ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) ) )
344 342 343 ax-mp 
 |-  ( vol ` ( A [,] B ) ) = ( vol* ` ( A [,] B ) )
345 1 2 7 ltleii 
 |-  A <_ B
346 ovolicc 
 |-  ( ( A e. RR /\ B e. RR /\ A <_ B ) -> ( vol* ` ( A [,] B ) ) = ( B - A ) )
347 1 2 345 346 mp3an 
 |-  ( vol* ` ( A [,] B ) ) = ( B - A )
348 344 347 eqtri 
 |-  ( vol ` ( A [,] B ) ) = ( B - A )
349 348 21 eqeltri 
 |-  ( vol ` ( A [,] B ) ) e. RR
350 itgconst 
 |-  ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ E e. CC ) -> S. ( A [,] B ) E _d x = ( E x. ( vol ` ( A [,] B ) ) ) )
351 342 349 63 350 mp3an 
 |-  S. ( A [,] B ) E _d x = ( E x. ( vol ` ( A [,] B ) ) )
352 348 oveq2i 
 |-  ( E x. ( vol ` ( A [,] B ) ) ) = ( E x. ( B - A ) )
353 351 352 eqtri 
 |-  S. ( A [,] B ) E _d x = ( E x. ( B - A ) )
354 65 a1i 
 |-  ( T. -> F e. CC )
355 63 a1i 
 |-  ( T. -> E e. CC )
356 354 355 subcld 
 |-  ( T. -> ( F - E ) e. CC )
357 256 mptru 
 |-  ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC )
358 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. L^1 )
359 1 2 357 358 mp3an 
 |-  ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. L^1
360 359 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( ( x - A ) / ( B - A ) ) ) e. L^1 )
361 356 331 360 itgmulc2 
 |-  ( T. -> ( ( F - E ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x ) = S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x )
362 361 mptru 
 |-  ( ( F - E ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x ) = S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x
363 itgeq2 
 |-  ( A. x e. ( A [,] B ) ( ( x - A ) / ( B - A ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) ) -> S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x )
364 139 recnd 
 |-  ( x e. ( A [,] B ) -> ( x - A ) e. CC )
365 364 237 238 divrec2d 
 |-  ( x e. ( A [,] B ) -> ( ( x - A ) / ( B - A ) ) = ( ( 1 / ( B - A ) ) x. ( x - A ) ) )
366 363 365 mprg 
 |-  S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x
367 15 adantl 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> x e. RR )
368 cncfmptid 
 |-  ( ( ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) )
369 230 231 368 mp2an 
 |-  ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC )
370 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> x ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> x ) e. L^1 )
371 1 2 369 370 mp3an 
 |-  ( x e. ( A [,] B ) |-> x ) e. L^1
372 371 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> x ) e. L^1 )
373 1 a1i 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> A e. RR )
374 cncfmptc 
 |-  ( ( A e. CC /\ ( A [,] B ) C_ CC /\ CC C_ CC ) -> ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC ) )
375 141 230 231 374 mp3an 
 |-  ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC )
376 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> A ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> A ) e. L^1 )
377 1 2 375 376 mp3an 
 |-  ( x e. ( A [,] B ) |-> A ) e. L^1
378 377 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> A ) e. L^1 )
379 367 372 373 378 itgsub 
 |-  ( T. -> S. ( A [,] B ) ( x - A ) _d x = ( S. ( A [,] B ) x _d x - S. ( A [,] B ) A _d x ) )
380 379 mptru 
 |-  S. ( A [,] B ) ( x - A ) _d x = ( S. ( A [,] B ) x _d x - S. ( A [,] B ) A _d x )
381 1 a1i 
 |-  ( T. -> A e. RR )
382 2 a1i 
 |-  ( T. -> B e. RR )
383 345 a1i 
 |-  ( T. -> A <_ B )
384 1nn0 
 |-  1 e. NN0
385 384 a1i 
 |-  ( T. -> 1 e. NN0 )
386 381 382 383 385 itgpowd 
 |-  ( T. -> S. ( A [,] B ) ( x ^ 1 ) _d x = ( ( ( B ^ ( 1 + 1 ) ) - ( A ^ ( 1 + 1 ) ) ) / ( 1 + 1 ) ) )
387 386 mptru 
 |-  S. ( A [,] B ) ( x ^ 1 ) _d x = ( ( ( B ^ ( 1 + 1 ) ) - ( A ^ ( 1 + 1 ) ) ) / ( 1 + 1 ) )
388 1p1e2 
 |-  ( 1 + 1 ) = 2
389 388 oveq2i 
 |-  ( ( ( B ^ ( 1 + 1 ) ) - ( A ^ ( 1 + 1 ) ) ) / ( 1 + 1 ) ) = ( ( ( B ^ ( 1 + 1 ) ) - ( A ^ ( 1 + 1 ) ) ) / 2 )
390 387 389 eqtri 
 |-  S. ( A [,] B ) ( x ^ 1 ) _d x = ( ( ( B ^ ( 1 + 1 ) ) - ( A ^ ( 1 + 1 ) ) ) / 2 )
391 itgeq2 
 |-  ( A. x e. ( A [,] B ) ( x ^ 1 ) = x -> S. ( A [,] B ) ( x ^ 1 ) _d x = S. ( A [,] B ) x _d x )
392 235 exp1d 
 |-  ( x e. ( A [,] B ) -> ( x ^ 1 ) = x )
393 391 392 mprg 
 |-  S. ( A [,] B ) ( x ^ 1 ) _d x = S. ( A [,] B ) x _d x
394 388 oveq2i 
 |-  ( B ^ ( 1 + 1 ) ) = ( B ^ 2 )
395 388 oveq2i 
 |-  ( A ^ ( 1 + 1 ) ) = ( A ^ 2 )
396 394 395 oveq12i 
 |-  ( ( B ^ ( 1 + 1 ) ) - ( A ^ ( 1 + 1 ) ) ) = ( ( B ^ 2 ) - ( A ^ 2 ) )
397 396 oveq1i 
 |-  ( ( ( B ^ ( 1 + 1 ) ) - ( A ^ ( 1 + 1 ) ) ) / 2 ) = ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 )
398 390 393 397 3eqtr3i 
 |-  S. ( A [,] B ) x _d x = ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 )
399 itgconst 
 |-  ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ A e. CC ) -> S. ( A [,] B ) A _d x = ( A x. ( vol ` ( A [,] B ) ) ) )
400 342 349 141 399 mp3an 
 |-  S. ( A [,] B ) A _d x = ( A x. ( vol ` ( A [,] B ) ) )
401 348 oveq2i 
 |-  ( A x. ( vol ` ( A [,] B ) ) ) = ( A x. ( B - A ) )
402 400 401 eqtri 
 |-  S. ( A [,] B ) A _d x = ( A x. ( B - A ) )
403 398 402 oveq12i 
 |-  ( S. ( A [,] B ) x _d x - S. ( A [,] B ) A _d x ) = ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) )
404 380 403 eqtri 
 |-  S. ( A [,] B ) ( x - A ) _d x = ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) )
405 404 oveq2i 
 |-  ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x ) = ( ( 1 / ( B - A ) ) x. ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) ) )
406 23 a1i 
 |-  ( T. -> B e. CC )
407 141 a1i 
 |-  ( T. -> A e. CC )
408 406 407 subcld 
 |-  ( T. -> ( B - A ) e. CC )
409 26 a1i 
 |-  ( T. -> B =/= A )
410 406 407 409 subne0d 
 |-  ( T. -> ( B - A ) =/= 0 )
411 408 410 reccld 
 |-  ( T. -> ( 1 / ( B - A ) ) e. CC )
412 411 mptru 
 |-  ( 1 / ( B - A ) ) e. CC
413 23 sqcli 
 |-  ( B ^ 2 ) e. CC
414 141 sqcli 
 |-  ( A ^ 2 ) e. CC
415 413 414 subcli 
 |-  ( ( B ^ 2 ) - ( A ^ 2 ) ) e. CC
416 415 300 301 divcli 
 |-  ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) e. CC
417 141 149 mulcli 
 |-  ( A x. ( B - A ) ) e. CC
418 412 416 417 subdii 
 |-  ( ( 1 / ( B - A ) ) x. ( ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) - ( A x. ( B - A ) ) ) ) = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) )
419 405 418 eqtri 
 |-  ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x ) = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) )
420 139 adantl 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> ( x - A ) e. RR )
421 367 372 373 378 iblsub 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( x - A ) ) e. L^1 )
422 411 420 421 itgmulc2 
 |-  ( T. -> ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x ) = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x )
423 422 mptru 
 |-  ( ( 1 / ( B - A ) ) x. S. ( A [,] B ) ( x - A ) _d x ) = S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x
424 412 417 mulcomi 
 |-  ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) = ( ( A x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
425 417 149 29 divreci 
 |-  ( ( A x. ( B - A ) ) / ( B - A ) ) = ( ( A x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
426 141 149 29 divcan4i 
 |-  ( ( A x. ( B - A ) ) / ( B - A ) ) = A
427 424 425 426 3eqtr2i 
 |-  ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) = A
428 427 oveq2i 
 |-  ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - ( ( 1 / ( B - A ) ) x. ( A x. ( B - A ) ) ) ) = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
429 419 423 428 3eqtr3i 
 |-  S. ( A [,] B ) ( ( 1 / ( B - A ) ) x. ( x - A ) ) _d x = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
430 366 429 eqtri 
 |-  S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A )
431 23 141 subsqi 
 |-  ( ( B ^ 2 ) - ( A ^ 2 ) ) = ( ( B + A ) x. ( B - A ) )
432 431 oveq1i 
 |-  ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) = ( ( ( B + A ) x. ( B - A ) ) / 2 )
433 432 oveq2i 
 |-  ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) = ( ( 1 / ( B - A ) ) x. ( ( ( B + A ) x. ( B - A ) ) / 2 ) )
434 431 415 eqeltrri 
 |-  ( ( B + A ) x. ( B - A ) ) e. CC
435 412 434 300 301 divassi 
 |-  ( ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) / 2 ) = ( ( 1 / ( B - A ) ) x. ( ( ( B + A ) x. ( B - A ) ) / 2 ) )
436 412 434 mulcomi 
 |-  ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) = ( ( ( B + A ) x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
437 434 149 29 divreci 
 |-  ( ( ( B + A ) x. ( B - A ) ) / ( B - A ) ) = ( ( ( B + A ) x. ( B - A ) ) x. ( 1 / ( B - A ) ) )
438 23 141 addcli 
 |-  ( B + A ) e. CC
439 438 149 29 divcan4i 
 |-  ( ( ( B + A ) x. ( B - A ) ) / ( B - A ) ) = ( B + A )
440 436 437 439 3eqtr2i 
 |-  ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) = ( B + A )
441 440 oveq1i 
 |-  ( ( ( 1 / ( B - A ) ) x. ( ( B + A ) x. ( B - A ) ) ) / 2 ) = ( ( B + A ) / 2 )
442 433 435 441 3eqtr2i 
 |-  ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) = ( ( B + A ) / 2 )
443 442 oveq1i 
 |-  ( ( ( 1 / ( B - A ) ) x. ( ( ( B ^ 2 ) - ( A ^ 2 ) ) / 2 ) ) - A ) = ( ( ( B + A ) / 2 ) - A )
444 141 300 mulcli 
 |-  ( A x. 2 ) e. CC
445 divsubdir 
 |-  ( ( ( B + A ) e. CC /\ ( A x. 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) ) )
446 438 444 293 445 mp3an 
 |-  ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) )
447 23 141 444 addsubassi 
 |-  ( ( B + A ) - ( A x. 2 ) ) = ( B + ( A - ( A x. 2 ) ) )
448 subsub2 
 |-  ( ( B e. CC /\ ( A x. 2 ) e. CC /\ A e. CC ) -> ( B - ( ( A x. 2 ) - A ) ) = ( B + ( A - ( A x. 2 ) ) ) )
449 23 444 141 448 mp3an 
 |-  ( B - ( ( A x. 2 ) - A ) ) = ( B + ( A - ( A x. 2 ) ) )
450 141 times2i 
 |-  ( A x. 2 ) = ( A + A )
451 450 oveq1i 
 |-  ( ( A x. 2 ) - A ) = ( ( A + A ) - A )
452 141 141 pncan3oi 
 |-  ( ( A + A ) - A ) = A
453 451 452 eqtri 
 |-  ( ( A x. 2 ) - A ) = A
454 453 oveq2i 
 |-  ( B - ( ( A x. 2 ) - A ) ) = ( B - A )
455 447 449 454 3eqtr2i 
 |-  ( ( B + A ) - ( A x. 2 ) ) = ( B - A )
456 455 oveq1i 
 |-  ( ( ( B + A ) - ( A x. 2 ) ) / 2 ) = ( ( B - A ) / 2 )
457 141 300 301 divcan4i 
 |-  ( ( A x. 2 ) / 2 ) = A
458 457 oveq2i 
 |-  ( ( ( B + A ) / 2 ) - ( ( A x. 2 ) / 2 ) ) = ( ( ( B + A ) / 2 ) - A )
459 446 456 458 3eqtr3ri 
 |-  ( ( ( B + A ) / 2 ) - A ) = ( ( B - A ) / 2 )
460 430 443 459 3eqtri 
 |-  S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x = ( ( B - A ) / 2 )
461 460 oveq2i 
 |-  ( ( F - E ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x ) = ( ( F - E ) x. ( ( B - A ) / 2 ) )
462 itgeq2 
 |-  ( A. x e. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) -> S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x )
463 65 63 subcli 
 |-  ( F - E ) e. CC
464 463 a1i 
 |-  ( x e. ( A [,] B ) -> ( F - E ) e. CC )
465 464 129 mulcomd 
 |-  ( x e. ( A [,] B ) -> ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) )
466 462 465 mprg 
 |-  S. ( A [,] B ) ( ( F - E ) x. ( ( x - A ) / ( B - A ) ) ) _d x = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x
467 362 461 466 3eqtr3ri 
 |-  S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x = ( ( F - E ) x. ( ( B - A ) / 2 ) )
468 353 467 oveq12i 
 |-  ( S. ( A [,] B ) E _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( F - E ) ) _d x ) = ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
469 326 340 468 3eqtri 
 |-  S. ( A [,] B ) V _d x = ( ( E x. ( B - A ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
470 149 300 301 divcli 
 |-  ( ( B - A ) / 2 ) e. CC
471 319 463 470 adddiri 
 |-  ( ( ( E x. 2 ) + ( F - E ) ) x. ( ( B - A ) / 2 ) ) = ( ( ( E x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( F - E ) x. ( ( B - A ) / 2 ) ) )
472 323 469 471 3eqtr4i 
 |-  S. ( A [,] B ) V _d x = ( ( ( E x. 2 ) + ( F - E ) ) x. ( ( B - A ) / 2 ) )
473 addsub12 
 |-  ( ( F e. CC /\ ( E x. 2 ) e. CC /\ E e. CC ) -> ( F + ( ( E x. 2 ) - E ) ) = ( ( E x. 2 ) + ( F - E ) ) )
474 65 319 63 473 mp3an 
 |-  ( F + ( ( E x. 2 ) - E ) ) = ( ( E x. 2 ) + ( F - E ) )
475 63 times2i 
 |-  ( E x. 2 ) = ( E + E )
476 475 oveq1i 
 |-  ( ( E x. 2 ) - E ) = ( ( E + E ) - E )
477 63 63 pncan3oi 
 |-  ( ( E + E ) - E ) = E
478 476 477 eqtri 
 |-  ( ( E x. 2 ) - E ) = E
479 478 oveq2i 
 |-  ( F + ( ( E x. 2 ) - E ) ) = ( F + E )
480 474 479 eqtr3i 
 |-  ( ( E x. 2 ) + ( F - E ) ) = ( F + E )
481 480 oveq1i 
 |-  ( ( ( E x. 2 ) + ( F - E ) ) x. ( ( B - A ) / 2 ) ) = ( ( F + E ) x. ( ( B - A ) / 2 ) )
482 472 481 eqtri 
 |-  S. ( A [,] B ) V _d x = ( ( F + E ) x. ( ( B - A ) / 2 ) )
483 17 300 301 divcan4i 
 |-  ( ( C x. 2 ) / 2 ) = C
484 483 oveq1i 
 |-  ( ( ( C x. 2 ) / 2 ) x. ( B - A ) ) = ( C x. ( B - A ) )
485 17 300 mulcli 
 |-  ( C x. 2 ) e. CC
486 div32 
 |-  ( ( ( C x. 2 ) e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) /\ ( B - A ) e. CC ) -> ( ( ( C x. 2 ) / 2 ) x. ( B - A ) ) = ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) )
487 485 293 149 486 mp3an 
 |-  ( ( ( C x. 2 ) / 2 ) x. ( B - A ) ) = ( ( C x. 2 ) x. ( ( B - A ) / 2 ) )
488 484 487 eqtr3i 
 |-  ( C x. ( B - A ) ) = ( ( C x. 2 ) x. ( ( B - A ) / 2 ) )
489 488 oveq1i 
 |-  ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) ) = ( ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
490 10 a1i 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> U = ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) )
491 490 itgeq2dv 
 |-  ( T. -> S. ( A [,] B ) U _d x = S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x )
492 491 mptru 
 |-  S. ( A [,] B ) U _d x = S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x
493 3 a1i 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> C e. RR )
494 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> C ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> C ) e. L^1 )
495 1 2 266 494 mp3an 
 |-  ( x e. ( A [,] B ) |-> C ) e. L^1
496 495 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> C ) e. L^1 )
497 4 a1i 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> D e. RR )
498 497 493 resubcld 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> ( D - C ) e. RR )
499 331 498 remulcld 
 |-  ( ( T. /\ x e. ( A [,] B ) ) -> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) e. RR )
500 272 mptru 
 |-  ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. ( ( A [,] B ) -cn-> CC )
501 cniccibl 
 |-  ( ( A e. RR /\ B e. RR /\ ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. L^1 )
502 1 2 500 501 mp3an 
 |-  ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. L^1
503 502 a1i 
 |-  ( T. -> ( x e. ( A [,] B ) |-> ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) e. L^1 )
504 493 496 499 503 itgadd 
 |-  ( T. -> S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x = ( S. ( A [,] B ) C _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x ) )
505 504 mptru 
 |-  S. ( A [,] B ) ( C + ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) ) _d x = ( S. ( A [,] B ) C _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x )
506 itgconst 
 |-  ( ( ( A [,] B ) e. dom vol /\ ( vol ` ( A [,] B ) ) e. RR /\ C e. CC ) -> S. ( A [,] B ) C _d x = ( C x. ( vol ` ( A [,] B ) ) ) )
507 342 349 17 506 mp3an 
 |-  S. ( A [,] B ) C _d x = ( C x. ( vol ` ( A [,] B ) ) )
508 348 oveq2i 
 |-  ( C x. ( vol ` ( A [,] B ) ) ) = ( C x. ( B - A ) )
509 507 508 eqtri 
 |-  S. ( A [,] B ) C _d x = ( C x. ( B - A ) )
510 33 a1i 
 |-  ( T. -> D e. CC )
511 17 a1i 
 |-  ( T. -> C e. CC )
512 510 511 subcld 
 |-  ( T. -> ( D - C ) e. CC )
513 512 331 360 itgmulc2 
 |-  ( T. -> ( ( D - C ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x ) = S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x )
514 513 mptru 
 |-  ( ( D - C ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x ) = S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x
515 460 oveq2i 
 |-  ( ( D - C ) x. S. ( A [,] B ) ( ( x - A ) / ( B - A ) ) _d x ) = ( ( D - C ) x. ( ( B - A ) / 2 ) )
516 itgeq2 
 |-  ( A. x e. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) -> S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x )
517 33 17 subcli 
 |-  ( D - C ) e. CC
518 517 a1i 
 |-  ( x e. ( A [,] B ) -> ( D - C ) e. CC )
519 518 129 mulcomd 
 |-  ( x e. ( A [,] B ) -> ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) = ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) )
520 516 519 mprg 
 |-  S. ( A [,] B ) ( ( D - C ) x. ( ( x - A ) / ( B - A ) ) ) _d x = S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x
521 514 515 520 3eqtr3ri 
 |-  S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x = ( ( D - C ) x. ( ( B - A ) / 2 ) )
522 509 521 oveq12i 
 |-  ( S. ( A [,] B ) C _d x + S. ( A [,] B ) ( ( ( x - A ) / ( B - A ) ) x. ( D - C ) ) _d x ) = ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
523 492 505 522 3eqtri 
 |-  S. ( A [,] B ) U _d x = ( ( C x. ( B - A ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
524 485 517 470 adddiri 
 |-  ( ( ( C x. 2 ) + ( D - C ) ) x. ( ( B - A ) / 2 ) ) = ( ( ( C x. 2 ) x. ( ( B - A ) / 2 ) ) + ( ( D - C ) x. ( ( B - A ) / 2 ) ) )
525 489 523 524 3eqtr4i 
 |-  S. ( A [,] B ) U _d x = ( ( ( C x. 2 ) + ( D - C ) ) x. ( ( B - A ) / 2 ) )
526 addsub12 
 |-  ( ( D e. CC /\ ( C x. 2 ) e. CC /\ C e. CC ) -> ( D + ( ( C x. 2 ) - C ) ) = ( ( C x. 2 ) + ( D - C ) ) )
527 33 485 17 526 mp3an 
 |-  ( D + ( ( C x. 2 ) - C ) ) = ( ( C x. 2 ) + ( D - C ) )
528 17 times2i 
 |-  ( C x. 2 ) = ( C + C )
529 528 oveq1i 
 |-  ( ( C x. 2 ) - C ) = ( ( C + C ) - C )
530 17 17 pncan3oi 
 |-  ( ( C + C ) - C ) = C
531 529 530 eqtri 
 |-  ( ( C x. 2 ) - C ) = C
532 531 oveq2i 
 |-  ( D + ( ( C x. 2 ) - C ) ) = ( D + C )
533 527 532 eqtr3i 
 |-  ( ( C x. 2 ) + ( D - C ) ) = ( D + C )
534 533 oveq1i 
 |-  ( ( ( C x. 2 ) + ( D - C ) ) x. ( ( B - A ) / 2 ) ) = ( ( D + C ) x. ( ( B - A ) / 2 ) )
535 525 534 eqtri 
 |-  S. ( A [,] B ) U _d x = ( ( D + C ) x. ( ( B - A ) / 2 ) )
536 482 535 oveq12i 
 |-  ( S. ( A [,] B ) V _d x - S. ( A [,] B ) U _d x ) = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
537 316 536 eqtri 
 |-  S. ( A [,] B ) ( V - U ) _d x = ( ( ( F + E ) x. ( ( B - A ) / 2 ) ) - ( ( D + C ) x. ( ( B - A ) / 2 ) ) )
538 299 304 537 3eqtr4ri 
 |-  S. ( A [,] B ) ( V - U ) _d x = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
539 289 291 538 3eqtr2i 
 |-  S. RR ( vol ` ( S " { x } ) ) _d x = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )
540 286 539 eqtri 
 |-  ( area ` S ) = ( ( ( ( F + E ) / 2 ) - ( ( D + C ) / 2 ) ) x. ( B - A ) )