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 43971

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 13462	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
4	1, 2, 3	mp2an 704	. . . . . . . . 9 ⊢ (𝐴[,]𝐵) ⊆ ℝ
5	4	sseli 3932	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
6	5	adantr 485	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7		areaquad.3	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ∈ ℝ
8	7	recni 11229	. . . . . . . . . . . . . . 15 ⊢ 𝐶 ∈ ℂ
9	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10		resubcl 11528	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 − 𝐴) ∈ ℝ)
11	1, 10	mpan2 703	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝑥 − 𝐴) ∈ ℝ)
12	2, 1	resubcli 11526	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ∈ ℝ
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ∈ ℝ)
14	2	recni 11229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℂ
15	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16		recn 11196	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17		areaquad.7	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 < 𝐵
18	1, 17	gtneii 11328	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ≠ 𝐴
19	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ≠ 𝐴)
20	15, 16, 19	subne0d 11584	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
21	1, 20	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ≠ 0
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
23	11, 13, 22	redivcld 12049	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
24	23	recnd 11243	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
25		areaquad.4	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 ∈ ℝ
26	25	recni 11229	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ∈ ℂ
27	26	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
28	24, 27	mulcld 11235	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) ∈ ℂ)
29	24, 9	mulcld 11235	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶) ∈ ℂ)
30	9, 28, 29	addsub12d 11598	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
31		areaquad.10	. . . . . . . . . . . . . 14 ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
32	24, 27, 9	subdid 11676	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
33	32	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
34	31, 33	eqtrid 2809	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
35		1cnd 11208	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℂ)
36	35, 24, 9	subdird 11677	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
37	8	mullidi 11220	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐶) = 𝐶
38	37	oveq1i 7422	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))
39	36, 38	eqtrdi 2813	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
40	39	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
41	30, 34, 40	3eqtr4d 2807	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)))
42		1red 11215	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℝ)
43	42, 23	resubcld 11648	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
44	43	recnd 11243	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℂ)
45	44, 9	mulcld 11235	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) ∈ ℂ)
46	28, 45	addcomd 11418	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)))
47	44, 9	mulcomd 11236	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
48	24, 27	mulcomd 11236	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) = (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
49	47, 48	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
50	41, 46, 49	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
51	7	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
52	51, 43	remulcld 11245	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
53	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
54	53, 23	remulcld 11245	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
55	52, 54	readdcld 11244	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
56	50, 55	eqeltrd 2862	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57		areaquad.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 ∈ ℝ
58	57	recni 11229	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ∈ ℂ
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60		areaquad.6	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 ∈ ℝ
61	60	recni 11229	. . . . . . . . . . . . . . . 16 ⊢ 𝐹 ∈ ℂ
62	61	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
63	24, 62	mulcld 11235	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) ∈ ℂ)
64	24, 59	mulcld 11235	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸) ∈ ℂ)
65	59, 63, 64	addsub12d 11598	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
66		areaquad.11	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
67	24, 62, 59	subdid 11676	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
68	67	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
69	66, 68	eqtrid 2809	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
70	35, 24, 59	subdird 11677	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
71	58	mullidi 11220	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐸) = 𝐸
72	71	oveq1i 7422	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))
73	70, 72	eqtrdi 2813	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
74	73	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
75	65, 69, 74	3eqtr4d 2807	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)))
76	44, 59	mulcld 11235	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) ∈ ℂ)
77	63, 76	addcomd 11418	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)))
78	44, 59	mulcomd 11236	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
79	24, 62	mulcomd 11236	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) = (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
80	78, 79	oveq12d 7430	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
81	75, 77, 80	3eqtrd 2801	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
82	57	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
83	82, 43	remulcld 11245	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
84	60	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
85	84, 23	remulcld 11245	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
86	83, 85	readdcld 11244	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
87	81, 86	eqeltrd 2862	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88		iccssre 13462	. . . . . . . . . 10 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
89	56, 87, 88	syl2anc 595	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
90	5, 89	syl 18	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
91	90	sselda 3936	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
92	6, 91	jca 520	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
93	92	ssopab2i 5534	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94		areaquad.12	. . . . 5 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95		df-xp 5666	. . . . 5 ⊢ (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
96	93, 94, 95	3sstr4i 3987	. . . 4 ⊢ 𝑆 ⊆ (ℝ × ℝ)
97		iftrue 4492	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (𝑉 − 𝑈))
98		nfv 1943	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑥 ∈ (𝐴[,]𝐵)
99		nfopab2 5181	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
100	94, 99	nfcxfr 2922	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝑆
101		nfcv 2924	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦{𝑥}
102	100, 101	nfima 6069	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑆 “ {𝑥})
103		nfcv 2924	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑈[,]𝑉)
104		vex 3458	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
105		vex 3458	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
106	104, 105	elimasn 6091	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
107	94	eleq2i 2854	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108		opabidw 5507	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109	106, 107, 108	3bitri 300	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110	109	baib 544	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
111	98, 102, 103, 110	eqrd 3955	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112	111	fveq2d 6885	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
113	5, 56	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
114	5, 87	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115		iccmbl 25736	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116	113, 114, 115	syl2anc 595	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117		mblvol 25700	. . . . . . . . . . . 12 ⊢ ((𝑈[,]𝑉) ∈ dom vol → (vol‘(𝑈[,]𝑉)) = (vol*‘(𝑈[,]𝑉)))
118	116, 117	syl 18	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑈[,]𝑉)) = (vol*‘(𝑈[,]𝑉)))
119	5, 52	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
120	5, 54	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
121	5, 83	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
122	5, 85	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
123	7	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐶 ∈ ℝ)
124	57	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐸 ∈ ℝ)
125	5, 43	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
126	5, 23	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
127	126	recnd 11243	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
128	127	subidd 11563	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = 0)
129		1red 11215	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
130	2	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
131	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
132	1	rexri 11273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐴 ∈ ℝ^*
133	2	rexri 11273	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℝ^*
134		iccleub 13434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
135	132, 133, 134	mp3an12 1479	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ≤ 𝐵)
136	5, 130, 131, 135	lesub1dd 11836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ≤ (𝐵 − 𝐴))
137	5, 1, 10	sylancl 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℝ)
138	12	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ)
139	1	recni 11229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 ∈ ℂ
140	139	subidi 11535	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 − 𝐴) = 0
141	131, 130, 131	ltsub1d 11829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐴) < (𝐵 − 𝐴)))
142	17, 141	mpbii 236	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) < (𝐵 − 𝐴))
143	140, 142	eqbrtrrid 5146	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵 − 𝐴))
144		lediv1 12086	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 − 𝐴) ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ ∧ ((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴))) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
145	137, 138, 138, 143, 144	syl112anc 1400	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
146	136, 145	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴)))
147	12	recni 11229	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 − 𝐴) ∈ ℂ
148	147, 21	dividi 11954	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 − 𝐴) / (𝐵 − 𝐴)) = 1
149	146, 148	breqtrdi 5151	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ 1)
150	126, 129, 126, 149	lesub1dd 11836	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
151	128, 150	eqbrtrrd 5134	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
152		areaquad.8	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ≤ 𝐸
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐶 ≤ 𝐸)
154	123, 124, 125, 151, 153	lemul1ad 12160	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
155	25	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
156	60	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157	138, 143	elrpd 13063	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ⁺)
158		iccgelb 13435	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥)
159	132, 133, 158	mp3an12 1479	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑥)
160	131, 5, 131, 159	lesub1dd 11836	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) ≤ (𝑥 − 𝐴))
161	140, 160	eqbrtrrid 5146	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥 − 𝐴))
162	137, 157, 161	divge0d 13106	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥 − 𝐴) / (𝐵 − 𝐴)))
163		areaquad.9	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ≤ 𝐹
164	163	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ≤ 𝐹)
165	155, 156, 126, 162, 164	lemul1ad 12160	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
166	119, 120, 121, 122, 154, 165	le2addd 11839	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
167	5, 50	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
168	5, 81	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
169	166, 167, 168	3brtr4d 5142	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ≤ 𝑉)
170		ovolicc 25693	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈 ≤ 𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
171	113, 114, 169, 170	syl3anc 1397	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
172	112, 118, 171	3eqtrd 2801	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉 − 𝑈))
173	97, 172	eqtr4d 2800	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174		iffalse 4495	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = 0)
175		nfv 1943	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176		nfcv 2924	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∅
177	109	simplbi 501	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178		noel 4290	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑦 ∈ ∅
179	178	pm2.21i 120	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180	177, 179	pm5.21ni 380	. . . . . . . . . . . . 13 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181	175, 102, 176, 180	eqrd 3955	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182	181	fveq2d 6885	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183		0mbl 25709	. . . . . . . . . . . . 13 ⊢ ∅ ∈ dom vol
184		mblvol 25700	. . . . . . . . . . . . 13 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185	183, 184	ax-mp 5	. . . . . . . . . . . 12 ⊢ (vol‘∅) = (vol*‘∅)
186		ovol0 25663	. . . . . . . . . . . 12 ⊢ (vol*‘∅) = 0
187	185, 186	eqtri 2785	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
188	182, 187	eqtrdi 2813	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189	174, 188	eqtr4d 2800	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190	173, 189	pm2.61i 184	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191	190	eqcomi 2771	. . . . . . 7 ⊢ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0)
192	87, 56	resubcld 11648	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → (𝑉 − 𝑈) ∈ ℝ)
193		0re 11216	. . . . . . . 8 ⊢ 0 ∈ ℝ
194		ifcl 4532	. . . . . . . 8 ⊢ (((𝑉 − 𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
195	192, 193, 194	sylancl 597	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
196	191, 195	eqeltrid 2866	. . . . . 6 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197		volf 25699	. . . . . . . 8 ⊢ vol:dom vol⟶(0[,]+∞)
198		ffun 6708	. . . . . . . 8 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
199	197, 198	ax-mp 5	. . . . . . 7 ⊢ Fun vol
200		iftrue 4492	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201	111, 200	eqtr4d 2800	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202		iffalse 4495	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203	181, 202	eqtr4d 2800	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204	201, 203	pm2.61i 184	. . . . . . . 8 ⊢ (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
205	56, 87, 115	syl2anc 595	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206	183	a1i 11	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207	205, 206	ifcld 4533	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208	204, 207	eqeltrid 2866	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209		fvimacnv 7048	. . . . . . 7 ⊢ ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
210	199, 208, 209	sylancr 598	. . . . . 6 ⊢ (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
211	196, 210	mpbid 235	. . . . 5 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ))
212	211	rgen 3080	. . . 4 ⊢ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)
213	4	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214		rembl 25710	. . . . . . 7 ⊢ ℝ ∈ dom vol
215	214	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → ℝ ∈ dom vol)
216	114, 113	resubcld 11648	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑉 − 𝑈) ∈ ℝ)
217	172, 216	eqeltrd 2862	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218	217	adantl 486	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219		eldifn 4085	. . . . . . . 8 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220	219, 188	syl 18	. . . . . . 7 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221	220	adantl 486	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222	172	mpteq2ia 5205	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈))
223		eqid 2762	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
224	223	subcn 25035	. . . . . . . . . . . 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 5206	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
227	223	addcn 25034	. . . . . . . . . . . . . 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 11163	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
230	4, 229	sstri 3945	. . . . . . . . . . . . . . 15 ⊢ (𝐴[,]𝐵) ⊆ ℂ
231		ssid 3958	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
232		cncfmptc 25082	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
233	58, 230, 231, 232	mp3an 1489	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234	233	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235	230	sseli 3932	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236	139	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237	147	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℂ)
238	21	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ≠ 0)
239	235, 236, 237, 238	divsubdird 12036	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
240	239	adantl 486	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
241	240	mpteq2dva 5203	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))))
242		resmpt 6038	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))))
243	230, 242	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴)))
244		eqid 2762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴)))
245	244	divccncf 25076	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ))
246	147, 21, 245	mp2an 704	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ)
247		rescncf 25067	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248	230, 246, 247	mp2 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249	243, 248	eqeltrri 2859	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250	249	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251	139, 147, 21	divcli 11963	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (𝐵 − 𝐴)) ∈ ℂ
252		cncfmptc 25082	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 / (𝐵 − 𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253	251, 230, 231, 252	mp3an 1489	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254	253	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255	223, 225, 250, 254	cncfmpt2f 25085	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256	241, 255	eqeltrd 2862	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257		cncfmptc 25082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
258	61, 230, 231, 257	mp3an 1489	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259	258	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260	223, 225, 259, 234	cncfmpt2f 25085	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹 − 𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261	256, 260	mulcncf 25616	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262	223, 228, 234, 261	cncfmpt2f 25085	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263	226, 262	eqeltrid 2866	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
264	31	mpteq2i 5206	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
265		cncfmptc 25082	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
266	8, 230, 231, 265	mp3an 1489	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267	266	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268		cncfmptc 25082	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
269	26, 230, 231, 268	mp3an 1489	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270	269	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271	223, 225, 270, 267	cncfmpt2f 25085	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷 − 𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272	256, 271	mulcncf 25616	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273	223, 228, 267, 272	cncfmpt2f 25085	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274	264, 273	eqeltrid 2866	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275	223, 225, 263, 274	cncfmpt2f 25085	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276	275	mptru 1576	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277		cniccibl 26011	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹)
278	1, 2, 276, 277	mp3an 1489	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹
279	222, 278	eqeltri 2858	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
280	279	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
281	213, 215, 218, 221, 280	iblss2 25976	. . . . 5 ⊢ (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
282	193, 281	ax-mp 5	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
283		dmarea 27133	. . . 4 ⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹))
284	96, 212, 282, 283	mpbir3an 1359	. . 3 ⊢ 𝑆 ∈ dom area
285		areaval 27140	. . 3 ⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286	284, 285	ax-mp 5	. 2 ⊢ (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287		itgeq2 25948	. . . 4 ⊢ (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
288	191	a1i 11	. . . 4 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0))
289	287, 288	mprg 3084	. . 3 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
290		itgss2 25983	. . . 4 ⊢ ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
291	4, 290	ax-mp 5	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
292	61, 58	addcli 11221	. . . . . 6 ⊢ (𝐹 + 𝐸) ∈ ℂ
293		2cnne0 12459	. . . . . 6 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
294		div32 11898	. . . . . 6 ⊢ (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)))
295	292, 293, 147, 294	mp3an 1489	. . . . 5 ⊢ (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
296	26, 8	addcli 11221	. . . . . 6 ⊢ (𝐷 + 𝐶) ∈ ℂ
297		div32 11898	. . . . . 6 ⊢ (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
298	296, 293, 147, 297	mp3an 1489	. . . . 5 ⊢ (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
299	295, 298	oveq12i 7424	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴))) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
300		2cn 12322	. . . . . 6 ⊢ 2 ∈ ℂ
301		2ne0 12353	. . . . . 6 ⊢ 2 ≠ 0
302	292, 300, 301	divcli 11963	. . . . 5 ⊢ ((𝐹 + 𝐸) / 2) ∈ ℂ
303	296, 300, 301	divcli 11963	. . . . 5 ⊢ ((𝐷 + 𝐶) / 2) ∈ ℂ
304	302, 303, 147	subdiri 11670	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)))
305	114	adantl 486	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306	263	mptru 1576	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307		cniccibl 26011	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
308	1, 2, 306, 307	mp3an 1489	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹
309	308	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
310	113	adantl 486	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311	274	mptru 1576	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312		cniccibl 26011	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
313	1, 2, 311, 312	mp3an 1489	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹
314	313	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
315	305, 309, 310, 314	itgsub 25996	. . . . . 6 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316	315	mptru 1576	. . . . 5 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
317	58, 300, 301	divcan4i 11968	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) / 2) = 𝐸
318	317	oveq1i 7422	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = (𝐸 · (𝐵 − 𝐴))
319	58, 300	mulcli 11222	. . . . . . . . . . 11 ⊢ (𝐸 · 2) ∈ ℂ
320		div32 11898	. . . . . . . . . . 11 ⊢ (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2)))
321	319, 293, 147, 320	mp3an 1489	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
322	318, 321	eqtr3i 2787	. . . . . . . . 9 ⊢ (𝐸 · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
323	322	oveq1i 7422	. . . . . . . 8 ⊢ ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
324		itgeq2 25948	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥)
325	66	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
326	324, 325	mprg 3084	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥
327	57	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328		cniccibl 26011	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
329	1, 2, 233, 328	mp3an 1489	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹
330	329	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
331	126	adantl 486	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
332	60	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333	332, 327	resubcld 11648	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹 − 𝐸) ∈ ℝ)
334	331, 333	remulcld 11245	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) ∈ ℝ)
335	261	mptru 1576	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336		cniccibl 26011	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
337	1, 2, 335, 336	mp3an 1489	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹
338	337	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
339	327, 330, 334, 338	itgadd 25995	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥))
340	339	mptru 1576	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
341		iccmbl 25736	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
342	1, 2, 341	mp2an 704	. . . . . . . . . . . 12 ⊢ (𝐴[,]𝐵) ∈ dom vol
343		mblvol 25700	. . . . . . . . . . . . . . 15 ⊢ ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344	342, 343	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
345	1, 2, 17	ltleii 11339	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ≤ 𝐵
346		ovolicc 25693	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
347	1, 2, 345, 346	mp3an 1489	. . . . . . . . . . . . . 14 ⊢ (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
348	344, 347	eqtri 2785	. . . . . . . . . . . . 13 ⊢ (vol‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
349	348, 12	eqeltri 2858	. . . . . . . . . . . 12 ⊢ (vol‘(𝐴[,]𝐵)) ∈ ℝ
350		itgconst 25989	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351	342, 349, 58, 350	mp3an 1489	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352	348	oveq2i 7423	. . . . . . . . . . 11 ⊢ (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵 − 𝐴))
353	351, 352	eqtri 2785	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵 − 𝐴))
354	61	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐹 ∈ ℂ)
355	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐸 ∈ ℂ)
356	354, 355	subcld 11575	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐹 − 𝐸) ∈ ℂ)
357	256	mptru 1576	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358		cniccibl 26011	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
359	1, 2, 357, 358	mp3an 1489	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹
360	359	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
361	356, 331, 360	itgmulc2 26004	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
362	361	mptru 1576	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
363		itgeq2 25948	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) → ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
364	137	recnd 11243	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℂ)
365	364, 237, 238	divrec2d 12001	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)))
366	363, 365	mprg 3084	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
367	5	adantl 486	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368		cncfmptid 25083	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369	230, 231, 368	mp2an 704	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370		cniccibl 26011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
371	1, 2, 369, 370	mp3an 1489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹
372	371	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
373	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374		cncfmptc 25082	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375	139, 230, 231, 374	mp3an 1489	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376		cniccibl 26011	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
377	1, 2, 375, 376	mp3an 1489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹
378	377	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
379	367, 372, 373, 378	itgsub 25996	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥))
380	379	mptru 1576	. . . . . . . . . . . . . . . . . 18 ⊢ ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥)
381	1	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐴 ∈ ℝ)
382	2	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐵 ∈ ℝ)
383	345	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐴 ≤ 𝐵)
384		1nn0 12526	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
385	384	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 1 ∈ ℕ₀)
386	381, 382, 383, 385	itgpowd 26220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387	386	mptru 1576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388		1p1e2 12370	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
389	388	oveq2i 7423	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390	387, 389	eqtri 2785	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391		itgeq2 25948	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392	235	exp1d 14184	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393	391, 392	mprg 3084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394	388	oveq2i 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵↑(1 + 1)) = (𝐵↑2)
395	388	oveq2i 7423	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴↑(1 + 1)) = (𝐴↑2)
396	394, 395	oveq12i 7424	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397	396	oveq1i 7422	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398	390, 393, 397	3eqtr3i 2793	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399		itgconst 25989	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400	342, 349, 139, 399	mp3an 1489	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401	348	oveq2i 7423	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵 − 𝐴))
402	400, 401	eqtri 2785	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵 − 𝐴))
403	398, 402	oveq12i 7424	. . . . . . . . . . . . . . . . . 18 ⊢ (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
404	380, 403	eqtri 2785	. . . . . . . . . . . . . . . . 17 ⊢ ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
405	404	oveq2i 7423	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴))))
406	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ∈ ℂ)
407	139	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐴 ∈ ℂ)
408	406, 407	subcld 11575	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ∈ ℂ)
409	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ≠ 𝐴)
410	406, 407, 409	subne0d 11584	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ≠ 0)
411	408, 410	reccld 11990	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (1 / (𝐵 − 𝐴)) ∈ ℂ)
412	411	mptru 1576	. . . . . . . . . . . . . . . . 17 ⊢ (1 / (𝐵 − 𝐴)) ∈ ℂ
413	14	sqcli 14224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵↑2) ∈ ℂ
414	139	sqcli 14224	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴↑2) ∈ ℂ
415	413, 414	subcli 11540	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416	415, 300, 301	divcli 11963	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417	139, 147	mulcli 11222	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 · (𝐵 − 𝐴)) ∈ ℂ
418	412, 416, 417	subdii 11669	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
419	405, 418	eqtri 2785	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
420	137	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 − 𝐴) ∈ ℝ)
421	367, 372, 373, 378	iblsub 25992	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 − 𝐴)) ∈ 𝐿¹)
422	411, 420, 421	itgmulc2 26004	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
423	422	mptru 1576	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
424	412, 417	mulcomi 11223	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
425	417, 147, 21	divreci 11966	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
426	139, 147, 21	divcan4i 11968	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = 𝐴
427	424, 425, 426	3eqtr2i 2791	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = 𝐴
428	427	oveq2i 7423	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429	419, 423, 428	3eqtr3i 2793	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430	366, 429	eqtri 2785	. . . . . . . . . . . . 13 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
431	14, 139	subsqi 14256	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵 − 𝐴))
432	431	oveq1i 7422	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2)
433	432	oveq2i 7423	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
434	431, 415	eqeltrri 2859	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) · (𝐵 − 𝐴)) ∈ ℂ
435	412, 434, 300, 301	divassi 11977	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
436	412, 434	mulcomi 11223	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
437	434, 147, 21	divreci 11966	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
438	14, 139	addcli 11221	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 + 𝐴) ∈ ℂ
439	438, 147, 21	divcan4i 11968	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (𝐵 + 𝐴)
440	436, 437, 439	3eqtr2i 2791	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (𝐵 + 𝐴)
441	440	oveq1i 7422	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442	433, 435, 441	3eqtr2i 2791	. . . . . . . . . . . . . 14 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443	442	oveq1i 7422	. . . . . . . . . . . . 13 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444	139, 300	mulcli 11222	. . . . . . . . . . . . . . 15 ⊢ (𝐴 · 2) ∈ ℂ
445		divsubdir 11914	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446	438, 444, 293, 445	mp3an 1489	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
447	14, 139, 444	addsubassi 11555	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448		subsub2 11492	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
449	14, 444, 139, 448	mp3an 1489	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450	139	times2i 12385	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
451	450	oveq1i 7422	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452	139, 139	pncan3oi 11479	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 + 𝐴) − 𝐴) = 𝐴
453	451, 452	eqtri 2785	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · 2) − 𝐴) = 𝐴
454	453	oveq2i 7423	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 − 𝐴)
455	447, 449, 454	3eqtr2i 2791	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 − 𝐴)
456	455	oveq1i 7422	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵 − 𝐴) / 2)
457	139, 300, 301	divcan4i 11968	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 · 2) / 2) = 𝐴
458	457	oveq2i 7423	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459	446, 456, 458	3eqtr3ri 2794	. . . . . . . . . . . . 13 ⊢ (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵 − 𝐴) / 2)
460	430, 443, 459	3eqtri 2789	. . . . . . . . . . . 12 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ((𝐵 − 𝐴) / 2)
461	460	oveq2i 7423	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
462		itgeq2 25948	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) → ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
463	61, 58	subcli 11540	. . . . . . . . . . . . . 14 ⊢ (𝐹 − 𝐸) ∈ ℂ
464	463	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐹 − 𝐸) ∈ ℂ)
465	464, 127	mulcomd 11236	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
466	462, 465	mprg 3084	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥
467	362, 461, 466	3eqtr3ri 2794	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥 = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
468	353, 467	oveq12i 7424	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥) = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
469	326, 340, 468	3eqtri 2789	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
470	147, 300, 301	divcli 11963	. . . . . . . . 9 ⊢ ((𝐵 − 𝐴) / 2) ∈ ℂ
471	319, 463, 470	adddiri 11228	. . . . . . . 8 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
472	323, 469, 471	3eqtr4i 2795	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2))
473		addsub12 11476	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸)))
474	61, 319, 58, 473	mp3an 1489	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸))
475	58	times2i 12385	. . . . . . . . . . . 12 ⊢ (𝐸 · 2) = (𝐸 + 𝐸)
476	475	oveq1i 7422	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
477	58, 58	pncan3oi 11479	. . . . . . . . . . 11 ⊢ ((𝐸 + 𝐸) − 𝐸) = 𝐸
478	476, 477	eqtri 2785	. . . . . . . . . 10 ⊢ ((𝐸 · 2) − 𝐸) = 𝐸
479	478	oveq2i 7423	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480	474, 479	eqtr3i 2787	. . . . . . . 8 ⊢ ((𝐸 · 2) + (𝐹 − 𝐸)) = (𝐹 + 𝐸)
481	480	oveq1i 7422	. . . . . . 7 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
482	472, 481	eqtri 2785	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
483	8, 300, 301	divcan4i 11968	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) / 2) = 𝐶
484	483	oveq1i 7422	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = (𝐶 · (𝐵 − 𝐴))
485	8, 300	mulcli 11222	. . . . . . . . . . 11 ⊢ (𝐶 · 2) ∈ ℂ
486		div32 11898	. . . . . . . . . . 11 ⊢ (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2)))
487	485, 293, 147, 486	mp3an 1489	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
488	484, 487	eqtr3i 2787	. . . . . . . . 9 ⊢ (𝐶 · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
489	488	oveq1i 7422	. . . . . . . 8 ⊢ ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
490	31	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
491	490	itgeq2dv 25952	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥)
492	491	mptru 1576	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥
493	7	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494		cniccibl 26011	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
495	1, 2, 266, 494	mp3an 1489	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹
496	495	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
497	25	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498	497, 493	resubcld 11648	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷 − 𝐶) ∈ ℝ)
499	331, 498	remulcld 11245	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) ∈ ℝ)
500	272	mptru 1576	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501		cniccibl 26011	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
502	1, 2, 500, 501	mp3an 1489	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹
503	502	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
504	493, 496, 499, 503	itgadd 25995	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥))
505	504	mptru 1576	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
506		itgconst 25989	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507	342, 349, 8, 506	mp3an 1489	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508	348	oveq2i 7423	. . . . . . . . . . 11 ⊢ (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵 − 𝐴))
509	507, 508	eqtri 2785	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵 − 𝐴))
510	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐷 ∈ ℂ)
511	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐶 ∈ ℂ)
512	510, 511	subcld 11575	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐷 − 𝐶) ∈ ℂ)
513	512, 331, 360	itgmulc2 26004	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
514	513	mptru 1576	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
515	460	oveq2i 7423	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
516		itgeq2 25948	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) → ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
517	26, 8	subcli 11540	. . . . . . . . . . . . . 14 ⊢ (𝐷 − 𝐶) ∈ ℂ
518	517	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 − 𝐶) ∈ ℂ)
519	518, 127	mulcomd 11236	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
520	516, 519	mprg 3084	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥
521	514, 515, 520	3eqtr3ri 2794	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥 = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
522	509, 521	oveq12i 7424	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥) = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
523	492, 505, 522	3eqtri 2789	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
524	485, 517, 470	adddiri 11228	. . . . . . . 8 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
525	489, 523, 524	3eqtr4i 2795	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2))
526		addsub12 11476	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶)))
527	26, 485, 8, 526	mp3an 1489	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶))
528	8	times2i 12385	. . . . . . . . . . . 12 ⊢ (𝐶 · 2) = (𝐶 + 𝐶)
529	528	oveq1i 7422	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
530	8, 8	pncan3oi 11479	. . . . . . . . . . 11 ⊢ ((𝐶 + 𝐶) − 𝐶) = 𝐶
531	529, 530	eqtri 2785	. . . . . . . . . 10 ⊢ ((𝐶 · 2) − 𝐶) = 𝐶
532	531	oveq2i 7423	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533	527, 532	eqtr3i 2787	. . . . . . . 8 ⊢ ((𝐶 · 2) + (𝐷 − 𝐶)) = (𝐷 + 𝐶)
534	533	oveq1i 7422	. . . . . . 7 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
535	525, 534	eqtri 2785	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
536	482, 535	oveq12i 7424	. . . . 5 ⊢ (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
537	316, 536	eqtri 2785	. . . 4 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
538	299, 304, 537	3eqtr4ri 2796	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
539	289, 291, 538	3eqtr2i 2791	. 2 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
540	286, 539	eqtri 2785	1 ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 ↔ wb 209 ∧ wa 400 = wceq 1569 ⊤wtru 1570 ∈ wcel 2142 ≠ wne 2957 ∀wral 3078 ∖ cdif 3901 ⊆ wss 3904 ∅c0 4285 ifcif 4486 {csn 4588 ⟨cop 4594 class class class wbr 5108 {copab 5172 ↦ cmpt 5191 × cxp 5658 ^◡ccnv 5659 dom cdm 5660 ↾ cres 5662 “ cima 5663 Fun wfun 6530 ⟶wf 6532 ‘cfv 6536 (class class class)co 7412 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 +∞cpnf 11246 ℝ^*cxr 11248 < clt 11249 ≤ cle 11250 − cmin 11447 / cdiv 11877 2c2 12301 ℕ₀cn0 12510 [,]cicc 13381 ↑cexp 14104 TopOpenctopn 17480 ℂ_fldccnfld 21533 Cn ccn 23392 ×_t ctx 23728 –cn→ccncf 25046 vol*covol 25632 volcvol 25633 𝐿¹cibl 25787 ∫citg 25788 areacarea 27131

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-inf2 9608 ax-cc 10425 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184 ax-addf 11185

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-symdif 4205 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-iin 4958 df-disj 5076 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-of 7676 df-ofr 7677 df-om 7861 df-1st 7984 df-2nd 7985 df-supp 8155 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-2o 8452 df-oadd 8455 df-omul 8456 df-er 8692 df-map 8824 df-pm 8825 df-ixp 8894 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-fsupp 9320 df-fi 9369 df-sup 9400 df-inf 9401 df-oi 9470 df-dju 9894 df-card 9932 df-acn 9935 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-4 12311 df-5 12312 df-6 12313 df-7 12314 df-8 12315 df-9 12316 df-n0 12511 df-z 12598 df-dec 12718 df-uz 12869 df-q 12979 df-rp 13023 df-xneg 13143 df-xadd 13144 df-xmul 13145 df-ioo 13382 df-ioc 13383 df-ico 13384 df-icc 13385 df-fz 13542 df-fzo 13690 df-fl 13832 df-mod 13910 df-seq 14045 df-exp 14105 df-hash 14374 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-limsup 15529 df-clim 15546 df-rlim 15547 df-sum 15745 df-struct 17213 df-sets 17230 df-slot 17248 df-ndx 17260 df-base 17276 df-ress 17297 df-plusg 17329 df-mulr 17330 df-starv 17331 df-sca 17332 df-vsca 17333 df-ip 17334 df-tset 17335 df-ple 17336 df-ds 17338 df-unif 17339 df-hom 17340 df-cco 17341 df-rest 17481 df-topn 17482 df-0g 17500 df-gsum 17501 df-topgen 17502 df-pt 17503 df-prds 17506 df-xrs 17562 df-qtop 17567 df-imas 17568 df-xps 17570 df-mre 17644 df-mrc 17645 df-acs 17647 df-mgm 18704 df-sgrp 18783 df-mnd 18799 df-submnd 18848 df-mulg 19140 df-cntz 19393 df-cmn 19858 df-psmet 21525 df-xmet 21526 df-met 21527 df-bl 21528 df-mopn 21529 df-fbas 21530 df-fg 21531 df-cnfld 21534 df-top 23062 df-topon 23079 df-topsp 23101 df-bases 23114 df-cld 23187 df-ntr 23188 df-cls 23189 df-nei 23266 df-lp 23304 df-perf 23305 df-cn 23395 df-cnp 23396 df-haus 23483 df-cmp 23555 df-tx 23730 df-hmeo 23923 df-fil 24014 df-fm 24106 df-flim 24107 df-flf 24108 df-xms 24488 df-ms 24489 df-tms 24490 df-cncf 25048 df-ovol 25634 df-vol 25635 df-mbf 25789 df-itg1 25790 df-itg2 25791 df-ibl 25792 df-itg 25793 df-0p 25840 df-limc 26036 df-dv 26037 df-area 27132

This theorem is used by: (None)

W3C validator