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 43228

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 13469	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ⊆ ℝ)
4	1, 2, 3	mp2an 692	. . . . . . . . 9 ⊢ (𝐴[,]𝐵) ⊆ ℝ
5	4	sseli 3979	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℝ)
6	5	adantr 480	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑥 ∈ ℝ)
7		areaquad.3	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ∈ ℝ
8	7	recni 11275	. . . . . . . . . . . . . . 15 ⊢ 𝐶 ∈ ℂ
9	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℂ)
10		resubcl 11573	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝑥 − 𝐴) ∈ ℝ)
11	1, 10	mpan2 691	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝑥 − 𝐴) ∈ ℝ)
12	2, 1	resubcli 11571	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ∈ ℝ
13	12	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ∈ ℝ)
14	2	recni 11275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℂ
15	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ∈ ℂ)
16		recn 11245	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
17		areaquad.7	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 < 𝐵
18	1, 17	gtneii 11373	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ≠ 𝐴
19	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 ∈ ℝ → 𝐵 ≠ 𝐴)
20	15, 16, 19	subne0d 11629	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
21	1, 20	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 − 𝐴) ≠ 0
22	21	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℝ → (𝐵 − 𝐴) ≠ 0)
23	11, 13, 22	redivcld 12095	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
24	23	recnd 11289	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
25		areaquad.4	. . . . . . . . . . . . . . . . 17 ⊢ 𝐷 ∈ ℝ
26	25	recni 11275	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ∈ ℂ
27	26	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℂ)
28	24, 27	mulcld 11281	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) ∈ ℂ)
29	24, 9	mulcld 11281	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶) ∈ ℂ)
30	9, 28, 29	addsub12d 11643	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
31		areaquad.10	. . . . . . . . . . . . . 14 ⊢ 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
32	24, 27, 9	subdid 11719	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
33	32	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
34	31, 33	eqtrid 2789	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑈 = (𝐶 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
35		1cnd 11256	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℂ)
36	35, 24, 9	subdird 11720	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
37	8	mullidi 11266	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐶) = 𝐶
38	37	oveq1i 7441	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐶) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))
39	36, 38	eqtrdi 2793	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶)))
40	39	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + (𝐶 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐶))))
41	30, 34, 40	3eqtr4d 2787	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)))
42		1red 11262	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℝ → 1 ∈ ℝ)
43	42, 23	resubcld 11691	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
44	43	recnd 11289	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℂ)
45	44, 9	mulcld 11281	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) ∈ ℂ)
46	28, 45	addcomd 11463	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)))
47	44, 9	mulcomd 11282	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) = (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
48	24, 27	mulcomd 11282	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷) = (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
49	47, 48	oveq12d 7449	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐶) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐷)) = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
50	41, 46, 49	3eqtrd 2781	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
51	7	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐶 ∈ ℝ)
52	51, 43	remulcld 11291	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
53	25	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐷 ∈ ℝ)
54	53, 23	remulcld 11291	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
55	52, 54	readdcld 11290	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
56	50, 55	eqeltrd 2841	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑈 ∈ ℝ)
57		areaquad.5	. . . . . . . . . . . . . . . 16 ⊢ 𝐸 ∈ ℝ
58	57	recni 11275	. . . . . . . . . . . . . . 15 ⊢ 𝐸 ∈ ℂ
59	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℂ)
60		areaquad.6	. . . . . . . . . . . . . . . . 17 ⊢ 𝐹 ∈ ℝ
61	60	recni 11275	. . . . . . . . . . . . . . . 16 ⊢ 𝐹 ∈ ℂ
62	61	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℂ)
63	24, 62	mulcld 11281	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) ∈ ℂ)
64	24, 59	mulcld 11281	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸) ∈ ℂ)
65	59, 63, 64	addsub12d 11643	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
66		areaquad.11	. . . . . . . . . . . . . 14 ⊢ 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
67	24, 62, 59	subdid 11719	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
68	67	oveq2d 7447	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
69	66, 68	eqtrid 2789	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝑉 = (𝐸 + ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
70	35, 24, 59	subdird 11720	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
71	58	mullidi 11266	. . . . . . . . . . . . . . . 16 ⊢ (1 · 𝐸) = 𝐸
72	71	oveq1i 7441	. . . . . . . . . . . . . . 15 ⊢ ((1 · 𝐸) − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))
73	70, 72	eqtrdi 2793	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸)))
74	73	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + (𝐸 − (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐸))))
75	65, 69, 74	3eqtr4d 2787	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)))
76	44, 59	mulcld 11281	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) ∈ ℂ)
77	63, 76	addcomd 11463	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → ((((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) + ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸)) = (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)))
78	44, 59	mulcomd 11282	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → ((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) = (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
79	24, 62	mulcomd 11282	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹) = (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
80	78, 79	oveq12d 7449	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (((1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) · 𝐸) + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · 𝐹)) = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
81	75, 77, 80	3eqtrd 2781	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
82	57	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐸 ∈ ℝ)
83	82, 43	remulcld 11291	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
84	60	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℝ → 𝐹 ∈ ℝ)
85	84, 23	remulcld 11291	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℝ → (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ℝ)
86	83, 85	readdcld 11290	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ℝ → ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ∈ ℝ)
87	81, 86	eqeltrd 2841	. . . . . . . . . 10 ⊢ (𝑥 ∈ ℝ → 𝑉 ∈ ℝ)
88		iccssre 13469	. . . . . . . . . 10 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ⊆ ℝ)
89	56, 87, 88	syl2anc 584	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ⊆ ℝ)
90	5, 89	syl 17	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ⊆ ℝ)
91	90	sselda 3983	. . . . . . 7 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → 𝑦 ∈ ℝ)
92	6, 91	jca 511	. . . . . 6 ⊢ ((𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)) → (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ))
93	92	ssopab2i 5555	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
94		areaquad.12	. . . . 5 ⊢ 𝑆 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
95		df-xp 5691	. . . . 5 ⊢ (ℝ × ℝ) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)}
96	93, 94, 95	3sstr4i 4035	. . . 4 ⊢ 𝑆 ⊆ (ℝ × ℝ)
97		iftrue 4531	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (𝑉 − 𝑈))
98		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 𝑥 ∈ (𝐴[,]𝐵)
99		nfopab2 5214	. . . . . . . . . . . . . . 15 ⊢ Ⅎ𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))}
100	94, 99	nfcxfr 2903	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦𝑆
101		nfcv 2905	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑦{𝑥}
102	100, 101	nfima 6086	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑆 “ {𝑥})
103		nfcv 2905	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦(𝑈[,]𝑉)
104		vex 3484	. . . . . . . . . . . . . . . 16 ⊢ 𝑥 ∈ V
105		vex 3484	. . . . . . . . . . . . . . . 16 ⊢ 𝑦 ∈ V
106	104, 105	elimasn 6108	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ ⟨𝑥, 𝑦⟩ ∈ 𝑆)
107	94	eleq2i 2833	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝑆 ↔ ⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))})
108		opabidw 5529	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉))} ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
109	106, 107, 108	3bitri 297	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) ↔ (𝑥 ∈ (𝐴[,]𝐵) ∧ 𝑦 ∈ (𝑈[,]𝑉)))
110	109	baib 535	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ (𝑈[,]𝑉)))
111	98, 102, 103, 110	eqrd 4003	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = (𝑈[,]𝑉))
112	111	fveq2d 6910	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘(𝑈[,]𝑉)))
113	5, 56	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ∈ ℝ)
114	5, 87	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 ∈ ℝ)
115		iccmbl 25601	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ) → (𝑈[,]𝑉) ∈ dom vol)
116	113, 114, 115	syl2anc 584	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑈[,]𝑉) ∈ dom vol)
117		mblvol 25565	. . . . . . . . . . . 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 11289	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℂ)
128	127	subidd 11608	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = 0)
129		1red 11262	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 1 ∈ ℝ)
130	2	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐵 ∈ ℝ)
131	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℝ)
132	1	rexri 11319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐴 ∈ ℝ^*
133	2	rexri 11319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 𝐵 ∈ ℝ^*
134		iccleub 13442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ≤ 𝐵)
135	132, 133, 134	mp3an12 1453	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ≤ 𝐵)
136	5, 130, 131, 135	lesub1dd 11879	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ≤ (𝐵 − 𝐴))
137	5, 1, 10	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℝ)
138	12	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ)
139	1	recni 11275	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝐴 ∈ ℂ
140	139	subidi 11580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐴 − 𝐴) = 0
141	131, 130, 131	ltsub1d 11872	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 < 𝐵 ↔ (𝐴 − 𝐴) < (𝐵 − 𝐴)))
142	17, 141	mpbii 233	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) < (𝐵 − 𝐴))
143	140, 142	eqbrtrrid 5179	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 < (𝐵 − 𝐴))
144		lediv1 12133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑥 − 𝐴) ∈ ℝ ∧ (𝐵 − 𝐴) ∈ ℝ ∧ ((𝐵 − 𝐴) ∈ ℝ ∧ 0 < (𝐵 − 𝐴))) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
145	137, 138, 138, 143, 144	syl112anc 1376	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) ≤ (𝐵 − 𝐴) ↔ ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴))))
146	136, 145	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ ((𝐵 − 𝐴) / (𝐵 − 𝐴)))
147	12	recni 11275	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵 − 𝐴) ∈ ℂ
148	147, 21	dividi 12000	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵 − 𝐴) / (𝐵 − 𝐴)) = 1
149	146, 148	breqtrdi 5184	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ≤ 1)
150	126, 129, 126, 149	lesub1dd 11879	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) − ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
151	128, 150	eqbrtrrd 5167	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
152		areaquad.8	. . . . . . . . . . . . . . . 16 ⊢ 𝐶 ≤ 𝐸
153	152	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐶 ≤ 𝐸)
154	123, 124, 125, 151, 153	lemul1ad 12207	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ (𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
155	25	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ∈ ℝ)
156	60	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐹 ∈ ℝ)
157	138, 143	elrpd 13074	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℝ⁺)
158		iccgelb 13443	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴 ∈ ℝ^* ∧ 𝐵 ∈ ℝ^* ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ≤ 𝑥)
159	132, 133, 158	mp3an12 1453	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ≤ 𝑥)
160	131, 5, 131, 159	lesub1dd 11879	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐴 − 𝐴) ≤ (𝑥 − 𝐴))
161	140, 160	eqbrtrrid 5179	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ (𝑥 − 𝐴))
162	137, 157, 161	divge0d 13117	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 0 ≤ ((𝑥 − 𝐴) / (𝐵 − 𝐴)))
163		areaquad.9	. . . . . . . . . . . . . . . 16 ⊢ 𝐷 ≤ 𝐹
164	163	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐷 ≤ 𝐹)
165	155, 156, 126, 162, 164	lemul1ad 12207	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ≤ (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴))))
166	119, 120, 121, 122, 154, 165	le2addd 11882	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) ≤ ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
167	5, 50	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 = ((𝐶 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐷 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
168	5, 81	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = ((𝐸 · (1 − ((𝑥 − 𝐴) / (𝐵 − 𝐴)))) + (𝐹 · ((𝑥 − 𝐴) / (𝐵 − 𝐴)))))
169	166, 167, 168	3brtr4d 5175	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑈 ≤ 𝑉)
170		ovolicc 25558	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ ℝ ∧ 𝑉 ∈ ℝ ∧ 𝑈 ≤ 𝑉) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
171	113, 114, 169, 170	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol*‘(𝑈[,]𝑉)) = (𝑉 − 𝑈))
172	112, 118, 171	3eqtrd 2781	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (𝑉 − 𝑈))
173	97, 172	eqtr4d 2780	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
174		iffalse 4534	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = 0)
175		nfv 1914	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦 ¬ 𝑥 ∈ (𝐴[,]𝐵)
176		nfcv 2905	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑦∅
177	109	simplbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (𝑆 “ {𝑥}) → 𝑥 ∈ (𝐴[,]𝐵))
178		noel 4338	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑦 ∈ ∅
179	178	pm2.21i 119	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ∅ → 𝑥 ∈ (𝐴[,]𝐵))
180	177, 179	pm5.21ni 377	. . . . . . . . . . . . 13 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑦 ∈ (𝑆 “ {𝑥}) ↔ 𝑦 ∈ ∅))
181	175, 102, 176, 180	eqrd 4003	. . . . . . . . . . . 12 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = ∅)
182	181	fveq2d 6910	. . . . . . . . . . 11 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = (vol‘∅))
183		0mbl 25574	. . . . . . . . . . . . 13 ⊢ ∅ ∈ dom vol
184		mblvol 25565	. . . . . . . . . . . . 13 ⊢ (∅ ∈ dom vol → (vol‘∅) = (vol*‘∅))
185	183, 184	ax-mp 5	. . . . . . . . . . . 12 ⊢ (vol‘∅) = (vol*‘∅)
186		ovol0 25528	. . . . . . . . . . . 12 ⊢ (vol*‘∅) = 0
187	185, 186	eqtri 2765	. . . . . . . . . . 11 ⊢ (vol‘∅) = 0
188	182, 187	eqtrdi 2793	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) = 0)
189	174, 188	eqtr4d 2780	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥})))
190	173, 189	pm2.61i 182	. . . . . . . 8 ⊢ if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) = (vol‘(𝑆 “ {𝑥}))
191	190	eqcomi 2746	. . . . . . 7 ⊢ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0)
192	87, 56	resubcld 11691	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → (𝑉 − 𝑈) ∈ ℝ)
193		0re 11263	. . . . . . . 8 ⊢ 0 ∈ ℝ
194		ifcl 4571	. . . . . . . 8 ⊢ (((𝑉 − 𝑈) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
195	192, 193, 194	sylancl 586	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) ∈ ℝ)
196	191, 195	eqeltrid 2845	. . . . . 6 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
197		volf 25564	. . . . . . . 8 ⊢ vol:dom vol⟶(0[,]+∞)
198		ffun 6739	. . . . . . . 8 ⊢ (vol:dom vol⟶(0[,]+∞) → Fun vol)
199	197, 198	ax-mp 5	. . . . . . 7 ⊢ Fun vol
200		iftrue 4531	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = (𝑈[,]𝑉))
201	111, 200	eqtr4d 2780	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
202		iffalse 4534	. . . . . . . . . 10 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) = ∅)
203	181, 202	eqtr4d 2780	. . . . . . . . 9 ⊢ (¬ 𝑥 ∈ (𝐴[,]𝐵) → (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅))
204	201, 203	pm2.61i 182	. . . . . . . 8 ⊢ (𝑆 “ {𝑥}) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅)
205	56, 87, 115	syl2anc 584	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → (𝑈[,]𝑉) ∈ dom vol)
206	183	a1i 11	. . . . . . . . 9 ⊢ (𝑥 ∈ ℝ → ∅ ∈ dom vol)
207	205, 206	ifcld 4572	. . . . . . . 8 ⊢ (𝑥 ∈ ℝ → if(𝑥 ∈ (𝐴[,]𝐵), (𝑈[,]𝑉), ∅) ∈ dom vol)
208	204, 207	eqeltrid 2845	. . . . . . 7 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ dom vol)
209		fvimacnv 7073	. . . . . . 7 ⊢ ((Fun vol ∧ (𝑆 “ {𝑥}) ∈ dom vol) → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
210	199, 208, 209	sylancr 587	. . . . . 6 ⊢ (𝑥 ∈ ℝ → ((vol‘(𝑆 “ {𝑥})) ∈ ℝ ↔ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)))
211	196, 210	mpbid 232	. . . . 5 ⊢ (𝑥 ∈ ℝ → (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ))
212	211	rgen 3063	. . . 4 ⊢ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ)
213	4	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝐴[,]𝐵) ⊆ ℝ)
214		rembl 25575	. . . . . . 7 ⊢ ℝ ∈ dom vol
215	214	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → ℝ ∈ dom vol)
216	114, 113	resubcld 11691	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑉 − 𝑈) ∈ ℝ)
217	172, 216	eqeltrd 2841	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
218	217	adantl 481	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) ∈ ℝ)
219		eldifn 4132	. . . . . . . 8 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → ¬ 𝑥 ∈ (𝐴[,]𝐵))
220	219, 188	syl 17	. . . . . . 7 ⊢ (𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵)) → (vol‘(𝑆 “ {𝑥})) = 0)
221	220	adantl 481	. . . . . 6 ⊢ ((0 ∈ ℝ ∧ 𝑥 ∈ (ℝ ∖ (𝐴[,]𝐵))) → (vol‘(𝑆 “ {𝑥})) = 0)
222	172	mpteq2ia 5245	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈))
223		eqid 2737	. . . . . . . . . . 11 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
224	223	subcn 24888	. . . . . . . . . . . 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 5247	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
227	223	addcn 24887	. . . . . . . . . . . . . 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 11212	. . . . . . . . . . . . . . . 16 ⊢ ℝ ⊆ ℂ
230	4, 229	sstri 3993	. . . . . . . . . . . . . . 15 ⊢ (𝐴[,]𝐵) ⊆ ℂ
231		ssid 4006	. . . . . . . . . . . . . . 15 ⊢ ℂ ⊆ ℂ
232		cncfmptc 24938	. . . . . . . . . . . . . . 15 ⊢ ((𝐸 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
233	58, 230, 231, 232	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)
234	233	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ))
235	230	sseli 3979	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑥 ∈ ℂ)
236	139	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝐴 ∈ ℂ)
237	147	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ∈ ℂ)
238	21	a1i 11	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐵 − 𝐴) ≠ 0)
239	235, 236, 237, 238	divsubdird 12082	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
240	239	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴))))
241	240	mpteq2dva 5242	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))))
242		resmpt 6055	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))))
243	230, 242	ax-mp 5	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴)))
244		eqid 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) = (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴)))
245	244	divccncf 24932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵 − 𝐴) ∈ ℂ ∧ (𝐵 − 𝐴) ≠ 0) → (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ))
246	147, 21, 245	mp2an 692	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ)
247		rescncf 24923	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐴[,]𝐵) ⊆ ℂ → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ∈ (ℂ–cn→ℂ) → ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)))
248	230, 246, 247	mp2 9	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 ∈ ℂ ↦ (𝑥 / (𝐵 − 𝐴))) ↾ (𝐴[,]𝐵)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
249	243, 248	eqeltrri 2838	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
250	249	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
251	139, 147, 21	divcli 12009	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐴 / (𝐵 − 𝐴)) ∈ ℂ
252		cncfmptc 24938	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝐴 / (𝐵 − 𝐴)) ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
253	251, 230, 231, 252	mp3an 1463	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
254	253	a1i 11	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐴 / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
255	223, 225, 250, 254	cncfmpt2f 24941	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 / (𝐵 − 𝐴)) − (𝐴 / (𝐵 − 𝐴)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
256	241, 255	eqeltrd 2841	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
257		cncfmptc 24938	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐹 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
258	61, 230, 231, 257	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ)
259	258	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐹) ∈ ((𝐴[,]𝐵)–cn→ℂ))
260	223, 225, 259, 234	cncfmpt2f 24941	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐹 − 𝐸)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
261	256, 260	mulcncf 25480	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
262	223, 228, 234, 261	cncfmpt2f 24941	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
263	226, 262	eqeltrid 2845	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ))
264	31	mpteq2i 5247	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) = (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
265		cncfmptc 24938	. . . . . . . . . . . . . . 15 ⊢ ((𝐶 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
266	8, 230, 231, 265	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)
267	266	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ))
268		cncfmptc 24938	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
269	26, 230, 231, 268	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ)
270	269	a1i 11	. . . . . . . . . . . . . . 15 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐷) ∈ ((𝐴[,]𝐵)–cn→ℂ))
271	223, 225, 270, 267	cncfmpt2f 24941	. . . . . . . . . . . . . 14 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐷 − 𝐶)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
272	256, 271	mulcncf 25480	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
273	223, 228, 267, 272	cncfmpt2f 24941	. . . . . . . . . . . 12 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))) ∈ ((𝐴[,]𝐵)–cn→ℂ))
274	264, 273	eqeltrid 2845	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ))
275	223, 225, 263, 274	cncfmpt2f 24941	. . . . . . . . . 10 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ))
276	275	mptru 1547	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)
277		cniccibl 25876	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹)
278	1, 2, 276, 277	mp3an 1463	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑉 − 𝑈)) ∈ 𝐿¹
279	222, 278	eqeltri 2837	. . . . . . 7 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
280	279	a1i 11	. . . . . 6 ⊢ (0 ∈ ℝ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
281	213, 215, 218, 221, 280	iblss2 25841	. . . . 5 ⊢ (0 ∈ ℝ → (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹)
282	193, 281	ax-mp 5	. . . 4 ⊢ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹
283		dmarea 27000	. . . 4 ⊢ (𝑆 ∈ dom area ↔ (𝑆 ⊆ (ℝ × ℝ) ∧ ∀𝑥 ∈ ℝ (𝑆 “ {𝑥}) ∈ (^◡vol “ ℝ) ∧ (𝑥 ∈ ℝ ↦ (vol‘(𝑆 “ {𝑥}))) ∈ 𝐿¹))
284	96, 212, 282, 283	mpbir3an 1342	. . 3 ⊢ 𝑆 ∈ dom area
285		areaval 27007	. . 3 ⊢ (𝑆 ∈ dom area → (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥)
286	284, 285	ax-mp 5	. 2 ⊢ (area‘𝑆) = ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥
287		itgeq2 25813	. . . 4 ⊢ (∀𝑥 ∈ ℝ (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) → ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
288	191	a1i 11	. . . 4 ⊢ (𝑥 ∈ ℝ → (vol‘(𝑆 “ {𝑥})) = if(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0))
289	287, 288	mprg 3067	. . 3 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
290		itgss2 25848	. . . 4 ⊢ ((𝐴[,]𝐵) ⊆ ℝ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥)
291	4, 290	ax-mp 5	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ∫ℝif(𝑥 ∈ (𝐴[,]𝐵), (𝑉 − 𝑈), 0) d𝑥
292	61, 58	addcli 11267	. . . . . 6 ⊢ (𝐹 + 𝐸) ∈ ℂ
293		2cnne0 12476	. . . . . 6 ⊢ (2 ∈ ℂ ∧ 2 ≠ 0)
294		div32 11942	. . . . . 6 ⊢ (((𝐹 + 𝐸) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)))
295	292, 293, 147, 294	mp3an 1463	. . . . 5 ⊢ (((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
296	26, 8	addcli 11267	. . . . . 6 ⊢ (𝐷 + 𝐶) ∈ ℂ
297		div32 11942	. . . . . 6 ⊢ (((𝐷 + 𝐶) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
298	296, 293, 147, 297	mp3an 1463	. . . . 5 ⊢ (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
299	295, 298	oveq12i 7443	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴))) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
300		2cn 12341	. . . . . 6 ⊢ 2 ∈ ℂ
301		2ne0 12370	. . . . . 6 ⊢ 2 ≠ 0
302	292, 300, 301	divcli 12009	. . . . 5 ⊢ ((𝐹 + 𝐸) / 2) ∈ ℂ
303	296, 300, 301	divcli 12009	. . . . 5 ⊢ ((𝐷 + 𝐶) / 2) ∈ ℂ
304	302, 303, 147	subdiri 11713	. . . 4 ⊢ ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴)) = ((((𝐹 + 𝐸) / 2) · (𝐵 − 𝐴)) − (((𝐷 + 𝐶) / 2) · (𝐵 − 𝐴)))
305	114	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑉 ∈ ℝ)
306	263	mptru 1547	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)
307		cniccibl 25876	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
308	1, 2, 306, 307	mp3an 1463	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹
309	308	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑉) ∈ 𝐿¹)
310	113	adantl 481	. . . . . . 7 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 ∈ ℝ)
311	274	mptru 1547	. . . . . . . . 9 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)
312		cniccibl 25876	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
313	1, 2, 311, 312	mp3an 1463	. . . . . . . 8 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹
314	313	a1i 11	. . . . . . 7 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑈) ∈ 𝐿¹)
315	305, 309, 310, 314	itgsub 25861	. . . . . 6 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥))
316	315	mptru 1547	. . . . 5 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥)
317	58, 300, 301	divcan4i 12014	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) / 2) = 𝐸
318	317	oveq1i 7441	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = (𝐸 · (𝐵 − 𝐴))
319	58, 300	mulcli 11268	. . . . . . . . . . 11 ⊢ (𝐸 · 2) ∈ ℂ
320		div32 11942	. . . . . . . . . . 11 ⊢ (((𝐸 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2)))
321	319, 293, 147, 320	mp3an 1463	. . . . . . . . . 10 ⊢ (((𝐸 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
322	318, 321	eqtr3i 2767	. . . . . . . . 9 ⊢ (𝐸 · (𝐵 − 𝐴)) = ((𝐸 · 2) · ((𝐵 − 𝐴) / 2))
323	322	oveq1i 7441	. . . . . . . 8 ⊢ ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
324		itgeq2 25813	. . . . . . . . . 10 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) → ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥)
325	66	a1i 11	. . . . . . . . . 10 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → 𝑉 = (𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))))
326	324, 325	mprg 3067	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥
327	57	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐸 ∈ ℝ)
328		cniccibl 25876	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
329	1, 2, 233, 328	mp3an 1463	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹
330	329	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐸) ∈ 𝐿¹)
331	126	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) ∈ ℝ)
332	60	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐹 ∈ ℝ)
333	332, 327	resubcld 11691	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹 − 𝐸) ∈ ℝ)
334	331, 333	remulcld 11291	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) ∈ ℝ)
335	261	mptru 1547	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
336		cniccibl 25876	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
337	1, 2, 335, 336	mp3an 1463	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹
338	337	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) ∈ 𝐿¹)
339	327, 330, 334, 338	itgadd 25860	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥))
340	339	mptru 1547	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐸 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸))) d𝑥 = (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
341		iccmbl 25601	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
342	1, 2, 341	mp2an 692	. . . . . . . . . . . 12 ⊢ (𝐴[,]𝐵) ∈ dom vol
343		mblvol 25565	. . . . . . . . . . . . . . 15 ⊢ ((𝐴[,]𝐵) ∈ dom vol → (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵)))
344	342, 343	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (vol‘(𝐴[,]𝐵)) = (vol*‘(𝐴[,]𝐵))
345	1, 2, 17	ltleii 11384	. . . . . . . . . . . . . . 15 ⊢ 𝐴 ≤ 𝐵
346		ovolicc 25558	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵) → (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴))
347	1, 2, 345, 346	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (vol*‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
348	344, 347	eqtri 2765	. . . . . . . . . . . . 13 ⊢ (vol‘(𝐴[,]𝐵)) = (𝐵 − 𝐴)
349	348, 12	eqeltri 2837	. . . . . . . . . . . 12 ⊢ (vol‘(𝐴[,]𝐵)) ∈ ℝ
350		itgconst 25854	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐸 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵))))
351	342, 349, 58, 350	mp3an 1463	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (vol‘(𝐴[,]𝐵)))
352	348	oveq2i 7442	. . . . . . . . . . 11 ⊢ (𝐸 · (vol‘(𝐴[,]𝐵))) = (𝐸 · (𝐵 − 𝐴))
353	351, 352	eqtri 2765	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐸 d𝑥 = (𝐸 · (𝐵 − 𝐴))
354	61	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐹 ∈ ℂ)
355	58	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐸 ∈ ℂ)
356	354, 355	subcld 11620	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐹 − 𝐸) ∈ ℂ)
357	256	mptru 1547	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
358		cniccibl 25876	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
359	1, 2, 357, 358	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹
360	359	a1i 11	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ ((𝑥 − 𝐴) / (𝐵 − 𝐴))) ∈ 𝐿¹)
361	356, 331, 360	itgmulc2 25869	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
362	361	mptru 1547	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
363		itgeq2 25813	. . . . . . . . . . . . . . 15 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) → ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
364	137	recnd 11289	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥 − 𝐴) ∈ ℂ)
365	364, 237, 238	divrec2d 12047	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝑥 − 𝐴) / (𝐵 − 𝐴)) = ((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)))
366	363, 365	mprg 3067	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
367	5	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑥 ∈ ℝ)
368		cncfmptid 24939	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ))
369	230, 231, 368	mp2an 692	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)
370		cniccibl 25876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
371	1, 2, 369, 370	mp3an 1463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹
372	371	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝑥) ∈ 𝐿¹)
373	1	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐴 ∈ ℝ)
374		cncfmptc 24938	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝐴 ∈ ℂ ∧ (𝐴[,]𝐵) ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ))
375	139, 230, 231, 374	mp3an 1463	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)
376		cniccibl 25876	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
377	1, 2, 375, 376	mp3an 1463	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹
378	377	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐴) ∈ 𝐿¹)
379	367, 372, 373, 378	itgsub 25861	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥))
380	379	mptru 1547	. . . . . . . . . . . . . . . . . 18 ⊢ ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥)
381	1	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐴 ∈ ℝ)
382	2	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐵 ∈ ℝ)
383	345	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 𝐴 ≤ 𝐵)
384		1nn0 12542	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℕ₀
385	384	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⊤ → 1 ∈ ℕ₀)
386	381, 382, 383, 385	itgpowd 26091	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)))
387	386	mptru 1547	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1))
388		1p1e2 12391	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (1 + 1) = 2
389	388	oveq2i 7442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / (1 + 1)) = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
390	387, 389	eqtri 2765	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2)
391		itgeq2 25813	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)(𝑥↑1) = 𝑥 → ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥)
392	235	exp1d 14181	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝑥↑1) = 𝑥)
393	391, 392	mprg 3067	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)(𝑥↑1) d𝑥 = ∫(𝐴[,]𝐵)𝑥 d𝑥
394	388	oveq2i 7442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐵↑(1 + 1)) = (𝐵↑2)
395	388	oveq2i 7442	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐴↑(1 + 1)) = (𝐴↑2)
396	394, 395	oveq12i 7443	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) = ((𝐵↑2) − (𝐴↑2))
397	396	oveq1i 7441	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝐵↑(1 + 1)) − (𝐴↑(1 + 1))) / 2) = (((𝐵↑2) − (𝐴↑2)) / 2)
398	390, 393, 397	3eqtr3i 2773	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝑥 d𝑥 = (((𝐵↑2) − (𝐴↑2)) / 2)
399		itgconst 25854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐴 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵))))
400	342, 349, 139, 399	mp3an 1463	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (vol‘(𝐴[,]𝐵)))
401	348	oveq2i 7442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐴 · (vol‘(𝐴[,]𝐵))) = (𝐴 · (𝐵 − 𝐴))
402	400, 401	eqtri 2765	. . . . . . . . . . . . . . . . . . 19 ⊢ ∫(𝐴[,]𝐵)𝐴 d𝑥 = (𝐴 · (𝐵 − 𝐴))
403	398, 402	oveq12i 7443	. . . . . . . . . . . . . . . . . 18 ⊢ (∫(𝐴[,]𝐵)𝑥 d𝑥 − ∫(𝐴[,]𝐵)𝐴 d𝑥) = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
404	380, 403	eqtri 2765	. . . . . . . . . . . . . . . . 17 ⊢ ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥 = ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))
405	404	oveq2i 7442	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴))))
406	14	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ∈ ℂ)
407	139	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐴 ∈ ℂ)
408	406, 407	subcld 11620	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ∈ ℂ)
409	18	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ (⊤ → 𝐵 ≠ 𝐴)
410	406, 407, 409	subne0d 11629	. . . . . . . . . . . . . . . . . . 19 ⊢ (⊤ → (𝐵 − 𝐴) ≠ 0)
411	408, 410	reccld 12036	. . . . . . . . . . . . . . . . . 18 ⊢ (⊤ → (1 / (𝐵 − 𝐴)) ∈ ℂ)
412	411	mptru 1547	. . . . . . . . . . . . . . . . 17 ⊢ (1 / (𝐵 − 𝐴)) ∈ ℂ
413	14	sqcli 14220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐵↑2) ∈ ℂ
414	139	sqcli 14220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴↑2) ∈ ℂ
415	413, 414	subcli 11585	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐵↑2) − (𝐴↑2)) ∈ ℂ
416	415, 300, 301	divcli 12009	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) ∈ ℂ
417	139, 147	mulcli 11268	. . . . . . . . . . . . . . . . 17 ⊢ (𝐴 · (𝐵 − 𝐴)) ∈ ℂ
418	412, 416, 417	subdii 11712	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((((𝐵↑2) − (𝐴↑2)) / 2) − (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
419	405, 418	eqtri 2765	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))))
420	137	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝑥 − 𝐴) ∈ ℝ)
421	367, 372, 373, 378	iblsub 25857	. . . . . . . . . . . . . . . . 17 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (𝑥 − 𝐴)) ∈ 𝐿¹)
422	411, 420, 421	itgmulc2 25869	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥)
423	422	mptru 1547	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · ∫(𝐴[,]𝐵)(𝑥 − 𝐴) d𝑥) = ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥
424	412, 417	mulcomi 11269	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
425	417, 147, 21	divreci 12012	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = ((𝐴 · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
426	139, 147, 21	divcan4i 12014	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = 𝐴
427	424, 425, 426	3eqtr2i 2771	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴))) = 𝐴
428	427	oveq2i 7442	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − ((1 / (𝐵 − 𝐴)) · (𝐴 · (𝐵 − 𝐴)))) = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
429	419, 423, 428	3eqtr3i 2773	. . . . . . . . . . . . . 14 ⊢ ∫(𝐴[,]𝐵)((1 / (𝐵 − 𝐴)) · (𝑥 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
430	366, 429	eqtri 2765	. . . . . . . . . . . . 13 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴)
431	14, 139	subsqi 14252	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵↑2) − (𝐴↑2)) = ((𝐵 + 𝐴) · (𝐵 − 𝐴))
432	431	oveq1i 7441	. . . . . . . . . . . . . . . 16 ⊢ (((𝐵↑2) − (𝐴↑2)) / 2) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2)
433	432	oveq2i 7442	. . . . . . . . . . . . . . 15 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
434	431, 415	eqeltrri 2838	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) · (𝐵 − 𝐴)) ∈ ℂ
435	412, 434, 300, 301	divassi 12023	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((1 / (𝐵 − 𝐴)) · (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / 2))
436	412, 434	mulcomi 11269	. . . . . . . . . . . . . . . . 17 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
437	434, 147, 21	divreci 12012	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (((𝐵 + 𝐴) · (𝐵 − 𝐴)) · (1 / (𝐵 − 𝐴)))
438	14, 139	addcli 11267	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐵 + 𝐴) ∈ ℂ
439	438, 147, 21	divcan4i 12014	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 + 𝐴) · (𝐵 − 𝐴)) / (𝐵 − 𝐴)) = (𝐵 + 𝐴)
440	436, 437, 439	3eqtr2i 2771	. . . . . . . . . . . . . . . 16 ⊢ ((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) = (𝐵 + 𝐴)
441	440	oveq1i 7441	. . . . . . . . . . . . . . 15 ⊢ (((1 / (𝐵 − 𝐴)) · ((𝐵 + 𝐴) · (𝐵 − 𝐴))) / 2) = ((𝐵 + 𝐴) / 2)
442	433, 435, 441	3eqtr2i 2771	. . . . . . . . . . . . . 14 ⊢ ((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) = ((𝐵 + 𝐴) / 2)
443	442	oveq1i 7441	. . . . . . . . . . . . 13 ⊢ (((1 / (𝐵 − 𝐴)) · (((𝐵↑2) − (𝐴↑2)) / 2)) − 𝐴) = (((𝐵 + 𝐴) / 2) − 𝐴)
444	139, 300	mulcli 11268	. . . . . . . . . . . . . . 15 ⊢ (𝐴 · 2) ∈ ℂ
445		divsubdir 11961	. . . . . . . . . . . . . . 15 ⊢ (((𝐵 + 𝐴) ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)))
446	438, 444, 293, 445	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2))
447	14, 139, 444	addsubassi 11600	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 + (𝐴 − (𝐴 · 2)))
448		subsub2 11537	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 ∈ ℂ ∧ (𝐴 · 2) ∈ ℂ ∧ 𝐴 ∈ ℂ) → (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2))))
449	14, 444, 139, 448	mp3an 1463	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 + (𝐴 − (𝐴 · 2)))
450	139	times2i 12405	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐴 · 2) = (𝐴 + 𝐴)
451	450	oveq1i 7441	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 · 2) − 𝐴) = ((𝐴 + 𝐴) − 𝐴)
452	139, 139	pncan3oi 11524	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐴 + 𝐴) − 𝐴) = 𝐴
453	451, 452	eqtri 2765	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐴 · 2) − 𝐴) = 𝐴
454	453	oveq2i 7442	. . . . . . . . . . . . . . . 16 ⊢ (𝐵 − ((𝐴 · 2) − 𝐴)) = (𝐵 − 𝐴)
455	447, 449, 454	3eqtr2i 2771	. . . . . . . . . . . . . . 15 ⊢ ((𝐵 + 𝐴) − (𝐴 · 2)) = (𝐵 − 𝐴)
456	455	oveq1i 7441	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) − (𝐴 · 2)) / 2) = ((𝐵 − 𝐴) / 2)
457	139, 300, 301	divcan4i 12014	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 · 2) / 2) = 𝐴
458	457	oveq2i 7442	. . . . . . . . . . . . . 14 ⊢ (((𝐵 + 𝐴) / 2) − ((𝐴 · 2) / 2)) = (((𝐵 + 𝐴) / 2) − 𝐴)
459	446, 456, 458	3eqtr3ri 2774	. . . . . . . . . . . . 13 ⊢ (((𝐵 + 𝐴) / 2) − 𝐴) = ((𝐵 − 𝐴) / 2)
460	430, 443, 459	3eqtri 2769	. . . . . . . . . . . 12 ⊢ ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥 = ((𝐵 − 𝐴) / 2)
461	460	oveq2i 7442	. . . . . . . . . . 11 ⊢ ((𝐹 − 𝐸) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
462		itgeq2 25813	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) → ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥)
463	61, 58	subcli 11585	. . . . . . . . . . . . . 14 ⊢ (𝐹 − 𝐸) ∈ ℂ
464	463	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐹 − 𝐸) ∈ ℂ)
465	464, 127	mulcomd 11282	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)))
466	462, 465	mprg 3067	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐹 − 𝐸) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥
467	362, 461, 466	3eqtr3ri 2774	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥 = ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2))
468	353, 467	oveq12i 7443	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐸 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐹 − 𝐸)) d𝑥) = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
469	326, 340, 468	3eqtri 2769	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐸 · (𝐵 − 𝐴)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
470	147, 300, 301	divcli 12009	. . . . . . . . 9 ⊢ ((𝐵 − 𝐴) / 2) ∈ ℂ
471	319, 463, 470	adddiri 11274	. . . . . . . 8 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = (((𝐸 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐹 − 𝐸) · ((𝐵 − 𝐴) / 2)))
472	323, 469, 471	3eqtr4i 2775	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2))
473		addsub12 11521	. . . . . . . . . 10 ⊢ ((𝐹 ∈ ℂ ∧ (𝐸 · 2) ∈ ℂ ∧ 𝐸 ∈ ℂ) → (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸)))
474	61, 319, 58, 473	mp3an 1463	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = ((𝐸 · 2) + (𝐹 − 𝐸))
475	58	times2i 12405	. . . . . . . . . . . 12 ⊢ (𝐸 · 2) = (𝐸 + 𝐸)
476	475	oveq1i 7441	. . . . . . . . . . 11 ⊢ ((𝐸 · 2) − 𝐸) = ((𝐸 + 𝐸) − 𝐸)
477	58, 58	pncan3oi 11524	. . . . . . . . . . 11 ⊢ ((𝐸 + 𝐸) − 𝐸) = 𝐸
478	476, 477	eqtri 2765	. . . . . . . . . 10 ⊢ ((𝐸 · 2) − 𝐸) = 𝐸
479	478	oveq2i 7442	. . . . . . . . 9 ⊢ (𝐹 + ((𝐸 · 2) − 𝐸)) = (𝐹 + 𝐸)
480	474, 479	eqtr3i 2767	. . . . . . . 8 ⊢ ((𝐸 · 2) + (𝐹 − 𝐸)) = (𝐹 + 𝐸)
481	480	oveq1i 7441	. . . . . . 7 ⊢ (((𝐸 · 2) + (𝐹 − 𝐸)) · ((𝐵 − 𝐴) / 2)) = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
482	472, 481	eqtri 2765	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑉 d𝑥 = ((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2))
483	8, 300, 301	divcan4i 12014	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) / 2) = 𝐶
484	483	oveq1i 7441	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = (𝐶 · (𝐵 − 𝐴))
485	8, 300	mulcli 11268	. . . . . . . . . . 11 ⊢ (𝐶 · 2) ∈ ℂ
486		div32 11942	. . . . . . . . . . 11 ⊢ (((𝐶 · 2) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 ≠ 0) ∧ (𝐵 − 𝐴) ∈ ℂ) → (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2)))
487	485, 293, 147, 486	mp3an 1463	. . . . . . . . . 10 ⊢ (((𝐶 · 2) / 2) · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
488	484, 487	eqtr3i 2767	. . . . . . . . 9 ⊢ (𝐶 · (𝐵 − 𝐴)) = ((𝐶 · 2) · ((𝐵 − 𝐴) / 2))
489	488	oveq1i 7441	. . . . . . . 8 ⊢ ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
490	31	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝑈 = (𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))))
491	490	itgeq2dv 25817	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥)
492	491	mptru 1547	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥
493	7	a1i 11	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐶 ∈ ℝ)
494		cniccibl 25876	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
495	1, 2, 266, 494	mp3an 1463	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹
496	495	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ 𝐶) ∈ 𝐿¹)
497	25	a1i 11	. . . . . . . . . . . . 13 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → 𝐷 ∈ ℝ)
498	497, 493	resubcld 11691	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐷 − 𝐶) ∈ ℝ)
499	331, 498	remulcld 11291	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) ∈ ℝ)
500	272	mptru 1547	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)
501		cniccibl 25876	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
502	1, 2, 500, 501	mp3an 1463	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹
503	502	a1i 11	. . . . . . . . . . 11 ⊢ (⊤ → (𝑥 ∈ (𝐴[,]𝐵) ↦ (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) ∈ 𝐿¹)
504	493, 496, 499, 503	itgadd 25860	. . . . . . . . . 10 ⊢ (⊤ → ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥))
505	504	mptru 1547	. . . . . . . . 9 ⊢ ∫(𝐴[,]𝐵)(𝐶 + (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶))) d𝑥 = (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
506		itgconst 25854	. . . . . . . . . . . 12 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ (vol‘(𝐴[,]𝐵)) ∈ ℝ ∧ 𝐶 ∈ ℂ) → ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵))))
507	342, 349, 8, 506	mp3an 1463	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (vol‘(𝐴[,]𝐵)))
508	348	oveq2i 7442	. . . . . . . . . . 11 ⊢ (𝐶 · (vol‘(𝐴[,]𝐵))) = (𝐶 · (𝐵 − 𝐴))
509	507, 508	eqtri 2765	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)𝐶 d𝑥 = (𝐶 · (𝐵 − 𝐴))
510	26	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐷 ∈ ℂ)
511	8	a1i 11	. . . . . . . . . . . . . 14 ⊢ (⊤ → 𝐶 ∈ ℂ)
512	510, 511	subcld 11620	. . . . . . . . . . . . 13 ⊢ (⊤ → (𝐷 − 𝐶) ∈ ℂ)
513	512, 331, 360	itgmulc2 25869	. . . . . . . . . . . 12 ⊢ (⊤ → ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥)
514	513	mptru 1547	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥
515	460	oveq2i 7442	. . . . . . . . . . 11 ⊢ ((𝐷 − 𝐶) · ∫(𝐴[,]𝐵)((𝑥 − 𝐴) / (𝐵 − 𝐴)) d𝑥) = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
516		itgeq2 25813	. . . . . . . . . . . 12 ⊢ (∀𝑥 ∈ (𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) → ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥)
517	26, 8	subcli 11585	. . . . . . . . . . . . . 14 ⊢ (𝐷 − 𝐶) ∈ ℂ
518	517	a1i 11	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → (𝐷 − 𝐶) ∈ ℂ)
519	518, 127	mulcomd 11282	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ (𝐴[,]𝐵) → ((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) = (((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)))
520	516, 519	mprg 3067	. . . . . . . . . . 11 ⊢ ∫(𝐴[,]𝐵)((𝐷 − 𝐶) · ((𝑥 − 𝐴) / (𝐵 − 𝐴))) d𝑥 = ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥
521	514, 515, 520	3eqtr3ri 2774	. . . . . . . . . 10 ⊢ ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥 = ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2))
522	509, 521	oveq12i 7443	. . . . . . . . 9 ⊢ (∫(𝐴[,]𝐵)𝐶 d𝑥 + ∫(𝐴[,]𝐵)(((𝑥 − 𝐴) / (𝐵 − 𝐴)) · (𝐷 − 𝐶)) d𝑥) = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
523	492, 505, 522	3eqtri 2769	. . . . . . . 8 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐶 · (𝐵 − 𝐴)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
524	485, 517, 470	adddiri 11274	. . . . . . . 8 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = (((𝐶 · 2) · ((𝐵 − 𝐴) / 2)) + ((𝐷 − 𝐶) · ((𝐵 − 𝐴) / 2)))
525	489, 523, 524	3eqtr4i 2775	. . . . . . 7 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2))
526		addsub12 11521	. . . . . . . . . 10 ⊢ ((𝐷 ∈ ℂ ∧ (𝐶 · 2) ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶)))
527	26, 485, 8, 526	mp3an 1463	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = ((𝐶 · 2) + (𝐷 − 𝐶))
528	8	times2i 12405	. . . . . . . . . . . 12 ⊢ (𝐶 · 2) = (𝐶 + 𝐶)
529	528	oveq1i 7441	. . . . . . . . . . 11 ⊢ ((𝐶 · 2) − 𝐶) = ((𝐶 + 𝐶) − 𝐶)
530	8, 8	pncan3oi 11524	. . . . . . . . . . 11 ⊢ ((𝐶 + 𝐶) − 𝐶) = 𝐶
531	529, 530	eqtri 2765	. . . . . . . . . 10 ⊢ ((𝐶 · 2) − 𝐶) = 𝐶
532	531	oveq2i 7442	. . . . . . . . 9 ⊢ (𝐷 + ((𝐶 · 2) − 𝐶)) = (𝐷 + 𝐶)
533	527, 532	eqtr3i 2767	. . . . . . . 8 ⊢ ((𝐶 · 2) + (𝐷 − 𝐶)) = (𝐷 + 𝐶)
534	533	oveq1i 7441	. . . . . . 7 ⊢ (((𝐶 · 2) + (𝐷 − 𝐶)) · ((𝐵 − 𝐴) / 2)) = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
535	525, 534	eqtri 2765	. . . . . 6 ⊢ ∫(𝐴[,]𝐵)𝑈 d𝑥 = ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2))
536	482, 535	oveq12i 7443	. . . . 5 ⊢ (∫(𝐴[,]𝐵)𝑉 d𝑥 − ∫(𝐴[,]𝐵)𝑈 d𝑥) = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
537	316, 536	eqtri 2765	. . . 4 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = (((𝐹 + 𝐸) · ((𝐵 − 𝐴) / 2)) − ((𝐷 + 𝐶) · ((𝐵 − 𝐴) / 2)))
538	299, 304, 537	3eqtr4ri 2776	. . 3 ⊢ ∫(𝐴[,]𝐵)(𝑉 − 𝑈) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
539	289, 291, 538	3eqtr2i 2771	. 2 ⊢ ∫ℝ(vol‘(𝑆 “ {𝑥})) d𝑥 = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))
540	286, 539	eqtri 2765	1 ⊢ (area‘𝑆) = ((((𝐹 + 𝐸) / 2) − ((𝐷 + 𝐶) / 2)) · (𝐵 − 𝐴))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 = wceq 1540 ⊤wtru 1541 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∖ cdif 3948 ⊆ wss 3951 ∅c0 4333 ifcif 4525 {csn 4626 ⟨cop 4632 class class class wbr 5143 {copab 5205 ↦ cmpt 5225 × cxp 5683 ^◡ccnv 5684 dom cdm 5685 ↾ cres 5687 “ cima 5688 Fun wfun 6555 ⟶wf 6557 ‘cfv 6561 (class class class)co 7431 ℂcc 11153 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 +∞cpnf 11292 ℝ^*cxr 11294 < clt 11295 ≤ cle 11296 − cmin 11492 / cdiv 11920 2c2 12321 ℕ₀cn0 12526 [,]cicc 13390 ↑cexp 14102 TopOpenctopn 17466 ℂ_fldccnfld 21364 Cn ccn 23232 ×_t ctx 23568 –cn→ccncf 24902 vol*covol 25497 volcvol 25498 𝐿¹cibl 25652 ∫citg 25653 areacarea 26998

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-inf2 9681 ax-cc 10475 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233 ax-addf 11234

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-symdif 4253 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-ofr 7698 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-omul 8511 df-er 8745 df-map 8868 df-pm 8869 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-fi 9451 df-sup 9482 df-inf 9483 df-oi 9550 df-dju 9941 df-card 9979 df-acn 9982 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-q 12991 df-rp 13035 df-xneg 13154 df-xadd 13155 df-xmul 13156 df-ioo 13391 df-ioc 13392 df-ico 13393 df-icc 13394 df-fz 13548 df-fzo 13695 df-fl 13832 df-mod 13910 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-limsup 15507 df-clim 15524 df-rlim 15525 df-sum 15723 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-starv 17312 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-unif 17320 df-hom 17321 df-cco 17322 df-rest 17467 df-topn 17468 df-0g 17486 df-gsum 17487 df-topgen 17488 df-pt 17489 df-prds 17492 df-xrs 17547 df-qtop 17552 df-imas 17553 df-xps 17555 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-submnd 18797 df-mulg 19086 df-cntz 19335 df-cmn 19800 df-psmet 21356 df-xmet 21357 df-met 21358 df-bl 21359 df-mopn 21360 df-fbas 21361 df-fg 21362 df-cnfld 21365 df-top 22900 df-topon 22917 df-topsp 22939 df-bases 22953 df-cld 23027 df-ntr 23028 df-cls 23029 df-nei 23106 df-lp 23144 df-perf 23145 df-cn 23235 df-cnp 23236 df-haus 23323 df-cmp 23395 df-tx 23570 df-hmeo 23763 df-fil 23854 df-fm 23946 df-flim 23947 df-flf 23948 df-xms 24330 df-ms 24331 df-tms 24332 df-cncf 24904 df-ovol 25499 df-vol 25500 df-mbf 25654 df-itg1 25655 df-itg2 25656 df-ibl 25657 df-itg 25658 df-0p 25705 df-limc 25901 df-dv 25902 df-area 26999

This theorem is referenced by: (None)

W3C validator