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 41536
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 13346 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
41, 2, 3mp2an 690 . . . . . . . . 9 (𝐴[,]𝐵) ⊆ ℝ
54sseli 3940 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
65adantr 481 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7 areaquad.3 . . . . . . . . . . . . . . . 16 𝐶 ∈ ℝ
87recni 11169 . . . . . . . . . . . . . . 15 𝐶 ∈ ℂ
98a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10 resubcl 11465 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥𝐴) ∈ ℝ)
111, 10mpan2 689 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝑥𝐴) ∈ ℝ)
122, 1resubcli 11463 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ∈ ℝ
1312a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ∈ ℝ)
142recni 11169 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℂ
1514a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16 recn 11141 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17 areaquad.7 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 < 𝐵
181, 17gtneii 11267 . . . . . . . . . . . . . . . . . . . . 21 𝐵𝐴
1918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝐴 ∈ ℝ → 𝐵𝐴)
2015, 16, 19subne0d 11521 . . . . . . . . . . . . . . . . . . 19 (𝐴 ∈ ℝ → (𝐵𝐴) ≠ 0)
211, 20ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝐵𝐴) ≠ 0
2221a1i 11 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ → (𝐵𝐴) ≠ 0)
2311, 13, 22redivcld 11983 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
2423recnd 11183 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
25 areaquad.4 . . . . . . . . . . . . . . . . 17 𝐷 ∈ ℝ
2625recni 11169 . . . . . . . . . . . . . . . 16 𝐷 ∈ ℂ
2726a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
2824, 27mulcld 11175 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) ∈ ℂ)
2924, 9mulcld 11175 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐶) ∈ ℂ)
309, 28, 29addsub12d 11535 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
31 areaquad.10 . . . . . . . . . . . . . 14 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
3224, 27, 9subdid 11611 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
3332oveq2d 7373 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
3431, 33eqtrid 2788 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
35 1cnd 11150 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℂ)
3635, 24, 9subdird 11612 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
378mulid2i 11160 . . . . . . . . . . . . . . . 16 (1 · 𝐶) = 𝐶
3837oveq1i 7367 . . . . . . . . . . . . . . 15 ((1 · 𝐶) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))
3936, 38eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶)))
4039oveq2d 7373 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + (𝐶 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐶))))
4130, 34, 403eqtr4d 2786 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑈 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)))
42 1red 11156 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → 1 ∈ ℝ)
4342, 23resubcld 11583 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
4443recnd 11183 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (1 − ((𝑥𝐴) / (𝐵𝐴))) ∈ ℂ)
4544, 9mulcld 11175 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) ∈ ℂ)
4628, 45addcomd 11357 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐷) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)))
4744, 9mulcomd 11176 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
4824, 27mulcomd 11176 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐷) = (𝐷 · ((𝑥𝐴) / (𝐵𝐴))))
4947, 48oveq12d 7375 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐶) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
5041, 46, 493eqtrd 2780 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
5251, 43remulcld 11185 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5325a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
5453, 23remulcld 11185 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
5552, 54readdcld 11184 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
5650, 55eqeltrd 2838 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57 areaquad.5 . . . . . . . . . . . . . . . 16 𝐸 ∈ ℝ
5857recni 11169 . . . . . . . . . . . . . . 15 𝐸 ∈ ℂ
5958a1i 11 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60 areaquad.6 . . . . . . . . . . . . . . . . 17 𝐹 ∈ ℝ
6160recni 11169 . . . . . . . . . . . . . . . 16 𝐹 ∈ ℂ
6261a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
6324, 62mulcld 11175 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) ∈ ℂ)
6424, 59mulcld 11175 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐸) ∈ ℂ)
6559, 63, 64addsub12d 11535 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
66 areaquad.11 . . . . . . . . . . . . . 14 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
6724, 62, 59subdid 11611 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
6867oveq2d 7373 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
6966, 68eqtrid 2788 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7035, 24, 59subdird 11612 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7158mulid2i 11160 . . . . . . . . . . . . . . . 16 (1 · 𝐸) = 𝐸
7271oveq1i 7367 . . . . . . . . . . . . . . 15 ((1 · 𝐸) − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))
7370, 72eqtrdi 2792 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸)))
7473oveq2d 7373 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + (𝐸 − (((𝑥𝐴) / (𝐵𝐴)) · 𝐸))))
7565, 69, 743eqtr4d 2786 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑉 = ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)))
7644, 59mulcld 11175 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) ∈ ℂ)
7763, 76addcomd 11357 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((((𝑥𝐴) / (𝐵𝐴)) · 𝐹) + ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸)) = (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)))
7844, 59mulcomd 11176 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
7924, 62mulcomd 11176 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (((𝑥𝐴) / (𝐵𝐴)) · 𝐹) = (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
8078, 79oveq12d 7375 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (((1 − ((𝑥𝐴) / (𝐵𝐴))) · 𝐸) + (((𝑥𝐴) / (𝐵𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8175, 77, 803eqtrd 2780 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
8257a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
8382, 43remulcld 11185 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8460a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
8584, 23remulcld 11185 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝐹 · ((𝑥𝐴) / (𝐵𝐴))) ∈ ℝ)
8683, 85readdcld 11184 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))) ∈ ℝ)
8781, 86eqeltrd 2838 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88 iccssre 13346 . . . . . . . . . 10 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
8956, 87, 88syl2anc 584 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
905, 89syl 17 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
9190sselda 3944 . . . . . . 7 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
926, 91jca 512 . . . . . 6 ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
9392ssopab2i 5507 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94 areaquad.12 . . . . 5 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95 df-xp 5639 . . . . 5 (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
9693, 94, 953sstr4i 3987 . . . 4 𝑆 ⊆ (ℝ × ℝ)
97 iftrue 4492 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (𝑉𝑈))
98 nfv 1917 . . . . . . . . . . . . 13 𝑦 𝑥 ∈ (𝐴[,]𝐵)
99 nfopab2 5176 . . . . . . . . . . . . . . 15 𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
10094, 99nfcxfr 2905 . . . . . . . . . . . . . 14 𝑦𝑆
101 nfcv 2907 . . . . . . . . . . . . . 14 𝑦{𝑥}
102100, 101nfima 6021 . . . . . . . . . . . . 13 𝑦(𝑆 “ {𝑥})
103 nfcv 2907 . . . . . . . . . . . . 13 𝑦(𝑈[,]𝑉)
104 vex 3449 . . . . . . . . . . . . . . . 16 𝑥 ∈ V
105 vex 3449 . . . . . . . . . . . . . . . 16 𝑦 ∈ V
106104, 105elimasn 6041 . . . . . . . . . . . . . . 15 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
10794eleq2i 2829 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108 opabidw 5481 . . . . . . . . . . . . . . 15 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109106, 107, 1083bitri 296 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110109baib 536 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
11198, 102, 103, 110eqrd 3963 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112111fveq2d 6846 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
1135, 56syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
1145, 87syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115 iccmbl 24930 . . . . . . . . . . . . 13 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116113, 114, 115syl2anc 584 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117 mblvol 24894 . . . . . . . . . . . 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 11183 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℂ)
128127subidd 11500 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) = 0)
129 1red 11156 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
1302a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
1311a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
1321rexri 11213 . . . . . . . . . . . . . . . . . . . . 21 𝐴 ∈ ℝ*
1332rexri 11213 . . . . . . . . . . . . . . . . . . . . 21 𝐵 ∈ ℝ*
134 iccleub 13319 . . . . . . . . . . . . . . . . . . . . 21 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝑥𝐵)
135132, 133, 134mp3an12 1451 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥𝐵)
1365, 130, 131, 135lesub1dd 11771 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ≤ (𝐵𝐴))
1375, 1, 10sylancl 586 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℝ)
13812a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ)
1391recni 11169 . . . . . . . . . . . . . . . . . . . . . 22 𝐴 ∈ ℂ
140139subidi 11472 . . . . . . . . . . . . . . . . . . . . 21 (𝐴𝐴) = 0
141131, 130, 131ltsub1d 11764 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴𝐴) < (𝐵𝐴)))
14217, 141mpbii 232 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) < (𝐵𝐴))
143140, 142eqbrtrrid 5141 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵𝐴))
144 lediv1 12020 . . . . . . . . . . . . . . . . . . . 20 (((𝑥𝐴) ∈ ℝ ∧ (𝐵𝐴) ∈ ℝ ∧ ((𝐵𝐴) ∈ ℝ ∧ 0 < (𝐵𝐴))) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
145137, 138, 138, 143, 144syl112anc 1374 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) ≤ (𝐵𝐴) ↔ ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴))))
146136, 145mpbid 231 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ ((𝐵𝐴) / (𝐵𝐴)))
14712recni 11169 . . . . . . . . . . . . . . . . . . 19 (𝐵𝐴) ∈ ℂ
148147, 21dividi 11888 . . . . . . . . . . . . . . . . . 18 ((𝐵𝐴) / (𝐵𝐴)) = 1
149146, 148breqtrdi 5146 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) ≤ 1)
150126, 129, 126, 149lesub1dd 11771 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥𝐴) / (𝐵𝐴)) − ((𝑥𝐴) / (𝐵𝐴))) ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
151128, 150eqbrtrrd 5129 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥𝐴) / (𝐵𝐴))))
152 areaquad.8 . . . . . . . . . . . . . . . 16 𝐶𝐸
153152a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐶𝐸)
154123, 124, 125, 151, 153lemul1ad 12094 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) ≤ (𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))))
15525a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
15660a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157138, 143elrpd 12954 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℝ+)
158 iccgelb 13320 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝑥 ∈ (𝐴[,]𝐵)) → 𝐴𝑥)
159132, 133, 158mp3an12 1451 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴𝑥)
160131, 5, 131, 159lesub1dd 11771 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → (𝐴𝐴) ≤ (𝑥𝐴))
161140, 160eqbrtrrid 5141 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥𝐴))
162137, 157, 161divge0d 12997 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥𝐴) / (𝐵𝐴)))
163 areaquad.9 . . . . . . . . . . . . . . . 16 𝐷𝐹
164163a1i 11 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → 𝐷𝐹)
165155, 156, 126, 162, 164lemul1ad 12094 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥𝐴) / (𝐵𝐴))) ≤ (𝐹 · ((𝑥𝐴) / (𝐵𝐴))))
166119, 120, 121, 122, 154, 165le2addd 11774 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))) ≤ ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
1675, 50syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐷 · ((𝑥𝐴) / (𝐵𝐴)))))
1685, 81syl 17 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥𝐴) / (𝐵𝐴)))) + (𝐹 · ((𝑥𝐴) / (𝐵𝐴)))))
169166, 167, 1683brtr4d 5137 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → 𝑈𝑉)
170 ovolicc 24887 . . . . . . . . . . . 12 ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
171113, 114, 169, 170syl3anc 1371 . . . . . . . . . . 11 (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉𝑈))
172112, 118, 1713eqtrd 2780 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉𝑈))
17397, 172eqtr4d 2779 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174 iffalse 4495 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = 0)
175 nfv 1917 . . . . . . . . . . . . 13 𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176 nfcv 2907 . . . . . . . . . . . . 13 𝑦
177109simplbi 498 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178 noel 4290 . . . . . . . . . . . . . . 15 ¬ 𝑦 ∈ ∅
179178pm2.21i 119 . . . . . . . . . . . . . 14 (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180177, 179pm5.21ni 378 . . . . . . . . . . . . 13 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181175, 102, 176, 180eqrd 3963 . . . . . . . . . . . 12 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182181fveq2d 6846 . . . . . . . . . . 11 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183 0mbl 24903 . . . . . . . . . . . . 13 ∅ ∈ dom vol
184 mblvol 24894 . . . . . . . . . . . . 13 (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185183, 184ax-mp 5 . . . . . . . . . . . 12 (vol‘∅) = (vol*‘∅)
186 ovol0 24857 . . . . . . . . . . . 12 (vol*‘∅) = 0
187185, 186eqtri 2764 . . . . . . . . . . 11 (vol‘∅) = 0
188182, 187eqtrdi 2792 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189174, 188eqtr4d 2779 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190173, 189pm2.61i 182 . . . . . . . 8 if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191190eqcomi 2745 . . . . . . 7 (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0)
19287, 56resubcld 11583 . . . . . . . 8 (𝑥 ∈ ℝ → (𝑉𝑈) ∈ ℝ)
193 0re 11157 . . . . . . . 8 0 ∈ ℝ
194 ifcl 4531 . . . . . . . 8 (((𝑉𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
195192, 193, 194sylancl 586 . . . . . . 7 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) ∈ ℝ)
196191, 195eqeltrid 2842 . . . . . 6 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197 volf 24893 . . . . . . . 8 vol:dom vol⟶(0[,]+∞)
198 ffun 6671 . . . . . . . 8 (vol:dom vol⟶(0[,]+∞) → Fun vol)
199197, 198ax-mp 5 . . . . . . 7 Fun vol
200 iftrue 4492 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201111, 200eqtr4d 2779 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202 iffalse 4495 . . . . . . . . . 10 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203181, 202eqtr4d 2779 . . . . . . . . 9 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204201, 203pm2.61i 182 . . . . . . . 8 (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
20556, 87, 115syl2anc 584 . . . . . . . . 9 (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206183a1i 11 . . . . . . . . 9 (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207205, 206ifcld 4532 . . . . . . . 8 (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208204, 207eqeltrid 2842 . . . . . . 7 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209 fvimacnv 7003 . . . . . . 7 ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
210199, 208, 209sylancr 587 . . . . . 6 (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)))
211196, 210mpbid 231 . . . . 5 (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (vol “ ℝ))
212211rgen 3066 . . . 4 𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ)
2134a1i 11 . . . . . 6 (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214 rembl 24904 . . . . . . 7 ℝ ∈ dom vol
215214a1i 11 . . . . . 6 (0 ∈ ℝ → ℝ ∈ dom vol)
216114, 113resubcld 11583 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) → (𝑉𝑈) ∈ ℝ)
217172, 216eqeltrd 2838 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218217adantl 482 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219 eldifn 4087 . . . . . . . 8 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220219, 188syl 17 . . . . . . 7 (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221220adantl 482 . . . . . 6 ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222172mpteq2ia 5208 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈))
223 eqid 2736 . . . . . . . . . . 11 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
224223subcn 24229 . . . . . . . . . . . 12 − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
225224a1i 11 . . . . . . . . . . 11 (⊤ → − ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
22666mpteq2i 5210 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
227223addcn 24228 . . . . . . . . . . . . . 14 + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld))
228227a1i 11 . . . . . . . . . . . . 13 (⊤ → + ∈ (((TopOpen‘ℂfld) ×t (TopOpen‘ℂfld)) Cn (TopOpen‘ℂfld)))
229 ax-resscn 11108 . . . . . . . . . . . . . . . 16 ℝ ⊆ ℂ
2304, 229sstri 3953 . . . . . . . . . . . . . . 15 (𝐴[,]𝐵) ⊆ ℂ
231 ssid 3966 . . . . . . . . . . . . . . 15 ℂ ⊆ ℂ
232 cncfmptc 24275 . . . . . . . . . . . . . . 15 ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
23358, 230, 231, 232mp3an 1461 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234233a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235230sseli 3940 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236139a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237147a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ∈ ℂ)
23821a1i 11 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ (𝐴[,]𝐵) → (𝐵𝐴) ≠ 0)
239235, 236, 237, 238divsubdird 11970 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
240239adantl 482 . . . . . . . . . . . . . . . 16 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) = ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴))))
241240mpteq2dva 5205 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))))
242 resmpt 5991 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))))
243230, 242ax-mp 5 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴)))
244 eqid 2736 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴)))
245244divccncf 24269 . . . . . . . . . . . . . . . . . . . 20 (((𝐵𝐴) ∈ ℂ ∧ (𝐵𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ))
246147, 21, 245mp2an 690 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ)
247 rescncf 24260 . . . . . . . . . . . . . . . . . . 19 ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248230, 246, 247mp2 9 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249243, 248eqeltrri 2835 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250249a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251139, 147, 21divcli 11897 . . . . . . . . . . . . . . . . . 18 (𝐴 / (𝐵𝐴)) ∈ ℂ
252 cncfmptc 24275 . . . . . . . . . . . . . . . . . 18 (((𝐴 / (𝐵𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253251, 230, 231, 252mp3an 1461 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254253a1i 11 . . . . . . . . . . . . . . . 16 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255223, 225, 250, 254cncfmpt2f 24278 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵𝐴)) − (𝐴 / (𝐵𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256241, 255eqeltrd 2838 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257 cncfmptc 24275 . . . . . . . . . . . . . . . . 17 ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
25861, 230, 231, 257mp3an 1461 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259258a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260223, 225, 259, 234cncfmpt2f 24278 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261256, 260mulcncf 24810 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262223, 228, 234, 261cncfmpt2f 24278 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263226, 262eqeltrid 2842 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26431mpteq2i 5210 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
265 cncfmptc 24275 . . . . . . . . . . . . . . 15 ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
2668, 230, 231, 265mp3an 1461 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267266a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268 cncfmptc 24275 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
26926, 230, 231, 268mp3an 1461 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270269a1i 11 . . . . . . . . . . . . . . 15 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271223, 225, 270, 267cncfmpt2f 24278 . . . . . . . . . . . . . 14 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272256, 271mulcncf 24810 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273223, 228, 267, 272cncfmpt2f 24278 . . . . . . . . . . . 12 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274264, 273eqeltrid 2842 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275223, 225, 263, 274cncfmpt2f 24278 . . . . . . . . . 10 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276275mptru 1548 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277 cniccibl 25205 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1)
2781, 2, 276, 277mp3an 1461 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉𝑈)) ∈ 𝐿1
279222, 278eqeltri 2834 . . . . . . 7 (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
280279a1i 11 . . . . . 6 (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
281213, 215, 218, 221, 280iblss2 25170 . . . . 5 (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1)
282193, 281ax-mp 5 . . . 4 (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1
283 dmarea 26307 . . . 4 (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿1))
28496, 212, 282, 283mpbir3an 1341 . . 3 𝑆 ∈ dom area
285 areaval 26314 . . 3 (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286284, 285ax-mp 5 . 2 (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287 itgeq2 25142 . . . 4 (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
288191a1i 11 . . . 4 (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0))
289287, 288mprg 3070 . . 3 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
290 itgss2 25177 . . . 4 ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥)
2914, 290ax-mp 5 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉𝑈), 0) d𝑥
29261, 58addcli 11161 . . . . . 6 (𝐹 + 𝐸) ∈ ℂ
293 2cnne0 12363 . . . . . 6 (2 ∈ ℂ ∧ 2 ≠ 0)
294 div32 11833 . . . . . 6 (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2)))
295292, 293, 147, 294mp3an 1461 . . . . 5 (((𝐹 + 𝐸) / 2) · (𝐵𝐴)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
29626, 8addcli 11161 . . . . . 6 (𝐷 + 𝐶) ∈ ℂ
297 div32 11833 . . . . . 6 (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
298296, 293, 147, 297mp3an 1461 . . . . 5 (((𝐷 + 𝐶) / 2) · (𝐵𝐴)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
299295, 298oveq12i 7369 . . . 4 ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴))) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
300 2cn 12228 . . . . . 6 2 ∈ ℂ
301 2ne0 12257 . . . . . 6 2 ≠ 0
302292, 300, 301divcli 11897 . . . . 5 ((𝐹 + 𝐸) / 2) ∈ ℂ
303296, 300, 301divcli 11897 . . . . 5 ((𝐷 + 𝐶) / 2) ∈ ℂ
304302, 303, 147subdiri 11605 . . . 4 ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵𝐴)))
305114adantl 482 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306263mptru 1548 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307 cniccibl 25205 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
3081, 2, 306, 307mp3an 1461 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1
309308a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿1)
310113adantl 482 . . . . . . 7 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311274mptru 1548 . . . . . . . . 9 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312 cniccibl 25205 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
3131, 2, 311, 312mp3an 1461 . . . . . . . 8 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1
314313a1i 11 . . . . . . 7 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿1)
315305, 309, 310, 314itgsub 25190 . . . . . 6 (⊤ → ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316315mptru 1548 . . . . 5 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
31758, 300, 301divcan4i 11902 . . . . . . . . . . 11 ((𝐸 · 2) / 2) = 𝐸
318317oveq1i 7367 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = (𝐸 · (𝐵𝐴))
31958, 300mulcli 11162 . . . . . . . . . . 11 (𝐸 · 2) ∈ ℂ
320 div32 11833 . . . . . . . . . . 11 (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2)))
321319, 293, 147, 320mp3an 1461 . . . . . . . . . 10 (((𝐸 · 2) / 2) · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
322318, 321eqtr3i 2766 . . . . . . . . 9 (𝐸 · (𝐵𝐴)) = ((𝐸 · 2) · ((𝐵𝐴) / 2))
323322oveq1i 7367 . . . . . . . 8 ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2))) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
324 itgeq2 25142 . . . . . . . . . 10 (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥)
32566a1i 11 . . . . . . . . . 10 (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))))
326324, 325mprg 3070 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥
32757a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328 cniccibl 25205 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
3291, 2, 233, 328mp3an 1461 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1
330329a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿1)
331126adantl 482 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥𝐴) / (𝐵𝐴)) ∈ ℝ)
33260a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333332, 327resubcld 11583 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹𝐸) ∈ ℝ)
334331, 333remulcld 11185 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) ∈ ℝ)
335261mptru 1548 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336 cniccibl 25205 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
3371, 2, 335, 336mp3an 1461 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1
338337a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) ∈ 𝐿1)
339327, 330, 334, 338itgadd 25189 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥))
340339mptru 1548 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐸 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
341 iccmbl 24930 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
3421, 2, 341mp2an 690 . . . . . . . . . . . 12 (𝐴[,]𝐵) ∈ dom vol
343 mblvol 24894 . . . . . . . . . . . . . . 15 ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344342, 343ax-mp 5 . . . . . . . . . . . . . 14 (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
3451, 2, 17ltleii 11278 . . . . . . . . . . . . . . 15 𝐴𝐵
346 ovolicc 24887 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴))
3471, 2, 345, 346mp3an 1461 . . . . . . . . . . . . . 14 (vol*‘(𝐴[,]𝐵)) = (𝐵𝐴)
348344, 347eqtri 2764 . . . . . . . . . . . . 13 (vol‘(𝐴[,]𝐵)) = (𝐵𝐴)
349348, 12eqeltri 2834 . . . . . . . . . . . 12 (vol‘(𝐴[,]𝐵)) ∈ ℝ
350 itgconst 25183 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351342, 349, 58, 350mp3an 1461 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352348oveq2i 7368 . . . . . . . . . . 11 (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵𝐴))
353351, 352eqtri 2764 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵𝐴))
35461a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐹 ∈ ℂ)
35558a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐸 ∈ ℂ)
356354, 355subcld 11512 . . . . . . . . . . . . 13 (⊤ → (𝐹𝐸) ∈ ℂ)
357256mptru 1548 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358 cniccibl 25205 . . . . . . . . . . . . . . 15 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
3591, 2, 357, 358mp3an 1461 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1
360359a1i 11 . . . . . . . . . . . . 13 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥𝐴) / (𝐵𝐴))) ∈ 𝐿1)
361356, 331, 360itgmulc2 25198 . . . . . . . . . . . 12 (⊤ → ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
362361mptru 1548 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
363 itgeq2 25142 . . . . . . . . . . . . . . 15 (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)) → ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
364137recnd 11183 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥𝐴) ∈ ℂ)
365364, 237, 238divrec2d 11935 . . . . . . . . . . . . . . 15 (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥𝐴) / (𝐵𝐴)) = ((1 / (𝐵𝐴)) · (𝑥𝐴)))
366363, 365mprg 3070 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
3675adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368 cncfmptid 24276 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369230, 231, 368mp2an 690 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370 cniccibl 25205 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3711, 2, 369, 370mp3an 1461 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1
372371a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿1)
3731a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374 cncfmptc 24275 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375139, 230, 231, 374mp3an 1461 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376 cniccibl 25205 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
3771, 2, 375, 376mp3an 1461 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1
378377a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿1)
379367, 372, 373, 378itgsub 25190 . . . . . . . . . . . . . . . . . . 19 (⊤ → ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥))
380379mptru 1548 . . . . . . . . . . . . . . . . . 18 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥)
3811a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴 ∈ ℝ)
3822a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐵 ∈ ℝ)
383345a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 𝐴𝐵)
384 1nn0 12429 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℕ0
385384a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (⊤ → 1 ∈ ℕ0)
386381, 382, 383, 385itgpowd 25414 . . . . . . . . . . . . . . . . . . . . . 22 (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387386mptru 1548 . . . . . . . . . . . . . . . . . . . . 21 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388 1p1e2 12278 . . . . . . . . . . . . . . . . . . . . . 22 (1 + 1) = 2
389388oveq2i 7368 . . . . . . . . . . . . . . . . . . . . 21 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390387, 389eqtri 2764 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391 itgeq2 25142 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392235exp1d 14046 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393391, 392mprg 3070 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394388oveq2i 7368 . . . . . . . . . . . . . . . . . . . . . 22 (𝐵↑(1 + 1)) = (𝐵↑2)
395388oveq2i 7368 . . . . . . . . . . . . . . . . . . . . . 22 (𝐴↑(1 + 1)) = (𝐴↑2)
396394, 395oveq12i 7369 . . . . . . . . . . . . . . . . . . . . 21 ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397396oveq1i 7367 . . . . . . . . . . . . . . . . . . . 20 (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398390, 393, 3973eqtr3i 2772 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399 itgconst 25183 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400342, 349, 139, 399mp3an 1461 . . . . . . . . . . . . . . . . . . . 20 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401348oveq2i 7368 . . . . . . . . . . . . . . . . . . . 20 (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵𝐴))
402400, 401eqtri 2764 . . . . . . . . . . . . . . . . . . 19 ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵𝐴))
403398, 402oveq12i 7369 . . . . . . . . . . . . . . . . . 18 (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
404380, 403eqtri 2764 . . . . . . . . . . . . . . . . 17 ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))
405404oveq2i 7368 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴))))
40614a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵 ∈ ℂ)
407139a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐴 ∈ ℂ)
408406, 407subcld 11512 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ∈ ℂ)
40918a1i 11 . . . . . . . . . . . . . . . . . . . 20 (⊤ → 𝐵𝐴)
410406, 407, 409subne0d 11521 . . . . . . . . . . . . . . . . . . 19 (⊤ → (𝐵𝐴) ≠ 0)
411408, 410reccld 11924 . . . . . . . . . . . . . . . . . 18 (⊤ → (1 / (𝐵𝐴)) ∈ ℂ)
412411mptru 1548 . . . . . . . . . . . . . . . . 17 (1 / (𝐵𝐴)) ∈ ℂ
41314sqcli 14085 . . . . . . . . . . . . . . . . . . 19 (𝐵↑2) ∈ ℂ
414139sqcli 14085 . . . . . . . . . . . . . . . . . . 19 (𝐴↑2) ∈ ℂ
415413, 414subcli 11477 . . . . . . . . . . . . . . . . . 18 ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416415, 300, 301divcli 11897 . . . . . . . . . . . . . . . . 17 (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417139, 147mulcli 11162 . . . . . . . . . . . . . . . . 17 (𝐴 · (𝐵𝐴)) ∈ ℂ
418412, 416, 417subdii 11604 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
419405, 418eqtri 2764 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))))
420137adantl 482 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥𝐴) ∈ ℝ)
421367, 372, 373, 378iblsub 25186 . . . . . . . . . . . . . . . . 17 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥𝐴)) ∈ 𝐿1)
422411, 420, 421itgmulc2 25198 . . . . . . . . . . . . . . . 16 (⊤ → ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥)
423422mptru 1548 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · ∫(𝐴[,]𝐵)(𝑥𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥
424412, 417mulcomi 11163 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
425417, 147, 21divreci 11900 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = ((𝐴 · (𝐵𝐴)) · (1 / (𝐵𝐴)))
426139, 147, 21divcan4i 11902 . . . . . . . . . . . . . . . . 17 ((𝐴 · (𝐵𝐴)) / (𝐵𝐴)) = 𝐴
427424, 425, 4263eqtr2i 2770 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴))) = 𝐴
428427oveq2i 7368 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵𝐴)) · (𝐴 · (𝐵𝐴)))) = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429419, 423, 4283eqtr3i 2772 . . . . . . . . . . . . . 14 ∫(𝐴[,]𝐵)((1 / (𝐵𝐴)) · (𝑥𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430366, 429eqtri 2764 . . . . . . . . . . . . 13 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
43114, 139subsqi 14117 . . . . . . . . . . . . . . . . 17 ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵𝐴))
432431oveq1i 7367 . . . . . . . . . . . . . . . 16 (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵𝐴)) / 2)
433432oveq2i 7368 . . . . . . . . . . . . . . 15 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
434431, 415eqeltrri 2835 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) · (𝐵𝐴)) ∈ ℂ
435412, 434, 300, 301divassi 11911 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((1 / (𝐵𝐴)) · (((𝐵 + 𝐴) · (𝐵𝐴)) / 2))
436412, 434mulcomi 11163 . . . . . . . . . . . . . . . . 17 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
437434, 147, 21divreci 11900 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (((𝐵 + 𝐴) · (𝐵𝐴)) · (1 / (𝐵𝐴)))
43814, 139addcli 11161 . . . . . . . . . . . . . . . . . 18 (𝐵 + 𝐴) ∈ ℂ
439438, 147, 21divcan4i 11902 . . . . . . . . . . . . . . . . 17 (((𝐵 + 𝐴) · (𝐵𝐴)) / (𝐵𝐴)) = (𝐵 + 𝐴)
440436, 437, 4393eqtr2i 2770 . . . . . . . . . . . . . . . 16 ((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) = (𝐵 + 𝐴)
441440oveq1i 7367 . . . . . . . . . . . . . . 15 (((1 / (𝐵𝐴)) · ((𝐵 + 𝐴) · (𝐵𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442433, 435, 4413eqtr2i 2770 . . . . . . . . . . . . . 14 ((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443442oveq1i 7367 . . . . . . . . . . . . 13 (((1 / (𝐵𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444139, 300mulcli 11162 . . . . . . . . . . . . . . 15 (𝐴 · 2) ∈ ℂ
445 divsubdir 11849 . . . . . . . . . . . . . . 15 (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446438, 444, 293, 445mp3an 1461 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
44714, 139, 444addsubassi 11492 . . . . . . . . . . . . . . . 16 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448 subsub2 11429 . . . . . . . . . . . . . . . . 17 ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
44914, 444, 139, 448mp3an 1461 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450139times2i 12292 . . . . . . . . . . . . . . . . . . 19 (𝐴 · 2) = (𝐴 + 𝐴)
451450oveq1i 7367 . . . . . . . . . . . . . . . . . 18 ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452139, 139pncan3oi 11417 . . . . . . . . . . . . . . . . . 18 ((𝐴 + 𝐴) − 𝐴) = 𝐴
453451, 452eqtri 2764 . . . . . . . . . . . . . . . . 17 ((𝐴 · 2) − 𝐴) = 𝐴
454453oveq2i 7368 . . . . . . . . . . . . . . . 16 (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵𝐴)
455447, 449, 4543eqtr2i 2770 . . . . . . . . . . . . . . 15 ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵𝐴)
456455oveq1i 7367 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵𝐴) / 2)
457139, 300, 301divcan4i 11902 . . . . . . . . . . . . . . 15 ((𝐴 · 2) / 2) = 𝐴
458457oveq2i 7368 . . . . . . . . . . . . . 14 (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459446, 456, 4583eqtr3ri 2773 . . . . . . . . . . . . 13 (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵𝐴) / 2)
460430, 443, 4593eqtri 2768 . . . . . . . . . . . 12 ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥 = ((𝐵𝐴) / 2)
461460oveq2i 7368 . . . . . . . . . . 11 ((𝐹𝐸) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐹𝐸) · ((𝐵𝐴) / 2))
462 itgeq2 25142 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) → ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥)
46361, 58subcli 11477 . . . . . . . . . . . . . 14 (𝐹𝐸) ∈ ℂ
464463a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐹𝐸) ∈ ℂ)
465464, 127mulcomd 11176 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)))
466462, 465mprg 3070 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐹𝐸) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥
467362, 461, 4663eqtr3ri 2773 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥 = ((𝐹𝐸) · ((𝐵𝐴) / 2))
468353, 467oveq12i 7369 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐹𝐸)) d𝑥) = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
469326, 340, 4683eqtri 2768 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵𝐴)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
470147, 300, 301divcli 11897 . . . . . . . . 9 ((𝐵𝐴) / 2) ∈ ℂ
471319, 463, 470adddiri 11168 . . . . . . . 8 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = (((𝐸 · 2) · ((𝐵𝐴) / 2)) + ((𝐹𝐸) · ((𝐵𝐴) / 2)))
472323, 469, 4713eqtr4i 2774 . . . . . . 7 ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2))
473 addsub12 11414 . . . . . . . . . 10 ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸)))
47461, 319, 58, 473mp3an 1461 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹𝐸))
47558times2i 12292 . . . . . . . . . . . 12 (𝐸 · 2) = (𝐸 + 𝐸)
476475oveq1i 7367 . . . . . . . . . . 11 ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
47758, 58pncan3oi 11417 . . . . . . . . . . 11 ((𝐸 + 𝐸) − 𝐸) = 𝐸
478476, 477eqtri 2764 . . . . . . . . . 10 ((𝐸 · 2) − 𝐸) = 𝐸
479478oveq2i 7368 . . . . . . . . 9 (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480474, 479eqtr3i 2766 . . . . . . . 8 ((𝐸 · 2) + (𝐹𝐸)) = (𝐹 + 𝐸)
481480oveq1i 7367 . . . . . . 7 (((𝐸 · 2) + (𝐹𝐸)) · ((𝐵𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
482472, 481eqtri 2764 . . . . . 6 ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵𝐴) / 2))
4838, 300, 301divcan4i 11902 . . . . . . . . . . 11 ((𝐶 · 2) / 2) = 𝐶
484483oveq1i 7367 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = (𝐶 · (𝐵𝐴))
4858, 300mulcli 11162 . . . . . . . . . . 11 (𝐶 · 2) ∈ ℂ
486 div32 11833 . . . . . . . . . . 11 (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2)))
487485, 293, 147, 486mp3an 1461 . . . . . . . . . 10 (((𝐶 · 2) / 2) · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
488484, 487eqtr3i 2766 . . . . . . . . 9 (𝐶 · (𝐵𝐴)) = ((𝐶 · 2) · ((𝐵𝐴) / 2))
489488oveq1i 7367 . . . . . . . 8 ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2))) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
49031a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))))
491490itgeq2dv 25146 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥)
492491mptru 1548 . . . . . . . . 9 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥
4937a1i 11 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494 cniccibl 25205 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
4951, 2, 266, 494mp3an 1461 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1
496495a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿1)
49725a1i 11 . . . . . . . . . . . . 13 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498497, 493resubcld 11583 . . . . . . . . . . . 12 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷𝐶) ∈ ℝ)
499331, 498remulcld 11185 . . . . . . . . . . 11 ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) ∈ ℝ)
500272mptru 1548 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501 cniccibl 25205 . . . . . . . . . . . . 13 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
5021, 2, 500, 501mp3an 1461 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1
503502a1i 11 . . . . . . . . . . 11 (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) ∈ 𝐿1)
504493, 496, 499, 503itgadd 25189 . . . . . . . . . 10 (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥))
505504mptru 1548 . . . . . . . . 9 ∫(𝐴[,]𝐵)(𝐶 + (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
506 itgconst 25183 . . . . . . . . . . . 12 (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507342, 349, 8, 506mp3an 1461 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508348oveq2i 7368 . . . . . . . . . . 11 (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵𝐴))
509507, 508eqtri 2764 . . . . . . . . . 10 ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵𝐴))
51026a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐷 ∈ ℂ)
5118a1i 11 . . . . . . . . . . . . . 14 (⊤ → 𝐶 ∈ ℂ)
512510, 511subcld 11512 . . . . . . . . . . . . 13 (⊤ → (𝐷𝐶) ∈ ℂ)
513512, 331, 360itgmulc2 25198 . . . . . . . . . . . 12 (⊤ → ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥)
514513mptru 1548 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥
515460oveq2i 7368 . . . . . . . . . . 11 ((𝐷𝐶) · ∫(𝐴[,]𝐵)((𝑥𝐴) / (𝐵𝐴)) d𝑥) = ((𝐷𝐶) · ((𝐵𝐴) / 2))
516 itgeq2 25142 . . . . . . . . . . . 12 (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) → ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥)
51726, 8subcli 11477 . . . . . . . . . . . . . 14 (𝐷𝐶) ∈ ℂ
518517a1i 11 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴[,]𝐵) → (𝐷𝐶) ∈ ℂ)
519518, 127mulcomd 11176 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) = (((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)))
520516, 519mprg 3070 . . . . . . . . . . 11 ∫(𝐴[,]𝐵)((𝐷𝐶) · ((𝑥𝐴) / (𝐵𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥
521514, 515, 5203eqtr3ri 2773 . . . . . . . . . 10 ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥 = ((𝐷𝐶) · ((𝐵𝐴) / 2))
522509, 521oveq12i 7369 . . . . . . . . 9 (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥𝐴) / (𝐵𝐴)) · (𝐷𝐶)) d𝑥) = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
523492, 505, 5223eqtri 2768 . . . . . . . 8 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵𝐴)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
524485, 517, 470adddiri 11168 . . . . . . . 8 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = (((𝐶 · 2) · ((𝐵𝐴) / 2)) + ((𝐷𝐶) · ((𝐵𝐴) / 2)))
525489, 523, 5243eqtr4i 2774 . . . . . . 7 ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2))
526 addsub12 11414 . . . . . . . . . 10 ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶)))
52726, 485, 8, 526mp3an 1461 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷𝐶))
5288times2i 12292 . . . . . . . . . . . 12 (𝐶 · 2) = (𝐶 + 𝐶)
529528oveq1i 7367 . . . . . . . . . . 11 ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
5308, 8pncan3oi 11417 . . . . . . . . . . 11 ((𝐶 + 𝐶) − 𝐶) = 𝐶
531529, 530eqtri 2764 . . . . . . . . . 10 ((𝐶 · 2) − 𝐶) = 𝐶
532531oveq2i 7368 . . . . . . . . 9 (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533527, 532eqtr3i 2766 . . . . . . . 8 ((𝐶 · 2) + (𝐷𝐶)) = (𝐷 + 𝐶)
534533oveq1i 7367 . . . . . . 7 (((𝐶 · 2) + (𝐷𝐶)) · ((𝐵𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
535525, 534eqtri 2764 . . . . . 6 ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵𝐴) / 2))
536482, 535oveq12i 7369 . . . . 5 (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
537316, 536eqtri 2764 . . . 4 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵𝐴) / 2)))
538299, 304, 5373eqtr4ri 2775 . . 3 ∫(𝐴[,]𝐵)(𝑉𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
539289, 291, 5383eqtr2i 2770 . 2 ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
540286, 539eqtri 2764 1 (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wa 396   = wceq 1541  wtru 1542  wcel 2106  wne 2943  wral 3064  cdif 3907  wss 3910  c0 4282  ifcif 4486  {csn 4586  cop 4592   class class class wbr 5105  {copab 5167  cmpt 5188   × cxp 5631  ccnv 5632  dom cdm 5633  cres 5635  cima 5636  Fun wfun 6490  wf 6492  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  +∞cpnf 11186  *cxr 11188   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  2c2 12208  0cn0 12413  [,]cicc 13267  cexp 13967  TopOpenctopn 17303  fldccnfld 20796   Cn ccn 22575   ×t ctx 22911  cnccncf 24239  vol*covol 24826  volcvol 24827  𝐿1cibl 24981  citg 24982  areacarea 26305
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cc 10371  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-symdif 4202  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-disj 5071  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-ofr 7618  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-oadd 8416  df-omul 8417  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-acn 9878  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-fbas 20793  df-fg 20794  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-perf 22488  df-cn 22578  df-cnp 22579  df-haus 22666  df-cmp 22738  df-tx 22913  df-hmeo 23106  df-fil 23197  df-fm 23289  df-flim 23290  df-flf 23291  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-ovol 24828  df-vol 24829  df-mbf 24983  df-itg1 24984  df-itg2 24985  df-ibl 24986  df-itg 24987  df-0p 25034  df-limc 25230  df-dv 25231  df-area 26306
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator