areaquad

Description: The area of a quadrilateral with two sides which are parallel to the y-axis in ( RR X. RR ) 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)

	Ref	Expression
Hypotheses	areaquad.1	$⊢ A \in ℝ$
	areaquad.2	$⊢ B \in ℝ$
	areaquad.3	$⊢ C \in ℝ$
	areaquad.4	$⊢ D \in ℝ$
	areaquad.5	$⊢ E \in ℝ$
	areaquad.6	$⊢ F \in ℝ$
	areaquad.7	$⊢ A < B$
	areaquad.8	$⊢ C \leq E$
	areaquad.9	$⊢ D \leq F$
	areaquad.10	$⊢ U = C + (\frac{x - A}{B - A}) (D - C)$
	areaquad.11	$⊢ V = E + (\frac{x - A}{B - A}) (F - E)$
	areaquad.12	$⊢ S = \{⟨x, y⟩ \| (x \in [A, B] \land y \in [U, V])\}$
Assertion	areaquad	$⊢ area (S) = ((\frac{F + E}{2}) - (\frac{D + C}{2})) (B - A)$

Proof

Step	Hyp	Ref	Expression
1		areaquad.1	$⊢ A \in ℝ$
2		areaquad.2	$⊢ B \in ℝ$
3		areaquad.3	$⊢ C \in ℝ$
4		areaquad.4	$⊢ D \in ℝ$
5		areaquad.5	$⊢ E \in ℝ$
6		areaquad.6	$⊢ F \in ℝ$
7		areaquad.7	$⊢ A < B$
8		areaquad.8	$⊢ C \leq E$
9		areaquad.9	$⊢ D \leq F$
10		areaquad.10	$⊢ U = C + (\frac{x - A}{B - A}) (D - C)$
11		areaquad.11	$⊢ V = E + (\frac{x - A}{B - A}) (F - E)$
12		areaquad.12	$⊢ S = \{⟨x, y⟩ \| (x \in [A, B] \land y \in [U, V])\}$
13		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
14	1 2 13	mp2an	$⊢ [A, B] \subseteq ℝ$
15	14	sseli	$⊢ x \in [A, B] \to x \in ℝ$
16	15	adantr	$⊢ (x \in [A, B] \land y \in [U, V]) \to x \in ℝ$
17	3	recni	$⊢ C \in ℂ$
18	17	a1i	$⊢ x \in ℝ \to C \in ℂ$
19		resubcl	$⊢ (x \in ℝ \land A \in ℝ) \to x - A \in ℝ$
20	1 19	mpan2	$⊢ x \in ℝ \to x - A \in ℝ$
21	2 1	resubcli	$⊢ B - A \in ℝ$
22	21	a1i	$⊢ x \in ℝ \to B - A \in ℝ$
23	2	recni	$⊢ B \in ℂ$
24	23	a1i	$⊢ A \in ℝ \to B \in ℂ$
25		recn	$⊢ A \in ℝ \to A \in ℂ$
26	1 7	gtneii	$⊢ B \neq A$
27	26	a1i	$⊢ A \in ℝ \to B \neq A$
28	24 25 27	subne0d	$⊢ A \in ℝ \to B - A \neq 0$
29	1 28	ax-mp	$⊢ B - A \neq 0$
30	29	a1i	$⊢ x \in ℝ \to B - A \neq 0$
31	20 22 30	redivcld	$⊢ x \in ℝ \to \frac{x - A}{B - A} \in ℝ$
32	31	recnd	$⊢ x \in ℝ \to \frac{x - A}{B - A} \in ℂ$
33	4	recni	$⊢ D \in ℂ$
34	33	a1i	$⊢ x \in ℝ \to D \in ℂ$
35	32 34	mulcld	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) D \in ℂ$
36	32 18	mulcld	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) C \in ℂ$
37	18 35 36	addsub12d	$⊢ x \in ℝ \to C + (\frac{x - A}{B - A}) D - (\frac{x - A}{B - A}) C = (\frac{x - A}{B - A}) D + C - (\frac{x - A}{B - A}) C$
38	32 34 18	subdid	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) (D - C) = (\frac{x - A}{B - A}) D - (\frac{x - A}{B - A}) C$
39	38	oveq2d	$⊢ x \in ℝ \to C + (\frac{x - A}{B - A}) (D - C) = C + (\frac{x - A}{B - A}) D - (\frac{x - A}{B - A}) C$
40	10 39	syl5eq	$⊢ x \in ℝ \to U = C + (\frac{x - A}{B - A}) D - (\frac{x - A}{B - A}) C$
41		1cnd	$⊢ x \in ℝ \to 1 \in ℂ$
42	41 32 18	subdird	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) C = 1 C - (\frac{x - A}{B - A}) C$
43	17	mulid2i	$⊢ 1 C = C$
44	43	oveq1i	$⊢ 1 C - (\frac{x - A}{B - A}) C = C - (\frac{x - A}{B - A}) C$
45	42 44	eqtrdi	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) C = C - (\frac{x - A}{B - A}) C$
46	45	oveq2d	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) D + (1 - (\frac{x - A}{B - A})) C = (\frac{x - A}{B - A}) D + C - (\frac{x - A}{B - A}) C$
47	37 40 46	3eqtr4d	$⊢ x \in ℝ \to U = (\frac{x - A}{B - A}) D + (1 - (\frac{x - A}{B - A})) C$
48		1red	$⊢ x \in ℝ \to 1 \in ℝ$
49	48 31	resubcld	$⊢ x \in ℝ \to 1 - (\frac{x - A}{B - A}) \in ℝ$
50	49	recnd	$⊢ x \in ℝ \to 1 - (\frac{x - A}{B - A}) \in ℂ$
51	50 18	mulcld	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) C \in ℂ$
52	35 51	addcomd	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) D + (1 - (\frac{x - A}{B - A})) C = (1 - (\frac{x - A}{B - A})) C + (\frac{x - A}{B - A}) D$
53	50 18	mulcomd	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) C = C (1 - (\frac{x - A}{B - A}))$
54	32 34	mulcomd	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) D = D (\frac{x - A}{B - A})$
55	53 54	oveq12d	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) C + (\frac{x - A}{B - A}) D = C (1 - (\frac{x - A}{B - A})) + D (\frac{x - A}{B - A})$
56	47 52 55	3eqtrd	$⊢ x \in ℝ \to U = C (1 - (\frac{x - A}{B - A})) + D (\frac{x - A}{B - A})$
57	3	a1i	$⊢ x \in ℝ \to C \in ℝ$
58	57 49	remulcld	$⊢ x \in ℝ \to C (1 - (\frac{x - A}{B - A})) \in ℝ$
59	4	a1i	$⊢ x \in ℝ \to D \in ℝ$
60	59 31	remulcld	$⊢ x \in ℝ \to D (\frac{x - A}{B - A}) \in ℝ$
61	58 60	readdcld	$⊢ x \in ℝ \to C (1 - (\frac{x - A}{B - A})) + D (\frac{x - A}{B - A}) \in ℝ$
62	56 61	eqeltrd	$⊢ x \in ℝ \to U \in ℝ$
63	5	recni	$⊢ E \in ℂ$
64	63	a1i	$⊢ x \in ℝ \to E \in ℂ$
65	6	recni	$⊢ F \in ℂ$
66	65	a1i	$⊢ x \in ℝ \to F \in ℂ$
67	32 66	mulcld	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) F \in ℂ$
68	32 64	mulcld	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) E \in ℂ$
69	64 67 68	addsub12d	$⊢ x \in ℝ \to E + (\frac{x - A}{B - A}) F - (\frac{x - A}{B - A}) E = (\frac{x - A}{B - A}) F + E - (\frac{x - A}{B - A}) E$
70	32 66 64	subdid	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) (F - E) = (\frac{x - A}{B - A}) F - (\frac{x - A}{B - A}) E$
71	70	oveq2d	$⊢ x \in ℝ \to E + (\frac{x - A}{B - A}) (F - E) = E + (\frac{x - A}{B - A}) F - (\frac{x - A}{B - A}) E$
72	11 71	syl5eq	$⊢ x \in ℝ \to V = E + (\frac{x - A}{B - A}) F - (\frac{x - A}{B - A}) E$
73	41 32 64	subdird	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) E = 1 E - (\frac{x - A}{B - A}) E$
74	63	mulid2i	$⊢ 1 E = E$
75	74	oveq1i	$⊢ 1 E - (\frac{x - A}{B - A}) E = E - (\frac{x - A}{B - A}) E$
76	73 75	eqtrdi	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) E = E - (\frac{x - A}{B - A}) E$
77	76	oveq2d	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) F + (1 - (\frac{x - A}{B - A})) E = (\frac{x - A}{B - A}) F + E - (\frac{x - A}{B - A}) E$
78	69 72 77	3eqtr4d	$⊢ x \in ℝ \to V = (\frac{x - A}{B - A}) F + (1 - (\frac{x - A}{B - A})) E$
79	50 64	mulcld	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) E \in ℂ$
80	67 79	addcomd	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) F + (1 - (\frac{x - A}{B - A})) E = (1 - (\frac{x - A}{B - A})) E + (\frac{x - A}{B - A}) F$
81	50 64	mulcomd	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) E = E (1 - (\frac{x - A}{B - A}))$
82	32 66	mulcomd	$⊢ x \in ℝ \to (\frac{x - A}{B - A}) F = F (\frac{x - A}{B - A})$
83	81 82	oveq12d	$⊢ x \in ℝ \to (1 - (\frac{x - A}{B - A})) E + (\frac{x - A}{B - A}) F = E (1 - (\frac{x - A}{B - A})) + F (\frac{x - A}{B - A})$
84	78 80 83	3eqtrd	$⊢ x \in ℝ \to V = E (1 - (\frac{x - A}{B - A})) + F (\frac{x - A}{B - A})$
85	5	a1i	$⊢ x \in ℝ \to E \in ℝ$
86	85 49	remulcld	$⊢ x \in ℝ \to E (1 - (\frac{x - A}{B - A})) \in ℝ$
87	6	a1i	$⊢ x \in ℝ \to F \in ℝ$
88	87 31	remulcld	$⊢ x \in ℝ \to F (\frac{x - A}{B - A}) \in ℝ$
89	86 88	readdcld	$⊢ x \in ℝ \to E (1 - (\frac{x - A}{B - A})) + F (\frac{x - A}{B - A}) \in ℝ$
90	84 89	eqeltrd	$⊢ x \in ℝ \to V \in ℝ$
91		iccssre	$⊢ (U \in ℝ \land V \in ℝ) \to [U, V] \subseteq ℝ$
92	62 90 91	syl2anc	$⊢ x \in ℝ \to [U, V] \subseteq ℝ$
93	15 92	syl	$⊢ x \in [A, B] \to [U, V] \subseteq ℝ$
94	93	sselda	$⊢ (x \in [A, B] \land y \in [U, V]) \to y \in ℝ$
95	16 94	jca	$⊢ (x \in [A, B] \land y \in [U, V]) \to (x \in ℝ \land y \in ℝ)$
96	95	ssopab2i	$⊢ \{⟨x, y⟩ \| (x \in [A, B] \land y \in [U, V])\} \subseteq \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ)\}$
97		df-xp	$⊢ ℝ^{2} = \{⟨x, y⟩ \| (x \in ℝ \land y \in ℝ)\}$
98	96 12 97	3sstr4i	$⊢ S \subseteq ℝ^{2}$
99		iftrue	$⊢ x \in [A, B] \to if (x \in [A, B], V - U, 0) = V - U$
100		nfv	$⊢ Ⅎ y x \in [A, B]$
101		nfopab2	$⊢ \underline{Ⅎ} y \{⟨x, y⟩ \| (x \in [A, B] \land y \in [U, V])\}$
102	12 101	nfcxfr	$⊢ \underline{Ⅎ} y S$
103		nfcv	$⊢ \underline{Ⅎ} y \{x\}$
104	102 103	nfima	$⊢ \underline{Ⅎ} y S [\{x\}]$
105		nfcv	$⊢ \underline{Ⅎ} y [U, V]$
106		vex	$⊢ x \in V$
107		vex	$⊢ y \in V$
108	106 107	elimasn	$⊢ y \in S [\{x\}] \leftrightarrow ⟨x, y⟩ \in S$
109	12	eleq2i	$⊢ ⟨x, y⟩ \in S \leftrightarrow ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in [A, B] \land y \in [U, V])\}$
110		opabidw	$⊢ ⟨x, y⟩ \in \{⟨x, y⟩ \| (x \in [A, B] \land y \in [U, V])\} \leftrightarrow (x \in [A, B] \land y \in [U, V])$
111	108 109 110	3bitri	$⊢ y \in S [\{x\}] \leftrightarrow (x \in [A, B] \land y \in [U, V])$
112	111	baib	$⊢ x \in [A, B] \to (y \in S [\{x\}] \leftrightarrow y \in [U, V])$
113	100 104 105 112	eqrd	$⊢ x \in [A, B] \to S [\{x\}] = [U, V]$
114	113	fveq2d	$⊢ x \in [A, B] \to vol (S [\{x\}]) = vol ([U, V])$
115	15 62	syl	$⊢ x \in [A, B] \to U \in ℝ$
116	15 90	syl	$⊢ x \in [A, B] \to V \in ℝ$
117		iccmbl	$⊢ (U \in ℝ \land V \in ℝ) \to [U, V] \in dom vol$
118	115 116 117	syl2anc	$⊢ x \in [A, B] \to [U, V] \in dom vol$
119		mblvol	$⊢ [U, V] \in dom vol \to vol ([U, V]) = {vol}^{*} ([U, V])$
120	118 119	syl	$⊢ x \in [A, B] \to vol ([U, V]) = {vol}^{*} ([U, V])$
121	15 58	syl	$⊢ x \in [A, B] \to C (1 - (\frac{x - A}{B - A})) \in ℝ$
122	15 60	syl	$⊢ x \in [A, B] \to D (\frac{x - A}{B - A}) \in ℝ$
123	15 86	syl	$⊢ x \in [A, B] \to E (1 - (\frac{x - A}{B - A})) \in ℝ$
124	15 88	syl	$⊢ x \in [A, B] \to F (\frac{x - A}{B - A}) \in ℝ$
125	3	a1i	$⊢ x \in [A, B] \to C \in ℝ$
126	5	a1i	$⊢ x \in [A, B] \to E \in ℝ$
127	15 49	syl	$⊢ x \in [A, B] \to 1 - (\frac{x - A}{B - A}) \in ℝ$
128	15 31	syl	$⊢ x \in [A, B] \to \frac{x - A}{B - A} \in ℝ$
129	128	recnd	$⊢ x \in [A, B] \to \frac{x - A}{B - A} \in ℂ$
130	129	subidd	$⊢ x \in [A, B] \to (\frac{x - A}{B - A}) - (\frac{x - A}{B - A}) = 0$
131		1red	$⊢ x \in [A, B] \to 1 \in ℝ$
132	2	a1i	$⊢ x \in [A, B] \to B \in ℝ$
133	1	a1i	$⊢ x \in [A, B] \to A \in ℝ$
134	1	rexri	$⊢ A \in ℝ^{*}$
135	2	rexri	$⊢ B \in ℝ^{*}$
136		iccleub	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to x \leq B$
137	134 135 136	mp3an12	$⊢ x \in [A, B] \to x \leq B$
138	15 132 133 137	lesub1dd	$⊢ x \in [A, B] \to x - A \leq B - A$
139	15 1 19	sylancl	$⊢ x \in [A, B] \to x - A \in ℝ$
140	21	a1i	$⊢ x \in [A, B] \to B - A \in ℝ$
141	1	recni	$⊢ A \in ℂ$
142	141	subidi	$⊢ A - A = 0$
143	133 132 133	ltsub1d	$⊢ x \in [A, B] \to (A < B \leftrightarrow A - A < B - A)$
144	7 143	mpbii	$⊢ x \in [A, B] \to A - A < B - A$
145	142 144	eqbrtrrid	$⊢ x \in [A, B] \to 0 < B - A$
146		lediv1	$⊢ (x - A \in ℝ \land B - A \in ℝ \land (B - A \in ℝ \land 0 < B - A)) \to (x - A \leq B - A \leftrightarrow \frac{x - A}{B - A} \leq \frac{B - A}{B - A})$
147	139 140 140 145 146	syl112anc	$⊢ x \in [A, B] \to (x - A \leq B - A \leftrightarrow \frac{x - A}{B - A} \leq \frac{B - A}{B - A})$
148	138 147	mpbid	$⊢ x \in [A, B] \to \frac{x - A}{B - A} \leq \frac{B - A}{B - A}$
149	21	recni	$⊢ B - A \in ℂ$
150	149 29	dividi	$⊢ \frac{B - A}{B - A} = 1$
151	148 150	breqtrdi	$⊢ x \in [A, B] \to \frac{x - A}{B - A} \leq 1$
152	128 131 128 151	lesub1dd	$⊢ x \in [A, B] \to (\frac{x - A}{B - A}) - (\frac{x - A}{B - A}) \leq 1 - (\frac{x - A}{B - A})$
153	130 152	eqbrtrrd	$⊢ x \in [A, B] \to 0 \leq 1 - (\frac{x - A}{B - A})$
154	8	a1i	$⊢ x \in [A, B] \to C \leq E$
155	125 126 127 153 154	lemul1ad	$⊢ x \in [A, B] \to C (1 - (\frac{x - A}{B - A})) \leq E (1 - (\frac{x - A}{B - A}))$
156	4	a1i	$⊢ x \in [A, B] \to D \in ℝ$
157	6	a1i	$⊢ x \in [A, B] \to F \in ℝ$
158	140 145	elrpd	$⊢ x \in [A, B] \to B - A \in ℝ^{+}$
159		iccgelb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land x \in [A, B]) \to A \leq x$
160	134 135 159	mp3an12	$⊢ x \in [A, B] \to A \leq x$
161	133 15 133 160	lesub1dd	$⊢ x \in [A, B] \to A - A \leq x - A$
162	142 161	eqbrtrrid	$⊢ x \in [A, B] \to 0 \leq x - A$
163	139 158 162	divge0d	$⊢ x \in [A, B] \to 0 \leq \frac{x - A}{B - A}$
164	9	a1i	$⊢ x \in [A, B] \to D \leq F$
165	156 157 128 163 164	lemul1ad	$⊢ x \in [A, B] \to D (\frac{x - A}{B - A}) \leq F (\frac{x - A}{B - A})$
166	121 122 123 124 155 165	le2addd	$⊢ x \in [A, B] \to C (1 - (\frac{x - A}{B - A})) + D (\frac{x - A}{B - A}) \leq E (1 - (\frac{x - A}{B - A})) + F (\frac{x - A}{B - A})$
167	15 56	syl	$⊢ x \in [A, B] \to U = C (1 - (\frac{x - A}{B - A})) + D (\frac{x - A}{B - A})$
168	15 84	syl	$⊢ x \in [A, B] \to V = E (1 - (\frac{x - A}{B - A})) + F (\frac{x - A}{B - A})$
169	166 167 168	3brtr4d	$⊢ x \in [A, B] \to U \leq V$
170		ovolicc	$⊢ (U \in ℝ \land V \in ℝ \land U \leq V) \to {vol}^{*} ([U, V]) = V - U$
171	115 116 169 170	syl3anc	$⊢ x \in [A, B] \to {vol}^{*} ([U, V]) = V - U$
172	114 120 171	3eqtrd	$⊢ x \in [A, B] \to vol (S [\{x\}]) = V - U$
173	99 172	eqtr4d	$⊢ x \in [A, B] \to if (x \in [A, B], V - U, 0) = vol (S [\{x\}])$
174		iffalse	$⊢ \neg x \in [A, B] \to if (x \in [A, B], V - U, 0) = 0$
175		nfv	$⊢ Ⅎ y \neg x \in [A, B]$
176		nfcv	$⊢ \underline{Ⅎ} y \emptyset$
177	111	simplbi	$⊢ y \in S [\{x\}] \to x \in [A, B]$
178		noel	$⊢ \neg y \in \emptyset$
179	178	pm2.21i	$⊢ y \in \emptyset \to x \in [A, B]$
180	177 179	pm5.21ni	$⊢ \neg x \in [A, B] \to (y \in S [\{x\}] \leftrightarrow y \in \emptyset)$
181	175 104 176 180	eqrd	$⊢ \neg x \in [A, B] \to S [\{x\}] = \emptyset$
182	181	fveq2d	$⊢ \neg x \in [A, B] \to vol (S [\{x\}]) = vol (\emptyset)$
183		0mbl	$⊢ \emptyset \in dom vol$
184		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
185	183 184	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
186		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
187	185 186	eqtri	$⊢ vol (\emptyset) = 0$
188	182 187	eqtrdi	$⊢ \neg x \in [A, B] \to vol (S [\{x\}]) = 0$
189	174 188	eqtr4d	$⊢ \neg x \in [A, B] \to if (x \in [A, B], V - U, 0) = vol (S [\{x\}])$
190	173 189	pm2.61i	$⊢ if (x \in [A, B], V - U, 0) = vol (S [\{x\}])$
191	190	eqcomi	$⊢ vol (S [\{x\}]) = if (x \in [A, B], V - U, 0)$
192	90 62	resubcld	$⊢ x \in ℝ \to V - U \in ℝ$
193		0re	$⊢ 0 \in ℝ$
194		ifcl	$⊢ (V - U \in ℝ \land 0 \in ℝ) \to if (x \in [A, B], V - U, 0) \in ℝ$
195	192 193 194	sylancl	$⊢ x \in ℝ \to if (x \in [A, B], V - U, 0) \in ℝ$
196	191 195	eqeltrid	$⊢ x \in ℝ \to vol (S [\{x\}]) \in ℝ$
197		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
198		ffun	$⊢ vol : dom vol ⟶ [0, +∞] \to Fun vol$
199	197 198	ax-mp	$⊢ Fun vol$
200		iftrue	$⊢ x \in [A, B] \to if (x \in [A, B], [U, V], \emptyset) = [U, V]$
201	113 200	eqtr4d	$⊢ x \in [A, B] \to S [\{x\}] = if (x \in [A, B], [U, V], \emptyset)$
202		iffalse	$⊢ \neg x \in [A, B] \to if (x \in [A, B], [U, V], \emptyset) = \emptyset$
203	181 202	eqtr4d	$⊢ \neg x \in [A, B] \to S [\{x\}] = if (x \in [A, B], [U, V], \emptyset)$
204	201 203	pm2.61i	$⊢ S [\{x\}] = if (x \in [A, B], [U, V], \emptyset)$
205	62 90 117	syl2anc	$⊢ x \in ℝ \to [U, V] \in dom vol$
206	183	a1i	$⊢ x \in ℝ \to \emptyset \in dom vol$
207	205 206	ifcld	$⊢ x \in ℝ \to if (x \in [A, B], [U, V], \emptyset) \in dom vol$
208	204 207	eqeltrid	$⊢ x \in ℝ \to S [\{x\}] \in dom vol$
209		fvimacnv	$⊢ (Fun vol \land S [\{x\}] \in dom vol) \to (vol (S [\{x\}]) \in ℝ \leftrightarrow S [\{x\}] \in {vol}^{-1} [ℝ])$
210	199 208 209	sylancr	$⊢ x \in ℝ \to (vol (S [\{x\}]) \in ℝ \leftrightarrow S [\{x\}] \in {vol}^{-1} [ℝ])$
211	196 210	mpbid	$⊢ x \in ℝ \to S [\{x\}] \in {vol}^{-1} [ℝ]$
212	211	rgen	$⊢ \forall x \in ℝ S [\{x\}] \in {vol}^{-1} [ℝ]$
213	14	a1i	$⊢ 0 \in ℝ \to [A, B] \subseteq ℝ$
214		rembl	$⊢ ℝ \in dom vol$
215	214	a1i	$⊢ 0 \in ℝ \to ℝ \in dom vol$
216	116 115	resubcld	$⊢ x \in [A, B] \to V - U \in ℝ$
217	172 216	eqeltrd	$⊢ x \in [A, B] \to vol (S [\{x\}]) \in ℝ$
218	217	adantl	$⊢ (0 \in ℝ \land x \in [A, B]) \to vol (S [\{x\}]) \in ℝ$
219		eldifn	$⊢ x \in (ℝ ∖ [A, B]) \to \neg x \in [A, B]$
220	219 188	syl	$⊢ x \in (ℝ ∖ [A, B]) \to vol (S [\{x\}]) = 0$
221	220	adantl	$⊢ (0 \in ℝ \land x \in (ℝ ∖ [A, B])) \to vol (S [\{x\}]) = 0$
222	172	mpteq2ia	$⊢ (x \in [A, B] ⟼ vol (S [\{x\}])) = (x \in [A, B] ⟼ V - U)$
223		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
224	223	subcn	$⊢ - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
225	224	a1i	$⊢ ⊤ \to - \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
226	11	mpteq2i	$⊢ (x \in [A, B] ⟼ V) = (x \in [A, B] ⟼ E + (\frac{x - A}{B - A}) (F - E))$
227	223	addcn	$⊢ + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
228	227	a1i	$⊢ ⊤ \to + \in ((TopOpen (ℂ_{fld}) \times_{t} TopOpen (ℂ_{fld})) Cn TopOpen (ℂ_{fld}))$
229		ax-resscn	$⊢ ℝ \subseteq ℂ$
230	14 229	sstri	$⊢ [A, B] \subseteq ℂ$
231		ssid	$⊢ ℂ \subseteq ℂ$
232		cncfmptc	$⊢ (E \in ℂ \land [A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [A, B] ⟼ E) : [A, B] \underset{cn}{⟶} ℂ$
233	63 230 231 232	mp3an	$⊢ (x \in [A, B] ⟼ E) : [A, B] \underset{cn}{⟶} ℂ$
234	233	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ E) : [A, B] \underset{cn}{⟶} ℂ$
235	230	sseli	$⊢ x \in [A, B] \to x \in ℂ$
236	141	a1i	$⊢ x \in [A, B] \to A \in ℂ$
237	149	a1i	$⊢ x \in [A, B] \to B - A \in ℂ$
238	29	a1i	$⊢ x \in [A, B] \to B - A \neq 0$
239	235 236 237 238	divsubdird	$⊢ x \in [A, B] \to \frac{x - A}{B - A} = (\frac{x}{B - A}) - (\frac{A}{B - A})$
240	239	adantl	$⊢ (⊤ \land x \in [A, B]) \to \frac{x - A}{B - A} = (\frac{x}{B - A}) - (\frac{A}{B - A})$
241	240	mpteq2dva	$⊢ ⊤ \to (x \in [A, B] ⟼ \frac{x - A}{B - A}) = (x \in [A, B] ⟼ (\frac{x}{B - A}) - (\frac{A}{B - A}))$
242		resmpt	$⊢ [A, B] \subseteq ℂ \to {(x \in ℂ ⟼ \frac{x}{B - A}) ↾}_{[A, B]} = (x \in [A, B] ⟼ \frac{x}{B - A})$
243	230 242	ax-mp	$⊢ {(x \in ℂ ⟼ \frac{x}{B - A}) ↾}_{[A, B]} = (x \in [A, B] ⟼ \frac{x}{B - A})$
244		eqid	$⊢ (x \in ℂ ⟼ \frac{x}{B - A}) = (x \in ℂ ⟼ \frac{x}{B - A})$
245	244	divccncf	$⊢ (B - A \in ℂ \land B - A \neq 0) \to (x \in ℂ ⟼ \frac{x}{B - A}) : ℂ \underset{cn}{⟶} ℂ$
246	149 29 245	mp2an	$⊢ (x \in ℂ ⟼ \frac{x}{B - A}) : ℂ \underset{cn}{⟶} ℂ$
247		rescncf	$⊢ [A, B] \subseteq ℂ \to ((x \in ℂ ⟼ \frac{x}{B - A}) : ℂ \underset{cn}{⟶} ℂ \to ({(x \in ℂ ⟼ \frac{x}{B - A}) ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ)$
248	230 246 247	mp2	$⊢ ({(x \in ℂ ⟼ \frac{x}{B - A}) ↾}_{[A, B]}) : [A, B] \underset{cn}{⟶} ℂ$
249	243 248	eqeltrri	$⊢ (x \in [A, B] ⟼ \frac{x}{B - A}) : [A, B] \underset{cn}{⟶} ℂ$
250	249	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ \frac{x}{B - A}) : [A, B] \underset{cn}{⟶} ℂ$
251	141 149 29	divcli	$⊢ \frac{A}{B - A} \in ℂ$
252		cncfmptc	$⊢ (\frac{A}{B - A} \in ℂ \land [A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [A, B] ⟼ \frac{A}{B - A}) : [A, B] \underset{cn}{⟶} ℂ$
253	251 230 231 252	mp3an	$⊢ (x \in [A, B] ⟼ \frac{A}{B - A}) : [A, B] \underset{cn}{⟶} ℂ$
254	253	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ \frac{A}{B - A}) : [A, B] \underset{cn}{⟶} ℂ$
255	223 225 250 254	cncfmpt2f	$⊢ ⊤ \to (x \in [A, B] ⟼ (\frac{x}{B - A}) - (\frac{A}{B - A})) : [A, B] \underset{cn}{⟶} ℂ$
256	241 255	eqeltrd	$⊢ ⊤ \to (x \in [A, B] ⟼ \frac{x - A}{B - A}) : [A, B] \underset{cn}{⟶} ℂ$
257		cncfmptc	$⊢ (F \in ℂ \land [A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [A, B] ⟼ F) : [A, B] \underset{cn}{⟶} ℂ$
258	65 230 231 257	mp3an	$⊢ (x \in [A, B] ⟼ F) : [A, B] \underset{cn}{⟶} ℂ$
259	258	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ F) : [A, B] \underset{cn}{⟶} ℂ$
260	223 225 259 234	cncfmpt2f	$⊢ ⊤ \to (x \in [A, B] ⟼ F - E) : [A, B] \underset{cn}{⟶} ℂ$
261	256 260	mulcncf	$⊢ ⊤ \to (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (F - E)) : [A, B] \underset{cn}{⟶} ℂ$
262	223 228 234 261	cncfmpt2f	$⊢ ⊤ \to (x \in [A, B] ⟼ E + (\frac{x - A}{B - A}) (F - E)) : [A, B] \underset{cn}{⟶} ℂ$
263	226 262	eqeltrid	$⊢ ⊤ \to (x \in [A, B] ⟼ V) : [A, B] \underset{cn}{⟶} ℂ$
264	10	mpteq2i	$⊢ (x \in [A, B] ⟼ U) = (x \in [A, B] ⟼ C + (\frac{x - A}{B - A}) (D - C))$
265		cncfmptc	$⊢ (C \in ℂ \land [A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [A, B] ⟼ C) : [A, B] \underset{cn}{⟶} ℂ$
266	17 230 231 265	mp3an	$⊢ (x \in [A, B] ⟼ C) : [A, B] \underset{cn}{⟶} ℂ$
267	266	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ C) : [A, B] \underset{cn}{⟶} ℂ$
268		cncfmptc	$⊢ (D \in ℂ \land [A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [A, B] ⟼ D) : [A, B] \underset{cn}{⟶} ℂ$
269	33 230 231 268	mp3an	$⊢ (x \in [A, B] ⟼ D) : [A, B] \underset{cn}{⟶} ℂ$
270	269	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ D) : [A, B] \underset{cn}{⟶} ℂ$
271	223 225 270 267	cncfmpt2f	$⊢ ⊤ \to (x \in [A, B] ⟼ D - C) : [A, B] \underset{cn}{⟶} ℂ$
272	256 271	mulcncf	$⊢ ⊤ \to (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (D - C)) : [A, B] \underset{cn}{⟶} ℂ$
273	223 228 267 272	cncfmpt2f	$⊢ ⊤ \to (x \in [A, B] ⟼ C + (\frac{x - A}{B - A}) (D - C)) : [A, B] \underset{cn}{⟶} ℂ$
274	264 273	eqeltrid	$⊢ ⊤ \to (x \in [A, B] ⟼ U) : [A, B] \underset{cn}{⟶} ℂ$
275	223 225 263 274	cncfmpt2f	$⊢ ⊤ \to (x \in [A, B] ⟼ V - U) : [A, B] \underset{cn}{⟶} ℂ$
276	275	mptru	$⊢ (x \in [A, B] ⟼ V - U) : [A, B] \underset{cn}{⟶} ℂ$
277		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ V - U) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ V - U) \in 𝐿^{1}$
278	1 2 276 277	mp3an	$⊢ (x \in [A, B] ⟼ V - U) \in 𝐿^{1}$
279	222 278	eqeltri	$⊢ (x \in [A, B] ⟼ vol (S [\{x\}])) \in 𝐿^{1}$
280	279	a1i	$⊢ 0 \in ℝ \to (x \in [A, B] ⟼ vol (S [\{x\}])) \in 𝐿^{1}$
281	213 215 218 221 280	iblss2	$⊢ 0 \in ℝ \to (x \in ℝ ⟼ vol (S [\{x\}])) \in 𝐿^{1}$
282	193 281	ax-mp	$⊢ (x \in ℝ ⟼ vol (S [\{x\}])) \in 𝐿^{1}$
283		dmarea	$⊢ S \in dom area \leftrightarrow (S \subseteq ℝ^{2} \land \forall x \in ℝ S [\{x\}] \in {vol}^{-1} [ℝ] \land (x \in ℝ ⟼ vol (S [\{x\}])) \in 𝐿^{1})$
284	98 212 282 283	mpbir3an	$⊢ S \in dom area$
285		areaval	$⊢ S \in dom area \to area (S) = \int_{ℝ} vol (S [\{x\}]) d x$
286	284 285	ax-mp	$⊢ area (S) = \int_{ℝ} vol (S [\{x\}]) d x$
287		itgeq2	$⊢ \forall x \in ℝ vol (S [\{x\}]) = if (x \in [A, B], V - U, 0) \to \int_{ℝ} vol (S [\{x\}]) d x = \int_{ℝ} if (x \in [A, B], V - U, 0) d x$
288	191	a1i	$⊢ x \in ℝ \to vol (S [\{x\}]) = if (x \in [A, B], V - U, 0)$
289	287 288	mprg	$⊢ \int_{ℝ} vol (S [\{x\}]) d x = \int_{ℝ} if (x \in [A, B], V - U, 0) d x$
290		itgss2	$⊢ [A, B] \subseteq ℝ \to \int_{[A, B]} (V - U) d x = \int_{ℝ} if (x \in [A, B], V - U, 0) d x$
291	14 290	ax-mp	$⊢ \int_{[A, B]} (V - U) d x = \int_{ℝ} if (x \in [A, B], V - U, 0) d x$
292	65 63	addcli	$⊢ F + E \in ℂ$
293		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
294		div32	$⊢ (F + E \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land B - A \in ℂ) \to (\frac{F + E}{2}) (B - A) = (F + E) (\frac{B - A}{2})$
295	292 293 149 294	mp3an	$⊢ (\frac{F + E}{2}) (B - A) = (F + E) (\frac{B - A}{2})$
296	33 17	addcli	$⊢ D + C \in ℂ$
297		div32	$⊢ (D + C \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land B - A \in ℂ) \to (\frac{D + C}{2}) (B - A) = (D + C) (\frac{B - A}{2})$
298	296 293 149 297	mp3an	$⊢ (\frac{D + C}{2}) (B - A) = (D + C) (\frac{B - A}{2})$
299	295 298	oveq12i	$⊢ (\frac{F + E}{2}) (B - A) - (\frac{D + C}{2}) (B - A) = (F + E) (\frac{B - A}{2}) - (D + C) (\frac{B - A}{2})$
300		2cn	$⊢ 2 \in ℂ$
301		2ne0	$⊢ 2 \neq 0$
302	292 300 301	divcli	$⊢ \frac{F + E}{2} \in ℂ$
303	296 300 301	divcli	$⊢ \frac{D + C}{2} \in ℂ$
304	302 303 149	subdiri	$⊢ ((\frac{F + E}{2}) - (\frac{D + C}{2})) (B - A) = (\frac{F + E}{2}) (B - A) - (\frac{D + C}{2}) (B - A)$
305	116	adantl	$⊢ (⊤ \land x \in [A, B]) \to V \in ℝ$
306	263	mptru	$⊢ (x \in [A, B] ⟼ V) : [A, B] \underset{cn}{⟶} ℂ$
307		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ V) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ V) \in 𝐿^{1}$
308	1 2 306 307	mp3an	$⊢ (x \in [A, B] ⟼ V) \in 𝐿^{1}$
309	308	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ V) \in 𝐿^{1}$
310	115	adantl	$⊢ (⊤ \land x \in [A, B]) \to U \in ℝ$
311	274	mptru	$⊢ (x \in [A, B] ⟼ U) : [A, B] \underset{cn}{⟶} ℂ$
312		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ U) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ U) \in 𝐿^{1}$
313	1 2 311 312	mp3an	$⊢ (x \in [A, B] ⟼ U) \in 𝐿^{1}$
314	313	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ U) \in 𝐿^{1}$
315	305 309 310 314	itgsub	$⊢ ⊤ \to \int_{[A, B]} (V - U) d x = \int_{[A, B]} V d x - \int_{[A, B]} U d x$
316	315	mptru	$⊢ \int_{[A, B]} (V - U) d x = \int_{[A, B]} V d x - \int_{[A, B]} U d x$
317	63 300 301	divcan4i	$⊢ \frac{E \cdot 2}{2} = E$
318	317	oveq1i	$⊢ (\frac{E \cdot 2}{2}) (B - A) = E (B - A)$
319	63 300	mulcli	$⊢ E \cdot 2 \in ℂ$
320		div32	$⊢ (E \cdot 2 \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land B - A \in ℂ) \to (\frac{E \cdot 2}{2}) (B - A) = E \cdot 2 (\frac{B - A}{2})$
321	319 293 149 320	mp3an	$⊢ (\frac{E \cdot 2}{2}) (B - A) = E \cdot 2 (\frac{B - A}{2})$
322	318 321	eqtr3i	$⊢ E (B - A) = E \cdot 2 (\frac{B - A}{2})$
323	322	oveq1i	$⊢ E (B - A) + (F - E) (\frac{B - A}{2}) = E \cdot 2 (\frac{B - A}{2}) + (F - E) (\frac{B - A}{2})$
324		itgeq2	$⊢ \forall x \in [A, B] V = E + (\frac{x - A}{B - A}) (F - E) \to \int_{[A, B]} V d x = \int_{[A, B]} (E + (\frac{x - A}{B - A}) (F - E)) d x$
325	11	a1i	$⊢ x \in [A, B] \to V = E + (\frac{x - A}{B - A}) (F - E)$
326	324 325	mprg	$⊢ \int_{[A, B]} V d x = \int_{[A, B]} (E + (\frac{x - A}{B - A}) (F - E)) d x$
327	5	a1i	$⊢ (⊤ \land x \in [A, B]) \to E \in ℝ$
328		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ E) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ E) \in 𝐿^{1}$
329	1 2 233 328	mp3an	$⊢ (x \in [A, B] ⟼ E) \in 𝐿^{1}$
330	329	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ E) \in 𝐿^{1}$
331	128	adantl	$⊢ (⊤ \land x \in [A, B]) \to \frac{x - A}{B - A} \in ℝ$
332	6	a1i	$⊢ (⊤ \land x \in [A, B]) \to F \in ℝ$
333	332 327	resubcld	$⊢ (⊤ \land x \in [A, B]) \to F - E \in ℝ$
334	331 333	remulcld	$⊢ (⊤ \land x \in [A, B]) \to (\frac{x - A}{B - A}) (F - E) \in ℝ$
335	261	mptru	$⊢ (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (F - E)) : [A, B] \underset{cn}{⟶} ℂ$
336		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (F - E)) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (F - E)) \in 𝐿^{1}$
337	1 2 335 336	mp3an	$⊢ (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (F - E)) \in 𝐿^{1}$
338	337	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (F - E)) \in 𝐿^{1}$
339	327 330 334 338	itgadd	$⊢ ⊤ \to \int_{[A, B]} (E + (\frac{x - A}{B - A}) (F - E)) d x = \int_{[A, B]} E d x + \int_{[A, B]} (\frac{x - A}{B - A}) (F - E) d x$
340	339	mptru	$⊢ \int_{[A, B]} (E + (\frac{x - A}{B - A}) (F - E)) d x = \int_{[A, B]} E d x + \int_{[A, B]} (\frac{x - A}{B - A}) (F - E) d x$
341		iccmbl	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \in dom vol$
342	1 2 341	mp2an	$⊢ [A, B] \in dom vol$
343		mblvol	$⊢ [A, B] \in dom vol \to vol ([A, B]) = {vol}^{*} ([A, B])$
344	342 343	ax-mp	$⊢ vol ([A, B]) = {vol}^{*} ([A, B])$
345	1 2 7	ltleii	$⊢ A \leq B$
346		ovolicc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ([A, B]) = B - A$
347	1 2 345 346	mp3an	$⊢ {vol}^{*} ([A, B]) = B - A$
348	344 347	eqtri	$⊢ vol ([A, B]) = B - A$
349	348 21	eqeltri	$⊢ vol ([A, B]) \in ℝ$
350		itgconst	$⊢ ([A, B] \in dom vol \land vol ([A, B]) \in ℝ \land E \in ℂ) \to \int_{[A, B]} E d x = E vol ([A, B])$
351	342 349 63 350	mp3an	$⊢ \int_{[A, B]} E d x = E vol ([A, B])$
352	348	oveq2i	$⊢ E vol ([A, B]) = E (B - A)$
353	351 352	eqtri	$⊢ \int_{[A, B]} E d x = E (B - A)$
354	65	a1i	$⊢ ⊤ \to F \in ℂ$
355	63	a1i	$⊢ ⊤ \to E \in ℂ$
356	354 355	subcld	$⊢ ⊤ \to F - E \in ℂ$
357	256	mptru	$⊢ (x \in [A, B] ⟼ \frac{x - A}{B - A}) : [A, B] \underset{cn}{⟶} ℂ$
358		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ \frac{x - A}{B - A}) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ \frac{x - A}{B - A}) \in 𝐿^{1}$
359	1 2 357 358	mp3an	$⊢ (x \in [A, B] ⟼ \frac{x - A}{B - A}) \in 𝐿^{1}$
360	359	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ \frac{x - A}{B - A}) \in 𝐿^{1}$
361	356 331 360	itgmulc2	$⊢ ⊤ \to (F - E) \int_{[A, B]} (\frac{x - A}{B - A}) d x = \int_{[A, B]} (F - E) (\frac{x - A}{B - A}) d x$
362	361	mptru	$⊢ (F - E) \int_{[A, B]} (\frac{x - A}{B - A}) d x = \int_{[A, B]} (F - E) (\frac{x - A}{B - A}) d x$
363		itgeq2	$⊢ \forall x \in [A, B] \frac{x - A}{B - A} = (\frac{1}{B - A}) (x - A) \to \int_{[A, B]} (\frac{x - A}{B - A}) d x = \int_{[A, B]} (\frac{1}{B - A}) (x - A) d x$
364	139	recnd	$⊢ x \in [A, B] \to x - A \in ℂ$
365	364 237 238	divrec2d	$⊢ x \in [A, B] \to \frac{x - A}{B - A} = (\frac{1}{B - A}) (x - A)$
366	363 365	mprg	$⊢ \int_{[A, B]} (\frac{x - A}{B - A}) d x = \int_{[A, B]} (\frac{1}{B - A}) (x - A) d x$
367	15	adantl	$⊢ (⊤ \land x \in [A, B]) \to x \in ℝ$
368		cncfmptid	$⊢ ([A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [A, B] ⟼ x) : [A, B] \underset{cn}{⟶} ℂ$
369	230 231 368	mp2an	$⊢ (x \in [A, B] ⟼ x) : [A, B] \underset{cn}{⟶} ℂ$
370		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ x) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ x) \in 𝐿^{1}$
371	1 2 369 370	mp3an	$⊢ (x \in [A, B] ⟼ x) \in 𝐿^{1}$
372	371	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ x) \in 𝐿^{1}$
373	1	a1i	$⊢ (⊤ \land x \in [A, B]) \to A \in ℝ$
374		cncfmptc	$⊢ (A \in ℂ \land [A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [A, B] ⟼ A) : [A, B] \underset{cn}{⟶} ℂ$
375	141 230 231 374	mp3an	$⊢ (x \in [A, B] ⟼ A) : [A, B] \underset{cn}{⟶} ℂ$
376		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ A) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ A) \in 𝐿^{1}$
377	1 2 375 376	mp3an	$⊢ (x \in [A, B] ⟼ A) \in 𝐿^{1}$
378	377	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ A) \in 𝐿^{1}$
379	367 372 373 378	itgsub	$⊢ ⊤ \to \int_{[A, B]} (x - A) d x = \int_{[A, B]} x d x - \int_{[A, B]} A d x$
380	379	mptru	$⊢ \int_{[A, B]} (x - A) d x = \int_{[A, B]} x d x - \int_{[A, B]} A d x$
381	1	a1i	$⊢ ⊤ \to A \in ℝ$
382	2	a1i	$⊢ ⊤ \to B \in ℝ$
383	345	a1i	$⊢ ⊤ \to A \leq B$
384		1nn0	$⊢ 1 \in ℕ_{0}$
385	384	a1i	$⊢ ⊤ \to 1 \in ℕ_{0}$
386	381 382 383 385	itgpowd	$⊢ ⊤ \to \int_{[A, B]} x^{1} d x = \frac{B^{1 + 1} - A^{1 + 1}}{1 + 1}$
387	386	mptru	$⊢ \int_{[A, B]} x^{1} d x = \frac{B^{1 + 1} - A^{1 + 1}}{1 + 1}$
388		1p1e2	$⊢ 1 + 1 = 2$
389	388	oveq2i	$⊢ \frac{B^{1 + 1} - A^{1 + 1}}{1 + 1} = \frac{B^{1 + 1} - A^{1 + 1}}{2}$
390	387 389	eqtri	$⊢ \int_{[A, B]} x^{1} d x = \frac{B^{1 + 1} - A^{1 + 1}}{2}$
391		itgeq2	$⊢ \forall x \in [A, B] x^{1} = x \to \int_{[A, B]} x^{1} d x = \int_{[A, B]} x d x$
392	235	exp1d	$⊢ x \in [A, B] \to x^{1} = x$
393	391 392	mprg	$⊢ \int_{[A, B]} x^{1} d x = \int_{[A, B]} x d x$
394	388	oveq2i	$⊢ B^{1 + 1} = B^{2}$
395	388	oveq2i	$⊢ A^{1 + 1} = A^{2}$
396	394 395	oveq12i	$⊢ B^{1 + 1} - A^{1 + 1} = B^{2} - A^{2}$
397	396	oveq1i	$⊢ \frac{B^{1 + 1} - A^{1 + 1}}{2} = \frac{B^{2} - A^{2}}{2}$
398	390 393 397	3eqtr3i	$⊢ \int_{[A, B]} x d x = \frac{B^{2} - A^{2}}{2}$
399		itgconst	$⊢ ([A, B] \in dom vol \land vol ([A, B]) \in ℝ \land A \in ℂ) \to \int_{[A, B]} A d x = A vol ([A, B])$
400	342 349 141 399	mp3an	$⊢ \int_{[A, B]} A d x = A vol ([A, B])$
401	348	oveq2i	$⊢ A vol ([A, B]) = A (B - A)$
402	400 401	eqtri	$⊢ \int_{[A, B]} A d x = A (B - A)$
403	398 402	oveq12i	$⊢ \int_{[A, B]} x d x - \int_{[A, B]} A d x = (\frac{B^{2} - A^{2}}{2}) - A (B - A)$
404	380 403	eqtri	$⊢ \int_{[A, B]} (x - A) d x = (\frac{B^{2} - A^{2}}{2}) - A (B - A)$
405	404	oveq2i	$⊢ (\frac{1}{B - A}) \int_{[A, B]} (x - A) d x = (\frac{1}{B - A}) ((\frac{B^{2} - A^{2}}{2}) - A (B - A))$
406	23	a1i	$⊢ ⊤ \to B \in ℂ$
407	141	a1i	$⊢ ⊤ \to A \in ℂ$
408	406 407	subcld	$⊢ ⊤ \to B - A \in ℂ$
409	26	a1i	$⊢ ⊤ \to B \neq A$
410	406 407 409	subne0d	$⊢ ⊤ \to B - A \neq 0$
411	408 410	reccld	$⊢ ⊤ \to \frac{1}{B - A} \in ℂ$
412	411	mptru	$⊢ \frac{1}{B - A} \in ℂ$
413	23	sqcli	$⊢ B^{2} \in ℂ$
414	141	sqcli	$⊢ A^{2} \in ℂ$
415	413 414	subcli	$⊢ B^{2} - A^{2} \in ℂ$
416	415 300 301	divcli	$⊢ \frac{B^{2} - A^{2}}{2} \in ℂ$
417	141 149	mulcli	$⊢ A (B - A) \in ℂ$
418	412 416 417	subdii	$⊢ (\frac{1}{B - A}) ((\frac{B^{2} - A^{2}}{2}) - A (B - A)) = (\frac{1}{B - A}) (\frac{B^{2} - A^{2}}{2}) - (\frac{1}{B - A}) A (B - A)$
419	405 418	eqtri	$⊢ (\frac{1}{B - A}) \int_{[A, B]} (x - A) d x = (\frac{1}{B - A}) (\frac{B^{2} - A^{2}}{2}) - (\frac{1}{B - A}) A (B - A)$
420	139	adantl	$⊢ (⊤ \land x \in [A, B]) \to x - A \in ℝ$
421	367 372 373 378	iblsub	$⊢ ⊤ \to (x \in [A, B] ⟼ x - A) \in 𝐿^{1}$
422	411 420 421	itgmulc2	$⊢ ⊤ \to (\frac{1}{B - A}) \int_{[A, B]} (x - A) d x = \int_{[A, B]} (\frac{1}{B - A}) (x - A) d x$
423	422	mptru	$⊢ (\frac{1}{B - A}) \int_{[A, B]} (x - A) d x = \int_{[A, B]} (\frac{1}{B - A}) (x - A) d x$
424	412 417	mulcomi	$⊢ (\frac{1}{B - A}) A (B - A) = A (B - A) (\frac{1}{B - A})$
425	417 149 29	divreci	$⊢ \frac{A (B - A)}{B - A} = A (B - A) (\frac{1}{B - A})$
426	141 149 29	divcan4i	$⊢ \frac{A (B - A)}{B - A} = A$
427	424 425 426	3eqtr2i	$⊢ (\frac{1}{B - A}) A (B - A) = A$
428	427	oveq2i	$⊢ (\frac{1}{B - A}) (\frac{B^{2} - A^{2}}{2}) - (\frac{1}{B - A}) A (B - A) = (\frac{1}{B - A}) (\frac{B^{2} - A^{2}}{2}) - A$
429	419 423 428	3eqtr3i	$⊢ \int_{[A, B]} (\frac{1}{B - A}) (x - A) d x = (\frac{1}{B - A}) (\frac{B^{2} - A^{2}}{2}) - A$
430	366 429	eqtri	$⊢ \int_{[A, B]} (\frac{x - A}{B - A}) d x = (\frac{1}{B - A}) (\frac{B^{2} - A^{2}}{2}) - A$
431	23 141	subsqi	$⊢ B^{2} - A^{2} = (B + A) (B - A)$
432	431	oveq1i	$⊢ \frac{B^{2} - A^{2}}{2} = \frac{(B + A) (B - A)}{2}$
433	432	oveq2i	$⊢ (\frac{1}{B - A}) (\frac{B^{2} - A^{2}}{2}) = (\frac{1}{B - A}) (\frac{(B + A) (B - A)}{2})$
434	431 415	eqeltrri	$⊢ (B + A) (B - A) \in ℂ$
435	412 434 300 301	divassi	$⊢ \frac{(\frac{1}{B - A}) (B + A) (B - A)}{2} = (\frac{1}{B - A}) (\frac{(B + A) (B - A)}{2})$
436	412 434	mulcomi	$⊢ (\frac{1}{B - A}) (B + A) (B - A) = (B + A) (B - A) (\frac{1}{B - A})$
437	434 149 29	divreci	$⊢ \frac{(B + A) (B - A)}{B - A} = (B + A) (B - A) (\frac{1}{B - A})$
438	23 141	addcli	$⊢ B + A \in ℂ$
439	438 149 29	divcan4i	$⊢ \frac{(B + A) (B - A)}{B - A} = B + A$
440	436 437 439	3eqtr2i	$⊢ (\frac{1}{B - A}) (B + A) (B - A) = B + A$
441	440	oveq1i	$⊢ \frac{(\frac{1}{B - A}) (B + A) (B - A)}{2} = \frac{B + A}{2}$
442	433 435 441	3eqtr2i	$⊢ (\frac{1}{B - A}) (\frac{B^{2} - A^{2}}{2}) = \frac{B + A}{2}$
443	442	oveq1i	$⊢ (\frac{1}{B - A}) (\frac{B^{2} - A^{2}}{2}) - A = (\frac{B + A}{2}) - A$
444	141 300	mulcli	$⊢ A \cdot 2 \in ℂ$
445		divsubdir	$⊢ (B + A \in ℂ \land A \cdot 2 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{B + A - A \cdot 2}{2} = (\frac{B + A}{2}) - (\frac{A \cdot 2}{2})$
446	438 444 293 445	mp3an	$⊢ \frac{B + A - A \cdot 2}{2} = (\frac{B + A}{2}) - (\frac{A \cdot 2}{2})$
447	23 141 444	addsubassi	$⊢ B + A - A \cdot 2 = B + A - A \cdot 2$
448		subsub2	$⊢ (B \in ℂ \land A \cdot 2 \in ℂ \land A \in ℂ) \to B - (A \cdot 2 - A) = B + A - A \cdot 2$
449	23 444 141 448	mp3an	$⊢ B - (A \cdot 2 - A) = B + A - A \cdot 2$
450	141	times2i	$⊢ A \cdot 2 = A + A$
451	450	oveq1i	$⊢ A \cdot 2 - A = A + A - A$
452	141 141	pncan3oi	$⊢ A + A - A = A$
453	451 452	eqtri	$⊢ A \cdot 2 - A = A$
454	453	oveq2i	$⊢ B - (A \cdot 2 - A) = B - A$
455	447 449 454	3eqtr2i	$⊢ B + A - A \cdot 2 = B - A$
456	455	oveq1i	$⊢ \frac{B + A - A \cdot 2}{2} = \frac{B - A}{2}$
457	141 300 301	divcan4i	$⊢ \frac{A \cdot 2}{2} = A$
458	457	oveq2i	$⊢ (\frac{B + A}{2}) - (\frac{A \cdot 2}{2}) = (\frac{B + A}{2}) - A$
459	446 456 458	3eqtr3ri	$⊢ (\frac{B + A}{2}) - A = \frac{B - A}{2}$
460	430 443 459	3eqtri	$⊢ \int_{[A, B]} (\frac{x - A}{B - A}) d x = \frac{B - A}{2}$
461	460	oveq2i	$⊢ (F - E) \int_{[A, B]} (\frac{x - A}{B - A}) d x = (F - E) (\frac{B - A}{2})$
462		itgeq2	$⊢ \forall x \in [A, B] (F - E) (\frac{x - A}{B - A}) = (\frac{x - A}{B - A}) (F - E) \to \int_{[A, B]} (F - E) (\frac{x - A}{B - A}) d x = \int_{[A, B]} (\frac{x - A}{B - A}) (F - E) d x$
463	65 63	subcli	$⊢ F - E \in ℂ$
464	463	a1i	$⊢ x \in [A, B] \to F - E \in ℂ$
465	464 129	mulcomd	$⊢ x \in [A, B] \to (F - E) (\frac{x - A}{B - A}) = (\frac{x - A}{B - A}) (F - E)$
466	462 465	mprg	$⊢ \int_{[A, B]} (F - E) (\frac{x - A}{B - A}) d x = \int_{[A, B]} (\frac{x - A}{B - A}) (F - E) d x$
467	362 461 466	3eqtr3ri	$⊢ \int_{[A, B]} (\frac{x - A}{B - A}) (F - E) d x = (F - E) (\frac{B - A}{2})$
468	353 467	oveq12i	$⊢ \int_{[A, B]} E d x + \int_{[A, B]} (\frac{x - A}{B - A}) (F - E) d x = E (B - A) + (F - E) (\frac{B - A}{2})$
469	326 340 468	3eqtri	$⊢ \int_{[A, B]} V d x = E (B - A) + (F - E) (\frac{B - A}{2})$
470	149 300 301	divcli	$⊢ \frac{B - A}{2} \in ℂ$
471	319 463 470	adddiri	$⊢ (E \cdot 2 + F - E) (\frac{B - A}{2}) = E \cdot 2 (\frac{B - A}{2}) + (F - E) (\frac{B - A}{2})$
472	323 469 471	3eqtr4i	$⊢ \int_{[A, B]} V d x = (E \cdot 2 + F - E) (\frac{B - A}{2})$
473		addsub12	$⊢ (F \in ℂ \land E \cdot 2 \in ℂ \land E \in ℂ) \to F + E \cdot 2 - E = E \cdot 2 + F - E$
474	65 319 63 473	mp3an	$⊢ F + E \cdot 2 - E = E \cdot 2 + F - E$
475	63	times2i	$⊢ E \cdot 2 = E + E$
476	475	oveq1i	$⊢ E \cdot 2 - E = E + E - E$
477	63 63	pncan3oi	$⊢ E + E - E = E$
478	476 477	eqtri	$⊢ E \cdot 2 - E = E$
479	478	oveq2i	$⊢ F + E \cdot 2 - E = F + E$
480	474 479	eqtr3i	$⊢ E \cdot 2 + F - E = F + E$
481	480	oveq1i	$⊢ (E \cdot 2 + F - E) (\frac{B - A}{2}) = (F + E) (\frac{B - A}{2})$
482	472 481	eqtri	$⊢ \int_{[A, B]} V d x = (F + E) (\frac{B - A}{2})$
483	17 300 301	divcan4i	$⊢ \frac{C \cdot 2}{2} = C$
484	483	oveq1i	$⊢ (\frac{C \cdot 2}{2}) (B - A) = C (B - A)$
485	17 300	mulcli	$⊢ C \cdot 2 \in ℂ$
486		div32	$⊢ (C \cdot 2 \in ℂ \land (2 \in ℂ \land 2 \neq 0) \land B - A \in ℂ) \to (\frac{C \cdot 2}{2}) (B - A) = C \cdot 2 (\frac{B - A}{2})$
487	485 293 149 486	mp3an	$⊢ (\frac{C \cdot 2}{2}) (B - A) = C \cdot 2 (\frac{B - A}{2})$
488	484 487	eqtr3i	$⊢ C (B - A) = C \cdot 2 (\frac{B - A}{2})$
489	488	oveq1i	$⊢ C (B - A) + (D - C) (\frac{B - A}{2}) = C \cdot 2 (\frac{B - A}{2}) + (D - C) (\frac{B - A}{2})$
490	10	a1i	$⊢ (⊤ \land x \in [A, B]) \to U = C + (\frac{x - A}{B - A}) (D - C)$
491	490	itgeq2dv	$⊢ ⊤ \to \int_{[A, B]} U d x = \int_{[A, B]} (C + (\frac{x - A}{B - A}) (D - C)) d x$
492	491	mptru	$⊢ \int_{[A, B]} U d x = \int_{[A, B]} (C + (\frac{x - A}{B - A}) (D - C)) d x$
493	3	a1i	$⊢ (⊤ \land x \in [A, B]) \to C \in ℝ$
494		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ C) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ C) \in 𝐿^{1}$
495	1 2 266 494	mp3an	$⊢ (x \in [A, B] ⟼ C) \in 𝐿^{1}$
496	495	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ C) \in 𝐿^{1}$
497	4	a1i	$⊢ (⊤ \land x \in [A, B]) \to D \in ℝ$
498	497 493	resubcld	$⊢ (⊤ \land x \in [A, B]) \to D - C \in ℝ$
499	331 498	remulcld	$⊢ (⊤ \land x \in [A, B]) \to (\frac{x - A}{B - A}) (D - C) \in ℝ$
500	272	mptru	$⊢ (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (D - C)) : [A, B] \underset{cn}{⟶} ℂ$
501		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (D - C)) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (D - C)) \in 𝐿^{1}$
502	1 2 500 501	mp3an	$⊢ (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (D - C)) \in 𝐿^{1}$
503	502	a1i	$⊢ ⊤ \to (x \in [A, B] ⟼ (\frac{x - A}{B - A}) (D - C)) \in 𝐿^{1}$
504	493 496 499 503	itgadd	$⊢ ⊤ \to \int_{[A, B]} (C + (\frac{x - A}{B - A}) (D - C)) d x = \int_{[A, B]} C d x + \int_{[A, B]} (\frac{x - A}{B - A}) (D - C) d x$
505	504	mptru	$⊢ \int_{[A, B]} (C + (\frac{x - A}{B - A}) (D - C)) d x = \int_{[A, B]} C d x + \int_{[A, B]} (\frac{x - A}{B - A}) (D - C) d x$
506		itgconst	$⊢ ([A, B] \in dom vol \land vol ([A, B]) \in ℝ \land C \in ℂ) \to \int_{[A, B]} C d x = C vol ([A, B])$
507	342 349 17 506	mp3an	$⊢ \int_{[A, B]} C d x = C vol ([A, B])$
508	348	oveq2i	$⊢ C vol ([A, B]) = C (B - A)$
509	507 508	eqtri	$⊢ \int_{[A, B]} C d x = C (B - A)$
510	33	a1i	$⊢ ⊤ \to D \in ℂ$
511	17	a1i	$⊢ ⊤ \to C \in ℂ$
512	510 511	subcld	$⊢ ⊤ \to D - C \in ℂ$
513	512 331 360	itgmulc2	$⊢ ⊤ \to (D - C) \int_{[A, B]} (\frac{x - A}{B - A}) d x = \int_{[A, B]} (D - C) (\frac{x - A}{B - A}) d x$
514	513	mptru	$⊢ (D - C) \int_{[A, B]} (\frac{x - A}{B - A}) d x = \int_{[A, B]} (D - C) (\frac{x - A}{B - A}) d x$
515	460	oveq2i	$⊢ (D - C) \int_{[A, B]} (\frac{x - A}{B - A}) d x = (D - C) (\frac{B - A}{2})$
516		itgeq2	$⊢ \forall x \in [A, B] (D - C) (\frac{x - A}{B - A}) = (\frac{x - A}{B - A}) (D - C) \to \int_{[A, B]} (D - C) (\frac{x - A}{B - A}) d x = \int_{[A, B]} (\frac{x - A}{B - A}) (D - C) d x$
517	33 17	subcli	$⊢ D - C \in ℂ$
518	517	a1i	$⊢ x \in [A, B] \to D - C \in ℂ$
519	518 129	mulcomd	$⊢ x \in [A, B] \to (D - C) (\frac{x - A}{B - A}) = (\frac{x - A}{B - A}) (D - C)$
520	516 519	mprg	$⊢ \int_{[A, B]} (D - C) (\frac{x - A}{B - A}) d x = \int_{[A, B]} (\frac{x - A}{B - A}) (D - C) d x$
521	514 515 520	3eqtr3ri	$⊢ \int_{[A, B]} (\frac{x - A}{B - A}) (D - C) d x = (D - C) (\frac{B - A}{2})$
522	509 521	oveq12i	$⊢ \int_{[A, B]} C d x + \int_{[A, B]} (\frac{x - A}{B - A}) (D - C) d x = C (B - A) + (D - C) (\frac{B - A}{2})$
523	492 505 522	3eqtri	$⊢ \int_{[A, B]} U d x = C (B - A) + (D - C) (\frac{B - A}{2})$
524	485 517 470	adddiri	$⊢ (C \cdot 2 + D - C) (\frac{B - A}{2}) = C \cdot 2 (\frac{B - A}{2}) + (D - C) (\frac{B - A}{2})$
525	489 523 524	3eqtr4i	$⊢ \int_{[A, B]} U d x = (C \cdot 2 + D - C) (\frac{B - A}{2})$
526		addsub12	$⊢ (D \in ℂ \land C \cdot 2 \in ℂ \land C \in ℂ) \to D + C \cdot 2 - C = C \cdot 2 + D - C$
527	33 485 17 526	mp3an	$⊢ D + C \cdot 2 - C = C \cdot 2 + D - C$
528	17	times2i	$⊢ C \cdot 2 = C + C$
529	528	oveq1i	$⊢ C \cdot 2 - C = C + C - C$
530	17 17	pncan3oi	$⊢ C + C - C = C$
531	529 530	eqtri	$⊢ C \cdot 2 - C = C$
532	531	oveq2i	$⊢ D + C \cdot 2 - C = D + C$
533	527 532	eqtr3i	$⊢ C \cdot 2 + D - C = D + C$
534	533	oveq1i	$⊢ (C \cdot 2 + D - C) (\frac{B - A}{2}) = (D + C) (\frac{B - A}{2})$
535	525 534	eqtri	$⊢ \int_{[A, B]} U d x = (D + C) (\frac{B - A}{2})$
536	482 535	oveq12i	$⊢ \int_{[A, B]} V d x - \int_{[A, B]} U d x = (F + E) (\frac{B - A}{2}) - (D + C) (\frac{B - A}{2})$
537	316 536	eqtri	$⊢ \int_{[A, B]} (V - U) d x = (F + E) (\frac{B - A}{2}) - (D + C) (\frac{B - A}{2})$
538	299 304 537	3eqtr4ri	$⊢ \int_{[A, B]} (V - U) d x = ((\frac{F + E}{2}) - (\frac{D + C}{2})) (B - A)$
539	289 291 538	3eqtr2i	$⊢ \int_{ℝ} vol (S [\{x\}]) d x = ((\frac{F + E}{2}) - (\frac{D + C}{2})) (B - A)$
540	286 539	eqtri	$⊢ area (S) = ((\frac{F + E}{2}) - (\frac{D + C}{2})) (B - A)$

Metamath Proof Explorer

Theorem areaquad

Proof