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 38304
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 12448 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
41, 2, 3mp2an 710 . . . . . . . . 9 (𝐴[,]𝐵) ⊆ ℝ
54sseli 3740 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
65adantr 472 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7 areaquad.3 . . . . . . . . . . . . . . . 16 𝐶 ∈ ℝ
87recni 10244 . . . . . . . . . . . . . . 15 𝐶 ∈ ℂ
98a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10 resubcl 10537 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥𝐴) ∈ ℝ)
111, 10mpan2 709 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝑥𝐴) ∈ ℝ)
122, 1resubcli 10535 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ∈ ℝ
1312a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ∈ ℝ)
142recni 10244 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℂ
1514a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16 recn 10218 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17 areaquad.7 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 < 𝐵
181, 17gtneii 10341 . . . . . . . . . . . . . . . . . . . . 21 𝐵𝐴
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵𝐴)
2015, 16, 19subne0d 10593 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℝ → (𝐵𝐴) ≠ 0)
211, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ≠ 0
2221a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ≠ 0)
2311, 13, 22redivcld 11045 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
2423recnd 10260 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
25 areaquad.4 . . . . . . . . . . . . . . . . 17 𝐷 ∈ ℝ
2625recni 10244 . . . . . . . . . . . . . . . 16 𝐷 ∈ ℂ
2726a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
2824, 27mulcld 10252 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) ∈ ℂ)
2924, 9mulcld 10252 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐶) ∈ ℂ)
309, 28, 29addsub12d 10607 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
31 areaquad.10 . . . . . . . . . . . . . 14 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
3224, 27, 9subdid 10678 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
3332oveq2d 6829 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
3431, 33syl5eq 2806 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
35 1cnd 10248 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℂ)
3635, 24, 9subdird 10679 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
378mulid2i 10235 . . . . . . . . . . . . . . . 16 (1 · 𝐶) = 𝐶
3837oveq1i 6823 . . . . . . . . . . . . . . 15 ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))
3936, 38syl6eq 2810 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
4039oveq2d 6829 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
4130, 34, 403eqtr4d 2804 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑈 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)))
42 1red 10247 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℝ)
4342, 23resubcld 10650 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
4443recnd 10260 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℂ)
4544, 9mulcld 10252 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) ∈ ℂ)
4628, 45addcomd 10430 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)))
4744, 9mulcomd 10253 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
4824, 27mulcomd 10253 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) = (𝐷 · ((𝑥𝐴) / (𝐵𝐴))))
4947, 48oveq12d 6831 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
5041, 46, 493eqtrd 2798 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
5251, 43remulcld 10262 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5325a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
5453, 23remulcld 10262 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
5552, 54readdcld 10261 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5650, 55eqeltrd 2839 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57 areaquad.5 . . . . . . . . . . . . . . . 16 𝐸 ∈ ℝ
5857recni 10244 . . . . . . . . . . . . . . 15 𝐸 ∈ ℂ
5958a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60 areaquad.6 . . . . . . . . . . . . . . . . 17 𝐹 ∈ ℝ
6160recni 10244 . . . . . . . . . . . . . . . 16 𝐹 ∈ ℂ
6261a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
6324, 62mulcld 10252 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) ∈ ℂ)
6424, 59mulcld 10252 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐸) ∈ ℂ)
6559, 63, 64addsub12d 10607 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
66 areaquad.11 . . . . . . . . . . . . . 14 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
6724, 62, 59subdid 10678 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
6867oveq2d 6829 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
6966, 68syl5eq 2806 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7035, 24, 59subdird 10679 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7158mulid2i 10235 . . . . . . . . . . . . . . . 16 (1 · 𝐸) = 𝐸
7271oveq1i 6823 . . . . . . . . . . . . . . 15 ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))
7370, 72syl6eq 2810 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7473oveq2d 6829 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7565, 69, 743eqtr4d 2804 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑉 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)))
7644, 59mulcld 10252 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) ∈ ℂ)
7763, 76addcomd 10430 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)))
7844, 59mulcomd 10253 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
7924, 62mulcomd 10253 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) = (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
8078, 79oveq12d 6831 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8175, 77, 803eqtrd 2798 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8257a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
8382, 43remulcld 10262 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8460a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
8584, 23remulcld 10262 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐹 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
8683, 85readdcld 10261 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8781, 86eqeltrd 2839 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88 iccssre 12448 . . . . . . . . . 10 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
8956, 87, 88syl2anc 696 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
905, 89syl 17 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
9190sselda 3744 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
926, 91jca 555 . . . . . 6 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
9392ssopab2i 5153 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94 areaquad.12 . . . . 5 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95 df-xp 5272 . . . . 5 (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
9693, 94, 953sstr4i 3785 . . . 4 𝑆 ⊆ (ℝ × ℝ)
97 iftrue 4236 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (𝑉𝑈))
98 nfv 1992 . . . . . . . . . . . . 13 𝑦 𝑥 ∈ (𝐴[,]𝐵)
99 nfopab2 4872 . . . . . . . . . . . . . . 15 𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
10094, 99nfcxfr 2900 . . . . . . . . . . . . . 14 𝑦𝑆
101 nfcv 2902 . . . . . . . . . . . . . 14 𝑦{𝑥}
102100, 101nfima 5632 . . . . . . . . . . . . 13 𝑦(𝑆 “ {𝑥})
103 nfcv 2902 . . . . . . . . . . . . 13 𝑦(𝑈[,]𝑉)
104 vex 3343 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
105 vex 3343 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
106104, 105elimasn 5648 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
10794eleq2i 2831 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108 opabid 5132 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109106, 107, 1083bitri 286 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110109baib 982 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
11198, 102, 103, 110eqrd 3763 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112111fveq2d 6356 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
1135, 56syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
1145, 87syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115 iccmbl 23534 . . . . . . . . . . . . 13 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116113, 114, 115syl2anc 696 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117 mblvol 23498 . . . . . . . . . . . 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 10260 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
128127subidd 10572 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) = 0)
129 1red 10247 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
1302a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
1311a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
1321rexri 10289 . . . . . . . . . . . . . . . . . . . . 21 𝐴 ∈ ℝ*
1332rexri 10289 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℝ*
134 iccleub 12422 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝑥𝐵)
135132, 133, 134mp3an12 1563 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥𝐵)
1365, 130, 131, 135lesub1dd 10835 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ≤ (𝐵𝐴))
1375, 1, 10sylancl 697 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℝ)
13812a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ)
1391recni 10244 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 ∈ ℂ
140139subidi 10544 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝐴) = 0
141131, 130, 131ltsub1d 10828 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴𝐴) < (𝐵𝐴)))
14217, 141mpbii 223 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) < (𝐵𝐴))
143140, 142syl5eqbrr 4840 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵𝐴))
144 lediv1 11080 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝐴) ∈ ℝ ∧ (𝐵𝐴) ∈ ℝ ∧ ((𝐵𝐴) ∈ ℝ ∧ 0 < (𝐵𝐴))) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
145137, 138, 138, 143, 144syl112anc 1481 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
146136, 145mpbid 222 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴)))
14712recni 10244 . . . . . . . . . . . . . . . . . . 19 (𝐵𝐴) ∈ ℂ
148147, 21dividi 10950 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐴) / (𝐵𝐴)) = 1
149146, 148syl6breq 4845 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ 1)
150126, 129, 126, 149lesub1dd 10835 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
151128, 150eqbrtrrd 4828 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
152 areaquad.8 . . . . . . . . . . . . . . . 16 𝐶𝐸
153152a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐶𝐸)
154123, 124, 125, 151, 153lemul1ad 11155 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ≤ (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
15525a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
15660a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157138, 143elrpd 12062 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ+)
158 iccgelb 12423 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝐴𝑥)
159132, 133, 158mp3an12 1563 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴𝑥)
160131, 5, 131, 159lesub1dd 10835 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) ≤ (𝑥𝐴))
161140, 160syl5eqbrr 4840 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥𝐴))
162137, 157, 161divge0d 12105 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥𝐴) / (𝐵𝐴)))
163 areaquad.9 . . . . . . . . . . . . . . . 16 𝐷𝐹
164163a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷𝐹)
165155, 156, 126, 162, 164lemul1ad 11155 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ≤ (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
166119, 120, 121, 122, 154, 165le2addd 10838 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ≤ ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
1675, 50syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
1685, 81syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
169166, 167, 1683brtr4d 4836 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈𝑉)
170 ovolicc 23491 . . . . . . . . . . . 12 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
171113, 114, 169, 170syl3anc 1477 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
172112, 118, 1713eqtrd 2798 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉𝑈))
17397, 172eqtr4d 2797 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174 iffalse 4239 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = 0)
175 nfv 1992 . . . . . . . . . . . . 13 𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176 nfcv 2902 . . . . . . . . . . . . 13 𝑦
177109simplbi 478 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178 noel 4062 . . . . . . . . . . . . . . 15 ¬ 𝑦 ∈ ∅
179178pm2.21i 116 . . . . . . . . . . . . . 14 (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180177, 179pm5.21ni 366 . . . . . . . . . . . . 13 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181175, 102, 176, 180eqrd 3763 . . . . . . . . . . . 12 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182181fveq2d 6356 . . . . . . . . . . 11 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183 0mbl 23507 . . . . . . . . . . . . 13 ∅ ∈ dom vol
184 mblvol 23498 . . . . . . . . . . . . 13 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185183, 184ax-mp 5 . . . . . . . . . . . 12 (vol‘∅) = (vol*‘∅)
186 ovol0 23461 . . . . . . . . . . . 12 (vol*‘∅) = 0
187185, 186eqtri 2782 . . . . . . . . . . 11 (vol‘∅) = 0
188182, 187syl6eq 2810 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189174, 188eqtr4d 2797 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190173, 189pm2.61i 176 . . . . . . . 8 if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191190eqcomi 2769 . . . . . . 7 (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0)
19287, 56resubcld 10650 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑉𝑈) ∈ ℝ)
193 0re 10232 . . . . . . . 8 0 ∈ ℝ
194 ifcl 4274 . . . . . . . 8 (((𝑉𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
195192, 193, 194sylancl 697 . . . . . . 7 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
196191, 195syl5eqel 2843 . . . . . 6 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197 volf 23497 . . . . . . . 8 vol:dom vol⟶(0[,]+∞)
198 ffun 6209 . . . . . . . 8 (vol:dom vol⟶(0[,]+∞) → Fun vol)
199197, 198ax-mp 5 . . . . . . 7 Fun vol
200 iftrue 4236 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201111, 200eqtr4d 2797 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202 iffalse 4239 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203181, 202eqtr4d 2797 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204201, 203pm2.61i 176 . . . . . . . 8 (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
20556, 87, 115syl2anc 696 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206183a1i 11 . . . . . . . . 9 (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207205, 206ifcld 4275 . . . . . . . 8 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208204, 207syl5eqel 2843 . . . . . . 7 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209 fvimacnv 6495 . . . . . . 7 ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
210199, 208, 209sylancr 698 . . . . . 6 (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
211196, 210mpbid 222 . . . . 5 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (vol “ ℝ))
212211rgen 3060 . . . 4 𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)
2134a1i 11 . . . . . 6 (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214 rembl 23508 . . . . . . 7 ℝ ∈ dom vol
215214a1i 11 . . . . . 6 (0 ∈ ℝ → ℝ ∈ dom vol)
216114, 113resubcld 10650 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑉𝑈) ∈ ℝ)
217172, 216eqeltrd 2839 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218217adantl 473 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219 eldifn 3876 . . . . . . . 8 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220219, 188syl 17 . . . . . . 7 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221220adantl 473 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222172mpteq2ia 4892 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈))
223 eqid 2760 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
224223subcn 22870 . . . . . . . . . . . 12 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
225224a1i 11 . . . . . . . . . . 11 (⊤ → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
22666mpteq2i 4893 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
227223addcn 22869 . . . . . . . . . . . . . 14 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
228227a1i 11 . . . . . . . . . . . . 13 (⊤ → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
229 ax-resscn 10185 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
2304, 229sstri 3753 . . . . . . . . . . . . . . 15 (𝐴[,]𝐵) ⊆ ℂ
231 ssid 3765 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
232 cncfmptc 22915 . . . . . . . . . . . . . . 15 ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
23358, 230, 231, 232mp3an 1573 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234233a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235230sseli 3740 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236139a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237147a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℂ)
23821a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ≠ 0)
239235, 236, 237, 238divsubdird 11032 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
240239adantl 473 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
241240mpteq2dva 4896 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))))
242 resmpt 5607 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))))
243230, 242ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴)))
244 eqid 2760 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴)))
245244divccncf 22910 . . . . . . . . . . . . . . . . . . . 20 (((𝐵𝐴) ∈ ℂ ∧ (𝐵𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ))
246147, 21, 245mp2an 710 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ)
247 rescncf 22901 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248230, 246, 247mp2 9 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249243, 248eqeltrri 2836 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250249a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251139, 147, 21divcli 10959 . . . . . . . . . . . . . . . . . 18 (𝐴 / (𝐵𝐴)) ∈ ℂ
252 cncfmptc 22915 . . . . . . . . . . . . . . . . . 18 (((𝐴 / (𝐵𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253251, 230, 231, 252mp3an 1573 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254253a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255223, 225, 250, 254cncfmpt2f 22918 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256241, 255eqeltrd 2839 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257 cncfmptc 22915 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
25861, 230, 231, 257mp3an 1573 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259258a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260223, 225, 259, 234cncfmpt2f 22918 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261256, 260mulcncf 23415 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262223, 228, 234, 261cncfmpt2f 22918 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263226, 262syl5eqel 2843 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26431mpteq2i 4893 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
265 cncfmptc 22915 . . . . . . . . . . . . . . 15 ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2668, 230, 231, 265mp3an 1573 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267266a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268 cncfmptc 22915 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26926, 230, 231, 268mp3an 1573 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270269a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271223, 225, 270, 267cncfmpt2f 22918 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272256, 271mulcncf 23415 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273223, 228, 267, 272cncfmpt2f 22918 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274264, 273syl5eqel 2843 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275223, 225, 263, 274cncfmpt2f 22918 . . . . . . . . . 10 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276275trud 1642 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277 cniccibl 23806 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1)
2781, 2, 276, 277mp3an 1573 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1
279222, 278eqeltri 2835 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
280279a1i 11 . . . . . 6 (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
281213, 215, 218, 221, 280iblss2 23771 . . . . 5 (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
282193, 281ax-mp 5 . . . 4 (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
283 dmarea 24883 . . . 4 (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1))
28496, 212, 282, 283mpbir3an 1427 . . 3 𝑆 ∈ dom area
285 areaval 24890 . . 3 (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286284, 285ax-mp 5 . 2 (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287 itgeq2 23743 . . . 4 (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
288191a1i 11 . . . 4 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0))
289287, 288mprg 3064 . . 3 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
290 itgss2 23778 . . . 4 ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
2914, 290ax-mp 5 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
29261, 58addcli 10236 . . . . . 6 (𝐹 + 𝐸) ∈ ℂ
293 2cnne0 11434 . . . . . 6 (2 ∈ ℂ ∧ 2 ≠ 0)
294 div32 10897 . . . . . 6 (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2)))
295292, 293, 147, 294mp3an 1573 . . . . 5 (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
29626, 8addcli 10236 . . . . . 6 (𝐷 + 𝐶) ∈ ℂ
297 div32 10897 . . . . . 6 (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
298296, 293, 147, 297mp3an 1573 . . . . 5 (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
299295, 298oveq12i 6825 . . . 4 ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴))) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
300 2cn 11283 . . . . . 6 2 ∈ ℂ
301 2ne0 11305 . . . . . 6 2 ≠ 0
302292, 300, 301divcli 10959 . . . . 5 ((𝐹 + 𝐸) / 2) ∈ ℂ
303296, 300, 301divcli 10959 . . . . 5 ((𝐷 + 𝐶) / 2) ∈ ℂ
304302, 303, 147subdiri 10672 . . . 4 ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴)))
305114adantl 473 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306263trud 1642 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307 cniccibl 23806 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
3081, 2, 306, 307mp3an 1573 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1
309308a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
310113adantl 473 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311274trud 1642 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312 cniccibl 23806 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
3131, 2, 311, 312mp3an 1573 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1
314313a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
315305, 309, 310, 314itgsub 23791 . . . . . 6 (⊤ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316315trud 1642 . . . . 5 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
31758, 300, 301divcan4i 10964 . . . . . . . . . . 11 ((𝐸 · 2) / 2) = 𝐸
318317oveq1i 6823 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = (𝐸 · (𝐵𝐴))
31958, 300mulcli 10237 . . . . . . . . . . 11 (𝐸 · 2) ∈ ℂ
320 div32 10897 . . . . . . . . . . 11 (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2)))
321319, 293, 147, 320mp3an 1573 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
322318, 321eqtr3i 2784 . . . . . . . . 9 (𝐸 · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
323322oveq1i 6823 . . . . . . . 8 ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2))) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
324 itgeq2 23743 . . . . . . . . . 10 (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥)
32566a1i 11 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
326324, 325mprg 3064 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥
32757a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328 cniccibl 23806 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
3291, 2, 233, 328mp3an 1573 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1
330329a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
331126adantl 473 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
33260a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333332, 327resubcld 10650 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝐸) ∈ ℝ)
334331, 333remulcld 10262 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) ∈ ℝ)
335261trud 1642 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336 cniccibl 23806 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
3371, 2, 335, 336mp3an 1573 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1
338337a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
339327, 330, 334, 338itgadd 23790 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥))
340339trud 1642 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
341 iccmbl 23534 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
3421, 2, 341mp2an 710 . . . . . . . . . . . 12 (𝐴[,]𝐵) ∈ dom vol
343 mblvol 23498 . . . . . . . . . . . . . . 15 ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344342, 343ax-mp 5 . . . . . . . . . . . . . 14 (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
3451, 2, 17ltleii 10352 . . . . . . . . . . . . . . 15 𝐴𝐵
346 ovolicc 23491 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴))
3471, 2, 345, 346mp3an 1573 . . . . . . . . . . . . . 14 (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴)
348344, 347eqtri 2782 . . . . . . . . . . . . 13 (vol‘(𝐴[,]𝐵)) = (𝐵𝐴)
349348, 12eqeltri 2835 . . . . . . . . . . . 12 (vol‘(𝐴[,]𝐵)) ∈ ℝ
350 itgconst 23784 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351342, 349, 58, 350mp3an 1573 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352348oveq2i 6824 . . . . . . . . . . 11 (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵𝐴))
353351, 352eqtri 2782 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵𝐴))
35461a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐹 ∈ ℂ)
35558a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐸 ∈ ℂ)
356354, 355subcld 10584 . . . . . . . . . . . . 13 (⊤ → (𝐹𝐸) ∈ ℂ)
357256trud 1642 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358 cniccibl 23806 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
3591, 2, 357, 358mp3an 1573 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1
360359a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
361356, 331, 360itgmulc2 23799 . . . . . . . . . . . 12 (⊤ → ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
362361trud 1642 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
363 itgeq2 23743 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)) → ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
364137recnd 10260 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℂ)
365364, 237, 238divrec2d 10997 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)))
366363, 365mprg 3064 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
3675adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368 cncfmptid 22916 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369230, 231, 368mp2an 710 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370 cniccibl 23806 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3711, 2, 369, 370mp3an 1573 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1
372371a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3731a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374 cncfmptc 22915 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375139, 230, 231, 374mp3an 1573 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376 cniccibl 23806 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
3771, 2, 375, 376mp3an 1573 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1
378377a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
379367, 372, 373, 378itgsub 23791 . . . . . . . . . . . . . . . . . . 19 (⊤ → ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥))
380379trud 1642 . . . . . . . . . . . . . . . . . 18 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥)
3811a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴 ∈ ℝ)
3822a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐵 ∈ ℝ)
383345a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴𝐵)
384 1nn0 11500 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℕ0
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 1 ∈ ℕ0)
386381, 382, 383, 385itgpowd 38302 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387386trud 1642 . . . . . . . . . . . . . . . . . . . . 21 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388 1p1e2 11326 . . . . . . . . . . . . . . . . . . . . . 22 (1 + 1) = 2
389388oveq2i 6824 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390387, 389eqtri 2782 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391 itgeq2 23743 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392235exp1d 13197 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393391, 392mprg 3064 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394388oveq2i 6824 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵↑(1 + 1)) = (𝐵↑2)
395388oveq2i 6824 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴↑(1 + 1)) = (𝐴↑2)
396394, 395oveq12i 6825 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397396oveq1i 6823 . . . . . . . . . . . . . . . . . . . 20 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398390, 393, 3973eqtr3i 2790 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399 itgconst 23784 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400342, 349, 139, 399mp3an 1573 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401348oveq2i 6824 . . . . . . . . . . . . . . . . . . . 20 (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵𝐴))
402400, 401eqtri 2782 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵𝐴))
403398, 402oveq12i 6825 . . . . . . . . . . . . . . . . . 18 (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
404380, 403eqtri 2782 . . . . . . . . . . . . . . . . 17 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
405404oveq2i 6824 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴))))
40614a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵 ∈ ℂ)
407139a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐴 ∈ ℂ)
408406, 407subcld 10584 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ∈ ℂ)
40918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵𝐴)
410406, 407, 409subne0d 10593 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ≠ 0)
411408, 410reccld 10986 . . . . . . . . . . . . . . . . . 18 (⊤ → (1 / (𝐵𝐴)) ∈ ℂ)
412411trud 1642 . . . . . . . . . . . . . . . . 17 (1 / (𝐵𝐴)) ∈ ℂ
41314sqcli 13138 . . . . . . . . . . . . . . . . . . 19 (𝐵↑2) ∈ ℂ
414139sqcli 13138 . . . . . . . . . . . . . . . . . . 19 (𝐴↑2) ∈ ℂ
415413, 414subcli 10549 . . . . . . . . . . . . . . . . . 18 ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416415, 300, 301divcli 10959 . . . . . . . . . . . . . . . . 17 (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417139, 147mulcli 10237 . . . . . . . . . . . . . . . . 17 (𝐴 · (𝐵𝐴)) ∈ ℂ
418412, 416, 417subdii 10671 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
419405, 418eqtri 2782 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
420137adantl 473 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥𝐴) ∈ ℝ)
421367, 372, 373, 378iblsub 23787 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥𝐴)) ∈ 𝐿1)
422411, 420, 421itgmulc2 23799 . . . . . . . . . . . . . . . 16 (⊤ → ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
423422trud 1642 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
424412, 417mulcomi 10238 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
425417, 147, 21divreci 10962 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
426139, 147, 21divcan4i 10964 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = 𝐴
427424, 425, 4263eqtr2i 2788 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = 𝐴
428427oveq2i 6824 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429419, 423, 4283eqtr3i 2790 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430366, 429eqtri 2782 . . . . . . . . . . . . 13 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
43114, 139subsqi 13169 . . . . . . . . . . . . . . . . 17 ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵𝐴))
432431oveq1i 6823 . . . . . . . . . . . . . . . 16 (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵𝐴)) / 2)
433432oveq2i 6824 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
434431, 415eqeltrri 2836 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) · (𝐵𝐴)) ∈ ℂ
435412, 434, 300, 301divassi 10973 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
436412, 434mulcomi 10238 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
437434, 147, 21divreci 10962 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
43814, 139addcli 10236 . . . . . . . . . . . . . . . . . 18 (𝐵 + 𝐴) ∈ ℂ
439438, 147, 21divcan4i 10964 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (𝐵 + 𝐴)
440436, 437, 4393eqtr2i 2788 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (𝐵 + 𝐴)
441440oveq1i 6823 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442433, 435, 4413eqtr2i 2788 . . . . . . . . . . . . . 14 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443442oveq1i 6823 . . . . . . . . . . . . 13 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444139, 300mulcli 10237 . . . . . . . . . . . . . . 15 (𝐴 · 2) ∈ ℂ
445 divsubdir 10913 . . . . . . . . . . . . . . 15 (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446438, 444, 293, 445mp3an 1573 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
44714, 139, 444addsubassi 10564 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448 subsub2 10501 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
44914, 444, 139, 448mp3an 1573 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450139times2i 11340 . . . . . . . . . . . . . . . . . . 19 (𝐴 · 2) = (𝐴 + 𝐴)
451450oveq1i 6823 . . . . . . . . . . . . . . . . . 18 ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452139, 139pncan3oi 10489 . . . . . . . . . . . . . . . . . 18 ((𝐴 + 𝐴) − 𝐴) = 𝐴
453451, 452eqtri 2782 . . . . . . . . . . . . . . . . 17 ((𝐴 · 2) − 𝐴) = 𝐴
454453oveq2i 6824 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵𝐴)
455447, 449, 4543eqtr2i 2788 . . . . . . . . . . . . . . 15 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵𝐴)
456455oveq1i 6823 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵𝐴) / 2)
457139, 300, 301divcan4i 10964 . . . . . . . . . . . . . . 15 ((𝐴 · 2) / 2) = 𝐴
458457oveq2i 6824 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459446, 456, 4583eqtr3ri 2791 . . . . . . . . . . . . 13 (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵𝐴) / 2)
460430, 443, 4593eqtri 2786 . . . . . . . . . . . 12 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ((𝐵𝐴) / 2)
461460oveq2i 6824 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐹𝐸) · ((𝐵𝐴) / 2))
462 itgeq2 23743 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) → ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
46361, 58subcli 10549 . . . . . . . . . . . . . 14 (𝐹𝐸) ∈ ℂ
464463a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐹𝐸) ∈ ℂ)
465464, 127mulcomd 10253 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
466462, 465mprg 3064 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥
467362, 461, 4663eqtr3ri 2791 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥 = ((𝐹𝐸) · ((𝐵𝐴) / 2))
468353, 467oveq12i 6825 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥) = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
469326, 340, 4683eqtri 2786 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
470147, 300, 301divcli 10959 . . . . . . . . 9 ((𝐵𝐴) / 2) ∈ ℂ
471319, 463, 470adddiri 10243 . . . . . . . 8 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
472323, 469, 4713eqtr4i 2792 . . . . . . 7 ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2))
473 addsub12 10486 . . . . . . . . . 10 ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸)))
47461, 319, 58, 473mp3an 1573 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸))
47558times2i 11340 . . . . . . . . . . . 12 (𝐸 · 2) = (𝐸 + 𝐸)
476475oveq1i 6823 . . . . . . . . . . 11 ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
47758, 58pncan3oi 10489 . . . . . . . . . . 11 ((𝐸 + 𝐸) − 𝐸) = 𝐸
478476, 477eqtri 2782 . . . . . . . . . 10 ((𝐸 · 2) − 𝐸) = 𝐸
479478oveq2i 6824 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480474, 479eqtr3i 2784 . . . . . . . 8 ((𝐸 · 2) + (𝐹𝐸)) = (𝐹 + 𝐸)
481480oveq1i 6823 . . . . . . 7 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
482472, 481eqtri 2782 . . . . . 6 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
4838, 300, 301divcan4i 10964 . . . . . . . . . . 11 ((𝐶 · 2) / 2) = 𝐶
484483oveq1i 6823 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = (𝐶 · (𝐵𝐴))
4858, 300mulcli 10237 . . . . . . . . . . 11 (𝐶 · 2) ∈ ℂ
486 div32 10897 . . . . . . . . . . 11 (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2)))
487485, 293, 147, 486mp3an 1573 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
488484, 487eqtr3i 2784 . . . . . . . . 9 (𝐶 · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
489488oveq1i 6823 . . . . . . . 8 ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2))) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
49031a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
491490itgeq2dv 23747 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥)
492491trud 1642 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥
4937a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494 cniccibl 23806 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
4951, 2, 266, 494mp3an 1573 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1
496495a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
49725a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498497, 493resubcld 10650 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷𝐶) ∈ ℝ)
499331, 498remulcld 10262 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ)
500272trud 1642 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501 cniccibl 23806 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
5021, 2, 500, 501mp3an 1573 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1
503502a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
504493, 496, 499, 503itgadd 23790 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥))
505504trud 1642 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
506 itgconst 23784 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507342, 349, 8, 506mp3an 1573 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508348oveq2i 6824 . . . . . . . . . . 11 (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵𝐴))
509507, 508eqtri 2782 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵𝐴))
51026a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐷 ∈ ℂ)
5118a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐶 ∈ ℂ)
512510, 511subcld 10584 . . . . . . . . . . . . 13 (⊤ → (𝐷𝐶) ∈ ℂ)
513512, 331, 360itgmulc2 23799 . . . . . . . . . . . 12 (⊤ → ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
514513trud 1642 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
515460oveq2i 6824 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐷𝐶) · ((𝐵𝐴) / 2))
516 itgeq2 23743 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) → ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
51726, 8subcli 10549 . . . . . . . . . . . . . 14 (𝐷𝐶) ∈ ℂ
518517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷𝐶) ∈ ℂ)
519518, 127mulcomd 10253 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
520516, 519mprg 3064 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥
521514, 515, 5203eqtr3ri 2791 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥 = ((𝐷𝐶) · ((𝐵𝐴) / 2))
522509, 521oveq12i 6825 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥) = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
523492, 505, 5223eqtri 2786 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
524485, 517, 470adddiri 10243 . . . . . . . 8 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
525489, 523, 5243eqtr4i 2792 . . . . . . 7 ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2))
526 addsub12 10486 . . . . . . . . . 10 ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶)))
52726, 485, 8, 526mp3an 1573 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶))
5288times2i 11340 . . . . . . . . . . . 12 (𝐶 · 2) = (𝐶 + 𝐶)
529528oveq1i 6823 . . . . . . . . . . 11 ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
5308, 8pncan3oi 10489 . . . . . . . . . . 11 ((𝐶 + 𝐶) − 𝐶) = 𝐶
531529, 530eqtri 2782 . . . . . . . . . 10 ((𝐶 · 2) − 𝐶) = 𝐶
532531oveq2i 6824 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533527, 532eqtr3i 2784 . . . . . . . 8 ((𝐶 · 2) + (𝐷𝐶)) = (𝐷 + 𝐶)
534533oveq1i 6823 . . . . . . 7 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
535525, 534eqtri 2782 . . . . . 6 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
536482, 535oveq12i 6825 . . . . 5 (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
537316, 536eqtri 2782 . . . 4 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
538299, 304, 5373eqtr4ri 2793 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
539289, 291, 5383eqtr2i 2788 . 2 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
540286, 539eqtri 2782 1 (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wa 383   = wceq 1632  wtru 1633  wcel 2139  wne 2932  wral 3050  cdif 3712  wss 3715  c0 4058  ifcif 4230  {csn 4321  cop 4327   class class class wbr 4804  {copab 4864  cmpt 4881   × cxp 5264  ccnv 5265  dom cdm 5266  cres 5268  cima 5269  Fun wfun 6043  wf 6045  cfv 6049  (class class class)co 6813  cc 10126  cr 10127  0cc0 10128  1c1 10129   + caddc 10131   · cmul 10133  +∞cpnf 10263  *cxr 10265   < clt 10266  cle 10267  cmin 10458   / cdiv 10876  2c2 11262  0cn0 11484  [,]cicc 12371  cexp 13054  TopOpenctopn 16284  fldccnfld 19948   Cn ccn 21230   ×t ctx 21565  cnccncf 22880  vol*covol 23431  volcvol 23432  𝐿1cibl 23585  citg 23586  areacarea 24881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cc 9449  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207  ax-mulf 10208
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-ofr 7063  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-omul 7734  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-fi 8482  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-acn 8958  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-ioc 12373  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-hash 13312  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-limsup 14401  df-clim 14418  df-rlim 14419  df-sum 14616  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-rest 16285  df-topn 16286  df-0g 16304  df-gsum 16305  df-topgen 16306  df-pt 16307  df-prds 16310  df-xrs 16364  df-qtop 16369  df-imas 16370  df-xps 16372  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17950  df-cmn 18395  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-fbas 19945  df-fg 19946  df-cnfld 19949  df-top 20901  df-topon 20918  df-topsp 20939  df-bases 20952  df-cld 21025  df-ntr 21026  df-cls 21027  df-nei 21104  df-lp 21142  df-perf 21143  df-cn 21233  df-cnp 21234  df-haus 21321  df-cmp 21392  df-tx 21567  df-hmeo 21760  df-fil 21851  df-fm 21943  df-flim 21944  df-flf 21945  df-xms 22326  df-ms 22327  df-tms 22328  df-cncf 22882  df-ovol 23433  df-vol 23434  df-mbf 23587  df-itg1 23588  df-itg2 23589  df-ibl 23590  df-itg 23591  df-0p 23636  df-limc 23829  df-dv 23830  df-area 24882
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator