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 39684
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 12811 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
41, 2, 3mp2an 688 . . . . . . . . 9 (𝐴[,]𝐵) ⊆ ℝ
54sseli 3966 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
65adantr 481 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7 areaquad.3 . . . . . . . . . . . . . . . 16 𝐶 ∈ ℝ
87recni 10647 . . . . . . . . . . . . . . 15 𝐶 ∈ ℂ
98a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10 resubcl 10942 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥𝐴) ∈ ℝ)
111, 10mpan2 687 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝑥𝐴) ∈ ℝ)
122, 1resubcli 10940 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ∈ ℝ
1312a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ∈ ℝ)
142recni 10647 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℂ
1514a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16 recn 10619 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17 areaquad.7 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 < 𝐵
181, 17gtneii 10744 . . . . . . . . . . . . . . . . . . . . 21 𝐵𝐴
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵𝐴)
2015, 16, 19subne0d 10998 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℝ → (𝐵𝐴) ≠ 0)
211, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ≠ 0
2221a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ≠ 0)
2311, 13, 22redivcld 11460 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
2423recnd 10661 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
25 areaquad.4 . . . . . . . . . . . . . . . . 17 𝐷 ∈ ℝ
2625recni 10647 . . . . . . . . . . . . . . . 16 𝐷 ∈ ℂ
2726a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
2824, 27mulcld 10653 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) ∈ ℂ)
2924, 9mulcld 10653 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐶) ∈ ℂ)
309, 28, 29addsub12d 11012 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
31 areaquad.10 . . . . . . . . . . . . . 14 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
3224, 27, 9subdid 11088 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
3332oveq2d 7167 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
3431, 33syl5eq 2872 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
35 1cnd 10628 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℂ)
3635, 24, 9subdird 11089 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
378mulid2i 10638 . . . . . . . . . . . . . . . 16 (1 · 𝐶) = 𝐶
3837oveq1i 7161 . . . . . . . . . . . . . . 15 ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))
3936, 38syl6eq 2876 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
4039oveq2d 7167 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
4130, 34, 403eqtr4d 2870 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑈 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)))
42 1red 10634 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℝ)
4342, 23resubcld 11060 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
4443recnd 10661 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℂ)
4544, 9mulcld 10653 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) ∈ ℂ)
4628, 45addcomd 10834 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)))
4744, 9mulcomd 10654 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
4824, 27mulcomd 10654 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) = (𝐷 · ((𝑥𝐴) / (𝐵𝐴))))
4947, 48oveq12d 7169 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
5041, 46, 493eqtrd 2864 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
5251, 43remulcld 10663 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5325a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
5453, 23remulcld 10663 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
5552, 54readdcld 10662 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5650, 55eqeltrd 2917 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57 areaquad.5 . . . . . . . . . . . . . . . 16 𝐸 ∈ ℝ
5857recni 10647 . . . . . . . . . . . . . . 15 𝐸 ∈ ℂ
5958a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60 areaquad.6 . . . . . . . . . . . . . . . . 17 𝐹 ∈ ℝ
6160recni 10647 . . . . . . . . . . . . . . . 16 𝐹 ∈ ℂ
6261a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
6324, 62mulcld 10653 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) ∈ ℂ)
6424, 59mulcld 10653 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐸) ∈ ℂ)
6559, 63, 64addsub12d 11012 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
66 areaquad.11 . . . . . . . . . . . . . 14 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
6724, 62, 59subdid 11088 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
6867oveq2d 7167 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
6966, 68syl5eq 2872 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7035, 24, 59subdird 11089 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7158mulid2i 10638 . . . . . . . . . . . . . . . 16 (1 · 𝐸) = 𝐸
7271oveq1i 7161 . . . . . . . . . . . . . . 15 ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))
7370, 72syl6eq 2876 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7473oveq2d 7167 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7565, 69, 743eqtr4d 2870 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑉 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)))
7644, 59mulcld 10653 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) ∈ ℂ)
7763, 76addcomd 10834 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)))
7844, 59mulcomd 10654 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
7924, 62mulcomd 10654 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) = (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
8078, 79oveq12d 7169 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8175, 77, 803eqtrd 2864 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8257a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
8382, 43remulcld 10663 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8460a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
8584, 23remulcld 10663 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐹 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
8683, 85readdcld 10662 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8781, 86eqeltrd 2917 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88 iccssre 12811 . . . . . . . . . 10 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
8956, 87, 88syl2anc 584 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
905, 89syl 17 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
9190sselda 3970 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
926, 91jca 512 . . . . . 6 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
9392ssopab2i 5433 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94 areaquad.12 . . . . 5 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95 df-xp 5559 . . . . 5 (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
9693, 94, 953sstr4i 4013 . . . 4 𝑆 ⊆ (ℝ × ℝ)
97 iftrue 4475 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (𝑉𝑈))
98 nfv 1908 . . . . . . . . . . . . 13 𝑦 𝑥 ∈ (𝐴[,]𝐵)
99 nfopab2 5132 . . . . . . . . . . . . . . 15 𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
10094, 99nfcxfr 2979 . . . . . . . . . . . . . 14 𝑦𝑆
101 nfcv 2981 . . . . . . . . . . . . . 14 𝑦{𝑥}
102100, 101nfima 5934 . . . . . . . . . . . . 13 𝑦(𝑆 “ {𝑥})
103 nfcv 2981 . . . . . . . . . . . . 13 𝑦(𝑈[,]𝑉)
104 vex 3502 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
105 vex 3502 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
106104, 105elimasn 5951 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
10794eleq2i 2908 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108 opabid 5409 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109106, 107, 1083bitri 298 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110109baib 536 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
11198, 102, 103, 110eqrd 3989 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112111fveq2d 6670 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
1135, 56syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
1145, 87syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115 iccmbl 24082 . . . . . . . . . . . . 13 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116113, 114, 115syl2anc 584 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117 mblvol 24046 . . . . . . . . . . . 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 10661 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
128127subidd 10977 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) = 0)
129 1red 10634 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
1302a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
1311a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
1321rexri 10691 . . . . . . . . . . . . . . . . . . . . 21 𝐴 ∈ ℝ*
1332rexri 10691 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℝ*
134 iccleub 12785 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝑥𝐵)
135132, 133, 134mp3an12 1444 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥𝐵)
1365, 130, 131, 135lesub1dd 11248 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ≤ (𝐵𝐴))
1375, 1, 10sylancl 586 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℝ)
13812a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ)
1391recni 10647 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 ∈ ℂ
140139subidi 10949 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝐴) = 0
141131, 130, 131ltsub1d 11241 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴𝐴) < (𝐵𝐴)))
14217, 141mpbii 234 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) < (𝐵𝐴))
143140, 142eqbrtrrid 5098 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵𝐴))
144 lediv1 11497 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝐴) ∈ ℝ ∧ (𝐵𝐴) ∈ ℝ ∧ ((𝐵𝐴) ∈ ℝ ∧ 0 < (𝐵𝐴))) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
145137, 138, 138, 143, 144syl112anc 1368 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
146136, 145mpbid 233 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴)))
14712recni 10647 . . . . . . . . . . . . . . . . . . 19 (𝐵𝐴) ∈ ℂ
148147, 21dividi 11365 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐴) / (𝐵𝐴)) = 1
149146, 148breqtrdi 5103 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ 1)
150126, 129, 126, 149lesub1dd 11248 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
151128, 150eqbrtrrd 5086 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
152 areaquad.8 . . . . . . . . . . . . . . . 16 𝐶𝐸
153152a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐶𝐸)
154123, 124, 125, 151, 153lemul1ad 11571 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ≤ (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
15525a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
15660a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157138, 143elrpd 12421 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ+)
158 iccgelb 12786 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝐴𝑥)
159132, 133, 158mp3an12 1444 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴𝑥)
160131, 5, 131, 159lesub1dd 11248 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) ≤ (𝑥𝐴))
161140, 160eqbrtrrid 5098 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥𝐴))
162137, 157, 161divge0d 12464 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥𝐴) / (𝐵𝐴)))
163 areaquad.9 . . . . . . . . . . . . . . . 16 𝐷𝐹
164163a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷𝐹)
165155, 156, 126, 162, 164lemul1ad 11571 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ≤ (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
166119, 120, 121, 122, 154, 165le2addd 11251 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ≤ ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
1675, 50syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
1685, 81syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
169166, 167, 1683brtr4d 5094 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈𝑉)
170 ovolicc 24039 . . . . . . . . . . . 12 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
171113, 114, 169, 170syl3anc 1365 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
172112, 118, 1713eqtrd 2864 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉𝑈))
17397, 172eqtr4d 2863 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174 iffalse 4478 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = 0)
175 nfv 1908 . . . . . . . . . . . . 13 𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176 nfcv 2981 . . . . . . . . . . . . 13 𝑦
177109simplbi 498 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178 noel 4299 . . . . . . . . . . . . . . 15 ¬ 𝑦 ∈ ∅
179178pm2.21i 119 . . . . . . . . . . . . . 14 (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180177, 179pm5.21ni 379 . . . . . . . . . . . . 13 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181175, 102, 176, 180eqrd 3989 . . . . . . . . . . . 12 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182181fveq2d 6670 . . . . . . . . . . 11 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183 0mbl 24055 . . . . . . . . . . . . 13 ∅ ∈ dom vol
184 mblvol 24046 . . . . . . . . . . . . 13 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185183, 184ax-mp 5 . . . . . . . . . . . 12 (vol‘∅) = (vol*‘∅)
186 ovol0 24009 . . . . . . . . . . . 12 (vol*‘∅) = 0
187185, 186eqtri 2848 . . . . . . . . . . 11 (vol‘∅) = 0
188182, 187syl6eq 2876 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189174, 188eqtr4d 2863 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190173, 189pm2.61i 183 . . . . . . . 8 if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191190eqcomi 2834 . . . . . . 7 (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0)
19287, 56resubcld 11060 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑉𝑈) ∈ ℝ)
193 0re 10635 . . . . . . . 8 0 ∈ ℝ
194 ifcl 4513 . . . . . . . 8 (((𝑉𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
195192, 193, 194sylancl 586 . . . . . . 7 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
196191, 195eqeltrid 2921 . . . . . 6 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197 volf 24045 . . . . . . . 8 vol:dom vol⟶(0[,]+∞)
198 ffun 6513 . . . . . . . 8 (vol:dom vol⟶(0[,]+∞) → Fun vol)
199197, 198ax-mp 5 . . . . . . 7 Fun vol
200 iftrue 4475 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201111, 200eqtr4d 2863 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202 iffalse 4478 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203181, 202eqtr4d 2863 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204201, 203pm2.61i 183 . . . . . . . 8 (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
20556, 87, 115syl2anc 584 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206183a1i 11 . . . . . . . . 9 (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207205, 206ifcld 4514 . . . . . . . 8 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208204, 207eqeltrid 2921 . . . . . . 7 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209 fvimacnv 6818 . . . . . . 7 ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
210199, 208, 209sylancr 587 . . . . . 6 (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
211196, 210mpbid 233 . . . . 5 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (vol “ ℝ))
212211rgen 3152 . . . 4 𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)
2134a1i 11 . . . . . 6 (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214 rembl 24056 . . . . . . 7 ℝ ∈ dom vol
215214a1i 11 . . . . . 6 (0 ∈ ℝ → ℝ ∈ dom vol)
216114, 113resubcld 11060 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑉𝑈) ∈ ℝ)
217172, 216eqeltrd 2917 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218217adantl 482 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219 eldifn 4107 . . . . . . . 8 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220219, 188syl 17 . . . . . . 7 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221220adantl 482 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222172mpteq2ia 5153 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈))
223 eqid 2825 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
224223subcn 23389 . . . . . . . . . . . 12 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
225224a1i 11 . . . . . . . . . . 11 (⊤ → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
22666mpteq2i 5154 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
227223addcn 23388 . . . . . . . . . . . . . 14 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
228227a1i 11 . . . . . . . . . . . . 13 (⊤ → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
229 ax-resscn 10586 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
2304, 229sstri 3979 . . . . . . . . . . . . . . 15 (𝐴[,]𝐵) ⊆ ℂ
231 ssid 3992 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
232 cncfmptc 23434 . . . . . . . . . . . . . . 15 ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
23358, 230, 231, 232mp3an 1454 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234233a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235230sseli 3966 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236139a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237147a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℂ)
23821a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ≠ 0)
239235, 236, 237, 238divsubdird 11447 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
240239adantl 482 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
241240mpteq2dva 5157 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))))
242 resmpt 5903 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))))
243230, 242ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴)))
244 eqid 2825 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴)))
245244divccncf 23429 . . . . . . . . . . . . . . . . . . . 20 (((𝐵𝐴) ∈ ℂ ∧ (𝐵𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ))
246147, 21, 245mp2an 688 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ)
247 rescncf 23420 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248230, 246, 247mp2 9 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249243, 248eqeltrri 2914 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250249a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251139, 147, 21divcli 11374 . . . . . . . . . . . . . . . . . 18 (𝐴 / (𝐵𝐴)) ∈ ℂ
252 cncfmptc 23434 . . . . . . . . . . . . . . . . . 18 (((𝐴 / (𝐵𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253251, 230, 231, 252mp3an 1454 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254253a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255223, 225, 250, 254cncfmpt2f 23437 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256241, 255eqeltrd 2917 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257 cncfmptc 23434 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
25861, 230, 231, 257mp3an 1454 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259258a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260223, 225, 259, 234cncfmpt2f 23437 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261256, 260mulcncf 23962 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262223, 228, 234, 261cncfmpt2f 23437 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263226, 262eqeltrid 2921 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26431mpteq2i 5154 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
265 cncfmptc 23434 . . . . . . . . . . . . . . 15 ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2668, 230, 231, 265mp3an 1454 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267266a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268 cncfmptc 23434 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26926, 230, 231, 268mp3an 1454 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270269a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271223, 225, 270, 267cncfmpt2f 23437 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272256, 271mulcncf 23962 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273223, 228, 267, 272cncfmpt2f 23437 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274264, 273eqeltrid 2921 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275223, 225, 263, 274cncfmpt2f 23437 . . . . . . . . . 10 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276275mptru 1537 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277 cniccibl 24356 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1)
2781, 2, 276, 277mp3an 1454 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1
279222, 278eqeltri 2913 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
280279a1i 11 . . . . . 6 (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
281213, 215, 218, 221, 280iblss2 24321 . . . . 5 (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
282193, 281ax-mp 5 . . . 4 (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
283 dmarea 25449 . . . 4 (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1))
28496, 212, 282, 283mpbir3an 1335 . . 3 𝑆 ∈ dom area
285 areaval 25456 . . 3 (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286284, 285ax-mp 5 . 2 (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287 itgeq2 24293 . . . 4 (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
288191a1i 11 . . . 4 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0))
289287, 288mprg 3156 . . 3 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
290 itgss2 24328 . . . 4 ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
2914, 290ax-mp 5 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
29261, 58addcli 10639 . . . . . 6 (𝐹 + 𝐸) ∈ ℂ
293 2cnne0 11839 . . . . . 6 (2 ∈ ℂ ∧ 2 ≠ 0)
294 div32 11310 . . . . . 6 (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2)))
295292, 293, 147, 294mp3an 1454 . . . . 5 (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
29626, 8addcli 10639 . . . . . 6 (𝐷 + 𝐶) ∈ ℂ
297 div32 11310 . . . . . 6 (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
298296, 293, 147, 297mp3an 1454 . . . . 5 (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
299295, 298oveq12i 7163 . . . 4 ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴))) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
300 2cn 11704 . . . . . 6 2 ∈ ℂ
301 2ne0 11733 . . . . . 6 2 ≠ 0
302292, 300, 301divcli 11374 . . . . 5 ((𝐹 + 𝐸) / 2) ∈ ℂ
303296, 300, 301divcli 11374 . . . . 5 ((𝐷 + 𝐶) / 2) ∈ ℂ
304302, 303, 147subdiri 11082 . . . 4 ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴)))
305114adantl 482 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306263mptru 1537 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307 cniccibl 24356 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
3081, 2, 306, 307mp3an 1454 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1
309308a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
310113adantl 482 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311274mptru 1537 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312 cniccibl 24356 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
3131, 2, 311, 312mp3an 1454 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1
314313a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
315305, 309, 310, 314itgsub 24341 . . . . . 6 (⊤ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316315mptru 1537 . . . . 5 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
31758, 300, 301divcan4i 11379 . . . . . . . . . . 11 ((𝐸 · 2) / 2) = 𝐸
318317oveq1i 7161 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = (𝐸 · (𝐵𝐴))
31958, 300mulcli 10640 . . . . . . . . . . 11 (𝐸 · 2) ∈ ℂ
320 div32 11310 . . . . . . . . . . 11 (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2)))
321319, 293, 147, 320mp3an 1454 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
322318, 321eqtr3i 2850 . . . . . . . . 9 (𝐸 · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
323322oveq1i 7161 . . . . . . . 8 ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2))) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
324 itgeq2 24293 . . . . . . . . . 10 (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥)
32566a1i 11 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
326324, 325mprg 3156 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥
32757a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328 cniccibl 24356 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
3291, 2, 233, 328mp3an 1454 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1
330329a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
331126adantl 482 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
33260a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333332, 327resubcld 11060 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝐸) ∈ ℝ)
334331, 333remulcld 10663 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) ∈ ℝ)
335261mptru 1537 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336 cniccibl 24356 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
3371, 2, 335, 336mp3an 1454 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1
338337a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
339327, 330, 334, 338itgadd 24340 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥))
340339mptru 1537 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
341 iccmbl 24082 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
3421, 2, 341mp2an 688 . . . . . . . . . . . 12 (𝐴[,]𝐵) ∈ dom vol
343 mblvol 24046 . . . . . . . . . . . . . . 15 ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344342, 343ax-mp 5 . . . . . . . . . . . . . 14 (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
3451, 2, 17ltleii 10755 . . . . . . . . . . . . . . 15 𝐴𝐵
346 ovolicc 24039 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴))
3471, 2, 345, 346mp3an 1454 . . . . . . . . . . . . . 14 (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴)
348344, 347eqtri 2848 . . . . . . . . . . . . 13 (vol‘(𝐴[,]𝐵)) = (𝐵𝐴)
349348, 12eqeltri 2913 . . . . . . . . . . . 12 (vol‘(𝐴[,]𝐵)) ∈ ℝ
350 itgconst 24334 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351342, 349, 58, 350mp3an 1454 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352348oveq2i 7162 . . . . . . . . . . 11 (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵𝐴))
353351, 352eqtri 2848 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵𝐴))
35461a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐹 ∈ ℂ)
35558a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐸 ∈ ℂ)
356354, 355subcld 10989 . . . . . . . . . . . . 13 (⊤ → (𝐹𝐸) ∈ ℂ)
357256mptru 1537 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358 cniccibl 24356 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
3591, 2, 357, 358mp3an 1454 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1
360359a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
361356, 331, 360itgmulc2 24349 . . . . . . . . . . . 12 (⊤ → ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
362361mptru 1537 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
363 itgeq2 24293 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)) → ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
364137recnd 10661 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℂ)
365364, 237, 238divrec2d 11412 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)))
366363, 365mprg 3156 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
3675adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368 cncfmptid 23435 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369230, 231, 368mp2an 688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370 cniccibl 24356 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3711, 2, 369, 370mp3an 1454 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1
372371a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3731a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374 cncfmptc 23434 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375139, 230, 231, 374mp3an 1454 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376 cniccibl 24356 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
3771, 2, 375, 376mp3an 1454 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1
378377a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
379367, 372, 373, 378itgsub 24341 . . . . . . . . . . . . . . . . . . 19 (⊤ → ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥))
380379mptru 1537 . . . . . . . . . . . . . . . . . 18 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥)
3811a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴 ∈ ℝ)
3822a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐵 ∈ ℝ)
383345a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴𝐵)
384 1nn0 11905 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℕ0
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 1 ∈ ℕ0)
386381, 382, 383, 385itgpowd 39682 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387386mptru 1537 . . . . . . . . . . . . . . . . . . . . 21 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388 1p1e2 11754 . . . . . . . . . . . . . . . . . . . . . 22 (1 + 1) = 2
389388oveq2i 7162 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390387, 389eqtri 2848 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391 itgeq2 24293 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392235exp1d 13498 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393391, 392mprg 3156 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394388oveq2i 7162 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵↑(1 + 1)) = (𝐵↑2)
395388oveq2i 7162 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴↑(1 + 1)) = (𝐴↑2)
396394, 395oveq12i 7163 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397396oveq1i 7161 . . . . . . . . . . . . . . . . . . . 20 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398390, 393, 3973eqtr3i 2856 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399 itgconst 24334 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400342, 349, 139, 399mp3an 1454 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401348oveq2i 7162 . . . . . . . . . . . . . . . . . . . 20 (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵𝐴))
402400, 401eqtri 2848 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵𝐴))
403398, 402oveq12i 7163 . . . . . . . . . . . . . . . . . 18 (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
404380, 403eqtri 2848 . . . . . . . . . . . . . . . . 17 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
405404oveq2i 7162 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴))))
40614a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵 ∈ ℂ)
407139a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐴 ∈ ℂ)
408406, 407subcld 10989 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ∈ ℂ)
40918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵𝐴)
410406, 407, 409subne0d 10998 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ≠ 0)
411408, 410reccld 11401 . . . . . . . . . . . . . . . . . 18 (⊤ → (1 / (𝐵𝐴)) ∈ ℂ)
412411mptru 1537 . . . . . . . . . . . . . . . . 17 (1 / (𝐵𝐴)) ∈ ℂ
41314sqcli 13537 . . . . . . . . . . . . . . . . . . 19 (𝐵↑2) ∈ ℂ
414139sqcli 13537 . . . . . . . . . . . . . . . . . . 19 (𝐴↑2) ∈ ℂ
415413, 414subcli 10954 . . . . . . . . . . . . . . . . . 18 ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416415, 300, 301divcli 11374 . . . . . . . . . . . . . . . . 17 (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417139, 147mulcli 10640 . . . . . . . . . . . . . . . . 17 (𝐴 · (𝐵𝐴)) ∈ ℂ
418412, 416, 417subdii 11081 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
419405, 418eqtri 2848 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
420137adantl 482 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥𝐴) ∈ ℝ)
421367, 372, 373, 378iblsub 24337 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥𝐴)) ∈ 𝐿1)
422411, 420, 421itgmulc2 24349 . . . . . . . . . . . . . . . 16 (⊤ → ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
423422mptru 1537 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
424412, 417mulcomi 10641 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
425417, 147, 21divreci 11377 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
426139, 147, 21divcan4i 11379 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = 𝐴
427424, 425, 4263eqtr2i 2854 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = 𝐴
428427oveq2i 7162 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429419, 423, 4283eqtr3i 2856 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430366, 429eqtri 2848 . . . . . . . . . . . . 13 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
43114, 139subsqi 13568 . . . . . . . . . . . . . . . . 17 ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵𝐴))
432431oveq1i 7161 . . . . . . . . . . . . . . . 16 (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵𝐴)) / 2)
433432oveq2i 7162 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
434431, 415eqeltrri 2914 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) · (𝐵𝐴)) ∈ ℂ
435412, 434, 300, 301divassi 11388 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
436412, 434mulcomi 10641 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
437434, 147, 21divreci 11377 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
43814, 139addcli 10639 . . . . . . . . . . . . . . . . . 18 (𝐵 + 𝐴) ∈ ℂ
439438, 147, 21divcan4i 11379 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (𝐵 + 𝐴)
440436, 437, 4393eqtr2i 2854 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (𝐵 + 𝐴)
441440oveq1i 7161 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442433, 435, 4413eqtr2i 2854 . . . . . . . . . . . . . 14 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443442oveq1i 7161 . . . . . . . . . . . . 13 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444139, 300mulcli 10640 . . . . . . . . . . . . . . 15 (𝐴 · 2) ∈ ℂ
445 divsubdir 11326 . . . . . . . . . . . . . . 15 (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446438, 444, 293, 445mp3an 1454 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
44714, 139, 444addsubassi 10969 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448 subsub2 10906 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
44914, 444, 139, 448mp3an 1454 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450139times2i 11768 . . . . . . . . . . . . . . . . . . 19 (𝐴 · 2) = (𝐴 + 𝐴)
451450oveq1i 7161 . . . . . . . . . . . . . . . . . 18 ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452139, 139pncan3oi 10894 . . . . . . . . . . . . . . . . . 18 ((𝐴 + 𝐴) − 𝐴) = 𝐴
453451, 452eqtri 2848 . . . . . . . . . . . . . . . . 17 ((𝐴 · 2) − 𝐴) = 𝐴
454453oveq2i 7162 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵𝐴)
455447, 449, 4543eqtr2i 2854 . . . . . . . . . . . . . . 15 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵𝐴)
456455oveq1i 7161 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵𝐴) / 2)
457139, 300, 301divcan4i 11379 . . . . . . . . . . . . . . 15 ((𝐴 · 2) / 2) = 𝐴
458457oveq2i 7162 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459446, 456, 4583eqtr3ri 2857 . . . . . . . . . . . . 13 (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵𝐴) / 2)
460430, 443, 4593eqtri 2852 . . . . . . . . . . . 12 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ((𝐵𝐴) / 2)
461460oveq2i 7162 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐹𝐸) · ((𝐵𝐴) / 2))
462 itgeq2 24293 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) → ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
46361, 58subcli 10954 . . . . . . . . . . . . . 14 (𝐹𝐸) ∈ ℂ
464463a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐹𝐸) ∈ ℂ)
465464, 127mulcomd 10654 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
466462, 465mprg 3156 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥
467362, 461, 4663eqtr3ri 2857 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥 = ((𝐹𝐸) · ((𝐵𝐴) / 2))
468353, 467oveq12i 7163 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥) = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
469326, 340, 4683eqtri 2852 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
470147, 300, 301divcli 11374 . . . . . . . . 9 ((𝐵𝐴) / 2) ∈ ℂ
471319, 463, 470adddiri 10646 . . . . . . . 8 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
472323, 469, 4713eqtr4i 2858 . . . . . . 7 ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2))
473 addsub12 10891 . . . . . . . . . 10 ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸)))
47461, 319, 58, 473mp3an 1454 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸))
47558times2i 11768 . . . . . . . . . . . 12 (𝐸 · 2) = (𝐸 + 𝐸)
476475oveq1i 7161 . . . . . . . . . . 11 ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
47758, 58pncan3oi 10894 . . . . . . . . . . 11 ((𝐸 + 𝐸) − 𝐸) = 𝐸
478476, 477eqtri 2848 . . . . . . . . . 10 ((𝐸 · 2) − 𝐸) = 𝐸
479478oveq2i 7162 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480474, 479eqtr3i 2850 . . . . . . . 8 ((𝐸 · 2) + (𝐹𝐸)) = (𝐹 + 𝐸)
481480oveq1i 7161 . . . . . . 7 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
482472, 481eqtri 2848 . . . . . 6 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
4838, 300, 301divcan4i 11379 . . . . . . . . . . 11 ((𝐶 · 2) / 2) = 𝐶
484483oveq1i 7161 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = (𝐶 · (𝐵𝐴))
4858, 300mulcli 10640 . . . . . . . . . . 11 (𝐶 · 2) ∈ ℂ
486 div32 11310 . . . . . . . . . . 11 (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2)))
487485, 293, 147, 486mp3an 1454 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
488484, 487eqtr3i 2850 . . . . . . . . 9 (𝐶 · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
489488oveq1i 7161 . . . . . . . 8 ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2))) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
49031a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
491490itgeq2dv 24297 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥)
492491mptru 1537 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥
4937a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494 cniccibl 24356 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
4951, 2, 266, 494mp3an 1454 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1
496495a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
49725a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498497, 493resubcld 11060 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷𝐶) ∈ ℝ)
499331, 498remulcld 10663 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ)
500272mptru 1537 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501 cniccibl 24356 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
5021, 2, 500, 501mp3an 1454 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1
503502a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
504493, 496, 499, 503itgadd 24340 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥))
505504mptru 1537 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
506 itgconst 24334 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507342, 349, 8, 506mp3an 1454 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508348oveq2i 7162 . . . . . . . . . . 11 (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵𝐴))
509507, 508eqtri 2848 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵𝐴))
51026a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐷 ∈ ℂ)
5118a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐶 ∈ ℂ)
512510, 511subcld 10989 . . . . . . . . . . . . 13 (⊤ → (𝐷𝐶) ∈ ℂ)
513512, 331, 360itgmulc2 24349 . . . . . . . . . . . 12 (⊤ → ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
514513mptru 1537 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
515460oveq2i 7162 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐷𝐶) · ((𝐵𝐴) / 2))
516 itgeq2 24293 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) → ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
51726, 8subcli 10954 . . . . . . . . . . . . . 14 (𝐷𝐶) ∈ ℂ
518517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷𝐶) ∈ ℂ)
519518, 127mulcomd 10654 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
520516, 519mprg 3156 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥
521514, 515, 5203eqtr3ri 2857 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥 = ((𝐷𝐶) · ((𝐵𝐴) / 2))
522509, 521oveq12i 7163 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥) = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
523492, 505, 5223eqtri 2852 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
524485, 517, 470adddiri 10646 . . . . . . . 8 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
525489, 523, 5243eqtr4i 2858 . . . . . . 7 ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2))
526 addsub12 10891 . . . . . . . . . 10 ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶)))
52726, 485, 8, 526mp3an 1454 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶))
5288times2i 11768 . . . . . . . . . . . 12 (𝐶 · 2) = (𝐶 + 𝐶)
529528oveq1i 7161 . . . . . . . . . . 11 ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
5308, 8pncan3oi 10894 . . . . . . . . . . 11 ((𝐶 + 𝐶) − 𝐶) = 𝐶
531529, 530eqtri 2848 . . . . . . . . . 10 ((𝐶 · 2) − 𝐶) = 𝐶
532531oveq2i 7162 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533527, 532eqtr3i 2850 . . . . . . . 8 ((𝐶 · 2) + (𝐷𝐶)) = (𝐷 + 𝐶)
534533oveq1i 7161 . . . . . . 7 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
535525, 534eqtri 2848 . . . . . 6 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
536482, 535oveq12i 7163 . . . . 5 (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
537316, 536eqtri 2848 . . . 4 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
538299, 304, 5373eqtr4ri 2859 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
539289, 291, 5383eqtr2i 2854 . 2 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
540286, 539eqtri 2848 1 (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396   = wceq 1530  wtru 1531  wcel 2107  wne 3020  wral 3142  cdif 3936  wss 3939  c0 4294  ifcif 4469  {csn 4563  cop 4569   class class class wbr 5062  {copab 5124  cmpt 5142   × cxp 5551  ccnv 5552  dom cdm 5553  cres 5555  cima 5556  Fun wfun 6345  wf 6347  cfv 6351  (class class class)co 7151  cc 10527  cr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  +∞cpnf 10664  *cxr 10666   < clt 10667  cle 10668  cmin 10862   / cdiv 11289  2c2 11684  0cn0 11889  [,]cicc 12734  cexp 13422  TopOpenctopn 16687  fldccnfld 20461   Cn ccn 21748   ×t ctx 22084  cnccncf 23399  vol*covol 23978  volcvol 23979  𝐿1cibl 24133  citg 24134  areacarea 25447
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-13 2385  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-inf2 9096  ax-cc 9849  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-fal 1543  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-symdif 4222  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-disj 5028  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7402  df-ofr 7403  df-om 7572  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-omul 8101  df-er 8282  df-map 8401  df-pm 8402  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-dju 9322  df-card 9360  df-acn 9363  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-ioo 12735  df-ioc 12736  df-ico 12737  df-icc 12738  df-fz 12886  df-fzo 13027  df-fl 13155  df-mod 13231  df-seq 13363  df-exp 13423  df-hash 13684  df-cj 14451  df-re 14452  df-im 14453  df-sqrt 14587  df-abs 14588  df-limsup 14821  df-clim 14838  df-rlim 14839  df-sum 15036  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-sets 16482  df-ress 16483  df-plusg 16570  df-mulr 16571  df-starv 16572  df-sca 16573  df-vsca 16574  df-ip 16575  df-tset 16576  df-ple 16577  df-ds 16579  df-unif 16580  df-hom 16581  df-cco 16582  df-rest 16688  df-topn 16689  df-0g 16707  df-gsum 16708  df-topgen 16709  df-pt 16710  df-prds 16713  df-xrs 16767  df-qtop 16772  df-imas 16773  df-xps 16775  df-mre 16849  df-mrc 16850  df-acs 16852  df-mgm 17844  df-sgrp 17892  df-mnd 17903  df-submnd 17947  df-mulg 18157  df-cntz 18379  df-cmn 18830  df-psmet 20453  df-xmet 20454  df-met 20455  df-bl 20456  df-mopn 20457  df-fbas 20458  df-fg 20459  df-cnfld 20462  df-top 21418  df-topon 21435  df-topsp 21457  df-bases 21470  df-cld 21543  df-ntr 21544  df-cls 21545  df-nei 21622  df-lp 21660  df-perf 21661  df-cn 21751  df-cnp 21752  df-haus 21839  df-cmp 21911  df-tx 22086  df-hmeo 22279  df-fil 22370  df-fm 22462  df-flim 22463  df-flf 22464  df-xms 22845  df-ms 22846  df-tms 22847  df-cncf 23401  df-ovol 23980  df-vol 23981  df-mbf 24135  df-itg1 24136  df-itg2 24137  df-ibl 24138  df-itg 24139  df-0p 24186  df-limc 24379  df-dv 24380  df-area 25448
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator