Users' Mathboxes Mathbox for Jon Pennant < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  areaquad Structured version   Visualization version   GIF version

Theorem areaquad 41579
Description: The area of a quadrilateral with two sides which are parallel to the y-axis in (ℝ Γ— ℝ) 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.)
Hypotheses
Ref Expression
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
Ref Expression
areaquad (areaβ€˜π‘†) = ((((𝐹 + 𝐸) / 2) βˆ’ ((𝐷 + 𝐢) / 2)) Β· (𝐡 βˆ’ 𝐴))
Distinct variable groups:   π‘₯,𝑦,𝐴   π‘₯,𝐡,𝑦   π‘₯,𝐢   π‘₯,𝐷   π‘₯,𝐸   π‘₯,𝐹   π‘₯,𝑆   𝑦,π‘ˆ   𝑦,𝑉
Allowed substitution hints:   𝐢(𝑦)   𝐷(𝑦)   𝑆(𝑦)   π‘ˆ(π‘₯)   𝐸(𝑦)   𝐹(𝑦)   𝑉(π‘₯)

Proof of Theorem areaquad
StepHypRef Expression
1 areaquad.1 . . . . . . . . . 10 𝐴 ∈ ℝ
2 areaquad.2 . . . . . . . . . 10 𝐡 ∈ ℝ
3 iccssre 13353 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) βŠ† ℝ)
41, 2, 3mp2an 691 . . . . . . . . 9 (𝐴[,]𝐡) βŠ† ℝ
54sseli 3945 . . . . . . . 8 (π‘₯ ∈ (𝐴[,]𝐡) β†’ π‘₯ ∈ ℝ)
65adantr 482 . . . . . . 7 ((π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉)) β†’ π‘₯ ∈ ℝ)
7 areaquad.3 . . . . . . . . . . . . . . . 16 𝐢 ∈ ℝ
87recni 11176 . . . . . . . . . . . . . . 15 𝐢 ∈ β„‚
98a1i 11 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ 𝐢 ∈ β„‚)
10 resubcl 11472 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ ℝ ∧ 𝐴 ∈ ℝ) β†’ (π‘₯ βˆ’ 𝐴) ∈ ℝ)
111, 10mpan2 690 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ ℝ β†’ (π‘₯ βˆ’ 𝐴) ∈ ℝ)
122, 1resubcli 11470 . . . . . . . . . . . . . . . . . 18 (𝐡 βˆ’ 𝐴) ∈ ℝ
1312a1i 11 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ ℝ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
142recni 11176 . . . . . . . . . . . . . . . . . . . . 21 𝐡 ∈ β„‚
1514a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ β†’ 𝐡 ∈ β„‚)
16 recn 11148 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ β†’ 𝐴 ∈ β„‚)
17 areaquad.7 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 < 𝐡
181, 17gtneii 11274 . . . . . . . . . . . . . . . . . . . . 21 𝐡 β‰  𝐴
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ β†’ 𝐡 β‰  𝐴)
2015, 16, 19subne0d 11528 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℝ β†’ (𝐡 βˆ’ 𝐴) β‰  0)
211, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝐡 βˆ’ 𝐴) β‰  0
2221a1i 11 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ ℝ β†’ (𝐡 βˆ’ 𝐴) β‰  0)
2311, 13, 22redivcld 11990 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) ∈ ℝ)
2423recnd 11190 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) ∈ β„‚)
25 areaquad.4 . . . . . . . . . . . . . . . . 17 𝐷 ∈ ℝ
2625recni 11176 . . . . . . . . . . . . . . . 16 𝐷 ∈ β„‚
2726a1i 11 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ 𝐷 ∈ β„‚)
2824, 27mulcld 11182 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) ∈ β„‚)
2924, 9mulcld 11182 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢) ∈ β„‚)
309, 28, 29addsub12d 11542 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ (𝐢 + ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢))) = ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) + (𝐢 βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢))))
31 areaquad.10 . . . . . . . . . . . . . 14 π‘ˆ = (𝐢 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)))
3224, 27, 9subdid 11618 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)) = ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢)))
3332oveq2d 7378 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (𝐢 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) = (𝐢 + ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢))))
3431, 33eqtrid 2789 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ π‘ˆ = (𝐢 + ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢))))
35 1cnd 11157 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ β†’ 1 ∈ β„‚)
3635, 24, 9subdird 11619 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐢) = ((1 Β· 𝐢) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢)))
378mulid2i 11167 . . . . . . . . . . . . . . . 16 (1 Β· 𝐢) = 𝐢
3837oveq1i 7372 . . . . . . . . . . . . . . 15 ((1 Β· 𝐢) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢)) = (𝐢 βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢))
3936, 38eqtrdi 2793 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐢) = (𝐢 βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢)))
4039oveq2d 7378 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) + ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐢)) = ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) + (𝐢 βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐢))))
4130, 34, 403eqtr4d 2787 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ π‘ˆ = ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) + ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐢)))
42 1red 11163 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ ℝ β†’ 1 ∈ ℝ)
4342, 23resubcld 11590 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ ℝ)
4443recnd 11190 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ β„‚)
4544, 9mulcld 11182 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐢) ∈ β„‚)
4628, 45addcomd 11364 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) + ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐢)) = (((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐢) + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷)))
4744, 9mulcomd 11183 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐢) = (𝐢 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
4824, 27mulcomd 11183 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷) = (𝐷 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))))
4947, 48oveq12d 7380 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ (((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐢) + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐷)) = ((𝐢 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐷 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
5041, 46, 493eqtrd 2781 . . . . . . . . . . 11 (π‘₯ ∈ ℝ β†’ π‘ˆ = ((𝐢 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐷 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
517a1i 11 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ 𝐢 ∈ ℝ)
5251, 43remulcld 11192 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ (𝐢 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) ∈ ℝ)
5325a1i 11 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ 𝐷 ∈ ℝ)
5453, 23remulcld 11192 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ (𝐷 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ ℝ)
5552, 54readdcld 11191 . . . . . . . . . . 11 (π‘₯ ∈ ℝ β†’ ((𝐢 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐷 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) ∈ ℝ)
5650, 55eqeltrd 2838 . . . . . . . . . 10 (π‘₯ ∈ ℝ β†’ π‘ˆ ∈ ℝ)
57 areaquad.5 . . . . . . . . . . . . . . . 16 𝐸 ∈ ℝ
5857recni 11176 . . . . . . . . . . . . . . 15 𝐸 ∈ β„‚
5958a1i 11 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ 𝐸 ∈ β„‚)
60 areaquad.6 . . . . . . . . . . . . . . . . 17 𝐹 ∈ ℝ
6160recni 11176 . . . . . . . . . . . . . . . 16 𝐹 ∈ β„‚
6261a1i 11 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ 𝐹 ∈ β„‚)
6324, 62mulcld 11182 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) ∈ β„‚)
6424, 59mulcld 11182 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸) ∈ β„‚)
6559, 63, 64addsub12d 11542 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ (𝐸 + ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸))) = ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) + (𝐸 βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸))))
66 areaquad.11 . . . . . . . . . . . . . 14 𝑉 = (𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)))
6724, 62, 59subdid 11618 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)) = ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸)))
6867oveq2d 7378 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ (𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) = (𝐸 + ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸))))
6966, 68eqtrid 2789 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ 𝑉 = (𝐸 + ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸))))
7035, 24, 59subdird 11619 . . . . . . . . . . . . . . 15 (π‘₯ ∈ ℝ β†’ ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐸) = ((1 Β· 𝐸) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸)))
7158mulid2i 11167 . . . . . . . . . . . . . . . 16 (1 Β· 𝐸) = 𝐸
7271oveq1i 7372 . . . . . . . . . . . . . . 15 ((1 Β· 𝐸) βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸)) = (𝐸 βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸))
7370, 72eqtrdi 2793 . . . . . . . . . . . . . 14 (π‘₯ ∈ ℝ β†’ ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐸) = (𝐸 βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸)))
7473oveq2d 7378 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) + ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐸)) = ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) + (𝐸 βˆ’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐸))))
7565, 69, 743eqtr4d 2787 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ 𝑉 = ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) + ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐸)))
7644, 59mulcld 11182 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐸) ∈ β„‚)
7763, 76addcomd 11364 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ ((((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) + ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐸)) = (((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐸) + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹)))
7844, 59mulcomd 11183 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ ((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐸) = (𝐸 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
7924, 62mulcomd 11183 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹) = (𝐹 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))))
8078, 79oveq12d 7380 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ (((1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) Β· 𝐸) + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· 𝐹)) = ((𝐸 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐹 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
8175, 77, 803eqtrd 2781 . . . . . . . . . . 11 (π‘₯ ∈ ℝ β†’ 𝑉 = ((𝐸 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐹 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
8257a1i 11 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ 𝐸 ∈ ℝ)
8382, 43remulcld 11192 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ (𝐸 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) ∈ ℝ)
8460a1i 11 . . . . . . . . . . . . 13 (π‘₯ ∈ ℝ β†’ 𝐹 ∈ ℝ)
8584, 23remulcld 11192 . . . . . . . . . . . 12 (π‘₯ ∈ ℝ β†’ (𝐹 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ ℝ)
8683, 85readdcld 11191 . . . . . . . . . . 11 (π‘₯ ∈ ℝ β†’ ((𝐸 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐹 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) ∈ ℝ)
8781, 86eqeltrd 2838 . . . . . . . . . 10 (π‘₯ ∈ ℝ β†’ 𝑉 ∈ ℝ)
88 iccssre 13353 . . . . . . . . . 10 ((π‘ˆ ∈ ℝ ∧ 𝑉 ∈ ℝ) β†’ (π‘ˆ[,]𝑉) βŠ† ℝ)
8956, 87, 88syl2anc 585 . . . . . . . . 9 (π‘₯ ∈ ℝ β†’ (π‘ˆ[,]𝑉) βŠ† ℝ)
905, 89syl 17 . . . . . . . 8 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (π‘ˆ[,]𝑉) βŠ† ℝ)
9190sselda 3949 . . . . . . 7 ((π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉)) β†’ 𝑦 ∈ ℝ)
926, 91jca 513 . . . . . 6 ((π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉)) β†’ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ))
9392ssopab2i 5512 . . . . 5 {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉))} βŠ† {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94 areaquad.12 . . . . 5 𝑆 = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉))}
95 df-xp 5644 . . . . 5 (ℝ Γ— ℝ) = {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ ℝ ∧ 𝑦 ∈ ℝ)}
9693, 94, 953sstr4i 3992 . . . 4 𝑆 βŠ† (ℝ Γ— ℝ)
97 iftrue 4497 . . . . . . . . . 10 (π‘₯ ∈ (𝐴[,]𝐡) β†’ if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) = (𝑉 βˆ’ π‘ˆ))
98 nfv 1918 . . . . . . . . . . . . 13 Ⅎ𝑦 π‘₯ ∈ (𝐴[,]𝐡)
99 nfopab2 5181 . . . . . . . . . . . . . . 15 Ⅎ𝑦{⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉))}
10094, 99nfcxfr 2906 . . . . . . . . . . . . . 14 Ⅎ𝑦𝑆
101 nfcv 2908 . . . . . . . . . . . . . 14 Ⅎ𝑦{π‘₯}
102100, 101nfima 6026 . . . . . . . . . . . . 13 Ⅎ𝑦(𝑆 β€œ {π‘₯})
103 nfcv 2908 . . . . . . . . . . . . 13 Ⅎ𝑦(π‘ˆ[,]𝑉)
104 vex 3452 . . . . . . . . . . . . . . . 16 π‘₯ ∈ V
105 vex 3452 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
106104, 105elimasn 6046 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑆 β€œ {π‘₯}) ↔ ⟨π‘₯, π‘¦βŸ© ∈ 𝑆)
10794eleq2i 2830 . . . . . . . . . . . . . . 15 (⟨π‘₯, π‘¦βŸ© ∈ 𝑆 ↔ ⟨π‘₯, π‘¦βŸ© ∈ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉))})
108 opabidw 5486 . . . . . . . . . . . . . . 15 (⟨π‘₯, π‘¦βŸ© ∈ {⟨π‘₯, π‘¦βŸ© ∣ (π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉))} ↔ (π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉)))
109106, 107, 1083bitri 297 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 β€œ {π‘₯}) ↔ (π‘₯ ∈ (𝐴[,]𝐡) ∧ 𝑦 ∈ (π‘ˆ[,]𝑉)))
110109baib 537 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝑦 ∈ (𝑆 β€œ {π‘₯}) ↔ 𝑦 ∈ (π‘ˆ[,]𝑉)))
11198, 102, 103, 110eqrd 3968 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝑆 β€œ {π‘₯}) = (π‘ˆ[,]𝑉))
112111fveq2d 6851 . . . . . . . . . . 11 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (volβ€˜(𝑆 β€œ {π‘₯})) = (volβ€˜(π‘ˆ[,]𝑉)))
1135, 56syl 17 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) β†’ π‘ˆ ∈ ℝ)
1145, 87syl 17 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝑉 ∈ ℝ)
115 iccmbl 24946 . . . . . . . . . . . . 13 ((π‘ˆ ∈ ℝ ∧ 𝑉 ∈ ℝ) β†’ (π‘ˆ[,]𝑉) ∈ dom vol)
116113, 114, 115syl2anc 585 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (π‘ˆ[,]𝑉) ∈ dom vol)
117 mblvol 24910 . . . . . . . . . . . 12 ((π‘ˆ[,]𝑉) ∈ dom vol β†’ (volβ€˜(π‘ˆ[,]𝑉)) = (vol*β€˜(π‘ˆ[,]𝑉)))
118116, 117syl 17 . . . . . . . . . . 11 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (volβ€˜(π‘ˆ[,]𝑉)) = (vol*β€˜(π‘ˆ[,]𝑉)))
1195, 52syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐢 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) ∈ ℝ)
1205, 54syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐷 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ ℝ)
1215, 83syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐸 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) ∈ ℝ)
1225, 85syl 17 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐹 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ ℝ)
1237a1i 11 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐢 ∈ ℝ)
12457a1i 11 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐸 ∈ ℝ)
1255, 43syl 17 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ ℝ)
1265, 23syl 17 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) ∈ ℝ)
127126recnd 11190 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) ∈ β„‚)
128127subidd 11507 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) = 0)
129 1red 11163 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 1 ∈ ℝ)
1302a1i 11 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐡 ∈ ℝ)
1311a1i 11 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐴 ∈ ℝ)
1321rexri 11220 . . . . . . . . . . . . . . . . . . . . 21 𝐴 ∈ ℝ*
1332rexri 11220 . . . . . . . . . . . . . . . . . . . . 21 𝐡 ∈ ℝ*
134 iccleub 13326 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ π‘₯ ≀ 𝐡)
135132, 133, 134mp3an12 1452 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (𝐴[,]𝐡) β†’ π‘₯ ≀ 𝐡)
1365, 130, 131, 135lesub1dd 11778 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (π‘₯ βˆ’ 𝐴) ≀ (𝐡 βˆ’ 𝐴))
1375, 1, 10sylancl 587 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (π‘₯ βˆ’ 𝐴) ∈ ℝ)
13812a1i 11 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
1391recni 11176 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 ∈ β„‚
140139subidi 11479 . . . . . . . . . . . . . . . . . . . . 21 (𝐴 βˆ’ 𝐴) = 0
141131, 130, 131ltsub1d 11771 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐴 < 𝐡 ↔ (𝐴 βˆ’ 𝐴) < (𝐡 βˆ’ 𝐴)))
14217, 141mpbii 232 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐴 βˆ’ 𝐴) < (𝐡 βˆ’ 𝐴))
143140, 142eqbrtrrid 5146 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 0 < (𝐡 βˆ’ 𝐴))
144 lediv1 12027 . . . . . . . . . . . . . . . . . . . 20 (((π‘₯ βˆ’ 𝐴) ∈ ℝ ∧ (𝐡 βˆ’ 𝐴) ∈ ℝ ∧ ((𝐡 βˆ’ 𝐴) ∈ ℝ ∧ 0 < (𝐡 βˆ’ 𝐴))) β†’ ((π‘₯ βˆ’ 𝐴) ≀ (𝐡 βˆ’ 𝐴) ↔ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) ≀ ((𝐡 βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))))
145137, 138, 138, 143, 144syl112anc 1375 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((π‘₯ βˆ’ 𝐴) ≀ (𝐡 βˆ’ 𝐴) ↔ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) ≀ ((𝐡 βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))))
146136, 145mpbid 231 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) ≀ ((𝐡 βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))
14712recni 11176 . . . . . . . . . . . . . . . . . . 19 (𝐡 βˆ’ 𝐴) ∈ β„‚
148147, 21dividi 11895 . . . . . . . . . . . . . . . . . 18 ((𝐡 βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) = 1
149146, 148breqtrdi 5151 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) ≀ 1)
150126, 129, 126, 149lesub1dd 11778 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ≀ (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))))
151128, 150eqbrtrrd 5134 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 0 ≀ (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))))
152 areaquad.8 . . . . . . . . . . . . . . . 16 𝐢 ≀ 𝐸
153152a1i 11 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐢 ≀ 𝐸)
154123, 124, 125, 151, 153lemul1ad 12101 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐢 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) ≀ (𝐸 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
15525a1i 11 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐷 ∈ ℝ)
15660a1i 11 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐹 ∈ ℝ)
157138, 143elrpd 12961 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ+)
158 iccgelb 13327 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ* ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝐴 ≀ π‘₯)
159132, 133, 158mp3an12 1452 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐴 ≀ π‘₯)
160131, 5, 131, 159lesub1dd 11778 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐴 βˆ’ 𝐴) ≀ (π‘₯ βˆ’ 𝐴))
161140, 160eqbrtrrid 5146 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 0 ≀ (π‘₯ βˆ’ 𝐴))
162137, 157, 161divge0d 13004 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 0 ≀ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))
163 areaquad.9 . . . . . . . . . . . . . . . 16 𝐷 ≀ 𝐹
164163a1i 11 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐷 ≀ 𝐹)
165155, 156, 126, 162, 164lemul1ad 12101 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐷 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ≀ (𝐹 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))))
166119, 120, 121, 122, 154, 165le2addd 11781 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((𝐢 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐷 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) ≀ ((𝐸 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐹 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
1675, 50syl 17 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) β†’ π‘ˆ = ((𝐢 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐷 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
1685, 81syl 17 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝑉 = ((𝐸 Β· (1 βˆ’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))) + (𝐹 Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)))))
169166, 167, 1683brtr4d 5142 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) β†’ π‘ˆ ≀ 𝑉)
170 ovolicc 24903 . . . . . . . . . . . 12 ((π‘ˆ ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ π‘ˆ ≀ 𝑉) β†’ (vol*β€˜(π‘ˆ[,]𝑉)) = (𝑉 βˆ’ π‘ˆ))
171113, 114, 169, 170syl3anc 1372 . . . . . . . . . . 11 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (vol*β€˜(π‘ˆ[,]𝑉)) = (𝑉 βˆ’ π‘ˆ))
172112, 118, 1713eqtrd 2781 . . . . . . . . . 10 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (volβ€˜(𝑆 β€œ {π‘₯})) = (𝑉 βˆ’ π‘ˆ))
17397, 172eqtr4d 2780 . . . . . . . . 9 (π‘₯ ∈ (𝐴[,]𝐡) β†’ if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) = (volβ€˜(𝑆 β€œ {π‘₯})))
174 iffalse 4500 . . . . . . . . . 10 (Β¬ π‘₯ ∈ (𝐴[,]𝐡) β†’ if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) = 0)
175 nfv 1918 . . . . . . . . . . . . 13 Ⅎ𝑦 Β¬ π‘₯ ∈ (𝐴[,]𝐡)
176 nfcv 2908 . . . . . . . . . . . . 13 β„²π‘¦βˆ…
177109simplbi 499 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 β€œ {π‘₯}) β†’ π‘₯ ∈ (𝐴[,]𝐡))
178 noel 4295 . . . . . . . . . . . . . . 15 Β¬ 𝑦 ∈ βˆ…
179178pm2.21i 119 . . . . . . . . . . . . . 14 (𝑦 ∈ βˆ… β†’ π‘₯ ∈ (𝐴[,]𝐡))
180177, 179pm5.21ni 379 . . . . . . . . . . . . 13 (Β¬ π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝑦 ∈ (𝑆 β€œ {π‘₯}) ↔ 𝑦 ∈ βˆ…))
181175, 102, 176, 180eqrd 3968 . . . . . . . . . . . 12 (Β¬ π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝑆 β€œ {π‘₯}) = βˆ…)
182181fveq2d 6851 . . . . . . . . . . 11 (Β¬ π‘₯ ∈ (𝐴[,]𝐡) β†’ (volβ€˜(𝑆 β€œ {π‘₯})) = (volβ€˜βˆ…))
183 0mbl 24919 . . . . . . . . . . . . 13 βˆ… ∈ dom vol
184 mblvol 24910 . . . . . . . . . . . . 13 (βˆ… ∈ dom vol β†’ (volβ€˜βˆ…) = (vol*β€˜βˆ…))
185183, 184ax-mp 5 . . . . . . . . . . . 12 (volβ€˜βˆ…) = (vol*β€˜βˆ…)
186 ovol0 24873 . . . . . . . . . . . 12 (vol*β€˜βˆ…) = 0
187185, 186eqtri 2765 . . . . . . . . . . 11 (volβ€˜βˆ…) = 0
188182, 187eqtrdi 2793 . . . . . . . . . 10 (Β¬ π‘₯ ∈ (𝐴[,]𝐡) β†’ (volβ€˜(𝑆 β€œ {π‘₯})) = 0)
189174, 188eqtr4d 2780 . . . . . . . . 9 (Β¬ π‘₯ ∈ (𝐴[,]𝐡) β†’ if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) = (volβ€˜(𝑆 β€œ {π‘₯})))
190173, 189pm2.61i 182 . . . . . . . 8 if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) = (volβ€˜(𝑆 β€œ {π‘₯}))
191190eqcomi 2746 . . . . . . 7 (volβ€˜(𝑆 β€œ {π‘₯})) = if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0)
19287, 56resubcld 11590 . . . . . . . 8 (π‘₯ ∈ ℝ β†’ (𝑉 βˆ’ π‘ˆ) ∈ ℝ)
193 0re 11164 . . . . . . . 8 0 ∈ ℝ
194 ifcl 4536 . . . . . . . 8 (((𝑉 βˆ’ π‘ˆ) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) ∈ ℝ)
195192, 193, 194sylancl 587 . . . . . . 7 (π‘₯ ∈ ℝ β†’ if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) ∈ ℝ)
196191, 195eqeltrid 2842 . . . . . 6 (π‘₯ ∈ ℝ β†’ (volβ€˜(𝑆 β€œ {π‘₯})) ∈ ℝ)
197 volf 24909 . . . . . . . 8 vol:dom vol⟢(0[,]+∞)
198 ffun 6676 . . . . . . . 8 (vol:dom vol⟢(0[,]+∞) β†’ Fun vol)
199197, 198ax-mp 5 . . . . . . 7 Fun vol
200 iftrue 4497 . . . . . . . . . 10 (π‘₯ ∈ (𝐴[,]𝐡) β†’ if(π‘₯ ∈ (𝐴[,]𝐡), (π‘ˆ[,]𝑉), βˆ…) = (π‘ˆ[,]𝑉))
201111, 200eqtr4d 2780 . . . . . . . . 9 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝑆 β€œ {π‘₯}) = if(π‘₯ ∈ (𝐴[,]𝐡), (π‘ˆ[,]𝑉), βˆ…))
202 iffalse 4500 . . . . . . . . . 10 (Β¬ π‘₯ ∈ (𝐴[,]𝐡) β†’ if(π‘₯ ∈ (𝐴[,]𝐡), (π‘ˆ[,]𝑉), βˆ…) = βˆ…)
203181, 202eqtr4d 2780 . . . . . . . . 9 (Β¬ π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝑆 β€œ {π‘₯}) = if(π‘₯ ∈ (𝐴[,]𝐡), (π‘ˆ[,]𝑉), βˆ…))
204201, 203pm2.61i 182 . . . . . . . 8 (𝑆 β€œ {π‘₯}) = if(π‘₯ ∈ (𝐴[,]𝐡), (π‘ˆ[,]𝑉), βˆ…)
20556, 87, 115syl2anc 585 . . . . . . . . 9 (π‘₯ ∈ ℝ β†’ (π‘ˆ[,]𝑉) ∈ dom vol)
206183a1i 11 . . . . . . . . 9 (π‘₯ ∈ ℝ β†’ βˆ… ∈ dom vol)
207205, 206ifcld 4537 . . . . . . . 8 (π‘₯ ∈ ℝ β†’ if(π‘₯ ∈ (𝐴[,]𝐡), (π‘ˆ[,]𝑉), βˆ…) ∈ dom vol)
208204, 207eqeltrid 2842 . . . . . . 7 (π‘₯ ∈ ℝ β†’ (𝑆 β€œ {π‘₯}) ∈ dom vol)
209 fvimacnv 7008 . . . . . . 7 ((Fun vol ∧ (𝑆 β€œ {π‘₯}) ∈ dom vol) β†’ ((volβ€˜(𝑆 β€œ {π‘₯})) ∈ ℝ ↔ (𝑆 β€œ {π‘₯}) ∈ (β—‘vol β€œ ℝ)))
210199, 208, 209sylancr 588 . . . . . 6 (π‘₯ ∈ ℝ β†’ ((volβ€˜(𝑆 β€œ {π‘₯})) ∈ ℝ ↔ (𝑆 β€œ {π‘₯}) ∈ (β—‘vol β€œ ℝ)))
211196, 210mpbid 231 . . . . 5 (π‘₯ ∈ ℝ β†’ (𝑆 β€œ {π‘₯}) ∈ (β—‘vol β€œ ℝ))
212211rgen 3067 . . . 4 βˆ€π‘₯ ∈ ℝ (𝑆 β€œ {π‘₯}) ∈ (β—‘vol β€œ ℝ)
2134a1i 11 . . . . . 6 (0 ∈ ℝ β†’ (𝐴[,]𝐡) βŠ† ℝ)
214 rembl 24920 . . . . . . 7 ℝ ∈ dom vol
215214a1i 11 . . . . . 6 (0 ∈ ℝ β†’ ℝ ∈ dom vol)
216114, 113resubcld 11590 . . . . . . . 8 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝑉 βˆ’ π‘ˆ) ∈ ℝ)
217172, 216eqeltrd 2838 . . . . . . 7 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (volβ€˜(𝑆 β€œ {π‘₯})) ∈ ℝ)
218217adantl 483 . . . . . 6 ((0 ∈ ℝ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ (volβ€˜(𝑆 β€œ {π‘₯})) ∈ ℝ)
219 eldifn 4092 . . . . . . . 8 (π‘₯ ∈ (ℝ βˆ– (𝐴[,]𝐡)) β†’ Β¬ π‘₯ ∈ (𝐴[,]𝐡))
220219, 188syl 17 . . . . . . 7 (π‘₯ ∈ (ℝ βˆ– (𝐴[,]𝐡)) β†’ (volβ€˜(𝑆 β€œ {π‘₯})) = 0)
221220adantl 483 . . . . . 6 ((0 ∈ ℝ ∧ π‘₯ ∈ (ℝ βˆ– (𝐴[,]𝐡))) β†’ (volβ€˜(𝑆 β€œ {π‘₯})) = 0)
222172mpteq2ia 5213 . . . . . . . 8 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (volβ€˜(𝑆 β€œ {π‘₯}))) = (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝑉 βˆ’ π‘ˆ))
223 eqid 2737 . . . . . . . . . . 11 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
224223subcn 24245 . . . . . . . . . . . 12 βˆ’ ∈ (((TopOpenβ€˜β„‚fld) Γ—t (TopOpenβ€˜β„‚fld)) Cn (TopOpenβ€˜β„‚fld))
225224a1i 11 . . . . . . . . . . 11 (⊀ β†’ βˆ’ ∈ (((TopOpenβ€˜β„‚fld) Γ—t (TopOpenβ€˜β„‚fld)) Cn (TopOpenβ€˜β„‚fld)))
22666mpteq2i 5215 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝑉) = (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))))
227223addcn 24244 . . . . . . . . . . . . . 14 + ∈ (((TopOpenβ€˜β„‚fld) Γ—t (TopOpenβ€˜β„‚fld)) Cn (TopOpenβ€˜β„‚fld))
228227a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ + ∈ (((TopOpenβ€˜β„‚fld) Γ—t (TopOpenβ€˜β„‚fld)) Cn (TopOpenβ€˜β„‚fld)))
229 ax-resscn 11115 . . . . . . . . . . . . . . . 16 ℝ βŠ† β„‚
2304, 229sstri 3958 . . . . . . . . . . . . . . 15 (𝐴[,]𝐡) βŠ† β„‚
231 ssid 3971 . . . . . . . . . . . . . . 15 β„‚ βŠ† β„‚
232 cncfmptc 24291 . . . . . . . . . . . . . . 15 ((𝐸 ∈ β„‚ ∧ (𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐸) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
23358, 230, 231, 232mp3an 1462 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐸) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
234233a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐸) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
235230sseli 3945 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴[,]𝐡) β†’ π‘₯ ∈ β„‚)
236139a1i 11 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝐴 ∈ β„‚)
237147a1i 11 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐡 βˆ’ 𝐴) ∈ β„‚)
23821a1i 11 . . . . . . . . . . . . . . . . . 18 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐡 βˆ’ 𝐴) β‰  0)
239235, 236, 237, 238divsubdird 11977 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) = ((π‘₯ / (𝐡 βˆ’ 𝐴)) βˆ’ (𝐴 / (𝐡 βˆ’ 𝐴))))
240239adantl 483 . . . . . . . . . . . . . . . 16 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) = ((π‘₯ / (𝐡 βˆ’ 𝐴)) βˆ’ (𝐴 / (𝐡 βˆ’ 𝐴))))
241240mpteq2dva 5210 . . . . . . . . . . . . . . 15 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) = (π‘₯ ∈ (𝐴[,]𝐡) ↦ ((π‘₯ / (𝐡 βˆ’ 𝐴)) βˆ’ (𝐴 / (𝐡 βˆ’ 𝐴)))))
242 resmpt 5996 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐡) βŠ† β„‚ β†’ ((π‘₯ ∈ β„‚ ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) β†Ύ (𝐴[,]𝐡)) = (π‘₯ ∈ (𝐴[,]𝐡) ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))))
243230, 242ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ β„‚ ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) β†Ύ (𝐴[,]𝐡)) = (π‘₯ ∈ (𝐴[,]𝐡) ↦ (π‘₯ / (𝐡 βˆ’ 𝐴)))
244 eqid 2737 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ β„‚ ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) = (π‘₯ ∈ β„‚ ↦ (π‘₯ / (𝐡 βˆ’ 𝐴)))
245244divccncf 24285 . . . . . . . . . . . . . . . . . . . 20 (((𝐡 βˆ’ 𝐴) ∈ β„‚ ∧ (𝐡 βˆ’ 𝐴) β‰  0) β†’ (π‘₯ ∈ β„‚ ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) ∈ (ℂ–cnβ†’β„‚))
246147, 21, 245mp2an 691 . . . . . . . . . . . . . . . . . . 19 (π‘₯ ∈ β„‚ ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) ∈ (ℂ–cnβ†’β„‚)
247 rescncf 24276 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐡) βŠ† β„‚ β†’ ((π‘₯ ∈ β„‚ ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) ∈ (ℂ–cnβ†’β„‚) β†’ ((π‘₯ ∈ β„‚ ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) β†Ύ (𝐴[,]𝐡)) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)))
248230, 246, 247mp2 9 . . . . . . . . . . . . . . . . . 18 ((π‘₯ ∈ β„‚ ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) β†Ύ (𝐴[,]𝐡)) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
249243, 248eqeltrri 2835 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
250249a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (π‘₯ / (𝐡 βˆ’ 𝐴))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
251139, 147, 21divcli 11904 . . . . . . . . . . . . . . . . . 18 (𝐴 / (𝐡 βˆ’ 𝐴)) ∈ β„‚
252 cncfmptc 24291 . . . . . . . . . . . . . . . . . 18 (((𝐴 / (𝐡 βˆ’ 𝐴)) ∈ β„‚ ∧ (𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝐴 / (𝐡 βˆ’ 𝐴))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
253251, 230, 231, 252mp3an 1462 . . . . . . . . . . . . . . . . 17 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝐴 / (𝐡 βˆ’ 𝐴))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
254253a1i 11 . . . . . . . . . . . . . . . 16 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝐴 / (𝐡 βˆ’ 𝐴))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
255223, 225, 250, 254cncfmpt2f 24294 . . . . . . . . . . . . . . 15 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ ((π‘₯ / (𝐡 βˆ’ 𝐴)) βˆ’ (𝐴 / (𝐡 βˆ’ 𝐴)))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
256241, 255eqeltrd 2838 . . . . . . . . . . . . . 14 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
257 cncfmptc 24291 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ β„‚ ∧ (𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐹) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
25861, 230, 231, 257mp3an 1462 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐹) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
259258a1i 11 . . . . . . . . . . . . . . 15 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐹) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
260223, 225, 259, 234cncfmpt2f 24294 . . . . . . . . . . . . . 14 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝐹 βˆ’ 𝐸)) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
261256, 260mulcncf 24826 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
262223, 228, 234, 261cncfmpt2f 24294 . . . . . . . . . . . 12 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
263226, 262eqeltrid 2842 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝑉) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
26431mpteq2i 5215 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘ˆ) = (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝐢 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))))
265 cncfmptc 24291 . . . . . . . . . . . . . . 15 ((𝐢 ∈ β„‚ ∧ (𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐢) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
2668, 230, 231, 265mp3an 1462 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐢) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
267266a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐢) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
268 cncfmptc 24291 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ β„‚ ∧ (𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐷) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
26926, 230, 231, 268mp3an 1462 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐷) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
270269a1i 11 . . . . . . . . . . . . . . 15 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐷) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
271223, 225, 270, 267cncfmpt2f 24294 . . . . . . . . . . . . . 14 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝐷 βˆ’ 𝐢)) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
272256, 271mulcncf 24826 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
273223, 228, 267, 272cncfmpt2f 24294 . . . . . . . . . . . 12 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝐢 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
274264, 273eqeltrid 2842 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘ˆ) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
275223, 225, 263, 274cncfmpt2f 24294 . . . . . . . . . 10 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝑉 βˆ’ π‘ˆ)) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
276275mptru 1549 . . . . . . . . 9 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝑉 βˆ’ π‘ˆ)) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
277 cniccibl 25221 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝑉 βˆ’ π‘ˆ)) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝑉 βˆ’ π‘ˆ)) ∈ 𝐿1)
2781, 2, 276, 277mp3an 1462 . . . . . . . 8 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (𝑉 βˆ’ π‘ˆ)) ∈ 𝐿1
279222, 278eqeltri 2834 . . . . . . 7 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (volβ€˜(𝑆 β€œ {π‘₯}))) ∈ 𝐿1
280279a1i 11 . . . . . 6 (0 ∈ ℝ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (volβ€˜(𝑆 β€œ {π‘₯}))) ∈ 𝐿1)
281213, 215, 218, 221, 280iblss2 25186 . . . . 5 (0 ∈ ℝ β†’ (π‘₯ ∈ ℝ ↦ (volβ€˜(𝑆 β€œ {π‘₯}))) ∈ 𝐿1)
282193, 281ax-mp 5 . . . 4 (π‘₯ ∈ ℝ ↦ (volβ€˜(𝑆 β€œ {π‘₯}))) ∈ 𝐿1
283 dmarea 26323 . . . 4 (𝑆 ∈ dom area ↔ (𝑆 βŠ† (ℝ Γ— ℝ) ∧ βˆ€π‘₯ ∈ ℝ (𝑆 β€œ {π‘₯}) ∈ (β—‘vol β€œ ℝ) ∧ (π‘₯ ∈ ℝ ↦ (volβ€˜(𝑆 β€œ {π‘₯}))) ∈ 𝐿1))
28496, 212, 282, 283mpbir3an 1342 . . 3 𝑆 ∈ dom area
285 areaval 26330 . . 3 (𝑆 ∈ dom area β†’ (areaβ€˜π‘†) = βˆ«β„(volβ€˜(𝑆 β€œ {π‘₯})) dπ‘₯)
286284, 285ax-mp 5 . 2 (areaβ€˜π‘†) = βˆ«β„(volβ€˜(𝑆 β€œ {π‘₯})) dπ‘₯
287 itgeq2 25158 . . . 4 (βˆ€π‘₯ ∈ ℝ (volβ€˜(𝑆 β€œ {π‘₯})) = if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) β†’ βˆ«β„(volβ€˜(𝑆 β€œ {π‘₯})) dπ‘₯ = βˆ«β„if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) dπ‘₯)
288191a1i 11 . . . 4 (π‘₯ ∈ ℝ β†’ (volβ€˜(𝑆 β€œ {π‘₯})) = if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0))
289287, 288mprg 3071 . . 3 βˆ«β„(volβ€˜(𝑆 β€œ {π‘₯})) dπ‘₯ = βˆ«β„if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) dπ‘₯
290 itgss2 25193 . . . 4 ((𝐴[,]𝐡) βŠ† ℝ β†’ ∫(𝐴[,]𝐡)(𝑉 βˆ’ π‘ˆ) dπ‘₯ = βˆ«β„if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) dπ‘₯)
2914, 290ax-mp 5 . . 3 ∫(𝐴[,]𝐡)(𝑉 βˆ’ π‘ˆ) dπ‘₯ = βˆ«β„if(π‘₯ ∈ (𝐴[,]𝐡), (𝑉 βˆ’ π‘ˆ), 0) dπ‘₯
29261, 58addcli 11168 . . . . . 6 (𝐹 + 𝐸) ∈ β„‚
293 2cnne0 12370 . . . . . 6 (2 ∈ β„‚ ∧ 2 β‰  0)
294 div32 11840 . . . . . 6 (((𝐹 + 𝐸) ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0) ∧ (𝐡 βˆ’ 𝐴) ∈ β„‚) β†’ (((𝐹 + 𝐸) / 2) Β· (𝐡 βˆ’ 𝐴)) = ((𝐹 + 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2)))
295292, 293, 147, 294mp3an 1462 . . . . 5 (((𝐹 + 𝐸) / 2) Β· (𝐡 βˆ’ 𝐴)) = ((𝐹 + 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2))
29626, 8addcli 11168 . . . . . 6 (𝐷 + 𝐢) ∈ β„‚
297 div32 11840 . . . . . 6 (((𝐷 + 𝐢) ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0) ∧ (𝐡 βˆ’ 𝐴) ∈ β„‚) β†’ (((𝐷 + 𝐢) / 2) Β· (𝐡 βˆ’ 𝐴)) = ((𝐷 + 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2)))
298296, 293, 147, 297mp3an 1462 . . . . 5 (((𝐷 + 𝐢) / 2) Β· (𝐡 βˆ’ 𝐴)) = ((𝐷 + 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2))
299295, 298oveq12i 7374 . . . 4 ((((𝐹 + 𝐸) / 2) Β· (𝐡 βˆ’ 𝐴)) βˆ’ (((𝐷 + 𝐢) / 2) Β· (𝐡 βˆ’ 𝐴))) = (((𝐹 + 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2)) βˆ’ ((𝐷 + 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2)))
300 2cn 12235 . . . . . 6 2 ∈ β„‚
301 2ne0 12264 . . . . . 6 2 β‰  0
302292, 300, 301divcli 11904 . . . . 5 ((𝐹 + 𝐸) / 2) ∈ β„‚
303296, 300, 301divcli 11904 . . . . 5 ((𝐷 + 𝐢) / 2) ∈ β„‚
304302, 303, 147subdiri 11612 . . . 4 ((((𝐹 + 𝐸) / 2) βˆ’ ((𝐷 + 𝐢) / 2)) Β· (𝐡 βˆ’ 𝐴)) = ((((𝐹 + 𝐸) / 2) Β· (𝐡 βˆ’ 𝐴)) βˆ’ (((𝐷 + 𝐢) / 2) Β· (𝐡 βˆ’ 𝐴)))
305114adantl 483 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝑉 ∈ ℝ)
306263mptru 1549 . . . . . . . . 9 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝑉) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
307 cniccibl 25221 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝑉) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝑉) ∈ 𝐿1)
3081, 2, 306, 307mp3an 1462 . . . . . . . 8 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝑉) ∈ 𝐿1
309308a1i 11 . . . . . . 7 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝑉) ∈ 𝐿1)
310113adantl 483 . . . . . . 7 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ π‘ˆ ∈ ℝ)
311274mptru 1549 . . . . . . . . 9 (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘ˆ) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
312 cniccibl 25221 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘ˆ) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘ˆ) ∈ 𝐿1)
3131, 2, 311, 312mp3an 1462 . . . . . . . 8 (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘ˆ) ∈ 𝐿1
314313a1i 11 . . . . . . 7 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘ˆ) ∈ 𝐿1)
315305, 309, 310, 314itgsub 25206 . . . . . 6 (⊀ β†’ ∫(𝐴[,]𝐡)(𝑉 βˆ’ π‘ˆ) dπ‘₯ = (∫(𝐴[,]𝐡)𝑉 dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)π‘ˆ dπ‘₯))
316315mptru 1549 . . . . 5 ∫(𝐴[,]𝐡)(𝑉 βˆ’ π‘ˆ) dπ‘₯ = (∫(𝐴[,]𝐡)𝑉 dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)π‘ˆ dπ‘₯)
31758, 300, 301divcan4i 11909 . . . . . . . . . . 11 ((𝐸 Β· 2) / 2) = 𝐸
318317oveq1i 7372 . . . . . . . . . 10 (((𝐸 Β· 2) / 2) Β· (𝐡 βˆ’ 𝐴)) = (𝐸 Β· (𝐡 βˆ’ 𝐴))
31958, 300mulcli 11169 . . . . . . . . . . 11 (𝐸 Β· 2) ∈ β„‚
320 div32 11840 . . . . . . . . . . 11 (((𝐸 Β· 2) ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0) ∧ (𝐡 βˆ’ 𝐴) ∈ β„‚) β†’ (((𝐸 Β· 2) / 2) Β· (𝐡 βˆ’ 𝐴)) = ((𝐸 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2)))
321319, 293, 147, 320mp3an 1462 . . . . . . . . . 10 (((𝐸 Β· 2) / 2) Β· (𝐡 βˆ’ 𝐴)) = ((𝐸 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2))
322318, 321eqtr3i 2767 . . . . . . . . 9 (𝐸 Β· (𝐡 βˆ’ 𝐴)) = ((𝐸 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2))
323322oveq1i 7372 . . . . . . . 8 ((𝐸 Β· (𝐡 βˆ’ 𝐴)) + ((𝐹 βˆ’ 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2))) = (((𝐸 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2)) + ((𝐹 βˆ’ 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2)))
324 itgeq2 25158 . . . . . . . . . 10 (βˆ€π‘₯ ∈ (𝐴[,]𝐡)𝑉 = (𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) β†’ ∫(𝐴[,]𝐡)𝑉 dπ‘₯ = ∫(𝐴[,]𝐡)(𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) dπ‘₯)
32566a1i 11 . . . . . . . . . 10 (π‘₯ ∈ (𝐴[,]𝐡) β†’ 𝑉 = (𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))))
326324, 325mprg 3071 . . . . . . . . 9 ∫(𝐴[,]𝐡)𝑉 dπ‘₯ = ∫(𝐴[,]𝐡)(𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) dπ‘₯
32757a1i 11 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝐸 ∈ ℝ)
328 cniccibl 25221 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐸) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐸) ∈ 𝐿1)
3291, 2, 233, 328mp3an 1462 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐸) ∈ 𝐿1
330329a1i 11 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐸) ∈ 𝐿1)
331126adantl 483 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) ∈ ℝ)
33260a1i 11 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝐹 ∈ ℝ)
333332, 327resubcld 11590 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ (𝐹 βˆ’ 𝐸) ∈ ℝ)
334331, 333remulcld 11192 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)) ∈ ℝ)
335261mptru 1549 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
336 cniccibl 25221 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) ∈ 𝐿1)
3371, 2, 335, 336mp3an 1462 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) ∈ 𝐿1
338337a1i 11 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) ∈ 𝐿1)
339327, 330, 334, 338itgadd 25205 . . . . . . . . . 10 (⊀ β†’ ∫(𝐴[,]𝐡)(𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) dπ‘₯ = (∫(𝐴[,]𝐡)𝐸 dπ‘₯ + ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)) dπ‘₯))
340339mptru 1549 . . . . . . . . 9 ∫(𝐴[,]𝐡)(𝐸 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸))) dπ‘₯ = (∫(𝐴[,]𝐡)𝐸 dπ‘₯ + ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)) dπ‘₯)
341 iccmbl 24946 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ) β†’ (𝐴[,]𝐡) ∈ dom vol)
3421, 2, 341mp2an 691 . . . . . . . . . . . 12 (𝐴[,]𝐡) ∈ dom vol
343 mblvol 24910 . . . . . . . . . . . . . . 15 ((𝐴[,]𝐡) ∈ dom vol β†’ (volβ€˜(𝐴[,]𝐡)) = (vol*β€˜(𝐴[,]𝐡)))
344342, 343ax-mp 5 . . . . . . . . . . . . . 14 (volβ€˜(𝐴[,]𝐡)) = (vol*β€˜(𝐴[,]𝐡))
3451, 2, 17ltleii 11285 . . . . . . . . . . . . . . 15 𝐴 ≀ 𝐡
346 ovolicc 24903 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐴 ≀ 𝐡) β†’ (vol*β€˜(𝐴[,]𝐡)) = (𝐡 βˆ’ 𝐴))
3471, 2, 345, 346mp3an 1462 . . . . . . . . . . . . . 14 (vol*β€˜(𝐴[,]𝐡)) = (𝐡 βˆ’ 𝐴)
348344, 347eqtri 2765 . . . . . . . . . . . . 13 (volβ€˜(𝐴[,]𝐡)) = (𝐡 βˆ’ 𝐴)
349348, 12eqeltri 2834 . . . . . . . . . . . 12 (volβ€˜(𝐴[,]𝐡)) ∈ ℝ
350 itgconst 25199 . . . . . . . . . . . 12 (((𝐴[,]𝐡) ∈ dom vol ∧ (volβ€˜(𝐴[,]𝐡)) ∈ ℝ ∧ 𝐸 ∈ β„‚) β†’ ∫(𝐴[,]𝐡)𝐸 dπ‘₯ = (𝐸 Β· (volβ€˜(𝐴[,]𝐡))))
351342, 349, 58, 350mp3an 1462 . . . . . . . . . . 11 ∫(𝐴[,]𝐡)𝐸 dπ‘₯ = (𝐸 Β· (volβ€˜(𝐴[,]𝐡)))
352348oveq2i 7373 . . . . . . . . . . 11 (𝐸 Β· (volβ€˜(𝐴[,]𝐡))) = (𝐸 Β· (𝐡 βˆ’ 𝐴))
353351, 352eqtri 2765 . . . . . . . . . 10 ∫(𝐴[,]𝐡)𝐸 dπ‘₯ = (𝐸 Β· (𝐡 βˆ’ 𝐴))
35461a1i 11 . . . . . . . . . . . . . 14 (⊀ β†’ 𝐹 ∈ β„‚)
35558a1i 11 . . . . . . . . . . . . . 14 (⊀ β†’ 𝐸 ∈ β„‚)
356354, 355subcld 11519 . . . . . . . . . . . . 13 (⊀ β†’ (𝐹 βˆ’ 𝐸) ∈ β„‚)
357256mptru 1549 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) ↦ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
358 cniccibl 25221 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ 𝐿1)
3591, 2, 357, 358mp3an 1462 . . . . . . . . . . . . . 14 (π‘₯ ∈ (𝐴[,]𝐡) ↦ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ 𝐿1
360359a1i 11 . . . . . . . . . . . . 13 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) ∈ 𝐿1)
361356, 331, 360itgmulc2 25214 . . . . . . . . . . . 12 (⊀ β†’ ((𝐹 βˆ’ 𝐸) Β· ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯) = ∫(𝐴[,]𝐡)((𝐹 βˆ’ 𝐸) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) dπ‘₯)
362361mptru 1549 . . . . . . . . . . 11 ((𝐹 βˆ’ 𝐸) Β· ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯) = ∫(𝐴[,]𝐡)((𝐹 βˆ’ 𝐸) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) dπ‘₯
363 itgeq2 25158 . . . . . . . . . . . . . . 15 (βˆ€π‘₯ ∈ (𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) = ((1 / (𝐡 βˆ’ 𝐴)) Β· (π‘₯ βˆ’ 𝐴)) β†’ ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯ = ∫(𝐴[,]𝐡)((1 / (𝐡 βˆ’ 𝐴)) Β· (π‘₯ βˆ’ 𝐴)) dπ‘₯)
364137recnd 11190 . . . . . . . . . . . . . . . 16 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (π‘₯ βˆ’ 𝐴) ∈ β„‚)
365364, 237, 238divrec2d 11942 . . . . . . . . . . . . . . 15 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) = ((1 / (𝐡 βˆ’ 𝐴)) Β· (π‘₯ βˆ’ 𝐴)))
366363, 365mprg 3071 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯ = ∫(𝐴[,]𝐡)((1 / (𝐡 βˆ’ 𝐴)) Β· (π‘₯ βˆ’ 𝐴)) dπ‘₯
3675adantl 483 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ π‘₯ ∈ ℝ)
368 cncfmptid 24292 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘₯) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
369230, 231, 368mp2an 691 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘₯) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
370 cniccibl 25221 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘₯) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘₯) ∈ 𝐿1)
3711, 2, 369, 370mp3an 1462 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘₯) ∈ 𝐿1
372371a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ π‘₯) ∈ 𝐿1)
3731a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝐴 ∈ ℝ)
374 cncfmptc 24291 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ β„‚ ∧ (𝐴[,]𝐡) βŠ† β„‚ ∧ β„‚ βŠ† β„‚) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐴) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚))
375139, 230, 231, 374mp3an 1462 . . . . . . . . . . . . . . . . . . . . . 22 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐴) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
376 cniccibl 25221 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐴) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐴) ∈ 𝐿1)
3771, 2, 375, 376mp3an 1462 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐴) ∈ 𝐿1
378377a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐴) ∈ 𝐿1)
379367, 372, 373, 378itgsub 25206 . . . . . . . . . . . . . . . . . . 19 (⊀ β†’ ∫(𝐴[,]𝐡)(π‘₯ βˆ’ 𝐴) dπ‘₯ = (∫(𝐴[,]𝐡)π‘₯ dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)𝐴 dπ‘₯))
380379mptru 1549 . . . . . . . . . . . . . . . . . 18 ∫(𝐴[,]𝐡)(π‘₯ βˆ’ 𝐴) dπ‘₯ = (∫(𝐴[,]𝐡)π‘₯ dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)𝐴 dπ‘₯)
3811a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊀ β†’ 𝐴 ∈ ℝ)
3822a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊀ β†’ 𝐡 ∈ ℝ)
383345a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊀ β†’ 𝐴 ≀ 𝐡)
384 1nn0 12436 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ β„•0
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊀ β†’ 1 ∈ β„•0)
386381, 382, 383, 385itgpowd 25430 . . . . . . . . . . . . . . . . . . . . . 22 (⊀ β†’ ∫(𝐴[,]𝐡)(π‘₯↑1) dπ‘₯ = (((𝐡↑(1 + 1)) βˆ’ (𝐴↑(1 + 1))) / (1 + 1)))
387386mptru 1549 . . . . . . . . . . . . . . . . . . . . 21 ∫(𝐴[,]𝐡)(π‘₯↑1) dπ‘₯ = (((𝐡↑(1 + 1)) βˆ’ (𝐴↑(1 + 1))) / (1 + 1))
388 1p1e2 12285 . . . . . . . . . . . . . . . . . . . . . 22 (1 + 1) = 2
389388oveq2i 7373 . . . . . . . . . . . . . . . . . . . . 21 (((𝐡↑(1 + 1)) βˆ’ (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐡↑(1 + 1)) βˆ’ (𝐴↑(1 + 1))) / 2)
390387, 389eqtri 2765 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐡)(π‘₯↑1) dπ‘₯ = (((𝐡↑(1 + 1)) βˆ’ (𝐴↑(1 + 1))) / 2)
391 itgeq2 25158 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘₯ ∈ (𝐴[,]𝐡)(π‘₯↑1) = π‘₯ β†’ ∫(𝐴[,]𝐡)(π‘₯↑1) dπ‘₯ = ∫(𝐴[,]𝐡)π‘₯ dπ‘₯)
392235exp1d 14053 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (π‘₯↑1) = π‘₯)
393391, 392mprg 3071 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐡)(π‘₯↑1) dπ‘₯ = ∫(𝐴[,]𝐡)π‘₯ dπ‘₯
394388oveq2i 7373 . . . . . . . . . . . . . . . . . . . . . 22 (𝐡↑(1 + 1)) = (𝐡↑2)
395388oveq2i 7373 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴↑(1 + 1)) = (𝐴↑2)
396394, 395oveq12i 7374 . . . . . . . . . . . . . . . . . . . . 21 ((𝐡↑(1 + 1)) βˆ’ (𝐴↑(1 + 1))) = ((𝐡↑2) βˆ’ (𝐴↑2))
397396oveq1i 7372 . . . . . . . . . . . . . . . . . . . 20 (((𝐡↑(1 + 1)) βˆ’ (𝐴↑(1 + 1))) / 2) = (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)
398390, 393, 3973eqtr3i 2773 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐡)π‘₯ dπ‘₯ = (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)
399 itgconst 25199 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴[,]𝐡) ∈ dom vol ∧ (volβ€˜(𝐴[,]𝐡)) ∈ ℝ ∧ 𝐴 ∈ β„‚) β†’ ∫(𝐴[,]𝐡)𝐴 dπ‘₯ = (𝐴 Β· (volβ€˜(𝐴[,]𝐡))))
400342, 349, 139, 399mp3an 1462 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐡)𝐴 dπ‘₯ = (𝐴 Β· (volβ€˜(𝐴[,]𝐡)))
401348oveq2i 7373 . . . . . . . . . . . . . . . . . . . 20 (𝐴 Β· (volβ€˜(𝐴[,]𝐡))) = (𝐴 Β· (𝐡 βˆ’ 𝐴))
402400, 401eqtri 2765 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐡)𝐴 dπ‘₯ = (𝐴 Β· (𝐡 βˆ’ 𝐴))
403398, 402oveq12i 7374 . . . . . . . . . . . . . . . . . 18 (∫(𝐴[,]𝐡)π‘₯ dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)𝐴 dπ‘₯) = ((((𝐡↑2) βˆ’ (𝐴↑2)) / 2) βˆ’ (𝐴 Β· (𝐡 βˆ’ 𝐴)))
404380, 403eqtri 2765 . . . . . . . . . . . . . . . . 17 ∫(𝐴[,]𝐡)(π‘₯ βˆ’ 𝐴) dπ‘₯ = ((((𝐡↑2) βˆ’ (𝐴↑2)) / 2) βˆ’ (𝐴 Β· (𝐡 βˆ’ 𝐴)))
405404oveq2i 7373 . . . . . . . . . . . . . . . 16 ((1 / (𝐡 βˆ’ 𝐴)) Β· ∫(𝐴[,]𝐡)(π‘₯ βˆ’ 𝐴) dπ‘₯) = ((1 / (𝐡 βˆ’ 𝐴)) Β· ((((𝐡↑2) βˆ’ (𝐴↑2)) / 2) βˆ’ (𝐴 Β· (𝐡 βˆ’ 𝐴))))
40614a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊀ β†’ 𝐡 ∈ β„‚)
407139a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊀ β†’ 𝐴 ∈ β„‚)
408406, 407subcld 11519 . . . . . . . . . . . . . . . . . . 19 (⊀ β†’ (𝐡 βˆ’ 𝐴) ∈ β„‚)
40918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊀ β†’ 𝐡 β‰  𝐴)
410406, 407, 409subne0d 11528 . . . . . . . . . . . . . . . . . . 19 (⊀ β†’ (𝐡 βˆ’ 𝐴) β‰  0)
411408, 410reccld 11931 . . . . . . . . . . . . . . . . . 18 (⊀ β†’ (1 / (𝐡 βˆ’ 𝐴)) ∈ β„‚)
412411mptru 1549 . . . . . . . . . . . . . . . . 17 (1 / (𝐡 βˆ’ 𝐴)) ∈ β„‚
41314sqcli 14092 . . . . . . . . . . . . . . . . . . 19 (𝐡↑2) ∈ β„‚
414139sqcli 14092 . . . . . . . . . . . . . . . . . . 19 (𝐴↑2) ∈ β„‚
415413, 414subcli 11484 . . . . . . . . . . . . . . . . . 18 ((𝐡↑2) βˆ’ (𝐴↑2)) ∈ β„‚
416415, 300, 301divcli 11904 . . . . . . . . . . . . . . . . 17 (((𝐡↑2) βˆ’ (𝐴↑2)) / 2) ∈ β„‚
417139, 147mulcli 11169 . . . . . . . . . . . . . . . . 17 (𝐴 Β· (𝐡 βˆ’ 𝐴)) ∈ β„‚
418412, 416, 417subdii 11611 . . . . . . . . . . . . . . . 16 ((1 / (𝐡 βˆ’ 𝐴)) Β· ((((𝐡↑2) βˆ’ (𝐴↑2)) / 2) βˆ’ (𝐴 Β· (𝐡 βˆ’ 𝐴)))) = (((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)) βˆ’ ((1 / (𝐡 βˆ’ 𝐴)) Β· (𝐴 Β· (𝐡 βˆ’ 𝐴))))
419405, 418eqtri 2765 . . . . . . . . . . . . . . 15 ((1 / (𝐡 βˆ’ 𝐴)) Β· ∫(𝐴[,]𝐡)(π‘₯ βˆ’ 𝐴) dπ‘₯) = (((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)) βˆ’ ((1 / (𝐡 βˆ’ 𝐴)) Β· (𝐴 Β· (𝐡 βˆ’ 𝐴))))
420137adantl 483 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ (π‘₯ βˆ’ 𝐴) ∈ ℝ)
421367, 372, 373, 378iblsub 25202 . . . . . . . . . . . . . . . . 17 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (π‘₯ βˆ’ 𝐴)) ∈ 𝐿1)
422411, 420, 421itgmulc2 25214 . . . . . . . . . . . . . . . 16 (⊀ β†’ ((1 / (𝐡 βˆ’ 𝐴)) Β· ∫(𝐴[,]𝐡)(π‘₯ βˆ’ 𝐴) dπ‘₯) = ∫(𝐴[,]𝐡)((1 / (𝐡 βˆ’ 𝐴)) Β· (π‘₯ βˆ’ 𝐴)) dπ‘₯)
423422mptru 1549 . . . . . . . . . . . . . . 15 ((1 / (𝐡 βˆ’ 𝐴)) Β· ∫(𝐴[,]𝐡)(π‘₯ βˆ’ 𝐴) dπ‘₯) = ∫(𝐴[,]𝐡)((1 / (𝐡 βˆ’ 𝐴)) Β· (π‘₯ βˆ’ 𝐴)) dπ‘₯
424412, 417mulcomi 11170 . . . . . . . . . . . . . . . . 17 ((1 / (𝐡 βˆ’ 𝐴)) Β· (𝐴 Β· (𝐡 βˆ’ 𝐴))) = ((𝐴 Β· (𝐡 βˆ’ 𝐴)) Β· (1 / (𝐡 βˆ’ 𝐴)))
425417, 147, 21divreci 11907 . . . . . . . . . . . . . . . . 17 ((𝐴 Β· (𝐡 βˆ’ 𝐴)) / (𝐡 βˆ’ 𝐴)) = ((𝐴 Β· (𝐡 βˆ’ 𝐴)) Β· (1 / (𝐡 βˆ’ 𝐴)))
426139, 147, 21divcan4i 11909 . . . . . . . . . . . . . . . . 17 ((𝐴 Β· (𝐡 βˆ’ 𝐴)) / (𝐡 βˆ’ 𝐴)) = 𝐴
427424, 425, 4263eqtr2i 2771 . . . . . . . . . . . . . . . 16 ((1 / (𝐡 βˆ’ 𝐴)) Β· (𝐴 Β· (𝐡 βˆ’ 𝐴))) = 𝐴
428427oveq2i 7373 . . . . . . . . . . . . . . 15 (((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)) βˆ’ ((1 / (𝐡 βˆ’ 𝐴)) Β· (𝐴 Β· (𝐡 βˆ’ 𝐴)))) = (((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)) βˆ’ 𝐴)
429419, 423, 4283eqtr3i 2773 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐡)((1 / (𝐡 βˆ’ 𝐴)) Β· (π‘₯ βˆ’ 𝐴)) dπ‘₯ = (((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)) βˆ’ 𝐴)
430366, 429eqtri 2765 . . . . . . . . . . . . 13 ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯ = (((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)) βˆ’ 𝐴)
43114, 139subsqi 14124 . . . . . . . . . . . . . . . . 17 ((𝐡↑2) βˆ’ (𝐴↑2)) = ((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴))
432431oveq1i 7372 . . . . . . . . . . . . . . . 16 (((𝐡↑2) βˆ’ (𝐴↑2)) / 2) = (((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴)) / 2)
433432oveq2i 7373 . . . . . . . . . . . . . . 15 ((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)) = ((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴)) / 2))
434431, 415eqeltrri 2835 . . . . . . . . . . . . . . . 16 ((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴)) ∈ β„‚
435412, 434, 300, 301divassi 11918 . . . . . . . . . . . . . . 15 (((1 / (𝐡 βˆ’ 𝐴)) Β· ((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴))) / 2) = ((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴)) / 2))
436412, 434mulcomi 11170 . . . . . . . . . . . . . . . . 17 ((1 / (𝐡 βˆ’ 𝐴)) Β· ((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴))) = (((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴)) Β· (1 / (𝐡 βˆ’ 𝐴)))
437434, 147, 21divreci 11907 . . . . . . . . . . . . . . . . 17 (((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴)) / (𝐡 βˆ’ 𝐴)) = (((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴)) Β· (1 / (𝐡 βˆ’ 𝐴)))
43814, 139addcli 11168 . . . . . . . . . . . . . . . . . 18 (𝐡 + 𝐴) ∈ β„‚
439438, 147, 21divcan4i 11909 . . . . . . . . . . . . . . . . 17 (((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴)) / (𝐡 βˆ’ 𝐴)) = (𝐡 + 𝐴)
440436, 437, 4393eqtr2i 2771 . . . . . . . . . . . . . . . 16 ((1 / (𝐡 βˆ’ 𝐴)) Β· ((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴))) = (𝐡 + 𝐴)
441440oveq1i 7372 . . . . . . . . . . . . . . 15 (((1 / (𝐡 βˆ’ 𝐴)) Β· ((𝐡 + 𝐴) Β· (𝐡 βˆ’ 𝐴))) / 2) = ((𝐡 + 𝐴) / 2)
442433, 435, 4413eqtr2i 2771 . . . . . . . . . . . . . 14 ((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)) = ((𝐡 + 𝐴) / 2)
443442oveq1i 7372 . . . . . . . . . . . . 13 (((1 / (𝐡 βˆ’ 𝐴)) Β· (((𝐡↑2) βˆ’ (𝐴↑2)) / 2)) βˆ’ 𝐴) = (((𝐡 + 𝐴) / 2) βˆ’ 𝐴)
444139, 300mulcli 11169 . . . . . . . . . . . . . . 15 (𝐴 Β· 2) ∈ β„‚
445 divsubdir 11856 . . . . . . . . . . . . . . 15 (((𝐡 + 𝐴) ∈ β„‚ ∧ (𝐴 Β· 2) ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0)) β†’ (((𝐡 + 𝐴) βˆ’ (𝐴 Β· 2)) / 2) = (((𝐡 + 𝐴) / 2) βˆ’ ((𝐴 Β· 2) / 2)))
446438, 444, 293, 445mp3an 1462 . . . . . . . . . . . . . 14 (((𝐡 + 𝐴) βˆ’ (𝐴 Β· 2)) / 2) = (((𝐡 + 𝐴) / 2) βˆ’ ((𝐴 Β· 2) / 2))
44714, 139, 444addsubassi 11499 . . . . . . . . . . . . . . . 16 ((𝐡 + 𝐴) βˆ’ (𝐴 Β· 2)) = (𝐡 + (𝐴 βˆ’ (𝐴 Β· 2)))
448 subsub2 11436 . . . . . . . . . . . . . . . . 17 ((𝐡 ∈ β„‚ ∧ (𝐴 Β· 2) ∈ β„‚ ∧ 𝐴 ∈ β„‚) β†’ (𝐡 βˆ’ ((𝐴 Β· 2) βˆ’ 𝐴)) = (𝐡 + (𝐴 βˆ’ (𝐴 Β· 2))))
44914, 444, 139, 448mp3an 1462 . . . . . . . . . . . . . . . 16 (𝐡 βˆ’ ((𝐴 Β· 2) βˆ’ 𝐴)) = (𝐡 + (𝐴 βˆ’ (𝐴 Β· 2)))
450139times2i 12299 . . . . . . . . . . . . . . . . . . 19 (𝐴 Β· 2) = (𝐴 + 𝐴)
451450oveq1i 7372 . . . . . . . . . . . . . . . . . 18 ((𝐴 Β· 2) βˆ’ 𝐴) = ((𝐴 + 𝐴) βˆ’ 𝐴)
452139, 139pncan3oi 11424 . . . . . . . . . . . . . . . . . 18 ((𝐴 + 𝐴) βˆ’ 𝐴) = 𝐴
453451, 452eqtri 2765 . . . . . . . . . . . . . . . . 17 ((𝐴 Β· 2) βˆ’ 𝐴) = 𝐴
454453oveq2i 7373 . . . . . . . . . . . . . . . 16 (𝐡 βˆ’ ((𝐴 Β· 2) βˆ’ 𝐴)) = (𝐡 βˆ’ 𝐴)
455447, 449, 4543eqtr2i 2771 . . . . . . . . . . . . . . 15 ((𝐡 + 𝐴) βˆ’ (𝐴 Β· 2)) = (𝐡 βˆ’ 𝐴)
456455oveq1i 7372 . . . . . . . . . . . . . 14 (((𝐡 + 𝐴) βˆ’ (𝐴 Β· 2)) / 2) = ((𝐡 βˆ’ 𝐴) / 2)
457139, 300, 301divcan4i 11909 . . . . . . . . . . . . . . 15 ((𝐴 Β· 2) / 2) = 𝐴
458457oveq2i 7373 . . . . . . . . . . . . . 14 (((𝐡 + 𝐴) / 2) βˆ’ ((𝐴 Β· 2) / 2)) = (((𝐡 + 𝐴) / 2) βˆ’ 𝐴)
459446, 456, 4583eqtr3ri 2774 . . . . . . . . . . . . 13 (((𝐡 + 𝐴) / 2) βˆ’ 𝐴) = ((𝐡 βˆ’ 𝐴) / 2)
460430, 443, 4593eqtri 2769 . . . . . . . . . . . 12 ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯ = ((𝐡 βˆ’ 𝐴) / 2)
461460oveq2i 7373 . . . . . . . . . . 11 ((𝐹 βˆ’ 𝐸) Β· ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯) = ((𝐹 βˆ’ 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2))
462 itgeq2 25158 . . . . . . . . . . . 12 (βˆ€π‘₯ ∈ (𝐴[,]𝐡)((𝐹 βˆ’ 𝐸) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) = (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)) β†’ ∫(𝐴[,]𝐡)((𝐹 βˆ’ 𝐸) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) dπ‘₯ = ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)) dπ‘₯)
46361, 58subcli 11484 . . . . . . . . . . . . . 14 (𝐹 βˆ’ 𝐸) ∈ β„‚
464463a1i 11 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐹 βˆ’ 𝐸) ∈ β„‚)
465464, 127mulcomd 11183 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((𝐹 βˆ’ 𝐸) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) = (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)))
466462, 465mprg 3071 . . . . . . . . . . 11 ∫(𝐴[,]𝐡)((𝐹 βˆ’ 𝐸) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) dπ‘₯ = ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)) dπ‘₯
467362, 461, 4663eqtr3ri 2774 . . . . . . . . . 10 ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)) dπ‘₯ = ((𝐹 βˆ’ 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2))
468353, 467oveq12i 7374 . . . . . . . . 9 (∫(𝐴[,]𝐡)𝐸 dπ‘₯ + ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐹 βˆ’ 𝐸)) dπ‘₯) = ((𝐸 Β· (𝐡 βˆ’ 𝐴)) + ((𝐹 βˆ’ 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2)))
469326, 340, 4683eqtri 2769 . . . . . . . 8 ∫(𝐴[,]𝐡)𝑉 dπ‘₯ = ((𝐸 Β· (𝐡 βˆ’ 𝐴)) + ((𝐹 βˆ’ 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2)))
470147, 300, 301divcli 11904 . . . . . . . . 9 ((𝐡 βˆ’ 𝐴) / 2) ∈ β„‚
471319, 463, 470adddiri 11175 . . . . . . . 8 (((𝐸 Β· 2) + (𝐹 βˆ’ 𝐸)) Β· ((𝐡 βˆ’ 𝐴) / 2)) = (((𝐸 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2)) + ((𝐹 βˆ’ 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2)))
472323, 469, 4713eqtr4i 2775 . . . . . . 7 ∫(𝐴[,]𝐡)𝑉 dπ‘₯ = (((𝐸 Β· 2) + (𝐹 βˆ’ 𝐸)) Β· ((𝐡 βˆ’ 𝐴) / 2))
473 addsub12 11421 . . . . . . . . . 10 ((𝐹 ∈ β„‚ ∧ (𝐸 Β· 2) ∈ β„‚ ∧ 𝐸 ∈ β„‚) β†’ (𝐹 + ((𝐸 Β· 2) βˆ’ 𝐸)) = ((𝐸 Β· 2) + (𝐹 βˆ’ 𝐸)))
47461, 319, 58, 473mp3an 1462 . . . . . . . . 9 (𝐹 + ((𝐸 Β· 2) βˆ’ 𝐸)) = ((𝐸 Β· 2) + (𝐹 βˆ’ 𝐸))
47558times2i 12299 . . . . . . . . . . . 12 (𝐸 Β· 2) = (𝐸 + 𝐸)
476475oveq1i 7372 . . . . . . . . . . 11 ((𝐸 Β· 2) βˆ’ 𝐸) = ((𝐸 + 𝐸) βˆ’ 𝐸)
47758, 58pncan3oi 11424 . . . . . . . . . . 11 ((𝐸 + 𝐸) βˆ’ 𝐸) = 𝐸
478476, 477eqtri 2765 . . . . . . . . . 10 ((𝐸 Β· 2) βˆ’ 𝐸) = 𝐸
479478oveq2i 7373 . . . . . . . . 9 (𝐹 + ((𝐸 Β· 2) βˆ’ 𝐸)) = (𝐹 + 𝐸)
480474, 479eqtr3i 2767 . . . . . . . 8 ((𝐸 Β· 2) + (𝐹 βˆ’ 𝐸)) = (𝐹 + 𝐸)
481480oveq1i 7372 . . . . . . 7 (((𝐸 Β· 2) + (𝐹 βˆ’ 𝐸)) Β· ((𝐡 βˆ’ 𝐴) / 2)) = ((𝐹 + 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2))
482472, 481eqtri 2765 . . . . . 6 ∫(𝐴[,]𝐡)𝑉 dπ‘₯ = ((𝐹 + 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2))
4838, 300, 301divcan4i 11909 . . . . . . . . . . 11 ((𝐢 Β· 2) / 2) = 𝐢
484483oveq1i 7372 . . . . . . . . . 10 (((𝐢 Β· 2) / 2) Β· (𝐡 βˆ’ 𝐴)) = (𝐢 Β· (𝐡 βˆ’ 𝐴))
4858, 300mulcli 11169 . . . . . . . . . . 11 (𝐢 Β· 2) ∈ β„‚
486 div32 11840 . . . . . . . . . . 11 (((𝐢 Β· 2) ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0) ∧ (𝐡 βˆ’ 𝐴) ∈ β„‚) β†’ (((𝐢 Β· 2) / 2) Β· (𝐡 βˆ’ 𝐴)) = ((𝐢 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2)))
487485, 293, 147, 486mp3an 1462 . . . . . . . . . 10 (((𝐢 Β· 2) / 2) Β· (𝐡 βˆ’ 𝐴)) = ((𝐢 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2))
488484, 487eqtr3i 2767 . . . . . . . . 9 (𝐢 Β· (𝐡 βˆ’ 𝐴)) = ((𝐢 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2))
489488oveq1i 7372 . . . . . . . 8 ((𝐢 Β· (𝐡 βˆ’ 𝐴)) + ((𝐷 βˆ’ 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2))) = (((𝐢 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2)) + ((𝐷 βˆ’ 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2)))
49031a1i 11 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ π‘ˆ = (𝐢 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))))
491490itgeq2dv 25162 . . . . . . . . . 10 (⊀ β†’ ∫(𝐴[,]𝐡)π‘ˆ dπ‘₯ = ∫(𝐴[,]𝐡)(𝐢 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) dπ‘₯)
492491mptru 1549 . . . . . . . . 9 ∫(𝐴[,]𝐡)π‘ˆ dπ‘₯ = ∫(𝐴[,]𝐡)(𝐢 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) dπ‘₯
4937a1i 11 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝐢 ∈ ℝ)
494 cniccibl 25221 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐢) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐢) ∈ 𝐿1)
4951, 2, 266, 494mp3an 1462 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐢) ∈ 𝐿1
496495a1i 11 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ 𝐢) ∈ 𝐿1)
49725a1i 11 . . . . . . . . . . . . 13 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ 𝐷 ∈ ℝ)
498497, 493resubcld 11590 . . . . . . . . . . . 12 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ (𝐷 βˆ’ 𝐢) ∈ ℝ)
499331, 498remulcld 11192 . . . . . . . . . . 11 ((⊀ ∧ π‘₯ ∈ (𝐴[,]𝐡)) β†’ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)) ∈ ℝ)
500272mptru 1549 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)
501 cniccibl 25221 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) ∈ ((𝐴[,]𝐡)–cnβ†’β„‚)) β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) ∈ 𝐿1)
5021, 2, 500, 501mp3an 1462 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) ∈ 𝐿1
503502a1i 11 . . . . . . . . . . 11 (⊀ β†’ (π‘₯ ∈ (𝐴[,]𝐡) ↦ (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) ∈ 𝐿1)
504493, 496, 499, 503itgadd 25205 . . . . . . . . . 10 (⊀ β†’ ∫(𝐴[,]𝐡)(𝐢 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) dπ‘₯ = (∫(𝐴[,]𝐡)𝐢 dπ‘₯ + ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)) dπ‘₯))
505504mptru 1549 . . . . . . . . 9 ∫(𝐴[,]𝐡)(𝐢 + (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢))) dπ‘₯ = (∫(𝐴[,]𝐡)𝐢 dπ‘₯ + ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)) dπ‘₯)
506 itgconst 25199 . . . . . . . . . . . 12 (((𝐴[,]𝐡) ∈ dom vol ∧ (volβ€˜(𝐴[,]𝐡)) ∈ ℝ ∧ 𝐢 ∈ β„‚) β†’ ∫(𝐴[,]𝐡)𝐢 dπ‘₯ = (𝐢 Β· (volβ€˜(𝐴[,]𝐡))))
507342, 349, 8, 506mp3an 1462 . . . . . . . . . . 11 ∫(𝐴[,]𝐡)𝐢 dπ‘₯ = (𝐢 Β· (volβ€˜(𝐴[,]𝐡)))
508348oveq2i 7373 . . . . . . . . . . 11 (𝐢 Β· (volβ€˜(𝐴[,]𝐡))) = (𝐢 Β· (𝐡 βˆ’ 𝐴))
509507, 508eqtri 2765 . . . . . . . . . 10 ∫(𝐴[,]𝐡)𝐢 dπ‘₯ = (𝐢 Β· (𝐡 βˆ’ 𝐴))
51026a1i 11 . . . . . . . . . . . . . 14 (⊀ β†’ 𝐷 ∈ β„‚)
5118a1i 11 . . . . . . . . . . . . . 14 (⊀ β†’ 𝐢 ∈ β„‚)
512510, 511subcld 11519 . . . . . . . . . . . . 13 (⊀ β†’ (𝐷 βˆ’ 𝐢) ∈ β„‚)
513512, 331, 360itgmulc2 25214 . . . . . . . . . . . 12 (⊀ β†’ ((𝐷 βˆ’ 𝐢) Β· ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯) = ∫(𝐴[,]𝐡)((𝐷 βˆ’ 𝐢) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) dπ‘₯)
514513mptru 1549 . . . . . . . . . . 11 ((𝐷 βˆ’ 𝐢) Β· ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯) = ∫(𝐴[,]𝐡)((𝐷 βˆ’ 𝐢) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) dπ‘₯
515460oveq2i 7373 . . . . . . . . . . 11 ((𝐷 βˆ’ 𝐢) Β· ∫(𝐴[,]𝐡)((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) dπ‘₯) = ((𝐷 βˆ’ 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2))
516 itgeq2 25158 . . . . . . . . . . . 12 (βˆ€π‘₯ ∈ (𝐴[,]𝐡)((𝐷 βˆ’ 𝐢) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) = (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)) β†’ ∫(𝐴[,]𝐡)((𝐷 βˆ’ 𝐢) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) dπ‘₯ = ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)) dπ‘₯)
51726, 8subcli 11484 . . . . . . . . . . . . . 14 (𝐷 βˆ’ 𝐢) ∈ β„‚
518517a1i 11 . . . . . . . . . . . . 13 (π‘₯ ∈ (𝐴[,]𝐡) β†’ (𝐷 βˆ’ 𝐢) ∈ β„‚)
519518, 127mulcomd 11183 . . . . . . . . . . . 12 (π‘₯ ∈ (𝐴[,]𝐡) β†’ ((𝐷 βˆ’ 𝐢) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) = (((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)))
520516, 519mprg 3071 . . . . . . . . . . 11 ∫(𝐴[,]𝐡)((𝐷 βˆ’ 𝐢) Β· ((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴))) dπ‘₯ = ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)) dπ‘₯
521514, 515, 5203eqtr3ri 2774 . . . . . . . . . 10 ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)) dπ‘₯ = ((𝐷 βˆ’ 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2))
522509, 521oveq12i 7374 . . . . . . . . 9 (∫(𝐴[,]𝐡)𝐢 dπ‘₯ + ∫(𝐴[,]𝐡)(((π‘₯ βˆ’ 𝐴) / (𝐡 βˆ’ 𝐴)) Β· (𝐷 βˆ’ 𝐢)) dπ‘₯) = ((𝐢 Β· (𝐡 βˆ’ 𝐴)) + ((𝐷 βˆ’ 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2)))
523492, 505, 5223eqtri 2769 . . . . . . . 8 ∫(𝐴[,]𝐡)π‘ˆ dπ‘₯ = ((𝐢 Β· (𝐡 βˆ’ 𝐴)) + ((𝐷 βˆ’ 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2)))
524485, 517, 470adddiri 11175 . . . . . . . 8 (((𝐢 Β· 2) + (𝐷 βˆ’ 𝐢)) Β· ((𝐡 βˆ’ 𝐴) / 2)) = (((𝐢 Β· 2) Β· ((𝐡 βˆ’ 𝐴) / 2)) + ((𝐷 βˆ’ 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2)))
525489, 523, 5243eqtr4i 2775 . . . . . . 7 ∫(𝐴[,]𝐡)π‘ˆ dπ‘₯ = (((𝐢 Β· 2) + (𝐷 βˆ’ 𝐢)) Β· ((𝐡 βˆ’ 𝐴) / 2))
526 addsub12 11421 . . . . . . . . . 10 ((𝐷 ∈ β„‚ ∧ (𝐢 Β· 2) ∈ β„‚ ∧ 𝐢 ∈ β„‚) β†’ (𝐷 + ((𝐢 Β· 2) βˆ’ 𝐢)) = ((𝐢 Β· 2) + (𝐷 βˆ’ 𝐢)))
52726, 485, 8, 526mp3an 1462 . . . . . . . . 9 (𝐷 + ((𝐢 Β· 2) βˆ’ 𝐢)) = ((𝐢 Β· 2) + (𝐷 βˆ’ 𝐢))
5288times2i 12299 . . . . . . . . . . . 12 (𝐢 Β· 2) = (𝐢 + 𝐢)
529528oveq1i 7372 . . . . . . . . . . 11 ((𝐢 Β· 2) βˆ’ 𝐢) = ((𝐢 + 𝐢) βˆ’ 𝐢)
5308, 8pncan3oi 11424 . . . . . . . . . . 11 ((𝐢 + 𝐢) βˆ’ 𝐢) = 𝐢
531529, 530eqtri 2765 . . . . . . . . . 10 ((𝐢 Β· 2) βˆ’ 𝐢) = 𝐢
532531oveq2i 7373 . . . . . . . . 9 (𝐷 + ((𝐢 Β· 2) βˆ’ 𝐢)) = (𝐷 + 𝐢)
533527, 532eqtr3i 2767 . . . . . . . 8 ((𝐢 Β· 2) + (𝐷 βˆ’ 𝐢)) = (𝐷 + 𝐢)
534533oveq1i 7372 . . . . . . 7 (((𝐢 Β· 2) + (𝐷 βˆ’ 𝐢)) Β· ((𝐡 βˆ’ 𝐴) / 2)) = ((𝐷 + 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2))
535525, 534eqtri 2765 . . . . . 6 ∫(𝐴[,]𝐡)π‘ˆ dπ‘₯ = ((𝐷 + 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2))
536482, 535oveq12i 7374 . . . . 5 (∫(𝐴[,]𝐡)𝑉 dπ‘₯ βˆ’ ∫(𝐴[,]𝐡)π‘ˆ dπ‘₯) = (((𝐹 + 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2)) βˆ’ ((𝐷 + 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2)))
537316, 536eqtri 2765 . . . 4 ∫(𝐴[,]𝐡)(𝑉 βˆ’ π‘ˆ) dπ‘₯ = (((𝐹 + 𝐸) Β· ((𝐡 βˆ’ 𝐴) / 2)) βˆ’ ((𝐷 + 𝐢) Β· ((𝐡 βˆ’ 𝐴) / 2)))
538299, 304, 5373eqtr4ri 2776 . . 3 ∫(𝐴[,]𝐡)(𝑉 βˆ’ π‘ˆ) dπ‘₯ = ((((𝐹 + 𝐸) / 2) βˆ’ ((𝐷 + 𝐢) / 2)) Β· (𝐡 βˆ’ 𝐴))
539289, 291, 5383eqtr2i 2771 . 2 βˆ«β„(volβ€˜(𝑆 β€œ {π‘₯})) dπ‘₯ = ((((𝐹 + 𝐸) / 2) βˆ’ ((𝐷 + 𝐢) / 2)) Β· (𝐡 βˆ’ 𝐴))
540286, 539eqtri 2765 1 (areaβ€˜π‘†) = ((((𝐹 + 𝐸) / 2) βˆ’ ((𝐷 + 𝐢) / 2)) Β· (𝐡 βˆ’ 𝐴))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   ↔ wb 205   ∧ wa 397   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107   β‰  wne 2944  βˆ€wral 3065   βˆ– cdif 3912   βŠ† wss 3915  βˆ…c0 4287  ifcif 4491  {csn 4591  βŸ¨cop 4597   class class class wbr 5110  {copab 5172   ↦ cmpt 5193   Γ— cxp 5636  β—‘ccnv 5637  dom cdm 5638   β†Ύ cres 5640   β€œ cima 5641  Fun wfun 6495  βŸΆwf 6497  β€˜cfv 6501  (class class class)co 7362  β„‚cc 11056  β„cr 11057  0cc0 11058  1c1 11059   + caddc 11061   Β· cmul 11063  +∞cpnf 11193  β„*cxr 11195   < clt 11196   ≀ cle 11197   βˆ’ cmin 11392   / cdiv 11819  2c2 12215  β„•0cn0 12420  [,]cicc 13274  β†‘cexp 13974  TopOpenctopn 17310  β„‚fldccnfld 20812   Cn ccn 22591   Γ—t ctx 22927  β€“cnβ†’ccncf 24255  vol*covol 24842  volcvol 24843  πΏ1cibl 24997  βˆ«citg 24998  areacarea 26321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677  ax-inf2 9584  ax-cc 10378  ax-cnex 11114  ax-resscn 11115  ax-1cn 11116  ax-icn 11117  ax-addcl 11118  ax-addrcl 11119  ax-mulcl 11120  ax-mulrcl 11121  ax-mulcom 11122  ax-addass 11123  ax-mulass 11124  ax-distr 11125  ax-i2m1 11126  ax-1ne0 11127  ax-1rid 11128  ax-rnegex 11129  ax-rrecex 11130  ax-cnre 11131  ax-pre-lttri 11132  ax-pre-lttrn 11133  ax-pre-ltadd 11134  ax-pre-mulgt0 11135  ax-pre-sup 11136  ax-addf 11137  ax-mulf 11138
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rmo 3356  df-reu 3357  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-pss 3934  df-symdif 4207  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-tp 4596  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-disj 5076  df-br 5111  df-opab 5173  df-mpt 5194  df-tr 5228  df-id 5536  df-eprel 5542  df-po 5550  df-so 5551  df-fr 5593  df-se 5594  df-we 5595  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6258  df-ord 6325  df-on 6326  df-lim 6327  df-suc 6328  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-isom 6510  df-riota 7318  df-ov 7365  df-oprab 7366  df-mpo 7367  df-of 7622  df-ofr 7623  df-om 7808  df-1st 7926  df-2nd 7927  df-supp 8098  df-frecs 8217  df-wrecs 8248  df-recs 8322  df-rdg 8361  df-1o 8417  df-2o 8418  df-oadd 8421  df-omul 8422  df-er 8655  df-map 8774  df-pm 8775  df-ixp 8843  df-en 8891  df-dom 8892  df-sdom 8893  df-fin 8894  df-fsupp 9313  df-fi 9354  df-sup 9385  df-inf 9386  df-oi 9453  df-dju 9844  df-card 9882  df-acn 9885  df-pnf 11198  df-mnf 11199  df-xr 11200  df-ltxr 11201  df-le 11202  df-sub 11394  df-neg 11395  df-div 11820  df-nn 12161  df-2 12223  df-3 12224  df-4 12225  df-5 12226  df-6 12227  df-7 12228  df-8 12229  df-9 12230  df-n0 12421  df-z 12507  df-dec 12626  df-uz 12771  df-q 12881  df-rp 12923  df-xneg 13040  df-xadd 13041  df-xmul 13042  df-ioo 13275  df-ioc 13276  df-ico 13277  df-icc 13278  df-fz 13432  df-fzo 13575  df-fl 13704  df-mod 13782  df-seq 13914  df-exp 13975  df-hash 14238  df-cj 14991  df-re 14992  df-im 14993  df-sqrt 15127  df-abs 15128  df-limsup 15360  df-clim 15377  df-rlim 15378  df-sum 15578  df-struct 17026  df-sets 17043  df-slot 17061  df-ndx 17073  df-base 17091  df-ress 17120  df-plusg 17153  df-mulr 17154  df-starv 17155  df-sca 17156  df-vsca 17157  df-ip 17158  df-tset 17159  df-ple 17160  df-ds 17162  df-unif 17163  df-hom 17164  df-cco 17165  df-rest 17311  df-topn 17312  df-0g 17330  df-gsum 17331  df-topgen 17332  df-pt 17333  df-prds 17336  df-xrs 17391  df-qtop 17396  df-imas 17397  df-xps 17399  df-mre 17473  df-mrc 17474  df-acs 17476  df-mgm 18504  df-sgrp 18553  df-mnd 18564  df-submnd 18609  df-mulg 18880  df-cntz 19104  df-cmn 19571  df-psmet 20804  df-xmet 20805  df-met 20806  df-bl 20807  df-mopn 20808  df-fbas 20809  df-fg 20810  df-cnfld 20813  df-top 22259  df-topon 22276  df-topsp 22298  df-bases 22312  df-cld 22386  df-ntr 22387  df-cls 22388  df-nei 22465  df-lp 22503  df-perf 22504  df-cn 22594  df-cnp 22595  df-haus 22682  df-cmp 22754  df-tx 22929  df-hmeo 23122  df-fil 23213  df-fm 23305  df-flim 23306  df-flf 23307  df-xms 23689  df-ms 23690  df-tms 23691  df-cncf 24257  df-ovol 24844  df-vol 24845  df-mbf 24999  df-itg1 25000  df-itg2 25001  df-ibl 25002  df-itg 25003  df-0p 25050  df-limc 25246  df-dv 25247  df-area 26322
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator