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 43206

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 13451	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
4	1, 2, 3	mp2an 692	. . . . . . . . 9 ⊢ (𝐴[,]𝐵) ⊆ ℝ
5	4	sseli 3959	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
6	5	adantr 480	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7		areaquad.3	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ∈ ℝ
8	7	recni 11257	. . . . . . . . . . . . . . 15 ⊢ 𝐶 ∈ ℂ
9	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10		resubcl 11555	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 − 𝐴) ∈ ℝ)
11	1, 10	mpan2 691	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝑥 − 𝐴) ∈ ℝ)
12	2, 1	resubcli 11553	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ∈ ℝ
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ∈ ℝ)
14	2	recni 11257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℂ
15	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16		recn 11227	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17		areaquad.7	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 < 𝐵
18	1, 17	gtneii 11355	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ≠ 𝐴
19	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ≠ 𝐴)
20	15, 16, 19	subne0d 11611	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
21	1, 20	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ≠ 0
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
23	11, 13, 22	redivcld 12077	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
24	23	recnd 11271	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
25		areaquad.4	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 ∈ ℝ
26	25	recni 11257	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ∈ ℂ
27	26	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
28	24, 27	mulcld 11263	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) ∈ ℂ)
29	24, 9	mulcld 11263	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶) ∈ ℂ)
30	9, 28, 29	addsub12d 11625	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
31		areaquad.10	. . . . . . . . . . . . . 14 ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
32	24, 27, 9	subdid 11701	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
33	32	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
34	31, 33	eqtrid 2781	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
35		1cnd 11238	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℂ)
36	35, 24, 9	subdird 11702	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
37	8	mullidi 11248	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐶) = 𝐶
38	37	oveq1i 7423	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))
39	36, 38	eqtrdi 2785	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
40	39	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
41	30, 34, 40	3eqtr4d 2779	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)))
42		1red 11244	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℝ)
43	42, 23	resubcld 11673	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
44	43	recnd 11271	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℂ)
45	44, 9	mulcld 11263	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) ∈ ℂ)
46	28, 45	addcomd 11445	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)))
47	44, 9	mulcomd 11264	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
48	24, 27	mulcomd 11264	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) = (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
49	47, 48	oveq12d 7431	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
50	41, 46, 49	3eqtrd 2773	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
51	7	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
52	51, 43	remulcld 11273	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
53	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
54	53, 23	remulcld 11273	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
55	52, 54	readdcld 11272	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
56	50, 55	eqeltrd 2833	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57		areaquad.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 ∈ ℝ
58	57	recni 11257	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ∈ ℂ
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60		areaquad.6	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 ∈ ℝ
61	60	recni 11257	. . . . . . . . . . . . . . . 16 ⊢ 𝐹 ∈ ℂ
62	61	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
63	24, 62	mulcld 11263	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) ∈ ℂ)
64	24, 59	mulcld 11263	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸) ∈ ℂ)
65	59, 63, 64	addsub12d 11625	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
66		areaquad.11	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
67	24, 62, 59	subdid 11701	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
68	67	oveq2d 7429	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
69	66, 68	eqtrid 2781	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
70	35, 24, 59	subdird 11702	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
71	58	mullidi 11248	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐸) = 𝐸
72	71	oveq1i 7423	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))
73	70, 72	eqtrdi 2785	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
74	73	oveq2d 7429	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
75	65, 69, 74	3eqtr4d 2779	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)))
76	44, 59	mulcld 11263	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) ∈ ℂ)
77	63, 76	addcomd 11445	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)))
78	44, 59	mulcomd 11264	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
79	24, 62	mulcomd 11264	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) = (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
80	78, 79	oveq12d 7431	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
81	75, 77, 80	3eqtrd 2773	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
82	57	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
83	82, 43	remulcld 11273	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
84	60	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
85	84, 23	remulcld 11273	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
86	83, 85	readdcld 11272	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
87	81, 86	eqeltrd 2833	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88		iccssre 13451	. . . . . . . . . 10 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
89	56, 87, 88	syl2anc 584	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
90	5, 89	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
91	90	sselda 3963	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
92	6, 91	jca 511	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
93	92	ssopab2i 5535	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94		areaquad.12	. . . . 5 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95		df-xp 5671	. . . . 5 ⊢ (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
96	93, 94, 95	3sstr4i 4015	. . . 4 ⊢ 𝑆 ⊆ (ℝ × ℝ)
97		iftrue 4511	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (𝑉 − 𝑈))
98		nfv 1913	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑥 ∈ (𝐴[,]𝐵)
99		nfopab2 5194	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
100	94, 99	nfcxfr 2895	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝑆
101		nfcv 2897	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦{𝑥}
102	100, 101	nfima 6066	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑆 “ {𝑥})
103		nfcv 2897	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑈[,]𝑉)
104		vex 3467	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
105		vex 3467	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
106	104, 105	elimasn 6088	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
107	94	eleq2i 2825	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108		opabidw 5509	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109	106, 107, 108	3bitri 297	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110	109	baib 535	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
111	98, 102, 103, 110	eqrd 3983	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112	111	fveq2d 6890	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
113	5, 56	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
114	5, 87	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115		iccmbl 25538	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116	113, 114, 115	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117		mblvol 25502	. . . . . . . . . . . 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 11271	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
128	127	subidd 11590	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = 0)
129		1red 11244	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
130	2	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
131	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
132	1	rexri 11301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐴 ∈ ℝ^*
133	2	rexri 11301	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℝ^*
134		iccleub 13424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
135	132, 133, 134	mp3an12 1452	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ≤ 𝐵)
136	5, 130, 131, 135	lesub1dd 11861	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ≤ (𝐵 − 𝐴))
137	5, 1, 10	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℝ)
138	12	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ)
139	1	recni 11257	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 ∈ ℂ
140	139	subidi 11562	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 − 𝐴) = 0
141	131, 130, 131	ltsub1d 11854	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐴) < (𝐵 − 𝐴)))
142	17, 141	mpbii 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) < (𝐵 − 𝐴))
143	140, 142	eqbrtrrid 5159	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵 − 𝐴))
144		lediv1 12115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 − 𝐴) ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ ∧ ((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴))) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
145	137, 138, 138, 143, 144	syl112anc 1375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
146	136, 145	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴)))
147	12	recni 11257	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 − 𝐴) ∈ ℂ
148	147, 21	dividi 11982	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 − 𝐴) / (𝐵 − 𝐴)) = 1
149	146, 148	breqtrdi 5164	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ 1)
150	126, 129, 126, 149	lesub1dd 11861	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
151	128, 150	eqbrtrrd 5147	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
152		areaquad.8	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ≤ 𝐸
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐶 ≤ 𝐸)
154	123, 124, 125, 151, 153	lemul1ad 12189	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
155	25	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
156	60	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157	138, 143	elrpd 13056	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ⁺)
158		iccgelb 13425	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥)
159	132, 133, 158	mp3an12 1452	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑥)
160	131, 5, 131, 159	lesub1dd 11861	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) ≤ (𝑥 − 𝐴))
161	140, 160	eqbrtrrid 5159	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥 − 𝐴))
162	137, 157, 161	divge0d 13099	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥 − 𝐴) / (𝐵 − 𝐴)))
163		areaquad.9	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ≤ 𝐹
164	163	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ≤ 𝐹)
165	155, 156, 126, 162, 164	lemul1ad 12189	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
166	119, 120, 121, 122, 154, 165	le2addd 11864	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
167	5, 50	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
168	5, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
169	166, 167, 168	3brtr4d 5155	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ≤ 𝑉)
170		ovolicc 25495	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈 ≤ 𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
171	113, 114, 169, 170	syl3anc 1372	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
172	112, 118, 171	3eqtrd 2773	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉 − 𝑈))
173	97, 172	eqtr4d 2772	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174		iffalse 4514	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = 0)
175		nfv 1913	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176		nfcv 2897	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∅
177	109	simplbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178		noel 4318	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑦 ∈ ∅
179	178	pm2.21i 119	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180	177, 179	pm5.21ni 377	. . . . . . . . . . . . 13 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181	175, 102, 176, 180	eqrd 3983	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182	181	fveq2d 6890	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183		0mbl 25511	. . . . . . . . . . . . 13 ⊢ ∅ ∈ dom vol
184		mblvol 25502	. . . . . . . . . . . . 13 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185	183, 184	ax-mp 5	. . . . . . . . . . . 12 ⊢ (vol‘∅) = (vol*‘∅)
186		ovol0 25465	. . . . . . . . . . . 12 ⊢ (vol*‘∅) = 0
187	185, 186	eqtri 2757	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
188	182, 187	eqtrdi 2785	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189	174, 188	eqtr4d 2772	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190	173, 189	pm2.61i 182	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191	190	eqcomi 2743	. . . . . . 7 ⊢ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0)
192	87, 56	resubcld 11673	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → (𝑉 − 𝑈) ∈ ℝ)
193		0re 11245	. . . . . . . 8 ⊢ 0 ∈ ℝ
194		ifcl 4551	. . . . . . . 8 ⊢ (((𝑉 − 𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
195	192, 193, 194	sylancl 586	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
196	191, 195	eqeltrid 2837	. . . . . 6 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197		volf 25501	. . . . . . . 8 ⊢ vol:dom vol⟶(0[,]+∞)
198		ffun 6719	. . . . . . . 8 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
199	197, 198	ax-mp 5	. . . . . . 7 ⊢ Fun vol
200		iftrue 4511	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201	111, 200	eqtr4d 2772	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202		iffalse 4514	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203	181, 202	eqtr4d 2772	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204	201, 203	pm2.61i 182	. . . . . . . 8 ⊢ (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
205	56, 87, 115	syl2anc 584	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206	183	a1i 11	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207	205, 206	ifcld 4552	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208	204, 207	eqeltrid 2837	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209		fvimacnv 7053	. . . . . . 7 ⊢ ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
210	199, 208, 209	sylancr 587	. . . . . 6 ⊢ (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
211	196, 210	mpbid 232	. . . . 5 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ))
212	211	rgen 3052	. . . 4 ⊢ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)
213	4	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214		rembl 25512	. . . . . . 7 ⊢ ℝ ∈ dom vol
215	214	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → ℝ ∈ dom vol)
216	114, 113	resubcld 11673	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑉 − 𝑈) ∈ ℝ)
217	172, 216	eqeltrd 2833	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218	217	adantl 481	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219		eldifn 4112	. . . . . . . 8 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220	219, 188	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221	220	adantl 481	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222	172	mpteq2ia 5225	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈))
223		eqid 2734	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
224	223	subcn 24825	. . . . . . . . . . . 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 5227	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
227	223	addcn 24824	. . . . . . . . . . . . . 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 11194	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
230	4, 229	sstri 3973	. . . . . . . . . . . . . . 15 ⊢ (𝐴[,]𝐵) ⊆ ℂ
231		ssid 3986	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
232		cncfmptc 24875	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
233	58, 230, 231, 232	mp3an 1462	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234	233	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235	230	sseli 3959	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236	139	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237	147	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℂ)
238	21	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ≠ 0)
239	235, 236, 237, 238	divsubdird 12064	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
240	239	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
241	240	mpteq2dva 5222	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))))
242		resmpt 6035	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))))
243	230, 242	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴)))
244		eqid 2734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴)))
245	244	divccncf 24869	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ))
246	147, 21, 245	mp2an 692	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ)
247		rescncf 24860	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248	230, 246, 247	mp2 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249	243, 248	eqeltrri 2830	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250	249	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251	139, 147, 21	divcli 11991	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (𝐵 − 𝐴)) ∈ ℂ
252		cncfmptc 24875	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 / (𝐵 − 𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253	251, 230, 231, 252	mp3an 1462	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254	253	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255	223, 225, 250, 254	cncfmpt2f 24878	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256	241, 255	eqeltrd 2833	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257		cncfmptc 24875	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
258	61, 230, 231, 257	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259	258	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260	223, 225, 259, 234	cncfmpt2f 24878	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹 − 𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261	256, 260	mulcncf 25417	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262	223, 228, 234, 261	cncfmpt2f 24878	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263	226, 262	eqeltrid 2837	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
264	31	mpteq2i 5227	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
265		cncfmptc 24875	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
266	8, 230, 231, 265	mp3an 1462	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267	266	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268		cncfmptc 24875	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
269	26, 230, 231, 268	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270	269	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271	223, 225, 270, 267	cncfmpt2f 24878	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷 − 𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272	256, 271	mulcncf 25417	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273	223, 228, 267, 272	cncfmpt2f 24878	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274	264, 273	eqeltrid 2837	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275	223, 225, 263, 274	cncfmpt2f 24878	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276	275	mptru 1546	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277		cniccibl 25813	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹)
278	1, 2, 276, 277	mp3an 1462	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹
279	222, 278	eqeltri 2829	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
280	279	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
281	213, 215, 218, 221, 280	iblss2 25778	. . . . 5 ⊢ (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
282	193, 281	ax-mp 5	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
283		dmarea 26937	. . . 4 ⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹))
284	96, 212, 282, 283	mpbir3an 1341	. . 3 ⊢ 𝑆 ∈ dom area
285		areaval 26944	. . 3 ⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286	284, 285	ax-mp 5	. 2 ⊢ (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287		itgeq2 25750	. . . 4 ⊢ (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
288	191	a1i 11	. . . 4 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0))
289	287, 288	mprg 3056	. . 3 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
290		itgss2 25785	. . . 4 ⊢ ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
291	4, 290	ax-mp 5	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
292	61, 58	addcli 11249	. . . . . 6 ⊢ (𝐹 + 𝐸) ∈ ℂ
293		2cnne0 12458	. . . . . 6 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
294		div32 11924	. . . . . 6 ⊢ (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)))
295	292, 293, 147, 294	mp3an 1462	. . . . 5 ⊢ (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
296	26, 8	addcli 11249	. . . . . 6 ⊢ (𝐷 + 𝐶) ∈ ℂ
297		div32 11924	. . . . . 6 ⊢ (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
298	296, 293, 147, 297	mp3an 1462	. . . . 5 ⊢ (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
299	295, 298	oveq12i 7425	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴))) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
300		2cn 12323	. . . . . 6 ⊢ 2 ∈ ℂ
301		2ne0 12352	. . . . . 6 ⊢ 2 ≠ 0
302	292, 300, 301	divcli 11991	. . . . 5 ⊢ ((𝐹 + 𝐸) / 2) ∈ ℂ
303	296, 300, 301	divcli 11991	. . . . 5 ⊢ ((𝐷 + 𝐶) / 2) ∈ ℂ
304	302, 303, 147	subdiri 11695	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)))
305	114	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306	263	mptru 1546	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307		cniccibl 25813	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
308	1, 2, 306, 307	mp3an 1462	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹
309	308	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
310	113	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311	274	mptru 1546	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312		cniccibl 25813	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
313	1, 2, 311, 312	mp3an 1462	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹
314	313	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
315	305, 309, 310, 314	itgsub 25798	. . . . . 6 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316	315	mptru 1546	. . . . 5 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
317	58, 300, 301	divcan4i 11996	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) / 2) = 𝐸
318	317	oveq1i 7423	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = (𝐸 · (𝐵 − 𝐴))
319	58, 300	mulcli 11250	. . . . . . . . . . 11 ⊢ (𝐸 · 2) ∈ ℂ
320		div32 11924	. . . . . . . . . . 11 ⊢ (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2)))
321	319, 293, 147, 320	mp3an 1462	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
322	318, 321	eqtr3i 2759	. . . . . . . . 9 ⊢ (𝐸 · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
323	322	oveq1i 7423	. . . . . . . 8 ⊢ ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
324		itgeq2 25750	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥)
325	66	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
326	324, 325	mprg 3056	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥
327	57	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328		cniccibl 25813	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
329	1, 2, 233, 328	mp3an 1462	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹
330	329	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
331	126	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
332	60	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333	332, 327	resubcld 11673	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹 − 𝐸) ∈ ℝ)
334	331, 333	remulcld 11273	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) ∈ ℝ)
335	261	mptru 1546	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336		cniccibl 25813	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
337	1, 2, 335, 336	mp3an 1462	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹
338	337	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
339	327, 330, 334, 338	itgadd 25797	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥))
340	339	mptru 1546	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
341		iccmbl 25538	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
342	1, 2, 341	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝐴[,]𝐵) ∈ dom vol
343		mblvol 25502	. . . . . . . . . . . . . . 15 ⊢ ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344	342, 343	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
345	1, 2, 17	ltleii 11366	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ≤ 𝐵
346		ovolicc 25495	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
347	1, 2, 345, 346	mp3an 1462	. . . . . . . . . . . . . 14 ⊢ (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
348	344, 347	eqtri 2757	. . . . . . . . . . . . 13 ⊢ (vol‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
349	348, 12	eqeltri 2829	. . . . . . . . . . . 12 ⊢ (vol‘(𝐴[,]𝐵)) ∈ ℝ
350		itgconst 25791	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351	342, 349, 58, 350	mp3an 1462	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352	348	oveq2i 7424	. . . . . . . . . . 11 ⊢ (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵 − 𝐴))
353	351, 352	eqtri 2757	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵 − 𝐴))
354	61	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐹 ∈ ℂ)
355	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐸 ∈ ℂ)
356	354, 355	subcld 11602	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐹 − 𝐸) ∈ ℂ)
357	256	mptru 1546	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358		cniccibl 25813	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
359	1, 2, 357, 358	mp3an 1462	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹
360	359	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
361	356, 331, 360	itgmulc2 25806	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
362	361	mptru 1546	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
363		itgeq2 25750	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) → ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
364	137	recnd 11271	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℂ)
365	364, 237, 238	divrec2d 12029	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)))
366	363, 365	mprg 3056	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
367	5	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368		cncfmptid 24876	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369	230, 231, 368	mp2an 692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370		cniccibl 25813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
371	1, 2, 369, 370	mp3an 1462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹
372	371	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
373	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374		cncfmptc 24875	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375	139, 230, 231, 374	mp3an 1462	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376		cniccibl 25813	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
377	1, 2, 375, 376	mp3an 1462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹
378	377	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
379	367, 372, 373, 378	itgsub 25798	. . . . . . . . . . . . . . . . . . 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 12525	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
385	384	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 1 ∈ ℕ₀)
386	381, 382, 383, 385	itgpowd 26028	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387	386	mptru 1546	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388		1p1e2 12373	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
389	388	oveq2i 7424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390	387, 389	eqtri 2757	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391		itgeq2 25750	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392	235	exp1d 14164	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393	391, 392	mprg 3056	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394	388	oveq2i 7424	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵↑(1 + 1)) = (𝐵↑2)
395	388	oveq2i 7424	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴↑(1 + 1)) = (𝐴↑2)
396	394, 395	oveq12i 7425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397	396	oveq1i 7423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398	390, 393, 397	3eqtr3i 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399		itgconst 25791	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400	342, 349, 139, 399	mp3an 1462	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401	348	oveq2i 7424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵 − 𝐴))
402	400, 401	eqtri 2757	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵 − 𝐴))
403	398, 402	oveq12i 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
404	380, 403	eqtri 2757	. . . . . . . . . . . . . . . . 17 ⊢ ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
405	404	oveq2i 7424	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴))))
406	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ∈ ℂ)
407	139	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐴 ∈ ℂ)
408	406, 407	subcld 11602	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ∈ ℂ)
409	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ≠ 𝐴)
410	406, 407, 409	subne0d 11611	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ≠ 0)
411	408, 410	reccld 12018	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (1 / (𝐵 − 𝐴)) ∈ ℂ)
412	411	mptru 1546	. . . . . . . . . . . . . . . . 17 ⊢ (1 / (𝐵 − 𝐴)) ∈ ℂ
413	14	sqcli 14203	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵↑2) ∈ ℂ
414	139	sqcli 14203	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴↑2) ∈ ℂ
415	413, 414	subcli 11567	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416	415, 300, 301	divcli 11991	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417	139, 147	mulcli 11250	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 · (𝐵 − 𝐴)) ∈ ℂ
418	412, 416, 417	subdii 11694	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
419	405, 418	eqtri 2757	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
420	137	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 − 𝐴) ∈ ℝ)
421	367, 372, 373, 378	iblsub 25794	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 − 𝐴)) ∈ 𝐿¹)
422	411, 420, 421	itgmulc2 25806	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
423	422	mptru 1546	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
424	412, 417	mulcomi 11251	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
425	417, 147, 21	divreci 11994	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
426	139, 147, 21	divcan4i 11996	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = 𝐴
427	424, 425, 426	3eqtr2i 2763	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = 𝐴
428	427	oveq2i 7424	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429	419, 423, 428	3eqtr3i 2765	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430	366, 429	eqtri 2757	. . . . . . . . . . . . 13 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
431	14, 139	subsqi 14235	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵 − 𝐴))
432	431	oveq1i 7423	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2)
433	432	oveq2i 7424	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
434	431, 415	eqeltrri 2830	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) · (𝐵 − 𝐴)) ∈ ℂ
435	412, 434, 300, 301	divassi 12005	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
436	412, 434	mulcomi 11251	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
437	434, 147, 21	divreci 11994	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
438	14, 139	addcli 11249	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 + 𝐴) ∈ ℂ
439	438, 147, 21	divcan4i 11996	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (𝐵 + 𝐴)
440	436, 437, 439	3eqtr2i 2763	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (𝐵 + 𝐴)
441	440	oveq1i 7423	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442	433, 435, 441	3eqtr2i 2763	. . . . . . . . . . . . . 14 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443	442	oveq1i 7423	. . . . . . . . . . . . 13 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444	139, 300	mulcli 11250	. . . . . . . . . . . . . . 15 ⊢ (𝐴 · 2) ∈ ℂ
445		divsubdir 11943	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446	438, 444, 293, 445	mp3an 1462	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
447	14, 139, 444	addsubassi 11582	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448		subsub2 11519	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
449	14, 444, 139, 448	mp3an 1462	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450	139	times2i 12387	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
451	450	oveq1i 7423	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452	139, 139	pncan3oi 11506	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 + 𝐴) − 𝐴) = 𝐴
453	451, 452	eqtri 2757	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · 2) − 𝐴) = 𝐴
454	453	oveq2i 7424	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 − 𝐴)
455	447, 449, 454	3eqtr2i 2763	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 − 𝐴)
456	455	oveq1i 7423	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵 − 𝐴) / 2)
457	139, 300, 301	divcan4i 11996	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 · 2) / 2) = 𝐴
458	457	oveq2i 7424	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459	446, 456, 458	3eqtr3ri 2766	. . . . . . . . . . . . 13 ⊢ (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵 − 𝐴) / 2)
460	430, 443, 459	3eqtri 2761	. . . . . . . . . . . 12 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ((𝐵 − 𝐴) / 2)
461	460	oveq2i 7424	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
462		itgeq2 25750	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) → ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
463	61, 58	subcli 11567	. . . . . . . . . . . . . 14 ⊢ (𝐹 − 𝐸) ∈ ℂ
464	463	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐹 − 𝐸) ∈ ℂ)
465	464, 127	mulcomd 11264	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
466	462, 465	mprg 3056	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥
467	362, 461, 466	3eqtr3ri 2766	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥 = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
468	353, 467	oveq12i 7425	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥) = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
469	326, 340, 468	3eqtri 2761	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
470	147, 300, 301	divcli 11991	. . . . . . . . 9 ⊢ ((𝐵 − 𝐴) / 2) ∈ ℂ
471	319, 463, 470	adddiri 11256	. . . . . . . 8 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
472	323, 469, 471	3eqtr4i 2767	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2))
473		addsub12 11503	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸)))
474	61, 319, 58, 473	mp3an 1462	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸))
475	58	times2i 12387	. . . . . . . . . . . 12 ⊢ (𝐸 · 2) = (𝐸 + 𝐸)
476	475	oveq1i 7423	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
477	58, 58	pncan3oi 11506	. . . . . . . . . . 11 ⊢ ((𝐸 + 𝐸) − 𝐸) = 𝐸
478	476, 477	eqtri 2757	. . . . . . . . . 10 ⊢ ((𝐸 · 2) − 𝐸) = 𝐸
479	478	oveq2i 7424	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480	474, 479	eqtr3i 2759	. . . . . . . 8 ⊢ ((𝐸 · 2) + (𝐹 − 𝐸)) = (𝐹 + 𝐸)
481	480	oveq1i 7423	. . . . . . 7 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
482	472, 481	eqtri 2757	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
483	8, 300, 301	divcan4i 11996	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) / 2) = 𝐶
484	483	oveq1i 7423	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = (𝐶 · (𝐵 − 𝐴))
485	8, 300	mulcli 11250	. . . . . . . . . . 11 ⊢ (𝐶 · 2) ∈ ℂ
486		div32 11924	. . . . . . . . . . 11 ⊢ (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2)))
487	485, 293, 147, 486	mp3an 1462	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
488	484, 487	eqtr3i 2759	. . . . . . . . 9 ⊢ (𝐶 · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
489	488	oveq1i 7423	. . . . . . . 8 ⊢ ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
490	31	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
491	490	itgeq2dv 25754	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥)
492	491	mptru 1546	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥
493	7	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494		cniccibl 25813	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
495	1, 2, 266, 494	mp3an 1462	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹
496	495	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
497	25	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498	497, 493	resubcld 11673	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷 − 𝐶) ∈ ℝ)
499	331, 498	remulcld 11273	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) ∈ ℝ)
500	272	mptru 1546	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501		cniccibl 25813	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
502	1, 2, 500, 501	mp3an 1462	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹
503	502	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
504	493, 496, 499, 503	itgadd 25797	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥))
505	504	mptru 1546	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
506		itgconst 25791	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507	342, 349, 8, 506	mp3an 1462	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508	348	oveq2i 7424	. . . . . . . . . . 11 ⊢ (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵 − 𝐴))
509	507, 508	eqtri 2757	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵 − 𝐴))
510	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐷 ∈ ℂ)
511	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐶 ∈ ℂ)
512	510, 511	subcld 11602	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐷 − 𝐶) ∈ ℂ)
513	512, 331, 360	itgmulc2 25806	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
514	513	mptru 1546	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
515	460	oveq2i 7424	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
516		itgeq2 25750	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) → ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
517	26, 8	subcli 11567	. . . . . . . . . . . . . 14 ⊢ (𝐷 − 𝐶) ∈ ℂ
518	517	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 − 𝐶) ∈ ℂ)
519	518, 127	mulcomd 11264	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
520	516, 519	mprg 3056	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥
521	514, 515, 520	3eqtr3ri 2766	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥 = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
522	509, 521	oveq12i 7425	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥) = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
523	492, 505, 522	3eqtri 2761	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
524	485, 517, 470	adddiri 11256	. . . . . . . 8 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
525	489, 523, 524	3eqtr4i 2767	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2))
526		addsub12 11503	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶)))
527	26, 485, 8, 526	mp3an 1462	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶))
528	8	times2i 12387	. . . . . . . . . . . 12 ⊢ (𝐶 · 2) = (𝐶 + 𝐶)
529	528	oveq1i 7423	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
530	8, 8	pncan3oi 11506	. . . . . . . . . . 11 ⊢ ((𝐶 + 𝐶) − 𝐶) = 𝐶
531	529, 530	eqtri 2757	. . . . . . . . . 10 ⊢ ((𝐶 · 2) − 𝐶) = 𝐶
532	531	oveq2i 7424	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533	527, 532	eqtr3i 2759	. . . . . . . 8 ⊢ ((𝐶 · 2) + (𝐷 − 𝐶)) = (𝐷 + 𝐶)
534	533	oveq1i 7423	. . . . . . 7 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
535	525, 534	eqtri 2757	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
536	482, 535	oveq12i 7425	. . . . 5 ⊢ (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
537	316, 536	eqtri 2757	. . . 4 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
538	299, 304, 537	3eqtr4ri 2768	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
539	289, 291, 538	3eqtr2i 2763	. 2 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
540	286, 539	eqtri 2757	1 ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 = wceq 1539 ⊤wtru 1540 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 ∖ cdif 3928 ⊆ wss 3931 ∅c0 4313 ifcif 4505 {csn 4606 ⟨cop 4612 class class class wbr 5123 {copab 5185 ↦ cmpt 5205 × cxp 5663 ^◡ccnv 5664 dom cdm 5665 ↾ cres 5667 “ cima 5668 Fun wfun 6535 ⟶wf 6537 ‘cfv 6541 (class class class)co 7413 ℂcc 11135 ℝcr 11136 0cc0 11137 1c1 11138 + caddc 11140 · cmul 11142 +∞cpnf 11274 ℝ^*cxr 11276 < clt 11277 ≤ cle 11278 − cmin 11474 / cdiv 11902 2c2 12303 ℕ₀cn0 12509 [,]cicc 13372 ↑cexp 14084 TopOpenctopn 17438 ℂ_fldccnfld 21327 Cn ccn 23179 ×_t ctx 23515 –cn→ccncf 24839 vol*covol 25434 volcvol 25435 𝐿¹cibl 25589 ∫citg 25590 areacarea 26935

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-inf2 9663 ax-cc 10457 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215 ax-addf 11216

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-symdif 4233 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-int 4927 df-iun 4973 df-iin 4974 df-disj 5091 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-se 5618 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-of 7679 df-ofr 7680 df-om 7870 df-1st 7996 df-2nd 7997 df-supp 8168 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-2o 8489 df-oadd 8492 df-omul 8493 df-er 8727 df-map 8850 df-pm 8851 df-ixp 8920 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-fsupp 9384 df-fi 9433 df-sup 9464 df-inf 9465 df-oi 9532 df-dju 9923 df-card 9961 df-acn 9964 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 df-9 12318 df-n0 12510 df-z 12597 df-dec 12717 df-uz 12861 df-q 12973 df-rp 13017 df-xneg 13136 df-xadd 13137 df-xmul 13138 df-ioo 13373 df-ioc 13374 df-ico 13375 df-icc 13376 df-fz 13530 df-fzo 13677 df-fl 13814 df-mod 13892 df-seq 14025 df-exp 14085 df-hash 14353 df-cj 15121 df-re 15122 df-im 15123 df-sqrt 15257 df-abs 15258 df-limsup 15490 df-clim 15507 df-rlim 15508 df-sum 15706 df-struct 17167 df-sets 17184 df-slot 17202 df-ndx 17214 df-base 17231 df-ress 17254 df-plusg 17287 df-mulr 17288 df-starv 17289 df-sca 17290 df-vsca 17291 df-ip 17292 df-tset 17293 df-ple 17294 df-ds 17296 df-unif 17297 df-hom 17298 df-cco 17299 df-rest 17439 df-topn 17440 df-0g 17458 df-gsum 17459 df-topgen 17460 df-pt 17461 df-prds 17464 df-xrs 17519 df-qtop 17524 df-imas 17525 df-xps 17527 df-mre 17601 df-mrc 17602 df-acs 17604 df-mgm 18623 df-sgrp 18702 df-mnd 18718 df-submnd 18767 df-mulg 19056 df-cntz 19305 df-cmn 19769 df-psmet 21319 df-xmet 21320 df-met 21321 df-bl 21322 df-mopn 21323 df-fbas 21324 df-fg 21325 df-cnfld 21328 df-top 22849 df-topon 22866 df-topsp 22888 df-bases 22901 df-cld 22974 df-ntr 22975 df-cls 22976 df-nei 23053 df-lp 23091 df-perf 23092 df-cn 23182 df-cnp 23183 df-haus 23270 df-cmp 23342 df-tx 23517 df-hmeo 23710 df-fil 23801 df-fm 23893 df-flim 23894 df-flf 23895 df-xms 24276 df-ms 24277 df-tms 24278 df-cncf 24841 df-ovol 25436 df-vol 25437 df-mbf 25591 df-itg1 25592 df-itg2 25593 df-ibl 25594 df-itg 25595 df-0p 25642 df-limc 25838 df-dv 25839 df-area 26936

This theorem is referenced by: (None)

W3C validator