arearect

Description: The area of a rectangle whose sides are parallel to the coordinate axes in ( RR X. RR ) is its width multiplied by its height. (Contributed by Jon Pennant, 19-Mar-2019)

	Ref	Expression
Hypotheses	arearect.1	$⊢ A \in ℝ$
	arearect.2	$⊢ B \in ℝ$
	arearect.3	$⊢ C \in ℝ$
	arearect.4	$⊢ D \in ℝ$
	arearect.5	$⊢ A \leq B$
	arearect.6	$⊢ C \leq D$
	arearect.7	$⊢ S = [A, B] \times [C, D]$
Assertion	arearect	$⊢ area (S) = (B - A) (D - C)$

Proof

Step	Hyp	Ref	Expression
1		arearect.1	$⊢ A \in ℝ$
2		arearect.2	$⊢ B \in ℝ$
3		arearect.3	$⊢ C \in ℝ$
4		arearect.4	$⊢ D \in ℝ$
5		arearect.5	$⊢ A \leq B$
6		arearect.6	$⊢ C \leq D$
7		arearect.7	$⊢ S = [A, B] \times [C, D]$
8		iccssre	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \subseteq ℝ$
9	1 2 8	mp2an	$⊢ [A, B] \subseteq ℝ$
10		iccssre	$⊢ (C \in ℝ \land D \in ℝ) \to [C, D] \subseteq ℝ$
11	3 4 10	mp2an	$⊢ [C, D] \subseteq ℝ$
12		xpss12	$⊢ ([A, B] \subseteq ℝ \land [C, D] \subseteq ℝ) \to [A, B] \times [C, D] \subseteq ℝ^{2}$
13	9 11 12	mp2an	$⊢ [A, B] \times [C, D] \subseteq ℝ^{2}$
14	7 13	eqsstri	$⊢ S \subseteq ℝ^{2}$
15		iftrue	$⊢ x \in [A, B] \to if (x \in [A, B], D - C, 0) = D - C$
16	7	imaeq1i	$⊢ S [\{x\}] = ([A, B] \times [C, D]) [\{x\}]$
17		iftrue	$⊢ x \in [A, B] \to if (x \in [A, B], [C, D], \emptyset) = [C, D]$
18		xpimasn	$⊢ x \in [A, B] \to ([A, B] \times [C, D]) [\{x\}] = [C, D]$
19	17 18	eqtr4d	$⊢ x \in [A, B] \to if (x \in [A, B], [C, D], \emptyset) = ([A, B] \times [C, D]) [\{x\}]$
20		iffalse	$⊢ \neg x \in [A, B] \to if (x \in [A, B], [C, D], \emptyset) = \emptyset$
21		disjsn	$⊢ [A, B] \cap \{x\} = \emptyset \leftrightarrow \neg x \in [A, B]$
22		xpima1	$⊢ [A, B] \cap \{x\} = \emptyset \to ([A, B] \times [C, D]) [\{x\}] = \emptyset$
23	21 22	sylbir	$⊢ \neg x \in [A, B] \to ([A, B] \times [C, D]) [\{x\}] = \emptyset$
24	20 23	eqtr4d	$⊢ \neg x \in [A, B] \to if (x \in [A, B], [C, D], \emptyset) = ([A, B] \times [C, D]) [\{x\}]$
25	19 24	pm2.61i	$⊢ if (x \in [A, B], [C, D], \emptyset) = ([A, B] \times [C, D]) [\{x\}]$
26	16 25	eqtr4i	$⊢ S [\{x\}] = if (x \in [A, B], [C, D], \emptyset)$
27	26	fveq2i	$⊢ vol (S [\{x\}]) = vol (if (x \in [A, B], [C, D], \emptyset))$
28	17	fveq2d	$⊢ x \in [A, B] \to vol (if (x \in [A, B], [C, D], \emptyset)) = vol ([C, D])$
29	27 28	syl5eq	$⊢ x \in [A, B] \to vol (S [\{x\}]) = vol ([C, D])$
30		iccmbl	$⊢ (C \in ℝ \land D \in ℝ) \to [C, D] \in dom vol$
31	3 4 30	mp2an	$⊢ [C, D] \in dom vol$
32		mblvol	$⊢ [C, D] \in dom vol \to vol ([C, D]) = {vol}^{*} ([C, D])$
33	31 32	ax-mp	$⊢ vol ([C, D]) = {vol}^{*} ([C, D])$
34		ovolicc	$⊢ (C \in ℝ \land D \in ℝ \land C \leq D) \to {vol}^{*} ([C, D]) = D - C$
35	3 4 6 34	mp3an	$⊢ {vol}^{*} ([C, D]) = D - C$
36	33 35	eqtri	$⊢ vol ([C, D]) = D - C$
37	29 36	eqtrdi	$⊢ x \in [A, B] \to vol (S [\{x\}]) = D - C$
38	15 37	eqtr4d	$⊢ x \in [A, B] \to if (x \in [A, B], D - C, 0) = vol (S [\{x\}])$
39		iffalse	$⊢ \neg x \in [A, B] \to if (x \in [A, B], D - C, 0) = 0$
40	20	fveq2d	$⊢ \neg x \in [A, B] \to vol (if (x \in [A, B], [C, D], \emptyset)) = vol (\emptyset)$
41	27 40	syl5eq	$⊢ \neg x \in [A, B] \to vol (S [\{x\}]) = vol (\emptyset)$
42		0mbl	$⊢ \emptyset \in dom vol$
43		mblvol	$⊢ \emptyset \in dom vol \to vol (\emptyset) = {vol}^{*} (\emptyset)$
44	42 43	ax-mp	$⊢ vol (\emptyset) = {vol}^{*} (\emptyset)$
45		ovol0	$⊢ {vol}^{*} (\emptyset) = 0$
46	44 45	eqtri	$⊢ vol (\emptyset) = 0$
47	41 46	eqtrdi	$⊢ \neg x \in [A, B] \to vol (S [\{x\}]) = 0$
48	39 47	eqtr4d	$⊢ \neg x \in [A, B] \to if (x \in [A, B], D - C, 0) = vol (S [\{x\}])$
49	38 48	pm2.61i	$⊢ if (x \in [A, B], D - C, 0) = vol (S [\{x\}])$
50	49	eqcomi	$⊢ vol (S [\{x\}]) = if (x \in [A, B], D - C, 0)$
51	50	a1i	$⊢ x \in ℝ \to vol (S [\{x\}]) = if (x \in [A, B], D - C, 0)$
52	4 3	resubcli	$⊢ D - C \in ℝ$
53		0re	$⊢ 0 \in ℝ$
54	52 53	ifcli	$⊢ if (x \in [A, B], D - C, 0) \in ℝ$
55	51 54	eqeltrdi	$⊢ x \in ℝ \to vol (S [\{x\}]) \in ℝ$
56		volf	$⊢ vol : dom vol ⟶ [0, +∞]$
57		ffun	$⊢ vol : dom vol ⟶ [0, +∞] \to Fun vol$
58	56 57	ax-mp	$⊢ Fun vol$
59	31 42	ifcli	$⊢ if (x \in [A, B], [C, D], \emptyset) \in dom vol$
60	26 59	eqeltri	$⊢ S [\{x\}] \in dom vol$
61		fvimacnv	$⊢ (Fun vol \land S [\{x\}] \in dom vol) \to (vol (S [\{x\}]) \in ℝ \leftrightarrow S [\{x\}] \in {vol}^{-1} [ℝ])$
62	58 60 61	mp2an	$⊢ vol (S [\{x\}]) \in ℝ \leftrightarrow S [\{x\}] \in {vol}^{-1} [ℝ]$
63	55 62	sylib	$⊢ x \in ℝ \to S [\{x\}] \in {vol}^{-1} [ℝ]$
64	63	rgen	$⊢ \forall x \in ℝ S [\{x\}] \in {vol}^{-1} [ℝ]$
65	9	a1i	$⊢ 0 \in ℝ \to [A, B] \subseteq ℝ$
66		rembl	$⊢ ℝ \in dom vol$
67	66	a1i	$⊢ 0 \in ℝ \to ℝ \in dom vol$
68	37 52	eqeltrdi	$⊢ x \in [A, B] \to vol (S [\{x\}]) \in ℝ$
69	68	adantl	$⊢ (0 \in ℝ \land x \in [A, B]) \to vol (S [\{x\}]) \in ℝ$
70		eldifn	$⊢ x \in (ℝ ∖ [A, B]) \to \neg x \in [A, B]$
71	70 47	syl	$⊢ x \in (ℝ ∖ [A, B]) \to vol (S [\{x\}]) = 0$
72	71	adantl	$⊢ (0 \in ℝ \land x \in (ℝ ∖ [A, B])) \to vol (S [\{x\}]) = 0$
73	37	mpteq2ia	$⊢ (x \in [A, B] ⟼ vol (S [\{x\}])) = (x \in [A, B] ⟼ D - C)$
74	52	recni	$⊢ D - C \in ℂ$
75		ax-resscn	$⊢ ℝ \subseteq ℂ$
76	9 75	sstri	$⊢ [A, B] \subseteq ℂ$
77		ssid	$⊢ ℂ \subseteq ℂ$
78		cncfmptc	$⊢ (D - C \in ℂ \land [A, B] \subseteq ℂ \land ℂ \subseteq ℂ) \to (x \in [A, B] ⟼ D - C) : [A, B] \underset{cn}{⟶} ℂ$
79	74 76 77 78	mp3an	$⊢ (x \in [A, B] ⟼ D - C) : [A, B] \underset{cn}{⟶} ℂ$
80		cniccibl	$⊢ (A \in ℝ \land B \in ℝ \land (x \in [A, B] ⟼ D - C) : [A, B] \underset{cn}{⟶} ℂ) \to (x \in [A, B] ⟼ D - C) \in 𝐿^{1}$
81	1 2 79 80	mp3an	$⊢ (x \in [A, B] ⟼ D - C) \in 𝐿^{1}$
82	73 81	eqeltri	$⊢ (x \in [A, B] ⟼ vol (S [\{x\}])) \in 𝐿^{1}$
83	82	a1i	$⊢ 0 \in ℝ \to (x \in [A, B] ⟼ vol (S [\{x\}])) \in 𝐿^{1}$
84	65 67 69 72 83	iblss2	$⊢ 0 \in ℝ \to (x \in ℝ ⟼ vol (S [\{x\}])) \in 𝐿^{1}$
85	53 84	ax-mp	$⊢ (x \in ℝ ⟼ vol (S [\{x\}])) \in 𝐿^{1}$
86		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})$
87	14 64 85 86	mpbir3an	$⊢ S \in dom area$
88		areaval	$⊢ S \in dom area \to area (S) = \int_{ℝ} vol (S [\{x\}]) d x$
89	87 88	ax-mp	$⊢ area (S) = \int_{ℝ} vol (S [\{x\}]) d x$
90		itgeq2	$⊢ \forall x \in ℝ vol (S [\{x\}]) = if (x \in [A, B], D - C, 0) \to \int_{ℝ} vol (S [\{x\}]) d x = \int_{ℝ} if (x \in [A, B], D - C, 0) d x$
91	90 51	mprg	$⊢ \int_{ℝ} vol (S [\{x\}]) d x = \int_{ℝ} if (x \in [A, B], D - C, 0) d x$
92		iccmbl	$⊢ (A \in ℝ \land B \in ℝ) \to [A, B] \in dom vol$
93	1 2 92	mp2an	$⊢ [A, B] \in dom vol$
94		mblvol	$⊢ [A, B] \in dom vol \to vol ([A, B]) = {vol}^{*} ([A, B])$
95	93 94	ax-mp	$⊢ vol ([A, B]) = {vol}^{*} ([A, B])$
96		ovolicc	$⊢ (A \in ℝ \land B \in ℝ \land A \leq B) \to {vol}^{*} ([A, B]) = B - A$
97	1 2 5 96	mp3an	$⊢ {vol}^{*} ([A, B]) = B - A$
98	95 97	eqtri	$⊢ vol ([A, B]) = B - A$
99	2 1	resubcli	$⊢ B - A \in ℝ$
100	98 99	eqeltri	$⊢ vol ([A, B]) \in ℝ$
101		itgconst	$⊢ ([A, B] \in dom vol \land vol ([A, B]) \in ℝ \land D - C \in ℂ) \to \int_{[A, B]} (D - C) d x = (D - C) vol ([A, B])$
102	93 100 74 101	mp3an	$⊢ \int_{[A, B]} (D - C) d x = (D - C) vol ([A, B])$
103		itgss2	$⊢ [A, B] \subseteq ℝ \to \int_{[A, B]} (D - C) d x = \int_{ℝ} if (x \in [A, B], D - C, 0) d x$
104	9 103	ax-mp	$⊢ \int_{[A, B]} (D - C) d x = \int_{ℝ} if (x \in [A, B], D - C, 0) d x$
105	98	oveq2i	$⊢ (D - C) vol ([A, B]) = (D - C) (B - A)$
106	102 104 105	3eqtr3i	$⊢ \int_{ℝ} if (x \in [A, B], D - C, 0) d x = (D - C) (B - A)$
107	91 106	eqtri	$⊢ \int_{ℝ} vol (S [\{x\}]) d x = (D - C) (B - A)$
108	99	recni	$⊢ B - A \in ℂ$
109	74 108	mulcomi	$⊢ (D - C) (B - A) = (B - A) (D - C)$
110	89 107 109	3eqtri	$⊢ area (S) = (B - A) (D - C)$

Metamath Proof Explorer

Theorem arearect

Proof