areaquad - Mathbox for Jon Pennant

	Mathbox for Jon Pennant		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > areaquad		Structured version Visualization version GIF version

Theorem areaquad 40963

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**
Step	Hyp	Ref	Expression
1		areaquad.1	. . . . . . . . . 10 ⊢ 𝐴 ∈ ℝ
2		areaquad.2	. . . . . . . . . 10 ⊢ 𝐵 ∈ ℝ
3		iccssre 13090	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
4	1, 2, 3	mp2an 688	. . . . . . . . 9 ⊢ (𝐴[,]𝐵) ⊆ ℝ
5	4	sseli 3913	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
6	5	adantr 480	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7		areaquad.3	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ∈ ℝ
8	7	recni 10920	. . . . . . . . . . . . . . 15 ⊢ 𝐶 ∈ ℂ
9	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10		resubcl 11215	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 − 𝐴) ∈ ℝ)
11	1, 10	mpan2 687	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝑥 − 𝐴) ∈ ℝ)
12	2, 1	resubcli 11213	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ∈ ℝ
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ∈ ℝ)
14	2	recni 10920	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℂ
15	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16		recn 10892	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17		areaquad.7	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 < 𝐵
18	1, 17	gtneii 11017	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ≠ 𝐴
19	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ≠ 𝐴)
20	15, 16, 19	subne0d 11271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
21	1, 20	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ≠ 0
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
23	11, 13, 22	redivcld 11733	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
24	23	recnd 10934	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
25		areaquad.4	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 ∈ ℝ
26	25	recni 10920	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ∈ ℂ
27	26	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
28	24, 27	mulcld 10926	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) ∈ ℂ)
29	24, 9	mulcld 10926	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶) ∈ ℂ)
30	9, 28, 29	addsub12d 11285	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
31		areaquad.10	. . . . . . . . . . . . . 14 ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
32	24, 27, 9	subdid 11361	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
33	32	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
34	31, 33	syl5eq 2791	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
35		1cnd 10901	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℂ)
36	35, 24, 9	subdird 11362	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
37	8	mulid2i 10911	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐶) = 𝐶
38	37	oveq1i 7265	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))
39	36, 38	eqtrdi 2795	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
40	39	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
41	30, 34, 40	3eqtr4d 2788	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)))
42		1red 10907	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℝ)
43	42, 23	resubcld 11333	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
44	43	recnd 10934	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℂ)
45	44, 9	mulcld 10926	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) ∈ ℂ)
46	28, 45	addcomd 11107	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)))
47	44, 9	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
48	24, 27	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) = (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
49	47, 48	oveq12d 7273	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
50	41, 46, 49	3eqtrd 2782	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
51	7	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
52	51, 43	remulcld 10936	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
53	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
54	53, 23	remulcld 10936	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
55	52, 54	readdcld 10935	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
56	50, 55	eqeltrd 2839	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57		areaquad.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 ∈ ℝ
58	57	recni 10920	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ∈ ℂ
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60		areaquad.6	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 ∈ ℝ
61	60	recni 10920	. . . . . . . . . . . . . . . 16 ⊢ 𝐹 ∈ ℂ
62	61	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
63	24, 62	mulcld 10926	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) ∈ ℂ)
64	24, 59	mulcld 10926	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸) ∈ ℂ)
65	59, 63, 64	addsub12d 11285	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
66		areaquad.11	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
67	24, 62, 59	subdid 11361	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
68	67	oveq2d 7271	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
69	66, 68	syl5eq 2791	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
70	35, 24, 59	subdird 11362	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
71	58	mulid2i 10911	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐸) = 𝐸
72	71	oveq1i 7265	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))
73	70, 72	eqtrdi 2795	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
74	73	oveq2d 7271	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
75	65, 69, 74	3eqtr4d 2788	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)))
76	44, 59	mulcld 10926	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) ∈ ℂ)
77	63, 76	addcomd 11107	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)))
78	44, 59	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
79	24, 62	mulcomd 10927	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) = (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
80	78, 79	oveq12d 7273	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
81	75, 77, 80	3eqtrd 2782	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
82	57	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
83	82, 43	remulcld 10936	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
84	60	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
85	84, 23	remulcld 10936	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
86	83, 85	readdcld 10935	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
87	81, 86	eqeltrd 2839	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88		iccssre 13090	. . . . . . . . . 10 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
89	56, 87, 88	syl2anc 583	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
90	5, 89	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
91	90	sselda 3917	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
92	6, 91	jca 511	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
93	92	ssopab2i 5456	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94		areaquad.12	. . . . 5 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95		df-xp 5586	. . . . 5 ⊢ (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
96	93, 94, 95	3sstr4i 3960	. . . 4 ⊢ 𝑆 ⊆ (ℝ × ℝ)
97		iftrue 4462	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (𝑉 − 𝑈))
98		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑥 ∈ (𝐴[,]𝐵)
99		nfopab2 5141	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
100	94, 99	nfcxfr 2904	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝑆
101		nfcv 2906	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦{𝑥}
102	100, 101	nfima 5966	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑆 “ {𝑥})
103		nfcv 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑈[,]𝑉)
104		vex 3426	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
105		vex 3426	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
106	104, 105	elimasn 5986	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
107	94	eleq2i 2830	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108		opabidw 5431	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109	106, 107, 108	3bitri 296	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110	109	baib 535	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
111	98, 102, 103, 110	eqrd 3936	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112	111	fveq2d 6760	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
113	5, 56	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
114	5, 87	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115		iccmbl 24635	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116	113, 114, 115	syl2anc 583	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117		mblvol 24599	. . . . . . . . . . . 12 ⊢ ((𝑈[,]𝑉) ∈ dom vol → (vol‘(𝑈[,]𝑉)) = (vol*‘(𝑈[,]𝑉)))
118	116, 117	syl 17	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑈[,]𝑉)) = (vol*‘(𝑈[,]𝑉)))
119	5, 52	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
120	5, 54	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
121	5, 83	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
122	5, 85	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
123	7	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐶 ∈ ℝ)
124	57	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐸 ∈ ℝ)
125	5, 43	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
126	5, 23	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
127	126	recnd 10934	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
128	127	subidd 11250	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = 0)
129		1red 10907	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
130	2	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
131	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
132	1	rexri 10964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐴 ∈ ℝ^*
133	2	rexri 10964	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℝ^*
134		iccleub 13063	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
135	132, 133, 134	mp3an12 1449	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ≤ 𝐵)
136	5, 130, 131, 135	lesub1dd 11521	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ≤ (𝐵 − 𝐴))
137	5, 1, 10	sylancl 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℝ)
138	12	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ)
139	1	recni 10920	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 ∈ ℂ
140	139	subidi 11222	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 − 𝐴) = 0
141	131, 130, 131	ltsub1d 11514	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐴) < (𝐵 − 𝐴)))
142	17, 141	mpbii 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) < (𝐵 − 𝐴))
143	140, 142	eqbrtrrid 5106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵 − 𝐴))
144		lediv1 11770	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 − 𝐴) ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ ∧ ((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴))) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
145	137, 138, 138, 143, 144	syl112anc 1372	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
146	136, 145	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴)))
147	12	recni 10920	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 − 𝐴) ∈ ℂ
148	147, 21	dividi 11638	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 − 𝐴) / (𝐵 − 𝐴)) = 1
149	146, 148	breqtrdi 5111	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ 1)
150	126, 129, 126, 149	lesub1dd 11521	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
151	128, 150	eqbrtrrd 5094	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
152		areaquad.8	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ≤ 𝐸
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐶 ≤ 𝐸)
154	123, 124, 125, 151, 153	lemul1ad 11844	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
155	25	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
156	60	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157	138, 143	elrpd 12698	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ⁺)
158		iccgelb 13064	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥)
159	132, 133, 158	mp3an12 1449	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑥)
160	131, 5, 131, 159	lesub1dd 11521	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) ≤ (𝑥 − 𝐴))
161	140, 160	eqbrtrrid 5106	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥 − 𝐴))
162	137, 157, 161	divge0d 12741	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥 − 𝐴) / (𝐵 − 𝐴)))
163		areaquad.9	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ≤ 𝐹
164	163	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ≤ 𝐹)
165	155, 156, 126, 162, 164	lemul1ad 11844	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
166	119, 120, 121, 122, 154, 165	le2addd 11524	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
167	5, 50	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
168	5, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
169	166, 167, 168	3brtr4d 5102	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ≤ 𝑉)
170		ovolicc 24592	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈 ≤ 𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
171	113, 114, 169, 170	syl3anc 1369	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
172	112, 118, 171	3eqtrd 2782	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉 − 𝑈))
173	97, 172	eqtr4d 2781	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174		iffalse 4465	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = 0)
175		nfv 1918	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176		nfcv 2906	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∅
177	109	simplbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178		noel 4261	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑦 ∈ ∅
179	178	pm2.21i 119	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180	177, 179	pm5.21ni 378	. . . . . . . . . . . . 13 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181	175, 102, 176, 180	eqrd 3936	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182	181	fveq2d 6760	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183		0mbl 24608	. . . . . . . . . . . . 13 ⊢ ∅ ∈ dom vol
184		mblvol 24599	. . . . . . . . . . . . 13 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185	183, 184	ax-mp 5	. . . . . . . . . . . 12 ⊢ (vol‘∅) = (vol*‘∅)
186		ovol0 24562	. . . . . . . . . . . 12 ⊢ (vol*‘∅) = 0
187	185, 186	eqtri 2766	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
188	182, 187	eqtrdi 2795	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189	174, 188	eqtr4d 2781	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190	173, 189	pm2.61i 182	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191	190	eqcomi 2747	. . . . . . 7 ⊢ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0)
192	87, 56	resubcld 11333	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → (𝑉 − 𝑈) ∈ ℝ)
193		0re 10908	. . . . . . . 8 ⊢ 0 ∈ ℝ
194		ifcl 4501	. . . . . . . 8 ⊢ (((𝑉 − 𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
195	192, 193, 194	sylancl 585	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
196	191, 195	eqeltrid 2843	. . . . . 6 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197		volf 24598	. . . . . . . 8 ⊢ vol:dom vol⟶(0[,]+∞)
198		ffun 6587	. . . . . . . 8 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
199	197, 198	ax-mp 5	. . . . . . 7 ⊢ Fun vol
200		iftrue 4462	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201	111, 200	eqtr4d 2781	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202		iffalse 4465	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203	181, 202	eqtr4d 2781	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204	201, 203	pm2.61i 182	. . . . . . . 8 ⊢ (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
205	56, 87, 115	syl2anc 583	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206	183	a1i 11	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207	205, 206	ifcld 4502	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208	204, 207	eqeltrid 2843	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209		fvimacnv 6912	. . . . . . 7 ⊢ ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
210	199, 208, 209	sylancr 586	. . . . . 6 ⊢ (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
211	196, 210	mpbid 231	. . . . 5 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ))
212	211	rgen 3073	. . . 4 ⊢ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)
213	4	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214		rembl 24609	. . . . . . 7 ⊢ ℝ ∈ dom vol
215	214	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → ℝ ∈ dom vol)
216	114, 113	resubcld 11333	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑉 − 𝑈) ∈ ℝ)
217	172, 216	eqeltrd 2839	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218	217	adantl 481	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219		eldifn 4058	. . . . . . . 8 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220	219, 188	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221	220	adantl 481	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222	172	mpteq2ia 5173	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈))
223		eqid 2738	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
224	223	subcn 23935	. . . . . . . . . . . 12 ⊢ − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
225	224	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → − ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
226	66	mpteq2i 5175	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
227	223	addcn 23934	. . . . . . . . . . . . . 14 ⊢ + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld))
228	227	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → + ∈ (((TopOpen‘ℂ_fld) ×_t (TopOpen‘ℂ_fld)) Cn (TopOpen‘ℂ_fld)))
229		ax-resscn 10859	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
230	4, 229	sstri 3926	. . . . . . . . . . . . . . 15 ⊢ (𝐴[,]𝐵) ⊆ ℂ
231		ssid 3939	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
232		cncfmptc 23981	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
233	58, 230, 231, 232	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234	233	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235	230	sseli 3913	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236	139	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237	147	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℂ)
238	21	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ≠ 0)
239	235, 236, 237, 238	divsubdird 11720	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
240	239	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
241	240	mpteq2dva 5170	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))))
242		resmpt 5934	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))))
243	230, 242	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴)))
244		eqid 2738	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴)))
245	244	divccncf 23975	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ))
246	147, 21, 245	mp2an 688	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ)
247		rescncf 23966	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248	230, 246, 247	mp2 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249	243, 248	eqeltrri 2836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250	249	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251	139, 147, 21	divcli 11647	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (𝐵 − 𝐴)) ∈ ℂ
252		cncfmptc 23981	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 / (𝐵 − 𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253	251, 230, 231, 252	mp3an 1459	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254	253	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255	223, 225, 250, 254	cncfmpt2f 23984	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256	241, 255	eqeltrd 2839	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257		cncfmptc 23981	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
258	61, 230, 231, 257	mp3an 1459	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259	258	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260	223, 225, 259, 234	cncfmpt2f 23984	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹 − 𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261	256, 260	mulcncf 24515	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262	223, 228, 234, 261	cncfmpt2f 23984	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263	226, 262	eqeltrid 2843	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
264	31	mpteq2i 5175	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
265		cncfmptc 23981	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
266	8, 230, 231, 265	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267	266	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268		cncfmptc 23981	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
269	26, 230, 231, 268	mp3an 1459	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270	269	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271	223, 225, 270, 267	cncfmpt2f 23984	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷 − 𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272	256, 271	mulcncf 24515	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273	223, 228, 267, 272	cncfmpt2f 23984	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274	264, 273	eqeltrid 2843	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275	223, 225, 263, 274	cncfmpt2f 23984	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276	275	mptru 1546	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277		cniccibl 24910	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹)
278	1, 2, 276, 277	mp3an 1459	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹
279	222, 278	eqeltri 2835	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
280	279	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
281	213, 215, 218, 221, 280	iblss2 24875	. . . . 5 ⊢ (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
282	193, 281	ax-mp 5	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
283		dmarea 26012	. . . 4 ⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹))
284	96, 212, 282, 283	mpbir3an 1339	. . 3 ⊢ 𝑆 ∈ dom area
285		areaval 26019	. . 3 ⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286	284, 285	ax-mp 5	. 2 ⊢ (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287		itgeq2 24847	. . . 4 ⊢ (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
288	191	a1i 11	. . . 4 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0))
289	287, 288	mprg 3077	. . 3 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
290		itgss2 24882	. . . 4 ⊢ ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
291	4, 290	ax-mp 5	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
292	61, 58	addcli 10912	. . . . . 6 ⊢ (𝐹 + 𝐸) ∈ ℂ
293		2cnne0 12113	. . . . . 6 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
294		div32 11583	. . . . . 6 ⊢ (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)))
295	292, 293, 147, 294	mp3an 1459	. . . . 5 ⊢ (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
296	26, 8	addcli 10912	. . . . . 6 ⊢ (𝐷 + 𝐶) ∈ ℂ
297		div32 11583	. . . . . 6 ⊢ (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
298	296, 293, 147, 297	mp3an 1459	. . . . 5 ⊢ (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
299	295, 298	oveq12i 7267	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴))) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
300		2cn 11978	. . . . . 6 ⊢ 2 ∈ ℂ
301		2ne0 12007	. . . . . 6 ⊢ 2 ≠ 0
302	292, 300, 301	divcli 11647	. . . . 5 ⊢ ((𝐹 + 𝐸) / 2) ∈ ℂ
303	296, 300, 301	divcli 11647	. . . . 5 ⊢ ((𝐷 + 𝐶) / 2) ∈ ℂ
304	302, 303, 147	subdiri 11355	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)))
305	114	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306	263	mptru 1546	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307		cniccibl 24910	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
308	1, 2, 306, 307	mp3an 1459	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹
309	308	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
310	113	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311	274	mptru 1546	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312		cniccibl 24910	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
313	1, 2, 311, 312	mp3an 1459	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹
314	313	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
315	305, 309, 310, 314	itgsub 24895	. . . . . 6 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316	315	mptru 1546	. . . . 5 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
317	58, 300, 301	divcan4i 11652	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) / 2) = 𝐸
318	317	oveq1i 7265	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = (𝐸 · (𝐵 − 𝐴))
319	58, 300	mulcli 10913	. . . . . . . . . . 11 ⊢ (𝐸 · 2) ∈ ℂ
320		div32 11583	. . . . . . . . . . 11 ⊢ (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2)))
321	319, 293, 147, 320	mp3an 1459	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
322	318, 321	eqtr3i 2768	. . . . . . . . 9 ⊢ (𝐸 · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
323	322	oveq1i 7265	. . . . . . . 8 ⊢ ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
324		itgeq2 24847	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥)
325	66	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
326	324, 325	mprg 3077	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥
327	57	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328		cniccibl 24910	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
329	1, 2, 233, 328	mp3an 1459	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹
330	329	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
331	126	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
332	60	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333	332, 327	resubcld 11333	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹 − 𝐸) ∈ ℝ)
334	331, 333	remulcld 10936	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) ∈ ℝ)
335	261	mptru 1546	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336		cniccibl 24910	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
337	1, 2, 335, 336	mp3an 1459	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹
338	337	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
339	327, 330, 334, 338	itgadd 24894	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥))
340	339	mptru 1546	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
341		iccmbl 24635	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
342	1, 2, 341	mp2an 688	. . . . . . . . . . . 12 ⊢ (𝐴[,]𝐵) ∈ dom vol
343		mblvol 24599	. . . . . . . . . . . . . . 15 ⊢ ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344	342, 343	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
345	1, 2, 17	ltleii 11028	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ≤ 𝐵
346		ovolicc 24592	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
347	1, 2, 345, 346	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
348	344, 347	eqtri 2766	. . . . . . . . . . . . 13 ⊢ (vol‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
349	348, 12	eqeltri 2835	. . . . . . . . . . . 12 ⊢ (vol‘(𝐴[,]𝐵)) ∈ ℝ
350		itgconst 24888	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351	342, 349, 58, 350	mp3an 1459	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352	348	oveq2i 7266	. . . . . . . . . . 11 ⊢ (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵 − 𝐴))
353	351, 352	eqtri 2766	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵 − 𝐴))
354	61	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐹 ∈ ℂ)
355	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐸 ∈ ℂ)
356	354, 355	subcld 11262	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐹 − 𝐸) ∈ ℂ)
357	256	mptru 1546	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358		cniccibl 24910	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
359	1, 2, 357, 358	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹
360	359	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
361	356, 331, 360	itgmulc2 24903	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
362	361	mptru 1546	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
363		itgeq2 24847	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) → ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
364	137	recnd 10934	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℂ)
365	364, 237, 238	divrec2d 11685	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)))
366	363, 365	mprg 3077	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
367	5	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368		cncfmptid 23982	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369	230, 231, 368	mp2an 688	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370		cniccibl 24910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
371	1, 2, 369, 370	mp3an 1459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹
372	371	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
373	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374		cncfmptc 23981	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375	139, 230, 231, 374	mp3an 1459	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376		cniccibl 24910	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
377	1, 2, 375, 376	mp3an 1459	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹
378	377	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
379	367, 372, 373, 378	itgsub 24895	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥))
380	379	mptru 1546	. . . . . . . . . . . . . . . . . 18 ⊢ ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥)
381	1	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐴 ∈ ℝ)
382	2	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐵 ∈ ℝ)
383	345	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐴 ≤ 𝐵)
384		1nn0 12179	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
385	384	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 1 ∈ ℕ₀)
386	381, 382, 383, 385	itgpowd 25119	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387	386	mptru 1546	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388		1p1e2 12028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
389	388	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390	387, 389	eqtri 2766	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391		itgeq2 24847	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392	235	exp1d 13787	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393	391, 392	mprg 3077	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394	388	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵↑(1 + 1)) = (𝐵↑2)
395	388	oveq2i 7266	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴↑(1 + 1)) = (𝐴↑2)
396	394, 395	oveq12i 7267	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397	396	oveq1i 7265	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398	390, 393, 397	3eqtr3i 2774	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399		itgconst 24888	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400	342, 349, 139, 399	mp3an 1459	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401	348	oveq2i 7266	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵 − 𝐴))
402	400, 401	eqtri 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵 − 𝐴))
403	398, 402	oveq12i 7267	. . . . . . . . . . . . . . . . . 18 ⊢ (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
404	380, 403	eqtri 2766	. . . . . . . . . . . . . . . . 17 ⊢ ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
405	404	oveq2i 7266	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴))))
406	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ∈ ℂ)
407	139	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐴 ∈ ℂ)
408	406, 407	subcld 11262	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ∈ ℂ)
409	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ≠ 𝐴)
410	406, 407, 409	subne0d 11271	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ≠ 0)
411	408, 410	reccld 11674	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (1 / (𝐵 − 𝐴)) ∈ ℂ)
412	411	mptru 1546	. . . . . . . . . . . . . . . . 17 ⊢ (1 / (𝐵 − 𝐴)) ∈ ℂ
413	14	sqcli 13826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵↑2) ∈ ℂ
414	139	sqcli 13826	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴↑2) ∈ ℂ
415	413, 414	subcli 11227	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416	415, 300, 301	divcli 11647	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417	139, 147	mulcli 10913	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 · (𝐵 − 𝐴)) ∈ ℂ
418	412, 416, 417	subdii 11354	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
419	405, 418	eqtri 2766	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
420	137	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 − 𝐴) ∈ ℝ)
421	367, 372, 373, 378	iblsub 24891	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 − 𝐴)) ∈ 𝐿¹)
422	411, 420, 421	itgmulc2 24903	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
423	422	mptru 1546	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
424	412, 417	mulcomi 10914	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
425	417, 147, 21	divreci 11650	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
426	139, 147, 21	divcan4i 11652	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = 𝐴
427	424, 425, 426	3eqtr2i 2772	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = 𝐴
428	427	oveq2i 7266	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429	419, 423, 428	3eqtr3i 2774	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430	366, 429	eqtri 2766	. . . . . . . . . . . . 13 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
431	14, 139	subsqi 13857	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵 − 𝐴))
432	431	oveq1i 7265	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2)
433	432	oveq2i 7266	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
434	431, 415	eqeltrri 2836	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) · (𝐵 − 𝐴)) ∈ ℂ
435	412, 434, 300, 301	divassi 11661	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
436	412, 434	mulcomi 10914	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
437	434, 147, 21	divreci 11650	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
438	14, 139	addcli 10912	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 + 𝐴) ∈ ℂ
439	438, 147, 21	divcan4i 11652	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (𝐵 + 𝐴)
440	436, 437, 439	3eqtr2i 2772	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (𝐵 + 𝐴)
441	440	oveq1i 7265	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442	433, 435, 441	3eqtr2i 2772	. . . . . . . . . . . . . 14 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443	442	oveq1i 7265	. . . . . . . . . . . . 13 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444	139, 300	mulcli 10913	. . . . . . . . . . . . . . 15 ⊢ (𝐴 · 2) ∈ ℂ
445		divsubdir 11599	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446	438, 444, 293, 445	mp3an 1459	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
447	14, 139, 444	addsubassi 11242	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448		subsub2 11179	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
449	14, 444, 139, 448	mp3an 1459	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450	139	times2i 12042	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
451	450	oveq1i 7265	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452	139, 139	pncan3oi 11167	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 + 𝐴) − 𝐴) = 𝐴
453	451, 452	eqtri 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · 2) − 𝐴) = 𝐴
454	453	oveq2i 7266	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 − 𝐴)
455	447, 449, 454	3eqtr2i 2772	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 − 𝐴)
456	455	oveq1i 7265	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵 − 𝐴) / 2)
457	139, 300, 301	divcan4i 11652	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 · 2) / 2) = 𝐴
458	457	oveq2i 7266	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459	446, 456, 458	3eqtr3ri 2775	. . . . . . . . . . . . 13 ⊢ (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵 − 𝐴) / 2)
460	430, 443, 459	3eqtri 2770	. . . . . . . . . . . 12 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ((𝐵 − 𝐴) / 2)
461	460	oveq2i 7266	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
462		itgeq2 24847	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) → ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
463	61, 58	subcli 11227	. . . . . . . . . . . . . 14 ⊢ (𝐹 − 𝐸) ∈ ℂ
464	463	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐹 − 𝐸) ∈ ℂ)
465	464, 127	mulcomd 10927	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
466	462, 465	mprg 3077	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥
467	362, 461, 466	3eqtr3ri 2775	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥 = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
468	353, 467	oveq12i 7267	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥) = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
469	326, 340, 468	3eqtri 2770	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
470	147, 300, 301	divcli 11647	. . . . . . . . 9 ⊢ ((𝐵 − 𝐴) / 2) ∈ ℂ
471	319, 463, 470	adddiri 10919	. . . . . . . 8 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
472	323, 469, 471	3eqtr4i 2776	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2))
473		addsub12 11164	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸)))
474	61, 319, 58, 473	mp3an 1459	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸))
475	58	times2i 12042	. . . . . . . . . . . 12 ⊢ (𝐸 · 2) = (𝐸 + 𝐸)
476	475	oveq1i 7265	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
477	58, 58	pncan3oi 11167	. . . . . . . . . . 11 ⊢ ((𝐸 + 𝐸) − 𝐸) = 𝐸
478	476, 477	eqtri 2766	. . . . . . . . . 10 ⊢ ((𝐸 · 2) − 𝐸) = 𝐸
479	478	oveq2i 7266	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480	474, 479	eqtr3i 2768	. . . . . . . 8 ⊢ ((𝐸 · 2) + (𝐹 − 𝐸)) = (𝐹 + 𝐸)
481	480	oveq1i 7265	. . . . . . 7 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
482	472, 481	eqtri 2766	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
483	8, 300, 301	divcan4i 11652	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) / 2) = 𝐶
484	483	oveq1i 7265	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = (𝐶 · (𝐵 − 𝐴))
485	8, 300	mulcli 10913	. . . . . . . . . . 11 ⊢ (𝐶 · 2) ∈ ℂ
486		div32 11583	. . . . . . . . . . 11 ⊢ (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2)))
487	485, 293, 147, 486	mp3an 1459	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
488	484, 487	eqtr3i 2768	. . . . . . . . 9 ⊢ (𝐶 · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
489	488	oveq1i 7265	. . . . . . . 8 ⊢ ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
490	31	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
491	490	itgeq2dv 24851	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥)
492	491	mptru 1546	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥
493	7	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494		cniccibl 24910	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
495	1, 2, 266, 494	mp3an 1459	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹
496	495	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
497	25	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498	497, 493	resubcld 11333	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷 − 𝐶) ∈ ℝ)
499	331, 498	remulcld 10936	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) ∈ ℝ)
500	272	mptru 1546	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501		cniccibl 24910	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
502	1, 2, 500, 501	mp3an 1459	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹
503	502	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
504	493, 496, 499, 503	itgadd 24894	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥))
505	504	mptru 1546	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
506		itgconst 24888	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507	342, 349, 8, 506	mp3an 1459	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508	348	oveq2i 7266	. . . . . . . . . . 11 ⊢ (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵 − 𝐴))
509	507, 508	eqtri 2766	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵 − 𝐴))
510	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐷 ∈ ℂ)
511	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐶 ∈ ℂ)
512	510, 511	subcld 11262	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐷 − 𝐶) ∈ ℂ)
513	512, 331, 360	itgmulc2 24903	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
514	513	mptru 1546	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
515	460	oveq2i 7266	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
516		itgeq2 24847	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) → ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
517	26, 8	subcli 11227	. . . . . . . . . . . . . 14 ⊢ (𝐷 − 𝐶) ∈ ℂ
518	517	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 − 𝐶) ∈ ℂ)
519	518, 127	mulcomd 10927	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
520	516, 519	mprg 3077	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥
521	514, 515, 520	3eqtr3ri 2775	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥 = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
522	509, 521	oveq12i 7267	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥) = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
523	492, 505, 522	3eqtri 2770	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
524	485, 517, 470	adddiri 10919	. . . . . . . 8 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
525	489, 523, 524	3eqtr4i 2776	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2))
526		addsub12 11164	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶)))
527	26, 485, 8, 526	mp3an 1459	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶))
528	8	times2i 12042	. . . . . . . . . . . 12 ⊢ (𝐶 · 2) = (𝐶 + 𝐶)
529	528	oveq1i 7265	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
530	8, 8	pncan3oi 11167	. . . . . . . . . . 11 ⊢ ((𝐶 + 𝐶) − 𝐶) = 𝐶
531	529, 530	eqtri 2766	. . . . . . . . . 10 ⊢ ((𝐶 · 2) − 𝐶) = 𝐶
532	531	oveq2i 7266	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533	527, 532	eqtr3i 2768	. . . . . . . 8 ⊢ ((𝐶 · 2) + (𝐷 − 𝐶)) = (𝐷 + 𝐶)
534	533	oveq1i 7265	. . . . . . 7 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
535	525, 534	eqtri 2766	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
536	482, 535	oveq12i 7267	. . . . 5 ⊢ (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
537	316, 536	eqtri 2766	. . . 4 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
538	299, 304, 537	3eqtr4ri 2777	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
539	289, 291, 538	3eqtr2i 2772	. 2 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
540	286, 539	eqtri 2766	1 ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 395 = wceq 1539 ⊤wtru 1540 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∖ cdif 3880 ⊆ wss 3883 ∅c0 4253 ifcif 4456 {csn 4558 ⟨cop 4564 class class class wbr 5070 {copab 5132 ↦ cmpt 5153 × cxp 5578 ^◡ccnv 5579 dom cdm 5580 ↾ cres 5582 “ cima 5583 Fun wfun 6412 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 +∞cpnf 10937 ℝ^*cxr 10939 < clt 10940 ≤ cle 10941 − cmin 11135 / cdiv 11562 2c2 11958 ℕ₀cn0 12163 [,]cicc 13011 ↑cexp 13710 TopOpenctopn 17049 ℂ_fldccnfld 20510 Cn ccn 22283 ×_t ctx 22619 –cn→ccncf 23945 vol*covol 24531 volcvol 24532 𝐿¹cibl 24686 ∫citg 24687 areacarea 26010

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cc 10122 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880 ax-addf 10881 ax-mulf 10882

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-symdif 4173 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-disj 5036 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-of 7511 df-ofr 7512 df-om 7688 df-1st 7804 df-2nd 7805 df-supp 7949 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-oadd 8271 df-omul 8272 df-er 8456 df-map 8575 df-pm 8576 df-ixp 8644 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-fsupp 9059 df-fi 9100 df-sup 9131 df-inf 9132 df-oi 9199 df-dju 9590 df-card 9628 df-acn 9631 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-4 11968 df-5 11969 df-6 11970 df-7 11971 df-8 11972 df-9 11973 df-n0 12164 df-z 12250 df-dec 12367 df-uz 12512 df-q 12618 df-rp 12660 df-xneg 12777 df-xadd 12778 df-xmul 12779 df-ioo 13012 df-ioc 13013 df-ico 13014 df-icc 13015 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-limsup 15108 df-clim 15125 df-rlim 15126 df-sum 15326 df-struct 16776 df-sets 16793 df-slot 16811 df-ndx 16823 df-base 16841 df-ress 16868 df-plusg 16901 df-mulr 16902 df-starv 16903 df-sca 16904 df-vsca 16905 df-ip 16906 df-tset 16907 df-ple 16908 df-ds 16910 df-unif 16911 df-hom 16912 df-cco 16913 df-rest 17050 df-topn 17051 df-0g 17069 df-gsum 17070 df-topgen 17071 df-pt 17072 df-prds 17075 df-xrs 17130 df-qtop 17135 df-imas 17136 df-xps 17138 df-mre 17212 df-mrc 17213 df-acs 17215 df-mgm 18241 df-sgrp 18290 df-mnd 18301 df-submnd 18346 df-mulg 18616 df-cntz 18838 df-cmn 19303 df-psmet 20502 df-xmet 20503 df-met 20504 df-bl 20505 df-mopn 20506 df-fbas 20507 df-fg 20508 df-cnfld 20511 df-top 21951 df-topon 21968 df-topsp 21990 df-bases 22004 df-cld 22078 df-ntr 22079 df-cls 22080 df-nei 22157 df-lp 22195 df-perf 22196 df-cn 22286 df-cnp 22287 df-haus 22374 df-cmp 22446 df-tx 22621 df-hmeo 22814 df-fil 22905 df-fm 22997 df-flim 22998 df-flf 22999 df-xms 23381 df-ms 23382 df-tms 23383 df-cncf 23947 df-ovol 24533 df-vol 24534 df-mbf 24688 df-itg1 24689 df-itg2 24690 df-ibl 24691 df-itg 24692 df-0p 24739 df-limc 24935 df-dv 24936 df-area 26011

This theorem is referenced by: (None)

W3C validator