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 42681

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 13436	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
4	1, 2, 3	mp2an 690	. . . . . . . . 9 ⊢ (𝐴[,]𝐵) ⊆ ℝ
5	4	sseli 3968	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
6	5	adantr 479	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7		areaquad.3	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ∈ ℝ
8	7	recni 11256	. . . . . . . . . . . . . . 15 ⊢ 𝐶 ∈ ℂ
9	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10		resubcl 11552	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 − 𝐴) ∈ ℝ)
11	1, 10	mpan2 689	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝑥 − 𝐴) ∈ ℝ)
12	2, 1	resubcli 11550	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ∈ ℝ
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ∈ ℝ)
14	2	recni 11256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℂ
15	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16		recn 11226	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17		areaquad.7	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 < 𝐵
18	1, 17	gtneii 11354	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ≠ 𝐴
19	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ≠ 𝐴)
20	15, 16, 19	subne0d 11608	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
21	1, 20	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ≠ 0
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
23	11, 13, 22	redivcld 12070	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
24	23	recnd 11270	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
25		areaquad.4	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 ∈ ℝ
26	25	recni 11256	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ∈ ℂ
27	26	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
28	24, 27	mulcld 11262	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) ∈ ℂ)
29	24, 9	mulcld 11262	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶) ∈ ℂ)
30	9, 28, 29	addsub12d 11622	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
31		areaquad.10	. . . . . . . . . . . . . 14 ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
32	24, 27, 9	subdid 11698	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
33	32	oveq2d 7430	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
34	31, 33	eqtrid 2777	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
35		1cnd 11237	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℂ)
36	35, 24, 9	subdird 11699	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
37	8	mullidi 11247	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐶) = 𝐶
38	37	oveq1i 7424	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))
39	36, 38	eqtrdi 2781	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
40	39	oveq2d 7430	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
41	30, 34, 40	3eqtr4d 2775	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)))
42		1red 11243	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℝ)
43	42, 23	resubcld 11670	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
44	43	recnd 11270	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℂ)
45	44, 9	mulcld 11262	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) ∈ ℂ)
46	28, 45	addcomd 11444	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)))
47	44, 9	mulcomd 11263	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
48	24, 27	mulcomd 11263	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) = (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
49	47, 48	oveq12d 7432	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
50	41, 46, 49	3eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
51	7	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
52	51, 43	remulcld 11272	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
53	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
54	53, 23	remulcld 11272	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
55	52, 54	readdcld 11271	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
56	50, 55	eqeltrd 2825	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57		areaquad.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 ∈ ℝ
58	57	recni 11256	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ∈ ℂ
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60		areaquad.6	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 ∈ ℝ
61	60	recni 11256	. . . . . . . . . . . . . . . 16 ⊢ 𝐹 ∈ ℂ
62	61	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
63	24, 62	mulcld 11262	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) ∈ ℂ)
64	24, 59	mulcld 11262	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸) ∈ ℂ)
65	59, 63, 64	addsub12d 11622	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
66		areaquad.11	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
67	24, 62, 59	subdid 11698	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
68	67	oveq2d 7430	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
69	66, 68	eqtrid 2777	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
70	35, 24, 59	subdird 11699	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
71	58	mullidi 11247	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐸) = 𝐸
72	71	oveq1i 7424	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))
73	70, 72	eqtrdi 2781	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
74	73	oveq2d 7430	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
75	65, 69, 74	3eqtr4d 2775	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)))
76	44, 59	mulcld 11262	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) ∈ ℂ)
77	63, 76	addcomd 11444	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)))
78	44, 59	mulcomd 11263	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
79	24, 62	mulcomd 11263	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) = (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
80	78, 79	oveq12d 7432	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
81	75, 77, 80	3eqtrd 2769	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
82	57	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
83	82, 43	remulcld 11272	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
84	60	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
85	84, 23	remulcld 11272	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
86	83, 85	readdcld 11271	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
87	81, 86	eqeltrd 2825	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88		iccssre 13436	. . . . . . . . . 10 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
89	56, 87, 88	syl2anc 582	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
90	5, 89	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
91	90	sselda 3972	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
92	6, 91	jca 510	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
93	92	ssopab2i 5544	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94		areaquad.12	. . . . 5 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95		df-xp 5676	. . . . 5 ⊢ (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
96	93, 94, 95	3sstr4i 4015	. . . 4 ⊢ 𝑆 ⊆ (ℝ × ℝ)
97		iftrue 4528	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (𝑉 − 𝑈))
98		nfv 1909	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑥 ∈ (𝐴[,]𝐵)
99		nfopab2 5212	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
100	94, 99	nfcxfr 2890	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝑆
101		nfcv 2892	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦{𝑥}
102	100, 101	nfima 6064	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑆 “ {𝑥})
103		nfcv 2892	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑈[,]𝑉)
104		vex 3467	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
105		vex 3467	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
106	104, 105	elimasn 6086	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
107	94	eleq2i 2817	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108		opabidw 5518	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109	106, 107, 108	3bitri 296	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110	109	baib 534	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
111	98, 102, 103, 110	eqrd 3991	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112	111	fveq2d 6894	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
113	5, 56	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
114	5, 87	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115		iccmbl 25511	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116	113, 114, 115	syl2anc 582	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117		mblvol 25475	. . . . . . . . . . . 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 11270	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
128	127	subidd 11587	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = 0)
129		1red 11243	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
130	2	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
131	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
132	1	rexri 11300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐴 ∈ ℝ^*
133	2	rexri 11300	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℝ^*
134		iccleub 13409	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
135	132, 133, 134	mp3an12 1447	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ≤ 𝐵)
136	5, 130, 131, 135	lesub1dd 11858	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ≤ (𝐵 − 𝐴))
137	5, 1, 10	sylancl 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℝ)
138	12	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ)
139	1	recni 11256	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 ∈ ℂ
140	139	subidi 11559	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 − 𝐴) = 0
141	131, 130, 131	ltsub1d 11851	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐴) < (𝐵 − 𝐴)))
142	17, 141	mpbii 232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) < (𝐵 − 𝐴))
143	140, 142	eqbrtrrid 5177	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵 − 𝐴))
144		lediv1 12107	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 − 𝐴) ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ ∧ ((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴))) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
145	137, 138, 138, 143, 144	syl112anc 1371	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
146	136, 145	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴)))
147	12	recni 11256	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 − 𝐴) ∈ ℂ
148	147, 21	dividi 11975	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 − 𝐴) / (𝐵 − 𝐴)) = 1
149	146, 148	breqtrdi 5182	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ 1)
150	126, 129, 126, 149	lesub1dd 11858	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
151	128, 150	eqbrtrrd 5165	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
152		areaquad.8	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ≤ 𝐸
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐶 ≤ 𝐸)
154	123, 124, 125, 151, 153	lemul1ad 12181	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
155	25	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
156	60	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157	138, 143	elrpd 13043	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ⁺)
158		iccgelb 13410	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥)
159	132, 133, 158	mp3an12 1447	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑥)
160	131, 5, 131, 159	lesub1dd 11858	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) ≤ (𝑥 − 𝐴))
161	140, 160	eqbrtrrid 5177	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥 − 𝐴))
162	137, 157, 161	divge0d 13086	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥 − 𝐴) / (𝐵 − 𝐴)))
163		areaquad.9	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ≤ 𝐹
164	163	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ≤ 𝐹)
165	155, 156, 126, 162, 164	lemul1ad 12181	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
166	119, 120, 121, 122, 154, 165	le2addd 11861	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
167	5, 50	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
168	5, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
169	166, 167, 168	3brtr4d 5173	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ≤ 𝑉)
170		ovolicc 25468	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈 ≤ 𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
171	113, 114, 169, 170	syl3anc 1368	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
172	112, 118, 171	3eqtrd 2769	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉 − 𝑈))
173	97, 172	eqtr4d 2768	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174		iffalse 4531	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = 0)
175		nfv 1909	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176		nfcv 2892	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∅
177	109	simplbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178		noel 4324	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑦 ∈ ∅
179	178	pm2.21i 119	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180	177, 179	pm5.21ni 376	. . . . . . . . . . . . 13 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181	175, 102, 176, 180	eqrd 3991	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182	181	fveq2d 6894	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183		0mbl 25484	. . . . . . . . . . . . 13 ⊢ ∅ ∈ dom vol
184		mblvol 25475	. . . . . . . . . . . . 13 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185	183, 184	ax-mp 5	. . . . . . . . . . . 12 ⊢ (vol‘∅) = (vol*‘∅)
186		ovol0 25438	. . . . . . . . . . . 12 ⊢ (vol*‘∅) = 0
187	185, 186	eqtri 2753	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
188	182, 187	eqtrdi 2781	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189	174, 188	eqtr4d 2768	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190	173, 189	pm2.61i 182	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191	190	eqcomi 2734	. . . . . . 7 ⊢ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0)
192	87, 56	resubcld 11670	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → (𝑉 − 𝑈) ∈ ℝ)
193		0re 11244	. . . . . . . 8 ⊢ 0 ∈ ℝ
194		ifcl 4567	. . . . . . . 8 ⊢ (((𝑉 − 𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
195	192, 193, 194	sylancl 584	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
196	191, 195	eqeltrid 2829	. . . . . 6 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197		volf 25474	. . . . . . . 8 ⊢ vol:dom vol⟶(0[,]+∞)
198		ffun 6718	. . . . . . . 8 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
199	197, 198	ax-mp 5	. . . . . . 7 ⊢ Fun vol
200		iftrue 4528	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201	111, 200	eqtr4d 2768	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202		iffalse 4531	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203	181, 202	eqtr4d 2768	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204	201, 203	pm2.61i 182	. . . . . . . 8 ⊢ (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
205	56, 87, 115	syl2anc 582	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206	183	a1i 11	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207	205, 206	ifcld 4568	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208	204, 207	eqeltrid 2829	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209		fvimacnv 7055	. . . . . . 7 ⊢ ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
210	199, 208, 209	sylancr 585	. . . . . 6 ⊢ (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
211	196, 210	mpbid 231	. . . . 5 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ))
212	211	rgen 3053	. . . 4 ⊢ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)
213	4	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214		rembl 25485	. . . . . . 7 ⊢ ℝ ∈ dom vol
215	214	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → ℝ ∈ dom vol)
216	114, 113	resubcld 11670	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑉 − 𝑈) ∈ ℝ)
217	172, 216	eqeltrd 2825	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218	217	adantl 480	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219		eldifn 4118	. . . . . . . 8 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220	219, 188	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221	220	adantl 480	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222	172	mpteq2ia 5244	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈))
223		eqid 2725	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
224	223	subcn 24798	. . . . . . . . . . . 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 5246	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
227	223	addcn 24797	. . . . . . . . . . . . . 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 11193	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
230	4, 229	sstri 3981	. . . . . . . . . . . . . . 15 ⊢ (𝐴[,]𝐵) ⊆ ℂ
231		ssid 3994	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
232		cncfmptc 24848	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
233	58, 230, 231, 232	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234	233	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235	230	sseli 3968	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236	139	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237	147	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℂ)
238	21	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ≠ 0)
239	235, 236, 237, 238	divsubdird 12057	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
240	239	adantl 480	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
241	240	mpteq2dva 5241	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))))
242		resmpt 6034	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))))
243	230, 242	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴)))
244		eqid 2725	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴)))
245	244	divccncf 24842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ))
246	147, 21, 245	mp2an 690	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ)
247		rescncf 24833	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248	230, 246, 247	mp2 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249	243, 248	eqeltrri 2822	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250	249	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251	139, 147, 21	divcli 11984	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (𝐵 − 𝐴)) ∈ ℂ
252		cncfmptc 24848	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 / (𝐵 − 𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253	251, 230, 231, 252	mp3an 1457	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254	253	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255	223, 225, 250, 254	cncfmpt2f 24851	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256	241, 255	eqeltrd 2825	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257		cncfmptc 24848	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
258	61, 230, 231, 257	mp3an 1457	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259	258	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260	223, 225, 259, 234	cncfmpt2f 24851	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹 − 𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261	256, 260	mulcncf 25390	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262	223, 228, 234, 261	cncfmpt2f 24851	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263	226, 262	eqeltrid 2829	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
264	31	mpteq2i 5246	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
265		cncfmptc 24848	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
266	8, 230, 231, 265	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267	266	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268		cncfmptc 24848	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
269	26, 230, 231, 268	mp3an 1457	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270	269	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271	223, 225, 270, 267	cncfmpt2f 24851	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷 − 𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272	256, 271	mulcncf 25390	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273	223, 228, 267, 272	cncfmpt2f 24851	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274	264, 273	eqeltrid 2829	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275	223, 225, 263, 274	cncfmpt2f 24851	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276	275	mptru 1540	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277		cniccibl 25786	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹)
278	1, 2, 276, 277	mp3an 1457	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹
279	222, 278	eqeltri 2821	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
280	279	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
281	213, 215, 218, 221, 280	iblss2 25751	. . . . 5 ⊢ (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
282	193, 281	ax-mp 5	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
283		dmarea 26905	. . . 4 ⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹))
284	96, 212, 282, 283	mpbir3an 1338	. . 3 ⊢ 𝑆 ∈ dom area
285		areaval 26912	. . 3 ⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286	284, 285	ax-mp 5	. 2 ⊢ (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287		itgeq2 25723	. . . 4 ⊢ (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
288	191	a1i 11	. . . 4 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0))
289	287, 288	mprg 3057	. . 3 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
290		itgss2 25758	. . . 4 ⊢ ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
291	4, 290	ax-mp 5	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
292	61, 58	addcli 11248	. . . . . 6 ⊢ (𝐹 + 𝐸) ∈ ℂ
293		2cnne0 12450	. . . . . 6 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
294		div32 11920	. . . . . 6 ⊢ (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)))
295	292, 293, 147, 294	mp3an 1457	. . . . 5 ⊢ (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
296	26, 8	addcli 11248	. . . . . 6 ⊢ (𝐷 + 𝐶) ∈ ℂ
297		div32 11920	. . . . . 6 ⊢ (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
298	296, 293, 147, 297	mp3an 1457	. . . . 5 ⊢ (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
299	295, 298	oveq12i 7426	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴))) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
300		2cn 12315	. . . . . 6 ⊢ 2 ∈ ℂ
301		2ne0 12344	. . . . . 6 ⊢ 2 ≠ 0
302	292, 300, 301	divcli 11984	. . . . 5 ⊢ ((𝐹 + 𝐸) / 2) ∈ ℂ
303	296, 300, 301	divcli 11984	. . . . 5 ⊢ ((𝐷 + 𝐶) / 2) ∈ ℂ
304	302, 303, 147	subdiri 11692	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)))
305	114	adantl 480	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306	263	mptru 1540	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307		cniccibl 25786	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
308	1, 2, 306, 307	mp3an 1457	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹
309	308	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
310	113	adantl 480	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311	274	mptru 1540	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312		cniccibl 25786	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
313	1, 2, 311, 312	mp3an 1457	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹
314	313	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
315	305, 309, 310, 314	itgsub 25771	. . . . . 6 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316	315	mptru 1540	. . . . 5 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
317	58, 300, 301	divcan4i 11989	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) / 2) = 𝐸
318	317	oveq1i 7424	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = (𝐸 · (𝐵 − 𝐴))
319	58, 300	mulcli 11249	. . . . . . . . . . 11 ⊢ (𝐸 · 2) ∈ ℂ
320		div32 11920	. . . . . . . . . . 11 ⊢ (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2)))
321	319, 293, 147, 320	mp3an 1457	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
322	318, 321	eqtr3i 2755	. . . . . . . . 9 ⊢ (𝐸 · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
323	322	oveq1i 7424	. . . . . . . 8 ⊢ ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
324		itgeq2 25723	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥)
325	66	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
326	324, 325	mprg 3057	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥
327	57	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328		cniccibl 25786	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
329	1, 2, 233, 328	mp3an 1457	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹
330	329	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
331	126	adantl 480	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
332	60	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333	332, 327	resubcld 11670	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹 − 𝐸) ∈ ℝ)
334	331, 333	remulcld 11272	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) ∈ ℝ)
335	261	mptru 1540	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336		cniccibl 25786	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
337	1, 2, 335, 336	mp3an 1457	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹
338	337	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
339	327, 330, 334, 338	itgadd 25770	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥))
340	339	mptru 1540	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
341		iccmbl 25511	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
342	1, 2, 341	mp2an 690	. . . . . . . . . . . 12 ⊢ (𝐴[,]𝐵) ∈ dom vol
343		mblvol 25475	. . . . . . . . . . . . . . 15 ⊢ ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344	342, 343	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
345	1, 2, 17	ltleii 11365	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ≤ 𝐵
346		ovolicc 25468	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
347	1, 2, 345, 346	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
348	344, 347	eqtri 2753	. . . . . . . . . . . . 13 ⊢ (vol‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
349	348, 12	eqeltri 2821	. . . . . . . . . . . 12 ⊢ (vol‘(𝐴[,]𝐵)) ∈ ℝ
350		itgconst 25764	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351	342, 349, 58, 350	mp3an 1457	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352	348	oveq2i 7425	. . . . . . . . . . 11 ⊢ (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵 − 𝐴))
353	351, 352	eqtri 2753	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵 − 𝐴))
354	61	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐹 ∈ ℂ)
355	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐸 ∈ ℂ)
356	354, 355	subcld 11599	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐹 − 𝐸) ∈ ℂ)
357	256	mptru 1540	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358		cniccibl 25786	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
359	1, 2, 357, 358	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹
360	359	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
361	356, 331, 360	itgmulc2 25779	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
362	361	mptru 1540	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
363		itgeq2 25723	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) → ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
364	137	recnd 11270	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℂ)
365	364, 237, 238	divrec2d 12022	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)))
366	363, 365	mprg 3057	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
367	5	adantl 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368		cncfmptid 24849	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369	230, 231, 368	mp2an 690	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370		cniccibl 25786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
371	1, 2, 369, 370	mp3an 1457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹
372	371	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
373	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374		cncfmptc 24848	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375	139, 230, 231, 374	mp3an 1457	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376		cniccibl 25786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
377	1, 2, 375, 376	mp3an 1457	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹
378	377	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
379	367, 372, 373, 378	itgsub 25771	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥))
380	379	mptru 1540	. . . . . . . . . . . . . . . . . 18 ⊢ ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥)
381	1	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐴 ∈ ℝ)
382	2	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐵 ∈ ℝ)
383	345	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐴 ≤ 𝐵)
384		1nn0 12516	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
385	384	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 1 ∈ ℕ₀)
386	381, 382, 383, 385	itgpowd 26001	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387	386	mptru 1540	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388		1p1e2 12365	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
389	388	oveq2i 7425	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390	387, 389	eqtri 2753	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391		itgeq2 25723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392	235	exp1d 14135	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393	391, 392	mprg 3057	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394	388	oveq2i 7425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵↑(1 + 1)) = (𝐵↑2)
395	388	oveq2i 7425	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴↑(1 + 1)) = (𝐴↑2)
396	394, 395	oveq12i 7426	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397	396	oveq1i 7424	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398	390, 393, 397	3eqtr3i 2761	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399		itgconst 25764	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400	342, 349, 139, 399	mp3an 1457	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401	348	oveq2i 7425	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵 − 𝐴))
402	400, 401	eqtri 2753	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵 − 𝐴))
403	398, 402	oveq12i 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
404	380, 403	eqtri 2753	. . . . . . . . . . . . . . . . 17 ⊢ ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
405	404	oveq2i 7425	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴))))
406	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ∈ ℂ)
407	139	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐴 ∈ ℂ)
408	406, 407	subcld 11599	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ∈ ℂ)
409	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ≠ 𝐴)
410	406, 407, 409	subne0d 11608	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ≠ 0)
411	408, 410	reccld 12011	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (1 / (𝐵 − 𝐴)) ∈ ℂ)
412	411	mptru 1540	. . . . . . . . . . . . . . . . 17 ⊢ (1 / (𝐵 − 𝐴)) ∈ ℂ
413	14	sqcli 14174	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵↑2) ∈ ℂ
414	139	sqcli 14174	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴↑2) ∈ ℂ
415	413, 414	subcli 11564	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416	415, 300, 301	divcli 11984	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417	139, 147	mulcli 11249	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 · (𝐵 − 𝐴)) ∈ ℂ
418	412, 416, 417	subdii 11691	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
419	405, 418	eqtri 2753	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
420	137	adantl 480	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 − 𝐴) ∈ ℝ)
421	367, 372, 373, 378	iblsub 25767	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 − 𝐴)) ∈ 𝐿¹)
422	411, 420, 421	itgmulc2 25779	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
423	422	mptru 1540	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
424	412, 417	mulcomi 11250	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
425	417, 147, 21	divreci 11987	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
426	139, 147, 21	divcan4i 11989	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = 𝐴
427	424, 425, 426	3eqtr2i 2759	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = 𝐴
428	427	oveq2i 7425	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429	419, 423, 428	3eqtr3i 2761	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430	366, 429	eqtri 2753	. . . . . . . . . . . . 13 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
431	14, 139	subsqi 14206	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵 − 𝐴))
432	431	oveq1i 7424	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2)
433	432	oveq2i 7425	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
434	431, 415	eqeltrri 2822	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) · (𝐵 − 𝐴)) ∈ ℂ
435	412, 434, 300, 301	divassi 11998	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
436	412, 434	mulcomi 11250	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
437	434, 147, 21	divreci 11987	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
438	14, 139	addcli 11248	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 + 𝐴) ∈ ℂ
439	438, 147, 21	divcan4i 11989	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (𝐵 + 𝐴)
440	436, 437, 439	3eqtr2i 2759	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (𝐵 + 𝐴)
441	440	oveq1i 7424	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442	433, 435, 441	3eqtr2i 2759	. . . . . . . . . . . . . 14 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443	442	oveq1i 7424	. . . . . . . . . . . . 13 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444	139, 300	mulcli 11249	. . . . . . . . . . . . . . 15 ⊢ (𝐴 · 2) ∈ ℂ
445		divsubdir 11936	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446	438, 444, 293, 445	mp3an 1457	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
447	14, 139, 444	addsubassi 11579	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448		subsub2 11516	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
449	14, 444, 139, 448	mp3an 1457	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450	139	times2i 12379	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
451	450	oveq1i 7424	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452	139, 139	pncan3oi 11504	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 + 𝐴) − 𝐴) = 𝐴
453	451, 452	eqtri 2753	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · 2) − 𝐴) = 𝐴
454	453	oveq2i 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 − 𝐴)
455	447, 449, 454	3eqtr2i 2759	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 − 𝐴)
456	455	oveq1i 7424	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵 − 𝐴) / 2)
457	139, 300, 301	divcan4i 11989	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 · 2) / 2) = 𝐴
458	457	oveq2i 7425	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459	446, 456, 458	3eqtr3ri 2762	. . . . . . . . . . . . 13 ⊢ (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵 − 𝐴) / 2)
460	430, 443, 459	3eqtri 2757	. . . . . . . . . . . 12 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ((𝐵 − 𝐴) / 2)
461	460	oveq2i 7425	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
462		itgeq2 25723	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) → ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
463	61, 58	subcli 11564	. . . . . . . . . . . . . 14 ⊢ (𝐹 − 𝐸) ∈ ℂ
464	463	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐹 − 𝐸) ∈ ℂ)
465	464, 127	mulcomd 11263	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
466	462, 465	mprg 3057	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥
467	362, 461, 466	3eqtr3ri 2762	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥 = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
468	353, 467	oveq12i 7426	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥) = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
469	326, 340, 468	3eqtri 2757	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
470	147, 300, 301	divcli 11984	. . . . . . . . 9 ⊢ ((𝐵 − 𝐴) / 2) ∈ ℂ
471	319, 463, 470	adddiri 11255	. . . . . . . 8 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
472	323, 469, 471	3eqtr4i 2763	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2))
473		addsub12 11501	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸)))
474	61, 319, 58, 473	mp3an 1457	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸))
475	58	times2i 12379	. . . . . . . . . . . 12 ⊢ (𝐸 · 2) = (𝐸 + 𝐸)
476	475	oveq1i 7424	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
477	58, 58	pncan3oi 11504	. . . . . . . . . . 11 ⊢ ((𝐸 + 𝐸) − 𝐸) = 𝐸
478	476, 477	eqtri 2753	. . . . . . . . . 10 ⊢ ((𝐸 · 2) − 𝐸) = 𝐸
479	478	oveq2i 7425	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480	474, 479	eqtr3i 2755	. . . . . . . 8 ⊢ ((𝐸 · 2) + (𝐹 − 𝐸)) = (𝐹 + 𝐸)
481	480	oveq1i 7424	. . . . . . 7 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
482	472, 481	eqtri 2753	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
483	8, 300, 301	divcan4i 11989	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) / 2) = 𝐶
484	483	oveq1i 7424	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = (𝐶 · (𝐵 − 𝐴))
485	8, 300	mulcli 11249	. . . . . . . . . . 11 ⊢ (𝐶 · 2) ∈ ℂ
486		div32 11920	. . . . . . . . . . 11 ⊢ (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2)))
487	485, 293, 147, 486	mp3an 1457	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
488	484, 487	eqtr3i 2755	. . . . . . . . 9 ⊢ (𝐶 · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
489	488	oveq1i 7424	. . . . . . . 8 ⊢ ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
490	31	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
491	490	itgeq2dv 25727	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥)
492	491	mptru 1540	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥
493	7	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494		cniccibl 25786	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
495	1, 2, 266, 494	mp3an 1457	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹
496	495	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
497	25	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498	497, 493	resubcld 11670	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷 − 𝐶) ∈ ℝ)
499	331, 498	remulcld 11272	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) ∈ ℝ)
500	272	mptru 1540	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501		cniccibl 25786	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
502	1, 2, 500, 501	mp3an 1457	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹
503	502	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
504	493, 496, 499, 503	itgadd 25770	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥))
505	504	mptru 1540	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
506		itgconst 25764	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507	342, 349, 8, 506	mp3an 1457	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508	348	oveq2i 7425	. . . . . . . . . . 11 ⊢ (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵 − 𝐴))
509	507, 508	eqtri 2753	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵 − 𝐴))
510	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐷 ∈ ℂ)
511	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐶 ∈ ℂ)
512	510, 511	subcld 11599	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐷 − 𝐶) ∈ ℂ)
513	512, 331, 360	itgmulc2 25779	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
514	513	mptru 1540	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
515	460	oveq2i 7425	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
516		itgeq2 25723	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) → ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
517	26, 8	subcli 11564	. . . . . . . . . . . . . 14 ⊢ (𝐷 − 𝐶) ∈ ℂ
518	517	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 − 𝐶) ∈ ℂ)
519	518, 127	mulcomd 11263	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
520	516, 519	mprg 3057	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥
521	514, 515, 520	3eqtr3ri 2762	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥 = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
522	509, 521	oveq12i 7426	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥) = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
523	492, 505, 522	3eqtri 2757	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
524	485, 517, 470	adddiri 11255	. . . . . . . 8 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
525	489, 523, 524	3eqtr4i 2763	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2))
526		addsub12 11501	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶)))
527	26, 485, 8, 526	mp3an 1457	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶))
528	8	times2i 12379	. . . . . . . . . . . 12 ⊢ (𝐶 · 2) = (𝐶 + 𝐶)
529	528	oveq1i 7424	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
530	8, 8	pncan3oi 11504	. . . . . . . . . . 11 ⊢ ((𝐶 + 𝐶) − 𝐶) = 𝐶
531	529, 530	eqtri 2753	. . . . . . . . . 10 ⊢ ((𝐶 · 2) − 𝐶) = 𝐶
532	531	oveq2i 7425	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533	527, 532	eqtr3i 2755	. . . . . . . 8 ⊢ ((𝐶 · 2) + (𝐷 − 𝐶)) = (𝐷 + 𝐶)
534	533	oveq1i 7424	. . . . . . 7 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
535	525, 534	eqtri 2753	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
536	482, 535	oveq12i 7426	. . . . 5 ⊢ (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
537	316, 536	eqtri 2753	. . . 4 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
538	299, 304, 537	3eqtr4ri 2764	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
539	289, 291, 538	3eqtr2i 2759	. 2 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
540	286, 539	eqtri 2753	1 ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 394 = wceq 1533 ⊤wtru 1534 ∈ wcel 2098 ≠ wne 2930 ∀wral 3051 ∖ cdif 3936 ⊆ wss 3939 ∅c0 4316 ifcif 4522 {csn 4622 ⟨cop 4628 class class class wbr 5141 {copab 5203 ↦ cmpt 5224 × cxp 5668 ^◡ccnv 5669 dom cdm 5670 ↾ cres 5672 “ cima 5673 Fun wfun 6535 ⟶wf 6537 ‘cfv 6541 (class class class)co 7414 ℂcc 11134 ℝcr 11135 0cc0 11136 1c1 11137 + caddc 11139 · cmul 11141 +∞cpnf 11273 ℝ^*cxr 11275 < clt 11276 ≤ cle 11277 − cmin 11472 / cdiv 11899 2c2 12295 ℕ₀cn0 12500 [,]cicc 13357 ↑cexp 14056 TopOpenctopn 17400 ℂ_fldccnfld 21281 Cn ccn 23144 ×_t ctx 23480 –cn→ccncf 24812 vol*covol 25407 volcvol 25408 𝐿¹cibl 25562 ∫citg 25563 areacarea 26903

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-rep 5278 ax-sep 5292 ax-nul 5299 ax-pow 5357 ax-pr 5421 ax-un 7736 ax-inf2 9662 ax-cc 10456 ax-cnex 11192 ax-resscn 11193 ax-1cn 11194 ax-icn 11195 ax-addcl 11196 ax-addrcl 11197 ax-mulcl 11198 ax-mulrcl 11199 ax-mulcom 11200 ax-addass 11201 ax-mulass 11202 ax-distr 11203 ax-i2m1 11204 ax-1ne0 11205 ax-1rid 11206 ax-rnegex 11207 ax-rrecex 11208 ax-cnre 11209 ax-pre-lttri 11210 ax-pre-lttrn 11211 ax-pre-ltadd 11212 ax-pre-mulgt0 11213 ax-pre-sup 11214 ax-addf 11215

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3465 df-sbc 3769 df-csb 3885 df-dif 3942 df-un 3944 df-in 3946 df-ss 3956 df-pss 3958 df-symdif 4235 df-nul 4317 df-if 4523 df-pw 4598 df-sn 4623 df-pr 4625 df-tp 4627 df-op 4629 df-uni 4902 df-int 4943 df-iun 4991 df-iin 4992 df-disj 5107 df-br 5142 df-opab 5204 df-mpt 5225 df-tr 5259 df-id 5568 df-eprel 5574 df-po 5582 df-so 5583 df-fr 5625 df-se 5626 df-we 5627 df-xp 5676 df-rel 5677 df-cnv 5678 df-co 5679 df-dm 5680 df-rn 5681 df-res 5682 df-ima 5683 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 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 7417 df-oprab 7418 df-mpo 7419 df-of 7680 df-ofr 7681 df-om 7867 df-1st 7989 df-2nd 7990 df-supp 8162 df-frecs 8283 df-wrecs 8314 df-recs 8388 df-rdg 8427 df-1o 8483 df-2o 8484 df-oadd 8487 df-omul 8488 df-er 8721 df-map 8843 df-pm 8844 df-ixp 8913 df-en 8961 df-dom 8962 df-sdom 8963 df-fin 8964 df-fsupp 9384 df-fi 9432 df-sup 9463 df-inf 9464 df-oi 9531 df-dju 9922 df-card 9960 df-acn 9963 df-pnf 11278 df-mnf 11279 df-xr 11280 df-ltxr 11281 df-le 11282 df-sub 11474 df-neg 11475 df-div 11900 df-nn 12241 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-7 12308 df-8 12309 df-9 12310 df-n0 12501 df-z 12587 df-dec 12706 df-uz 12851 df-q 12961 df-rp 13005 df-xneg 13122 df-xadd 13123 df-xmul 13124 df-ioo 13358 df-ioc 13359 df-ico 13360 df-icc 13361 df-fz 13515 df-fzo 13658 df-fl 13787 df-mod 13865 df-seq 13997 df-exp 14057 df-hash 14320 df-cj 15076 df-re 15077 df-im 15078 df-sqrt 15212 df-abs 15213 df-limsup 15445 df-clim 15462 df-rlim 15463 df-sum 15663 df-struct 17113 df-sets 17130 df-slot 17148 df-ndx 17160 df-base 17178 df-ress 17207 df-plusg 17243 df-mulr 17244 df-starv 17245 df-sca 17246 df-vsca 17247 df-ip 17248 df-tset 17249 df-ple 17250 df-ds 17252 df-unif 17253 df-hom 17254 df-cco 17255 df-rest 17401 df-topn 17402 df-0g 17420 df-gsum 17421 df-topgen 17422 df-pt 17423 df-prds 17426 df-xrs 17481 df-qtop 17486 df-imas 17487 df-xps 17489 df-mre 17563 df-mrc 17564 df-acs 17566 df-mgm 18597 df-sgrp 18676 df-mnd 18692 df-submnd 18738 df-mulg 19026 df-cntz 19270 df-cmn 19739 df-psmet 21273 df-xmet 21274 df-met 21275 df-bl 21276 df-mopn 21277 df-fbas 21278 df-fg 21279 df-cnfld 21282 df-top 22812 df-topon 22829 df-topsp 22851 df-bases 22865 df-cld 22939 df-ntr 22940 df-cls 22941 df-nei 23018 df-lp 23056 df-perf 23057 df-cn 23147 df-cnp 23148 df-haus 23235 df-cmp 23307 df-tx 23482 df-hmeo 23675 df-fil 23766 df-fm 23858 df-flim 23859 df-flf 23860 df-xms 24242 df-ms 24243 df-tms 24244 df-cncf 24814 df-ovol 25409 df-vol 25410 df-mbf 25564 df-itg1 25565 df-itg2 25566 df-ibl 25567 df-itg 25568 df-0p 25615 df-limc 25811 df-dv 25812 df-area 26904

This theorem is referenced by: (None)

W3C validator