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 ⊢ 𝐴 ∈ ℝ
areaquad.2 ⊢ 𝐵 ∈ ℝ
areaquad.3 ⊢ 𝐶 ∈ ℝ
areaquad.4 ⊢ 𝐷 ∈ ℝ
areaquad.5 ⊢ 𝐸 ∈ ℝ
areaquad.6 ⊢ 𝐹 ∈ ℝ
areaquad.7 ⊢ 𝐴 < 𝐵
areaquad.8 ⊢ 𝐶 ≤ 𝐸
areaquad.9 ⊢ 𝐷 ≤ 𝐹
areaquad.10 ⊢ 𝑈 = ( 𝐶 + ( ( ( 𝑥 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · ( 𝐷 − 𝐶 ) ) )
areaquad.11 ⊢ 𝑉 = ( 𝐸 + ( ( ( 𝑥 − 𝐴 ) / ( 𝐵 − 𝐴 ) ) · ( 𝐹 − 𝐸 ) ) )
areaquad.12 ⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∧ 𝑦 ∈ ( 𝑈 [,] 𝑉 ) ) }
Assertion areaquad ( area ‘ 𝑆 ) = ( ( ( ( 𝐹 + 𝐸 ) / 2 ) − ( ( 𝐷 + 𝐶 ) / 2 ) ) · ( 𝐵 − 𝐴 ) )

Proof

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