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 39701
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 12806 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
41, 2, 3mp2an 688 . . . . . . . . 9 (𝐴[,]𝐵) ⊆ ℝ
54sseli 3960 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
65adantr 481 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7 areaquad.3 . . . . . . . . . . . . . . . 16 𝐶 ∈ ℝ
87recni 10643 . . . . . . . . . . . . . . 15 𝐶 ∈ ℂ
98a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10 resubcl 10938 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥𝐴) ∈ ℝ)
111, 10mpan2 687 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝑥𝐴) ∈ ℝ)
122, 1resubcli 10936 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ∈ ℝ
1312a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ∈ ℝ)
142recni 10643 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℂ
1514a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16 recn 10615 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17 areaquad.7 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 < 𝐵
181, 17gtneii 10740 . . . . . . . . . . . . . . . . . . . . 21 𝐵𝐴
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵𝐴)
2015, 16, 19subne0d 10994 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℝ → (𝐵𝐴) ≠ 0)
211, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ≠ 0
2221a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ≠ 0)
2311, 13, 22redivcld 11456 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
2423recnd 10657 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
25 areaquad.4 . . . . . . . . . . . . . . . . 17 𝐷 ∈ ℝ
2625recni 10643 . . . . . . . . . . . . . . . 16 𝐷 ∈ ℂ
2726a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
2824, 27mulcld 10649 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) ∈ ℂ)
2924, 9mulcld 10649 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐶) ∈ ℂ)
309, 28, 29addsub12d 11008 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
31 areaquad.10 . . . . . . . . . . . . . 14 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
3224, 27, 9subdid 11084 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
3332oveq2d 7161 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
3431, 33syl5eq 2865 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
35 1cnd 10624 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℂ)
3635, 24, 9subdird 11085 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
378mulid2i 10634 . . . . . . . . . . . . . . . 16 (1 · 𝐶) = 𝐶
3837oveq1i 7155 . . . . . . . . . . . . . . 15 ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))
3936, 38syl6eq 2869 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
4039oveq2d 7161 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
4130, 34, 403eqtr4d 2863 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑈 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)))
42 1red 10630 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℝ)
4342, 23resubcld 11056 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
4443recnd 10657 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℂ)
4544, 9mulcld 10649 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) ∈ ℂ)
4628, 45addcomd 10830 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)))
4744, 9mulcomd 10650 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
4824, 27mulcomd 10650 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) = (𝐷 · ((𝑥𝐴) / (𝐵𝐴))))
4947, 48oveq12d 7163 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
5041, 46, 493eqtrd 2857 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
5251, 43remulcld 10659 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5325a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
5453, 23remulcld 10659 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
5552, 54readdcld 10658 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5650, 55eqeltrd 2910 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57 areaquad.5 . . . . . . . . . . . . . . . 16 𝐸 ∈ ℝ
5857recni 10643 . . . . . . . . . . . . . . 15 𝐸 ∈ ℂ
5958a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60 areaquad.6 . . . . . . . . . . . . . . . . 17 𝐹 ∈ ℝ
6160recni 10643 . . . . . . . . . . . . . . . 16 𝐹 ∈ ℂ
6261a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
6324, 62mulcld 10649 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) ∈ ℂ)
6424, 59mulcld 10649 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐸) ∈ ℂ)
6559, 63, 64addsub12d 11008 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
66 areaquad.11 . . . . . . . . . . . . . 14 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
6724, 62, 59subdid 11084 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
6867oveq2d 7161 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
6966, 68syl5eq 2865 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7035, 24, 59subdird 11085 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7158mulid2i 10634 . . . . . . . . . . . . . . . 16 (1 · 𝐸) = 𝐸
7271oveq1i 7155 . . . . . . . . . . . . . . 15 ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))
7370, 72syl6eq 2869 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7473oveq2d 7161 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7565, 69, 743eqtr4d 2863 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑉 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)))
7644, 59mulcld 10649 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) ∈ ℂ)
7763, 76addcomd 10830 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)))
7844, 59mulcomd 10650 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
7924, 62mulcomd 10650 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) = (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
8078, 79oveq12d 7163 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8175, 77, 803eqtrd 2857 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8257a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
8382, 43remulcld 10659 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8460a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
8584, 23remulcld 10659 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐹 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
8683, 85readdcld 10658 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8781, 86eqeltrd 2910 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88 iccssre 12806 . . . . . . . . . 10 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
8956, 87, 88syl2anc 584 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
905, 89syl 17 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
9190sselda 3964 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
926, 91jca 512 . . . . . 6 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
9392ssopab2i 5428 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94 areaquad.12 . . . . 5 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95 df-xp 5554 . . . . 5 (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
9693, 94, 953sstr4i 4007 . . . 4 𝑆 ⊆ (ℝ × ℝ)
97 iftrue 4469 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (𝑉𝑈))
98 nfv 1906 . . . . . . . . . . . . 13 𝑦 𝑥 ∈ (𝐴[,]𝐵)
99 nfopab2 5127 . . . . . . . . . . . . . . 15 𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
10094, 99nfcxfr 2972 . . . . . . . . . . . . . 14 𝑦𝑆
101 nfcv 2974 . . . . . . . . . . . . . 14 𝑦{𝑥}
102100, 101nfima 5930 . . . . . . . . . . . . 13 𝑦(𝑆 “ {𝑥})
103 nfcv 2974 . . . . . . . . . . . . 13 𝑦(𝑈[,]𝑉)
104 vex 3495 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
105 vex 3495 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
106104, 105elimasn 5947 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
10794eleq2i 2901 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108 opabidw 5403 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109106, 107, 1083bitri 298 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110109baib 536 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
11198, 102, 103, 110eqrd 3983 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112111fveq2d 6667 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
1135, 56syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
1145, 87syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115 iccmbl 24094 . . . . . . . . . . . . 13 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116113, 114, 115syl2anc 584 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117 mblvol 24058 . . . . . . . . . . . 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 10657 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
128127subidd 10973 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) = 0)
129 1red 10630 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
1302a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
1311a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
1321rexri 10687 . . . . . . . . . . . . . . . . . . . . 21 𝐴 ∈ ℝ*
1332rexri 10687 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℝ*
134 iccleub 12780 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝑥𝐵)
135132, 133, 134mp3an12 1442 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥𝐵)
1365, 130, 131, 135lesub1dd 11244 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ≤ (𝐵𝐴))
1375, 1, 10sylancl 586 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℝ)
13812a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ)
1391recni 10643 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 ∈ ℂ
140139subidi 10945 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝐴) = 0
141131, 130, 131ltsub1d 11237 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴𝐴) < (𝐵𝐴)))
14217, 141mpbii 234 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) < (𝐵𝐴))
143140, 142eqbrtrrid 5093 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵𝐴))
144 lediv1 11493 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝐴) ∈ ℝ ∧ (𝐵𝐴) ∈ ℝ ∧ ((𝐵𝐴) ∈ ℝ ∧ 0 < (𝐵𝐴))) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
145137, 138, 138, 143, 144syl112anc 1366 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
146136, 145mpbid 233 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴)))
14712recni 10643 . . . . . . . . . . . . . . . . . . 19 (𝐵𝐴) ∈ ℂ
148147, 21dividi 11361 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐴) / (𝐵𝐴)) = 1
149146, 148breqtrdi 5098 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ 1)
150126, 129, 126, 149lesub1dd 11244 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
151128, 150eqbrtrrd 5081 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
152 areaquad.8 . . . . . . . . . . . . . . . 16 𝐶𝐸
153152a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐶𝐸)
154123, 124, 125, 151, 153lemul1ad 11567 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ≤ (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
15525a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
15660a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157138, 143elrpd 12416 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ+)
158 iccgelb 12781 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝐴𝑥)
159132, 133, 158mp3an12 1442 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴𝑥)
160131, 5, 131, 159lesub1dd 11244 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) ≤ (𝑥𝐴))
161140, 160eqbrtrrid 5093 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥𝐴))
162137, 157, 161divge0d 12459 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥𝐴) / (𝐵𝐴)))
163 areaquad.9 . . . . . . . . . . . . . . . 16 𝐷𝐹
164163a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷𝐹)
165155, 156, 126, 162, 164lemul1ad 11567 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ≤ (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
166119, 120, 121, 122, 154, 165le2addd 11247 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ≤ ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
1675, 50syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
1685, 81syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
169166, 167, 1683brtr4d 5089 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈𝑉)
170 ovolicc 24051 . . . . . . . . . . . 12 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
171113, 114, 169, 170syl3anc 1363 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
172112, 118, 1713eqtrd 2857 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉𝑈))
17397, 172eqtr4d 2856 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174 iffalse 4472 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = 0)
175 nfv 1906 . . . . . . . . . . . . 13 𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176 nfcv 2974 . . . . . . . . . . . . 13 𝑦
177109simplbi 498 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178 noel 4293 . . . . . . . . . . . . . . 15 ¬ 𝑦 ∈ ∅
179178pm2.21i 119 . . . . . . . . . . . . . 14 (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180177, 179pm5.21ni 379 . . . . . . . . . . . . 13 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181175, 102, 176, 180eqrd 3983 . . . . . . . . . . . 12 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182181fveq2d 6667 . . . . . . . . . . 11 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183 0mbl 24067 . . . . . . . . . . . . 13 ∅ ∈ dom vol
184 mblvol 24058 . . . . . . . . . . . . 13 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185183, 184ax-mp 5 . . . . . . . . . . . 12 (vol‘∅) = (vol*‘∅)
186 ovol0 24021 . . . . . . . . . . . 12 (vol*‘∅) = 0
187185, 186eqtri 2841 . . . . . . . . . . 11 (vol‘∅) = 0
188182, 187syl6eq 2869 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189174, 188eqtr4d 2856 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190173, 189pm2.61i 183 . . . . . . . 8 if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191190eqcomi 2827 . . . . . . 7 (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0)
19287, 56resubcld 11056 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑉𝑈) ∈ ℝ)
193 0re 10631 . . . . . . . 8 0 ∈ ℝ
194 ifcl 4507 . . . . . . . 8 (((𝑉𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
195192, 193, 194sylancl 586 . . . . . . 7 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
196191, 195eqeltrid 2914 . . . . . 6 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197 volf 24057 . . . . . . . 8 vol:dom vol⟶(0[,]+∞)
198 ffun 6510 . . . . . . . 8 (vol:dom vol⟶(0[,]+∞) → Fun vol)
199197, 198ax-mp 5 . . . . . . 7 Fun vol
200 iftrue 4469 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201111, 200eqtr4d 2856 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202 iffalse 4472 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203181, 202eqtr4d 2856 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204201, 203pm2.61i 183 . . . . . . . 8 (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
20556, 87, 115syl2anc 584 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206183a1i 11 . . . . . . . . 9 (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207205, 206ifcld 4508 . . . . . . . 8 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208204, 207eqeltrid 2914 . . . . . . 7 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209 fvimacnv 6815 . . . . . . 7 ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
210199, 208, 209sylancr 587 . . . . . 6 (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
211196, 210mpbid 233 . . . . 5 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (vol “ ℝ))
212211rgen 3145 . . . 4 𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)
2134a1i 11 . . . . . 6 (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214 rembl 24068 . . . . . . 7 ℝ ∈ dom vol
215214a1i 11 . . . . . 6 (0 ∈ ℝ → ℝ ∈ dom vol)
216114, 113resubcld 11056 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑉𝑈) ∈ ℝ)
217172, 216eqeltrd 2910 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218217adantl 482 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219 eldifn 4101 . . . . . . . 8 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220219, 188syl 17 . . . . . . 7 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221220adantl 482 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222172mpteq2ia 5148 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈))
223 eqid 2818 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
224223subcn 23401 . . . . . . . . . . . 12 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
225224a1i 11 . . . . . . . . . . 11 (⊤ → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
22666mpteq2i 5149 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
227223addcn 23400 . . . . . . . . . . . . . 14 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
228227a1i 11 . . . . . . . . . . . . 13 (⊤ → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
229 ax-resscn 10582 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
2304, 229sstri 3973 . . . . . . . . . . . . . . 15 (𝐴[,]𝐵) ⊆ ℂ
231 ssid 3986 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
232 cncfmptc 23446 . . . . . . . . . . . . . . 15 ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
23358, 230, 231, 232mp3an 1452 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234233a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235230sseli 3960 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236139a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237147a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℂ)
23821a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ≠ 0)
239235, 236, 237, 238divsubdird 11443 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
240239adantl 482 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
241240mpteq2dva 5152 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))))
242 resmpt 5898 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))))
243230, 242ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴)))
244 eqid 2818 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴)))
245244divccncf 23441 . . . . . . . . . . . . . . . . . . . 20 (((𝐵𝐴) ∈ ℂ ∧ (𝐵𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ))
246147, 21, 245mp2an 688 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ)
247 rescncf 23432 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248230, 246, 247mp2 9 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249243, 248eqeltrri 2907 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250249a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251139, 147, 21divcli 11370 . . . . . . . . . . . . . . . . . 18 (𝐴 / (𝐵𝐴)) ∈ ℂ
252 cncfmptc 23446 . . . . . . . . . . . . . . . . . 18 (((𝐴 / (𝐵𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253251, 230, 231, 252mp3an 1452 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254253a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255223, 225, 250, 254cncfmpt2f 23449 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256241, 255eqeltrd 2910 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257 cncfmptc 23446 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
25861, 230, 231, 257mp3an 1452 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259258a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260223, 225, 259, 234cncfmpt2f 23449 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261256, 260mulcncf 23974 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262223, 228, 234, 261cncfmpt2f 23449 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263226, 262eqeltrid 2914 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26431mpteq2i 5149 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
265 cncfmptc 23446 . . . . . . . . . . . . . . 15 ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2668, 230, 231, 265mp3an 1452 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267266a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268 cncfmptc 23446 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26926, 230, 231, 268mp3an 1452 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270269a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271223, 225, 270, 267cncfmpt2f 23449 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272256, 271mulcncf 23974 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273223, 228, 267, 272cncfmpt2f 23449 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274264, 273eqeltrid 2914 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275223, 225, 263, 274cncfmpt2f 23449 . . . . . . . . . 10 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276275mptru 1535 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277 cniccibl 24368 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1)
2781, 2, 276, 277mp3an 1452 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1
279222, 278eqeltri 2906 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
280279a1i 11 . . . . . 6 (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
281213, 215, 218, 221, 280iblss2 24333 . . . . 5 (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
282193, 281ax-mp 5 . . . 4 (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
283 dmarea 25462 . . . 4 (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1))
28496, 212, 282, 283mpbir3an 1333 . . 3 𝑆 ∈ dom area
285 areaval 25469 . . 3 (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286284, 285ax-mp 5 . 2 (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287 itgeq2 24305 . . . 4 (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
288191a1i 11 . . . 4 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0))
289287, 288mprg 3149 . . 3 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
290 itgss2 24340 . . . 4 ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
2914, 290ax-mp 5 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
29261, 58addcli 10635 . . . . . 6 (𝐹 + 𝐸) ∈ ℂ
293 2cnne0 11835 . . . . . 6 (2 ∈ ℂ ∧ 2 ≠ 0)
294 div32 11306 . . . . . 6 (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2)))
295292, 293, 147, 294mp3an 1452 . . . . 5 (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
29626, 8addcli 10635 . . . . . 6 (𝐷 + 𝐶) ∈ ℂ
297 div32 11306 . . . . . 6 (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
298296, 293, 147, 297mp3an 1452 . . . . 5 (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
299295, 298oveq12i 7157 . . . 4 ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴))) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
300 2cn 11700 . . . . . 6 2 ∈ ℂ
301 2ne0 11729 . . . . . 6 2 ≠ 0
302292, 300, 301divcli 11370 . . . . 5 ((𝐹 + 𝐸) / 2) ∈ ℂ
303296, 300, 301divcli 11370 . . . . 5 ((𝐷 + 𝐶) / 2) ∈ ℂ
304302, 303, 147subdiri 11078 . . . 4 ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴)))
305114adantl 482 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306263mptru 1535 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307 cniccibl 24368 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
3081, 2, 306, 307mp3an 1452 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1
309308a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
310113adantl 482 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311274mptru 1535 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312 cniccibl 24368 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
3131, 2, 311, 312mp3an 1452 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1
314313a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
315305, 309, 310, 314itgsub 24353 . . . . . 6 (⊤ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316315mptru 1535 . . . . 5 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
31758, 300, 301divcan4i 11375 . . . . . . . . . . 11 ((𝐸 · 2) / 2) = 𝐸
318317oveq1i 7155 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = (𝐸 · (𝐵𝐴))
31958, 300mulcli 10636 . . . . . . . . . . 11 (𝐸 · 2) ∈ ℂ
320 div32 11306 . . . . . . . . . . 11 (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2)))
321319, 293, 147, 320mp3an 1452 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
322318, 321eqtr3i 2843 . . . . . . . . 9 (𝐸 · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
323322oveq1i 7155 . . . . . . . 8 ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2))) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
324 itgeq2 24305 . . . . . . . . . 10 (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥)
32566a1i 11 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
326324, 325mprg 3149 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥
32757a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328 cniccibl 24368 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
3291, 2, 233, 328mp3an 1452 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1
330329a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
331126adantl 482 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
33260a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333332, 327resubcld 11056 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝐸) ∈ ℝ)
334331, 333remulcld 10659 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) ∈ ℝ)
335261mptru 1535 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336 cniccibl 24368 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
3371, 2, 335, 336mp3an 1452 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1
338337a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
339327, 330, 334, 338itgadd 24352 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥))
340339mptru 1535 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
341 iccmbl 24094 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
3421, 2, 341mp2an 688 . . . . . . . . . . . 12 (𝐴[,]𝐵) ∈ dom vol
343 mblvol 24058 . . . . . . . . . . . . . . 15 ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344342, 343ax-mp 5 . . . . . . . . . . . . . 14 (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
3451, 2, 17ltleii 10751 . . . . . . . . . . . . . . 15 𝐴𝐵
346 ovolicc 24051 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴))
3471, 2, 345, 346mp3an 1452 . . . . . . . . . . . . . 14 (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴)
348344, 347eqtri 2841 . . . . . . . . . . . . 13 (vol‘(𝐴[,]𝐵)) = (𝐵𝐴)
349348, 12eqeltri 2906 . . . . . . . . . . . 12 (vol‘(𝐴[,]𝐵)) ∈ ℝ
350 itgconst 24346 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351342, 349, 58, 350mp3an 1452 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352348oveq2i 7156 . . . . . . . . . . 11 (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵𝐴))
353351, 352eqtri 2841 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵𝐴))
35461a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐹 ∈ ℂ)
35558a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐸 ∈ ℂ)
356354, 355subcld 10985 . . . . . . . . . . . . 13 (⊤ → (𝐹𝐸) ∈ ℂ)
357256mptru 1535 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358 cniccibl 24368 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
3591, 2, 357, 358mp3an 1452 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1
360359a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
361356, 331, 360itgmulc2 24361 . . . . . . . . . . . 12 (⊤ → ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
362361mptru 1535 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
363 itgeq2 24305 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)) → ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
364137recnd 10657 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℂ)
365364, 237, 238divrec2d 11408 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)))
366363, 365mprg 3149 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
3675adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368 cncfmptid 23447 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369230, 231, 368mp2an 688 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370 cniccibl 24368 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3711, 2, 369, 370mp3an 1452 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1
372371a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3731a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374 cncfmptc 23446 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375139, 230, 231, 374mp3an 1452 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376 cniccibl 24368 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
3771, 2, 375, 376mp3an 1452 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1
378377a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
379367, 372, 373, 378itgsub 24353 . . . . . . . . . . . . . . . . . . 19 (⊤ → ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥))
380379mptru 1535 . . . . . . . . . . . . . . . . . 18 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥)
3811a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴 ∈ ℝ)
3822a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐵 ∈ ℝ)
383345a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴𝐵)
384 1nn0 11901 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℕ0
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 1 ∈ ℕ0)
386381, 382, 383, 385itgpowd 39699 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387386mptru 1535 . . . . . . . . . . . . . . . . . . . . 21 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388 1p1e2 11750 . . . . . . . . . . . . . . . . . . . . . 22 (1 + 1) = 2
389388oveq2i 7156 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390387, 389eqtri 2841 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391 itgeq2 24305 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392235exp1d 13493 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393391, 392mprg 3149 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394388oveq2i 7156 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵↑(1 + 1)) = (𝐵↑2)
395388oveq2i 7156 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴↑(1 + 1)) = (𝐴↑2)
396394, 395oveq12i 7157 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397396oveq1i 7155 . . . . . . . . . . . . . . . . . . . 20 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398390, 393, 3973eqtr3i 2849 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399 itgconst 24346 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400342, 349, 139, 399mp3an 1452 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401348oveq2i 7156 . . . . . . . . . . . . . . . . . . . 20 (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵𝐴))
402400, 401eqtri 2841 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵𝐴))
403398, 402oveq12i 7157 . . . . . . . . . . . . . . . . . 18 (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
404380, 403eqtri 2841 . . . . . . . . . . . . . . . . 17 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
405404oveq2i 7156 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴))))
40614a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵 ∈ ℂ)
407139a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐴 ∈ ℂ)
408406, 407subcld 10985 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ∈ ℂ)
40918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵𝐴)
410406, 407, 409subne0d 10994 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ≠ 0)
411408, 410reccld 11397 . . . . . . . . . . . . . . . . . 18 (⊤ → (1 / (𝐵𝐴)) ∈ ℂ)
412411mptru 1535 . . . . . . . . . . . . . . . . 17 (1 / (𝐵𝐴)) ∈ ℂ
41314sqcli 13532 . . . . . . . . . . . . . . . . . . 19 (𝐵↑2) ∈ ℂ
414139sqcli 13532 . . . . . . . . . . . . . . . . . . 19 (𝐴↑2) ∈ ℂ
415413, 414subcli 10950 . . . . . . . . . . . . . . . . . 18 ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416415, 300, 301divcli 11370 . . . . . . . . . . . . . . . . 17 (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417139, 147mulcli 10636 . . . . . . . . . . . . . . . . 17 (𝐴 · (𝐵𝐴)) ∈ ℂ
418412, 416, 417subdii 11077 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
419405, 418eqtri 2841 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
420137adantl 482 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥𝐴) ∈ ℝ)
421367, 372, 373, 378iblsub 24349 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥𝐴)) ∈ 𝐿1)
422411, 420, 421itgmulc2 24361 . . . . . . . . . . . . . . . 16 (⊤ → ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
423422mptru 1535 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
424412, 417mulcomi 10637 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
425417, 147, 21divreci 11373 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
426139, 147, 21divcan4i 11375 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = 𝐴
427424, 425, 4263eqtr2i 2847 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = 𝐴
428427oveq2i 7156 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429419, 423, 4283eqtr3i 2849 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430366, 429eqtri 2841 . . . . . . . . . . . . 13 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
43114, 139subsqi 13563 . . . . . . . . . . . . . . . . 17 ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵𝐴))
432431oveq1i 7155 . . . . . . . . . . . . . . . 16 (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵𝐴)) / 2)
433432oveq2i 7156 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
434431, 415eqeltrri 2907 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) · (𝐵𝐴)) ∈ ℂ
435412, 434, 300, 301divassi 11384 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
436412, 434mulcomi 10637 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
437434, 147, 21divreci 11373 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
43814, 139addcli 10635 . . . . . . . . . . . . . . . . . 18 (𝐵 + 𝐴) ∈ ℂ
439438, 147, 21divcan4i 11375 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (𝐵 + 𝐴)
440436, 437, 4393eqtr2i 2847 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (𝐵 + 𝐴)
441440oveq1i 7155 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442433, 435, 4413eqtr2i 2847 . . . . . . . . . . . . . 14 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443442oveq1i 7155 . . . . . . . . . . . . 13 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444139, 300mulcli 10636 . . . . . . . . . . . . . . 15 (𝐴 · 2) ∈ ℂ
445 divsubdir 11322 . . . . . . . . . . . . . . 15 (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446438, 444, 293, 445mp3an 1452 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
44714, 139, 444addsubassi 10965 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448 subsub2 10902 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
44914, 444, 139, 448mp3an 1452 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450139times2i 11764 . . . . . . . . . . . . . . . . . . 19 (𝐴 · 2) = (𝐴 + 𝐴)
451450oveq1i 7155 . . . . . . . . . . . . . . . . . 18 ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452139, 139pncan3oi 10890 . . . . . . . . . . . . . . . . . 18 ((𝐴 + 𝐴) − 𝐴) = 𝐴
453451, 452eqtri 2841 . . . . . . . . . . . . . . . . 17 ((𝐴 · 2) − 𝐴) = 𝐴
454453oveq2i 7156 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵𝐴)
455447, 449, 4543eqtr2i 2847 . . . . . . . . . . . . . . 15 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵𝐴)
456455oveq1i 7155 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵𝐴) / 2)
457139, 300, 301divcan4i 11375 . . . . . . . . . . . . . . 15 ((𝐴 · 2) / 2) = 𝐴
458457oveq2i 7156 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459446, 456, 4583eqtr3ri 2850 . . . . . . . . . . . . 13 (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵𝐴) / 2)
460430, 443, 4593eqtri 2845 . . . . . . . . . . . 12 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ((𝐵𝐴) / 2)
461460oveq2i 7156 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐹𝐸) · ((𝐵𝐴) / 2))
462 itgeq2 24305 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) → ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
46361, 58subcli 10950 . . . . . . . . . . . . . 14 (𝐹𝐸) ∈ ℂ
464463a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐹𝐸) ∈ ℂ)
465464, 127mulcomd 10650 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
466462, 465mprg 3149 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥
467362, 461, 4663eqtr3ri 2850 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥 = ((𝐹𝐸) · ((𝐵𝐴) / 2))
468353, 467oveq12i 7157 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥) = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
469326, 340, 4683eqtri 2845 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
470147, 300, 301divcli 11370 . . . . . . . . 9 ((𝐵𝐴) / 2) ∈ ℂ
471319, 463, 470adddiri 10642 . . . . . . . 8 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
472323, 469, 4713eqtr4i 2851 . . . . . . 7 ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2))
473 addsub12 10887 . . . . . . . . . 10 ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸)))
47461, 319, 58, 473mp3an 1452 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸))
47558times2i 11764 . . . . . . . . . . . 12 (𝐸 · 2) = (𝐸 + 𝐸)
476475oveq1i 7155 . . . . . . . . . . 11 ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
47758, 58pncan3oi 10890 . . . . . . . . . . 11 ((𝐸 + 𝐸) − 𝐸) = 𝐸
478476, 477eqtri 2841 . . . . . . . . . 10 ((𝐸 · 2) − 𝐸) = 𝐸
479478oveq2i 7156 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480474, 479eqtr3i 2843 . . . . . . . 8 ((𝐸 · 2) + (𝐹𝐸)) = (𝐹 + 𝐸)
481480oveq1i 7155 . . . . . . 7 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
482472, 481eqtri 2841 . . . . . 6 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
4838, 300, 301divcan4i 11375 . . . . . . . . . . 11 ((𝐶 · 2) / 2) = 𝐶
484483oveq1i 7155 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = (𝐶 · (𝐵𝐴))
4858, 300mulcli 10636 . . . . . . . . . . 11 (𝐶 · 2) ∈ ℂ
486 div32 11306 . . . . . . . . . . 11 (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2)))
487485, 293, 147, 486mp3an 1452 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
488484, 487eqtr3i 2843 . . . . . . . . 9 (𝐶 · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
489488oveq1i 7155 . . . . . . . 8 ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2))) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
49031a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
491490itgeq2dv 24309 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥)
492491mptru 1535 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥
4937a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494 cniccibl 24368 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
4951, 2, 266, 494mp3an 1452 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1
496495a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
49725a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498497, 493resubcld 11056 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷𝐶) ∈ ℝ)
499331, 498remulcld 10659 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ)
500272mptru 1535 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501 cniccibl 24368 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
5021, 2, 500, 501mp3an 1452 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1
503502a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
504493, 496, 499, 503itgadd 24352 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥))
505504mptru 1535 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
506 itgconst 24346 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507342, 349, 8, 506mp3an 1452 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508348oveq2i 7156 . . . . . . . . . . 11 (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵𝐴))
509507, 508eqtri 2841 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵𝐴))
51026a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐷 ∈ ℂ)
5118a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐶 ∈ ℂ)
512510, 511subcld 10985 . . . . . . . . . . . . 13 (⊤ → (𝐷𝐶) ∈ ℂ)
513512, 331, 360itgmulc2 24361 . . . . . . . . . . . 12 (⊤ → ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
514513mptru 1535 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
515460oveq2i 7156 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐷𝐶) · ((𝐵𝐴) / 2))
516 itgeq2 24305 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) → ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
51726, 8subcli 10950 . . . . . . . . . . . . . 14 (𝐷𝐶) ∈ ℂ
518517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷𝐶) ∈ ℂ)
519518, 127mulcomd 10650 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
520516, 519mprg 3149 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥
521514, 515, 5203eqtr3ri 2850 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥 = ((𝐷𝐶) · ((𝐵𝐴) / 2))
522509, 521oveq12i 7157 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥) = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
523492, 505, 5223eqtri 2845 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
524485, 517, 470adddiri 10642 . . . . . . . 8 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
525489, 523, 5243eqtr4i 2851 . . . . . . 7 ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2))
526 addsub12 10887 . . . . . . . . . 10 ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶)))
52726, 485, 8, 526mp3an 1452 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶))
5288times2i 11764 . . . . . . . . . . . 12 (𝐶 · 2) = (𝐶 + 𝐶)
529528oveq1i 7155 . . . . . . . . . . 11 ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
5308, 8pncan3oi 10890 . . . . . . . . . . 11 ((𝐶 + 𝐶) − 𝐶) = 𝐶
531529, 530eqtri 2841 . . . . . . . . . 10 ((𝐶 · 2) − 𝐶) = 𝐶
532531oveq2i 7156 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533527, 532eqtr3i 2843 . . . . . . . 8 ((𝐶 · 2) + (𝐷𝐶)) = (𝐷 + 𝐶)
534533oveq1i 7155 . . . . . . 7 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
535525, 534eqtri 2841 . . . . . 6 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
536482, 535oveq12i 7157 . . . . 5 (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
537316, 536eqtri 2841 . . . 4 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
538299, 304, 5373eqtr4ri 2852 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
539289, 291, 5383eqtr2i 2847 . 2 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
540286, 539eqtri 2841 1 (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wa 396   = wceq 1528  wtru 1529  wcel 2105  wne 3013  wral 3135  cdif 3930  wss 3933  c0 4288  ifcif 4463  {csn 4557  cop 4563   class class class wbr 5057  {copab 5119  cmpt 5137   × cxp 5546  ccnv 5547  dom cdm 5548  cres 5550  cima 5551  Fun wfun 6342  wf 6344  cfv 6348  (class class class)co 7145  cc 10523  cr 10524  0cc0 10525  1c1 10526   + caddc 10528   · cmul 10530  +∞cpnf 10660  *cxr 10662   < clt 10663  cle 10664  cmin 10858   / cdiv 11285  2c2 11680  0cn0 11885  [,]cicc 12729  cexp 13417  TopOpenctopn 16683  fldccnfld 20473   Cn ccn 21760   ×t ctx 22096  cnccncf 23411  vol*covol 23990  volcvol 23991  𝐿1cibl 24145  citg 24146  areacarea 25460
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7450  ax-inf2 9092  ax-cc 9845  ax-cnex 10581  ax-resscn 10582  ax-1cn 10583  ax-icn 10584  ax-addcl 10585  ax-addrcl 10586  ax-mulcl 10587  ax-mulrcl 10588  ax-mulcom 10589  ax-addass 10590  ax-mulass 10591  ax-distr 10592  ax-i2m1 10593  ax-1ne0 10594  ax-1rid 10595  ax-rnegex 10596  ax-rrecex 10597  ax-cnre 10598  ax-pre-lttri 10599  ax-pre-lttrn 10600  ax-pre-ltadd 10601  ax-pre-mulgt0 10602  ax-pre-sup 10603  ax-addf 10604  ax-mulf 10605
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-fal 1541  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ne 3014  df-nel 3121  df-ral 3140  df-rex 3141  df-reu 3142  df-rmo 3143  df-rab 3144  df-v 3494  df-sbc 3770  df-csb 3881  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-pss 3951  df-symdif 4216  df-nul 4289  df-if 4464  df-pw 4537  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4831  df-int 4868  df-iun 4912  df-iin 4913  df-disj 5023  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-isom 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-of 7398  df-ofr 7399  df-om 7570  df-1st 7678  df-2nd 7679  df-supp 7820  df-wrecs 7936  df-recs 7997  df-rdg 8035  df-1o 8091  df-2o 8092  df-oadd 8095  df-omul 8096  df-er 8278  df-map 8397  df-pm 8398  df-ixp 8450  df-en 8498  df-dom 8499  df-sdom 8500  df-fin 8501  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-acn 9359  df-pnf 10665  df-mnf 10666  df-xr 10667  df-ltxr 10668  df-le 10669  df-sub 10860  df-neg 10861  df-div 11286  df-nn 11627  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12881  df-fzo 13022  df-fl 13150  df-mod 13226  df-seq 13358  df-exp 13418  df-hash 13679  df-cj 14446  df-re 14447  df-im 14448  df-sqrt 14582  df-abs 14583  df-limsup 14816  df-clim 14833  df-rlim 14834  df-sum 15031  df-struct 16473  df-ndx 16474  df-slot 16475  df-base 16477  df-sets 16478  df-ress 16479  df-plusg 16566  df-mulr 16567  df-starv 16568  df-sca 16569  df-vsca 16570  df-ip 16571  df-tset 16572  df-ple 16573  df-ds 16575  df-unif 16576  df-hom 16577  df-cco 16578  df-rest 16684  df-topn 16685  df-0g 16703  df-gsum 16704  df-topgen 16705  df-pt 16706  df-prds 16709  df-xrs 16763  df-qtop 16768  df-imas 16769  df-xps 16771  df-mre 16845  df-mrc 16846  df-acs 16848  df-mgm 17840  df-sgrp 17889  df-mnd 17900  df-submnd 17945  df-mulg 18163  df-cntz 18385  df-cmn 18837  df-psmet 20465  df-xmet 20466  df-met 20467  df-bl 20468  df-mopn 20469  df-fbas 20470  df-fg 20471  df-cnfld 20474  df-top 21430  df-topon 21447  df-topsp 21469  df-bases 21482  df-cld 21555  df-ntr 21556  df-cls 21557  df-nei 21634  df-lp 21672  df-perf 21673  df-cn 21763  df-cnp 21764  df-haus 21851  df-cmp 21923  df-tx 22098  df-hmeo 22291  df-fil 22382  df-fm 22474  df-flim 22475  df-flf 22476  df-xms 22857  df-ms 22858  df-tms 22859  df-cncf 23413  df-ovol 23992  df-vol 23993  df-mbf 24147  df-itg1 24148  df-itg2 24149  df-ibl 24150  df-itg 24151  df-0p 24198  df-limc 24391  df-dv 24392  df-area 25461
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator