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 38320
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 12493 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
41, 2, 3mp2an 675 . . . . . . . . 9 (𝐴[,]𝐵) ⊆ ℝ
54sseli 3805 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
65adantr 468 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7 areaquad.3 . . . . . . . . . . . . . . . 16 𝐶 ∈ ℝ
87recni 10349 . . . . . . . . . . . . . . 15 𝐶 ∈ ℂ
98a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10 resubcl 10640 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥𝐴) ∈ ℝ)
111, 10mpan2 674 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝑥𝐴) ∈ ℝ)
122, 1resubcli 10638 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ∈ ℝ
1312a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ∈ ℝ)
142recni 10349 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℂ
1514a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16 recn 10321 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17 areaquad.7 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 < 𝐵
181, 17gtneii 10444 . . . . . . . . . . . . . . . . . . . . 21 𝐵𝐴
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵𝐴)
2015, 16, 19subne0d 10696 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℝ → (𝐵𝐴) ≠ 0)
211, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ≠ 0
2221a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ≠ 0)
2311, 13, 22redivcld 11148 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
2423recnd 10363 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
25 areaquad.4 . . . . . . . . . . . . . . . . 17 𝐷 ∈ ℝ
2625recni 10349 . . . . . . . . . . . . . . . 16 𝐷 ∈ ℂ
2726a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
2824, 27mulcld 10355 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) ∈ ℂ)
2924, 9mulcld 10355 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐶) ∈ ℂ)
309, 28, 29addsub12d 10710 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
31 areaquad.10 . . . . . . . . . . . . . 14 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
3224, 27, 9subdid 10781 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
3332oveq2d 6900 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
3431, 33syl5eq 2863 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
35 1cnd 10330 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℂ)
3635, 24, 9subdird 10782 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
378mulid2i 10340 . . . . . . . . . . . . . . . 16 (1 · 𝐶) = 𝐶
3837oveq1i 6894 . . . . . . . . . . . . . . 15 ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))
3936, 38syl6eq 2867 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
4039oveq2d 6900 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
4130, 34, 403eqtr4d 2861 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑈 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)))
42 1red 10336 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℝ)
4342, 23resubcld 10753 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
4443recnd 10363 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℂ)
4544, 9mulcld 10355 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) ∈ ℂ)
4628, 45addcomd 10533 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)))
4744, 9mulcomd 10356 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
4824, 27mulcomd 10356 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) = (𝐷 · ((𝑥𝐴) / (𝐵𝐴))))
4947, 48oveq12d 6902 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
5041, 46, 493eqtrd 2855 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
5251, 43remulcld 10365 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5325a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
5453, 23remulcld 10365 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
5552, 54readdcld 10364 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5650, 55eqeltrd 2896 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57 areaquad.5 . . . . . . . . . . . . . . . 16 𝐸 ∈ ℝ
5857recni 10349 . . . . . . . . . . . . . . 15 𝐸 ∈ ℂ
5958a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60 areaquad.6 . . . . . . . . . . . . . . . . 17 𝐹 ∈ ℝ
6160recni 10349 . . . . . . . . . . . . . . . 16 𝐹 ∈ ℂ
6261a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
6324, 62mulcld 10355 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) ∈ ℂ)
6424, 59mulcld 10355 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐸) ∈ ℂ)
6559, 63, 64addsub12d 10710 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
66 areaquad.11 . . . . . . . . . . . . . 14 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
6724, 62, 59subdid 10781 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
6867oveq2d 6900 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
6966, 68syl5eq 2863 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7035, 24, 59subdird 10782 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7158mulid2i 10340 . . . . . . . . . . . . . . . 16 (1 · 𝐸) = 𝐸
7271oveq1i 6894 . . . . . . . . . . . . . . 15 ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))
7370, 72syl6eq 2867 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7473oveq2d 6900 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7565, 69, 743eqtr4d 2861 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑉 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)))
7644, 59mulcld 10355 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) ∈ ℂ)
7763, 76addcomd 10533 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)))
7844, 59mulcomd 10356 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
7924, 62mulcomd 10356 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) = (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
8078, 79oveq12d 6902 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8175, 77, 803eqtrd 2855 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8257a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
8382, 43remulcld 10365 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8460a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
8584, 23remulcld 10365 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐹 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
8683, 85readdcld 10364 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8781, 86eqeltrd 2896 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88 iccssre 12493 . . . . . . . . . 10 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
8956, 87, 88syl2anc 575 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
905, 89syl 17 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
9190sselda 3809 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
926, 91jca 503 . . . . . 6 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
9392ssopab2i 5211 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94 areaquad.12 . . . . 5 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95 df-xp 5330 . . . . 5 (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
9693, 94, 953sstr4i 3852 . . . 4 𝑆 ⊆ (ℝ × ℝ)
97 iftrue 4296 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (𝑉𝑈))
98 nfv 2005 . . . . . . . . . . . . 13 𝑦 𝑥 ∈ (𝐴[,]𝐵)
99 nfopab2 4925 . . . . . . . . . . . . . . 15 𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
10094, 99nfcxfr 2957 . . . . . . . . . . . . . 14 𝑦𝑆
101 nfcv 2959 . . . . . . . . . . . . . 14 𝑦{𝑥}
102100, 101nfima 5698 . . . . . . . . . . . . 13 𝑦(𝑆 “ {𝑥})
103 nfcv 2959 . . . . . . . . . . . . 13 𝑦(𝑈[,]𝑉)
104 vex 3405 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
105 vex 3405 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
106104, 105elimasn 5714 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
10794eleq2i 2888 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108 opabid 5190 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109106, 107, 1083bitri 288 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110109baib 527 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
11198, 102, 103, 110eqrd 3828 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112111fveq2d 6422 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
1135, 56syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
1145, 87syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115 iccmbl 23570 . . . . . . . . . . . . 13 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116113, 114, 115syl2anc 575 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117 mblvol 23534 . . . . . . . . . . . 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 10363 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
128127subidd 10675 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) = 0)
129 1red 10336 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
1302a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
1311a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
1321rexri 10392 . . . . . . . . . . . . . . . . . . . . 21 𝐴 ∈ ℝ*
1332rexri 10392 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℝ*
134 iccleub 12467 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝑥𝐵)
135132, 133, 134mp3an12 1568 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥𝐵)
1365, 130, 131, 135lesub1dd 10938 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ≤ (𝐵𝐴))
1375, 1, 10sylancl 576 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℝ)
13812a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ)
1391recni 10349 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 ∈ ℂ
140139subidi 10647 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝐴) = 0
141131, 130, 131ltsub1d 10931 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴𝐴) < (𝐵𝐴)))
14217, 141mpbii 224 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) < (𝐵𝐴))
143140, 142syl5eqbrr 4891 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵𝐴))
144 lediv1 11183 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝐴) ∈ ℝ ∧ (𝐵𝐴) ∈ ℝ ∧ ((𝐵𝐴) ∈ ℝ ∧ 0 < (𝐵𝐴))) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
145137, 138, 138, 143, 144syl112anc 1486 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
146136, 145mpbid 223 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴)))
14712recni 10349 . . . . . . . . . . . . . . . . . . 19 (𝐵𝐴) ∈ ℂ
148147, 21dividi 11053 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐴) / (𝐵𝐴)) = 1
149146, 148syl6breq 4896 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ 1)
150126, 129, 126, 149lesub1dd 10938 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
151128, 150eqbrtrrd 4879 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
152 areaquad.8 . . . . . . . . . . . . . . . 16 𝐶𝐸
153152a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐶𝐸)
154123, 124, 125, 151, 153lemul1ad 11258 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ≤ (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
15525a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
15660a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157138, 143elrpd 12103 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ+)
158 iccgelb 12468 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝐴𝑥)
159132, 133, 158mp3an12 1568 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴𝑥)
160131, 5, 131, 159lesub1dd 10938 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) ≤ (𝑥𝐴))
161140, 160syl5eqbrr 4891 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥𝐴))
162137, 157, 161divge0d 12146 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥𝐴) / (𝐵𝐴)))
163 areaquad.9 . . . . . . . . . . . . . . . 16 𝐷𝐹
164163a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷𝐹)
165155, 156, 126, 162, 164lemul1ad 11258 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ≤ (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
166119, 120, 121, 122, 154, 165le2addd 10941 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ≤ ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
1675, 50syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
1685, 81syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
169166, 167, 1683brtr4d 4887 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈𝑉)
170 ovolicc 23527 . . . . . . . . . . . 12 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
171113, 114, 169, 170syl3anc 1483 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
172112, 118, 1713eqtrd 2855 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉𝑈))
17397, 172eqtr4d 2854 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174 iffalse 4299 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = 0)
175 nfv 2005 . . . . . . . . . . . . 13 𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176 nfcv 2959 . . . . . . . . . . . . 13 𝑦
177109simplbi 487 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178 noel 4131 . . . . . . . . . . . . . . 15 ¬ 𝑦 ∈ ∅
179178pm2.21i 117 . . . . . . . . . . . . . 14 (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180177, 179pm5.21ni 368 . . . . . . . . . . . . 13 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181175, 102, 176, 180eqrd 3828 . . . . . . . . . . . 12 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182181fveq2d 6422 . . . . . . . . . . 11 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183 0mbl 23543 . . . . . . . . . . . . 13 ∅ ∈ dom vol
184 mblvol 23534 . . . . . . . . . . . . 13 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185183, 184ax-mp 5 . . . . . . . . . . . 12 (vol‘∅) = (vol*‘∅)
186 ovol0 23497 . . . . . . . . . . . 12 (vol*‘∅) = 0
187185, 186eqtri 2839 . . . . . . . . . . 11 (vol‘∅) = 0
188182, 187syl6eq 2867 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189174, 188eqtr4d 2854 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190173, 189pm2.61i 176 . . . . . . . 8 if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191190eqcomi 2826 . . . . . . 7 (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0)
19287, 56resubcld 10753 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑉𝑈) ∈ ℝ)
193 0re 10337 . . . . . . . 8 0 ∈ ℝ
194 ifcl 4334 . . . . . . . 8 (((𝑉𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
195192, 193, 194sylancl 576 . . . . . . 7 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
196191, 195syl5eqel 2900 . . . . . 6 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197 volf 23533 . . . . . . . 8 vol:dom vol⟶(0[,]+∞)
198 ffun 6269 . . . . . . . 8 (vol:dom vol⟶(0[,]+∞) → Fun vol)
199197, 198ax-mp 5 . . . . . . 7 Fun vol
200 iftrue 4296 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201111, 200eqtr4d 2854 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202 iffalse 4299 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203181, 202eqtr4d 2854 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204201, 203pm2.61i 176 . . . . . . . 8 (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
20556, 87, 115syl2anc 575 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206183a1i 11 . . . . . . . . 9 (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207205, 206ifcld 4335 . . . . . . . 8 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208204, 207syl5eqel 2900 . . . . . . 7 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209 fvimacnv 6564 . . . . . . 7 ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
210199, 208, 209sylancr 577 . . . . . 6 (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
211196, 210mpbid 223 . . . . 5 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (vol “ ℝ))
212211rgen 3121 . . . 4 𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)
2134a1i 11 . . . . . 6 (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214 rembl 23544 . . . . . . 7 ℝ ∈ dom vol
215214a1i 11 . . . . . 6 (0 ∈ ℝ → ℝ ∈ dom vol)
216114, 113resubcld 10753 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑉𝑈) ∈ ℝ)
217172, 216eqeltrd 2896 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218217adantl 469 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219 eldifn 3943 . . . . . . . 8 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220219, 188syl 17 . . . . . . 7 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221220adantl 469 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222172mpteq2ia 4945 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈))
223 eqid 2817 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
224223subcn 22903 . . . . . . . . . . . 12 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
225224a1i 11 . . . . . . . . . . 11 (⊤ → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
22666mpteq2i 4946 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
227223addcn 22902 . . . . . . . . . . . . . 14 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
228227a1i 11 . . . . . . . . . . . . 13 (⊤ → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
229 ax-resscn 10288 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
2304, 229sstri 3818 . . . . . . . . . . . . . . 15 (𝐴[,]𝐵) ⊆ ℂ
231 ssid 3831 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
232 cncfmptc 22948 . . . . . . . . . . . . . . 15 ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
23358, 230, 231, 232mp3an 1578 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234233a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235230sseli 3805 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236139a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237147a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℂ)
23821a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ≠ 0)
239235, 236, 237, 238divsubdird 11135 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
240239adantl 469 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
241240mpteq2dva 4949 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))))
242 resmpt 5668 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))))
243230, 242ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴)))
244 eqid 2817 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴)))
245244divccncf 22943 . . . . . . . . . . . . . . . . . . . 20 (((𝐵𝐴) ∈ ℂ ∧ (𝐵𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ))
246147, 21, 245mp2an 675 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ)
247 rescncf 22934 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248230, 246, 247mp2 9 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249243, 248eqeltrri 2893 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250249a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251139, 147, 21divcli 11062 . . . . . . . . . . . . . . . . . 18 (𝐴 / (𝐵𝐴)) ∈ ℂ
252 cncfmptc 22948 . . . . . . . . . . . . . . . . . 18 (((𝐴 / (𝐵𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253251, 230, 231, 252mp3an 1578 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254253a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255223, 225, 250, 254cncfmpt2f 22951 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256241, 255eqeltrd 2896 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257 cncfmptc 22948 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
25861, 230, 231, 257mp3an 1578 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259258a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260223, 225, 259, 234cncfmpt2f 22951 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261256, 260mulcncf 23450 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262223, 228, 234, 261cncfmpt2f 22951 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263226, 262syl5eqel 2900 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26431mpteq2i 4946 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
265 cncfmptc 22948 . . . . . . . . . . . . . . 15 ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2668, 230, 231, 265mp3an 1578 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267266a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268 cncfmptc 22948 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26926, 230, 231, 268mp3an 1578 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270269a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271223, 225, 270, 267cncfmpt2f 22951 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272256, 271mulcncf 23450 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273223, 228, 267, 272cncfmpt2f 22951 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274264, 273syl5eqel 2900 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275223, 225, 263, 274cncfmpt2f 22951 . . . . . . . . . 10 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276275mptru 1645 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277 cniccibl 23844 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1)
2781, 2, 276, 277mp3an 1578 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1
279222, 278eqeltri 2892 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
280279a1i 11 . . . . . 6 (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
281213, 215, 218, 221, 280iblss2 23809 . . . . 5 (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
282193, 281ax-mp 5 . . . 4 (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
283 dmarea 24921 . . . 4 (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1))
28496, 212, 282, 283mpbir3an 1434 . . 3 𝑆 ∈ dom area
285 areaval 24928 . . 3 (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286284, 285ax-mp 5 . 2 (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287 itgeq2 23781 . . . 4 (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
288191a1i 11 . . . 4 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0))
289287, 288mprg 3125 . . 3 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
290 itgss2 23816 . . . 4 ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
2914, 290ax-mp 5 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
29261, 58addcli 10341 . . . . . 6 (𝐹 + 𝐸) ∈ ℂ
293 2cnne0 11529 . . . . . 6 (2 ∈ ℂ ∧ 2 ≠ 0)
294 div32 11000 . . . . . 6 (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2)))
295292, 293, 147, 294mp3an 1578 . . . . 5 (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
29626, 8addcli 10341 . . . . . 6 (𝐷 + 𝐶) ∈ ℂ
297 div32 11000 . . . . . 6 (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
298296, 293, 147, 297mp3an 1578 . . . . 5 (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
299295, 298oveq12i 6896 . . . 4 ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴))) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
300 2cn 11388 . . . . . 6 2 ∈ ℂ
301 2ne0 11424 . . . . . 6 2 ≠ 0
302292, 300, 301divcli 11062 . . . . 5 ((𝐹 + 𝐸) / 2) ∈ ℂ
303296, 300, 301divcli 11062 . . . . 5 ((𝐷 + 𝐶) / 2) ∈ ℂ
304302, 303, 147subdiri 10775 . . . 4 ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴)))
305114adantl 469 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306263mptru 1645 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307 cniccibl 23844 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
3081, 2, 306, 307mp3an 1578 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1
309308a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
310113adantl 469 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311274mptru 1645 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312 cniccibl 23844 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
3131, 2, 311, 312mp3an 1578 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1
314313a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
315305, 309, 310, 314itgsub 23829 . . . . . 6 (⊤ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316315mptru 1645 . . . . 5 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
31758, 300, 301divcan4i 11067 . . . . . . . . . . 11 ((𝐸 · 2) / 2) = 𝐸
318317oveq1i 6894 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = (𝐸 · (𝐵𝐴))
31958, 300mulcli 10342 . . . . . . . . . . 11 (𝐸 · 2) ∈ ℂ
320 div32 11000 . . . . . . . . . . 11 (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2)))
321319, 293, 147, 320mp3an 1578 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
322318, 321eqtr3i 2841 . . . . . . . . 9 (𝐸 · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
323322oveq1i 6894 . . . . . . . 8 ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2))) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
324 itgeq2 23781 . . . . . . . . . 10 (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥)
32566a1i 11 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
326324, 325mprg 3125 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥
32757a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328 cniccibl 23844 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
3291, 2, 233, 328mp3an 1578 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1
330329a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
331126adantl 469 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
33260a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333332, 327resubcld 10753 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝐸) ∈ ℝ)
334331, 333remulcld 10365 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) ∈ ℝ)
335261mptru 1645 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336 cniccibl 23844 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
3371, 2, 335, 336mp3an 1578 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1
338337a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
339327, 330, 334, 338itgadd 23828 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥))
340339mptru 1645 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
341 iccmbl 23570 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
3421, 2, 341mp2an 675 . . . . . . . . . . . 12 (𝐴[,]𝐵) ∈ dom vol
343 mblvol 23534 . . . . . . . . . . . . . . 15 ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344342, 343ax-mp 5 . . . . . . . . . . . . . 14 (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
3451, 2, 17ltleii 10455 . . . . . . . . . . . . . . 15 𝐴𝐵
346 ovolicc 23527 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴))
3471, 2, 345, 346mp3an 1578 . . . . . . . . . . . . . 14 (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴)
348344, 347eqtri 2839 . . . . . . . . . . . . 13 (vol‘(𝐴[,]𝐵)) = (𝐵𝐴)
349348, 12eqeltri 2892 . . . . . . . . . . . 12 (vol‘(𝐴[,]𝐵)) ∈ ℝ
350 itgconst 23822 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351342, 349, 58, 350mp3an 1578 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352348oveq2i 6895 . . . . . . . . . . 11 (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵𝐴))
353351, 352eqtri 2839 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵𝐴))
35461a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐹 ∈ ℂ)
35558a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐸 ∈ ℂ)
356354, 355subcld 10687 . . . . . . . . . . . . 13 (⊤ → (𝐹𝐸) ∈ ℂ)
357256mptru 1645 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358 cniccibl 23844 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
3591, 2, 357, 358mp3an 1578 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1
360359a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
361356, 331, 360itgmulc2 23837 . . . . . . . . . . . 12 (⊤ → ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
362361mptru 1645 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
363 itgeq2 23781 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)) → ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
364137recnd 10363 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℂ)
365364, 237, 238divrec2d 11100 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)))
366363, 365mprg 3125 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
3675adantl 469 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368 cncfmptid 22949 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369230, 231, 368mp2an 675 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370 cniccibl 23844 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3711, 2, 369, 370mp3an 1578 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1
372371a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3731a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374 cncfmptc 22948 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375139, 230, 231, 374mp3an 1578 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376 cniccibl 23844 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
3771, 2, 375, 376mp3an 1578 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1
378377a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
379367, 372, 373, 378itgsub 23829 . . . . . . . . . . . . . . . . . . 19 (⊤ → ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥))
380379mptru 1645 . . . . . . . . . . . . . . . . . 18 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥)
3811a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴 ∈ ℝ)
3822a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐵 ∈ ℝ)
383345a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴𝐵)
384 1nn0 11595 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℕ0
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 1 ∈ ℕ0)
386381, 382, 383, 385itgpowd 38318 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387386mptru 1645 . . . . . . . . . . . . . . . . . . . . 21 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388 1p1e2 11445 . . . . . . . . . . . . . . . . . . . . . 22 (1 + 1) = 2
389388oveq2i 6895 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390387, 389eqtri 2839 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391 itgeq2 23781 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392235exp1d 13246 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393391, 392mprg 3125 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394388oveq2i 6895 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵↑(1 + 1)) = (𝐵↑2)
395388oveq2i 6895 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴↑(1 + 1)) = (𝐴↑2)
396394, 395oveq12i 6896 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397396oveq1i 6894 . . . . . . . . . . . . . . . . . . . 20 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398390, 393, 3973eqtr3i 2847 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399 itgconst 23822 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400342, 349, 139, 399mp3an 1578 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401348oveq2i 6895 . . . . . . . . . . . . . . . . . . . 20 (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵𝐴))
402400, 401eqtri 2839 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵𝐴))
403398, 402oveq12i 6896 . . . . . . . . . . . . . . . . . 18 (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
404380, 403eqtri 2839 . . . . . . . . . . . . . . . . 17 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
405404oveq2i 6895 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴))))
40614a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵 ∈ ℂ)
407139a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐴 ∈ ℂ)
408406, 407subcld 10687 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ∈ ℂ)
40918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵𝐴)
410406, 407, 409subne0d 10696 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ≠ 0)
411408, 410reccld 11089 . . . . . . . . . . . . . . . . . 18 (⊤ → (1 / (𝐵𝐴)) ∈ ℂ)
412411mptru 1645 . . . . . . . . . . . . . . . . 17 (1 / (𝐵𝐴)) ∈ ℂ
41314sqcli 13187 . . . . . . . . . . . . . . . . . . 19 (𝐵↑2) ∈ ℂ
414139sqcli 13187 . . . . . . . . . . . . . . . . . . 19 (𝐴↑2) ∈ ℂ
415413, 414subcli 10652 . . . . . . . . . . . . . . . . . 18 ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416415, 300, 301divcli 11062 . . . . . . . . . . . . . . . . 17 (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417139, 147mulcli 10342 . . . . . . . . . . . . . . . . 17 (𝐴 · (𝐵𝐴)) ∈ ℂ
418412, 416, 417subdii 10774 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
419405, 418eqtri 2839 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
420137adantl 469 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥𝐴) ∈ ℝ)
421367, 372, 373, 378iblsub 23825 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥𝐴)) ∈ 𝐿1)
422411, 420, 421itgmulc2 23837 . . . . . . . . . . . . . . . 16 (⊤ → ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
423422mptru 1645 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
424412, 417mulcomi 10343 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
425417, 147, 21divreci 11065 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
426139, 147, 21divcan4i 11067 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = 𝐴
427424, 425, 4263eqtr2i 2845 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = 𝐴
428427oveq2i 6895 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429419, 423, 4283eqtr3i 2847 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430366, 429eqtri 2839 . . . . . . . . . . . . 13 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
43114, 139subsqi 13218 . . . . . . . . . . . . . . . . 17 ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵𝐴))
432431oveq1i 6894 . . . . . . . . . . . . . . . 16 (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵𝐴)) / 2)
433432oveq2i 6895 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
434431, 415eqeltrri 2893 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) · (𝐵𝐴)) ∈ ℂ
435412, 434, 300, 301divassi 11076 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
436412, 434mulcomi 10343 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
437434, 147, 21divreci 11065 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
43814, 139addcli 10341 . . . . . . . . . . . . . . . . . 18 (𝐵 + 𝐴) ∈ ℂ
439438, 147, 21divcan4i 11067 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (𝐵 + 𝐴)
440436, 437, 4393eqtr2i 2845 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (𝐵 + 𝐴)
441440oveq1i 6894 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442433, 435, 4413eqtr2i 2845 . . . . . . . . . . . . . 14 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443442oveq1i 6894 . . . . . . . . . . . . 13 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444139, 300mulcli 10342 . . . . . . . . . . . . . . 15 (𝐴 · 2) ∈ ℂ
445 divsubdir 11016 . . . . . . . . . . . . . . 15 (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446438, 444, 293, 445mp3an 1578 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
44714, 139, 444addsubassi 10667 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448 subsub2 10604 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
44914, 444, 139, 448mp3an 1578 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450139times2i 11459 . . . . . . . . . . . . . . . . . . 19 (𝐴 · 2) = (𝐴 + 𝐴)
451450oveq1i 6894 . . . . . . . . . . . . . . . . . 18 ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452139, 139pncan3oi 10592 . . . . . . . . . . . . . . . . . 18 ((𝐴 + 𝐴) − 𝐴) = 𝐴
453451, 452eqtri 2839 . . . . . . . . . . . . . . . . 17 ((𝐴 · 2) − 𝐴) = 𝐴
454453oveq2i 6895 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵𝐴)
455447, 449, 4543eqtr2i 2845 . . . . . . . . . . . . . . 15 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵𝐴)
456455oveq1i 6894 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵𝐴) / 2)
457139, 300, 301divcan4i 11067 . . . . . . . . . . . . . . 15 ((𝐴 · 2) / 2) = 𝐴
458457oveq2i 6895 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459446, 456, 4583eqtr3ri 2848 . . . . . . . . . . . . 13 (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵𝐴) / 2)
460430, 443, 4593eqtri 2843 . . . . . . . . . . . 12 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ((𝐵𝐴) / 2)
461460oveq2i 6895 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐹𝐸) · ((𝐵𝐴) / 2))
462 itgeq2 23781 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) → ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
46361, 58subcli 10652 . . . . . . . . . . . . . 14 (𝐹𝐸) ∈ ℂ
464463a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐹𝐸) ∈ ℂ)
465464, 127mulcomd 10356 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
466462, 465mprg 3125 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥
467362, 461, 4663eqtr3ri 2848 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥 = ((𝐹𝐸) · ((𝐵𝐴) / 2))
468353, 467oveq12i 6896 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥) = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
469326, 340, 4683eqtri 2843 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
470147, 300, 301divcli 11062 . . . . . . . . 9 ((𝐵𝐴) / 2) ∈ ℂ
471319, 463, 470adddiri 10348 . . . . . . . 8 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
472323, 469, 4713eqtr4i 2849 . . . . . . 7 ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2))
473 addsub12 10589 . . . . . . . . . 10 ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸)))
47461, 319, 58, 473mp3an 1578 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸))
47558times2i 11459 . . . . . . . . . . . 12 (𝐸 · 2) = (𝐸 + 𝐸)
476475oveq1i 6894 . . . . . . . . . . 11 ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
47758, 58pncan3oi 10592 . . . . . . . . . . 11 ((𝐸 + 𝐸) − 𝐸) = 𝐸
478476, 477eqtri 2839 . . . . . . . . . 10 ((𝐸 · 2) − 𝐸) = 𝐸
479478oveq2i 6895 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480474, 479eqtr3i 2841 . . . . . . . 8 ((𝐸 · 2) + (𝐹𝐸)) = (𝐹 + 𝐸)
481480oveq1i 6894 . . . . . . 7 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
482472, 481eqtri 2839 . . . . . 6 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
4838, 300, 301divcan4i 11067 . . . . . . . . . . 11 ((𝐶 · 2) / 2) = 𝐶
484483oveq1i 6894 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = (𝐶 · (𝐵𝐴))
4858, 300mulcli 10342 . . . . . . . . . . 11 (𝐶 · 2) ∈ ℂ
486 div32 11000 . . . . . . . . . . 11 (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2)))
487485, 293, 147, 486mp3an 1578 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
488484, 487eqtr3i 2841 . . . . . . . . 9 (𝐶 · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
489488oveq1i 6894 . . . . . . . 8 ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2))) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
49031a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
491490itgeq2dv 23785 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥)
492491mptru 1645 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥
4937a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494 cniccibl 23844 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
4951, 2, 266, 494mp3an 1578 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1
496495a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
49725a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498497, 493resubcld 10753 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷𝐶) ∈ ℝ)
499331, 498remulcld 10365 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ)
500272mptru 1645 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501 cniccibl 23844 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
5021, 2, 500, 501mp3an 1578 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1
503502a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
504493, 496, 499, 503itgadd 23828 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥))
505504mptru 1645 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
506 itgconst 23822 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507342, 349, 8, 506mp3an 1578 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508348oveq2i 6895 . . . . . . . . . . 11 (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵𝐴))
509507, 508eqtri 2839 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵𝐴))
51026a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐷 ∈ ℂ)
5118a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐶 ∈ ℂ)
512510, 511subcld 10687 . . . . . . . . . . . . 13 (⊤ → (𝐷𝐶) ∈ ℂ)
513512, 331, 360itgmulc2 23837 . . . . . . . . . . . 12 (⊤ → ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
514513mptru 1645 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
515460oveq2i 6895 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐷𝐶) · ((𝐵𝐴) / 2))
516 itgeq2 23781 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) → ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
51726, 8subcli 10652 . . . . . . . . . . . . . 14 (𝐷𝐶) ∈ ℂ
518517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷𝐶) ∈ ℂ)
519518, 127mulcomd 10356 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
520516, 519mprg 3125 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥
521514, 515, 5203eqtr3ri 2848 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥 = ((𝐷𝐶) · ((𝐵𝐴) / 2))
522509, 521oveq12i 6896 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥) = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
523492, 505, 5223eqtri 2843 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
524485, 517, 470adddiri 10348 . . . . . . . 8 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
525489, 523, 5243eqtr4i 2849 . . . . . . 7 ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2))
526 addsub12 10589 . . . . . . . . . 10 ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶)))
52726, 485, 8, 526mp3an 1578 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶))
5288times2i 11459 . . . . . . . . . . . 12 (𝐶 · 2) = (𝐶 + 𝐶)
529528oveq1i 6894 . . . . . . . . . . 11 ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
5308, 8pncan3oi 10592 . . . . . . . . . . 11 ((𝐶 + 𝐶) − 𝐶) = 𝐶
531529, 530eqtri 2839 . . . . . . . . . 10 ((𝐶 · 2) − 𝐶) = 𝐶
532531oveq2i 6895 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533527, 532eqtr3i 2841 . . . . . . . 8 ((𝐶 · 2) + (𝐷𝐶)) = (𝐷 + 𝐶)
534533oveq1i 6894 . . . . . . 7 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
535525, 534eqtri 2839 . . . . . 6 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
536482, 535oveq12i 6896 . . . . 5 (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
537316, 536eqtri 2839 . . . 4 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
538299, 304, 5373eqtr4ri 2850 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
539289, 291, 5383eqtr2i 2845 . 2 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
540286, 539eqtri 2839 1 (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wa 384   = wceq 1637  wtru 1638  wcel 2157  wne 2989  wral 3107  cdif 3777  wss 3780  c0 4127  ifcif 4290  {csn 4381  cop 4387   class class class wbr 4855  {copab 4917  cmpt 4934   × cxp 5322  ccnv 5323  dom cdm 5324  cres 5326  cima 5327  Fun wfun 6105  wf 6107  cfv 6111  (class class class)co 6884  cc 10229  cr 10230  0cc0 10231  1c1 10232   + caddc 10234   · cmul 10236  +∞cpnf 10366  *cxr 10368   < clt 10369  cle 10370  cmin 10561   / cdiv 10979  2c2 11368  0cn0 11579  [,]cicc 12416  cexp 13103  TopOpenctopn 16307  fldccnfld 19974   Cn ccn 21263   ×t ctx 21598  cnccncf 22913  vol*covol 23466  volcvol 23467  𝐿1cibl 23621  citg 23622  areacarea 24919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-rep 4977  ax-sep 4988  ax-nul 4996  ax-pow 5048  ax-pr 5109  ax-un 7189  ax-inf2 8795  ax-cc 9552  ax-cnex 10287  ax-resscn 10288  ax-1cn 10289  ax-icn 10290  ax-addcl 10291  ax-addrcl 10292  ax-mulcl 10293  ax-mulrcl 10294  ax-mulcom 10295  ax-addass 10296  ax-mulass 10297  ax-distr 10298  ax-i2m1 10299  ax-1ne0 10300  ax-1rid 10301  ax-rnegex 10302  ax-rrecex 10303  ax-cnre 10304  ax-pre-lttri 10305  ax-pre-lttrn 10306  ax-pre-ltadd 10307  ax-pre-mulgt0 10308  ax-pre-sup 10309  ax-addf 10310  ax-mulf 10311
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ne 2990  df-nel 3093  df-ral 3112  df-rex 3113  df-reu 3114  df-rmo 3115  df-rab 3116  df-v 3404  df-sbc 3645  df-csb 3740  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-pss 3796  df-symdif 4053  df-nul 4128  df-if 4291  df-pw 4364  df-sn 4382  df-pr 4384  df-tp 4386  df-op 4388  df-uni 4642  df-int 4681  df-iun 4725  df-iin 4726  df-disj 4824  df-br 4856  df-opab 4918  df-mpt 4935  df-tr 4958  df-id 5232  df-eprel 5237  df-po 5245  df-so 5246  df-fr 5283  df-se 5284  df-we 5285  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337  df-pred 5907  df-ord 5953  df-on 5954  df-lim 5955  df-suc 5956  df-iota 6074  df-fun 6113  df-fn 6114  df-f 6115  df-f1 6116  df-fo 6117  df-f1o 6118  df-fv 6119  df-isom 6120  df-riota 6845  df-ov 6887  df-oprab 6888  df-mpt2 6889  df-of 7137  df-ofr 7138  df-om 7306  df-1st 7408  df-2nd 7409  df-supp 7540  df-wrecs 7652  df-recs 7714  df-rdg 7752  df-1o 7806  df-2o 7807  df-oadd 7810  df-omul 7811  df-er 7989  df-map 8104  df-pm 8105  df-ixp 8156  df-en 8203  df-dom 8204  df-sdom 8205  df-fin 8206  df-fsupp 8525  df-fi 8566  df-sup 8597  df-inf 8598  df-oi 8664  df-card 9058  df-acn 9061  df-cda 9285  df-pnf 10371  df-mnf 10372  df-xr 10373  df-ltxr 10374  df-le 10375  df-sub 10563  df-neg 10564  df-div 10980  df-nn 11316  df-2 11376  df-3 11377  df-4 11378  df-5 11379  df-6 11380  df-7 11381  df-8 11382  df-9 11383  df-n0 11580  df-z 11664  df-dec 11780  df-uz 11925  df-q 12028  df-rp 12067  df-xneg 12182  df-xadd 12183  df-xmul 12184  df-ioo 12417  df-ioc 12418  df-ico 12419  df-icc 12420  df-fz 12570  df-fzo 12710  df-fl 12837  df-mod 12913  df-seq 13045  df-exp 13104  df-hash 13358  df-cj 14082  df-re 14083  df-im 14084  df-sqrt 14218  df-abs 14219  df-limsup 14445  df-clim 14462  df-rlim 14463  df-sum 14660  df-struct 16090  df-ndx 16091  df-slot 16092  df-base 16094  df-sets 16095  df-ress 16096  df-plusg 16186  df-mulr 16187  df-starv 16188  df-sca 16189  df-vsca 16190  df-ip 16191  df-tset 16192  df-ple 16193  df-ds 16195  df-unif 16196  df-hom 16197  df-cco 16198  df-rest 16308  df-topn 16309  df-0g 16327  df-gsum 16328  df-topgen 16329  df-pt 16330  df-prds 16333  df-xrs 16387  df-qtop 16392  df-imas 16393  df-xps 16395  df-mre 16471  df-mrc 16472  df-acs 16474  df-mgm 17467  df-sgrp 17509  df-mnd 17520  df-submnd 17561  df-mulg 17766  df-cntz 17971  df-cmn 18416  df-psmet 19966  df-xmet 19967  df-met 19968  df-bl 19969  df-mopn 19970  df-fbas 19971  df-fg 19972  df-cnfld 19975  df-top 20933  df-topon 20950  df-topsp 20972  df-bases 20985  df-cld 21058  df-ntr 21059  df-cls 21060  df-nei 21137  df-lp 21175  df-perf 21176  df-cn 21266  df-cnp 21267  df-haus 21354  df-cmp 21425  df-tx 21600  df-hmeo 21793  df-fil 21884  df-fm 21976  df-flim 21977  df-flf 21978  df-xms 22359  df-ms 22360  df-tms 22361  df-cncf 22915  df-ovol 23468  df-vol 23469  df-mbf 23623  df-itg1 23624  df-itg2 23625  df-ibl 23626  df-itg 23627  df-0p 23674  df-limc 23867  df-dv 23868  df-area 24920
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator