Metamath Proof Explorer

Theorem 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 ⊢ 𝐴 ∈ ℝ
arearect.2 ⊢ 𝐵 ∈ ℝ
arearect.3 ⊢ 𝐶 ∈ ℝ
arearect.4 ⊢ 𝐷 ∈ ℝ
arearect.5 ⊢ 𝐴 ≤ 𝐵
arearect.6 ⊢ 𝐶 ≤ 𝐷
arearect.7 ⊢ 𝑆 = ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) )
Assertion arearect ( area ‘ 𝑆 ) = ( ( 𝐵 − 𝐴 ) · ( 𝐷 − 𝐶 ) )

Proof

Step Hyp Ref Expression
1 arearect.1 ⊢ 𝐴 ∈ ℝ
2 arearect.2 ⊢ 𝐵 ∈ ℝ
3 arearect.3 ⊢ 𝐶 ∈ ℝ
4 arearect.4 ⊢ 𝐷 ∈ ℝ
5 arearect.5 ⊢ 𝐴 ≤ 𝐵
6 arearect.6 ⊢ 𝐶 ≤ 𝐷
7 arearect.7 ⊢ 𝑆 = ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) )
8 iccssre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
9 1 2 8 mp2an ⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ
10 iccssre ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 [,] 𝐷 ) ⊆ ℝ )
11 3 4 10 mp2an ⊢ ( 𝐶 [,] 𝐷 ) ⊆ ℝ
12 xpss12 ⊢ ( ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ ∧ ( 𝐶 [,] 𝐷 ) ⊆ ℝ ) → ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) ) ⊆ ( ℝ × ℝ ) )
13 9 11 12 mp2an ⊢ ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) ) ⊆ ( ℝ × ℝ )
14 7 13 eqsstri ⊢ 𝑆 ⊆ ( ℝ × ℝ )
15 iftrue ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) = ( 𝐷 − 𝐶 ) )
16 7 imaeq1i ⊢ ( 𝑆 “ { 𝑥 } ) = ( ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) ) “ { 𝑥 } )
17 iftrue ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ ) = ( 𝐶 [,] 𝐷 ) )
18 xpimasn ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) ) “ { 𝑥 } ) = ( 𝐶 [,] 𝐷 ) )
19 17 18 eqtr4d ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ ) = ( ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) ) “ { 𝑥 } ) )
20 iffalse ⊢ ( ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ ) = ∅ )
21 disjsn ⊢ ( ( ( 𝐴 [,] 𝐵 ) ∩ { 𝑥 } ) = ∅ ↔ ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
22 xpima1 ⊢ ( ( ( 𝐴 [,] 𝐵 ) ∩ { 𝑥 } ) = ∅ → ( ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) ) “ { 𝑥 } ) = ∅ )
23 21 22 sylbir ⊢ ( ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) ) “ { 𝑥 } ) = ∅ )
24 20 23 eqtr4d ⊢ ( ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ ) = ( ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) ) “ { 𝑥 } ) )
25 19 24 pm2.61i ⊢ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ ) = ( ( ( 𝐴 [,] 𝐵 ) × ( 𝐶 [,] 𝐷 ) ) “ { 𝑥 } )
26 16 25 eqtr4i ⊢ ( 𝑆 “ { 𝑥 } ) = if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ )
27 26 fveq2i ⊢ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = ( vol ‘ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ ) )
28 17 fveq2d ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( vol ‘ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ ) ) = ( vol ‘ ( 𝐶 [,] 𝐷 ) ) )
29 27 28 syl5eq ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = ( vol ‘ ( 𝐶 [,] 𝐷 ) ) )
30 iccmbl ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) → ( 𝐶 [,] 𝐷 ) ∈ dom vol )
31 3 4 30 mp2an ⊢ ( 𝐶 [,] 𝐷 ) ∈ dom vol
32 mblvol ⊢ ( ( 𝐶 [,] 𝐷 ) ∈ dom vol → ( vol ‘ ( 𝐶 [,] 𝐷 ) ) = ( vol* ‘ ( 𝐶 [,] 𝐷 ) ) )
33 31 32 ax-mp ⊢ ( vol ‘ ( 𝐶 [,] 𝐷 ) ) = ( vol* ‘ ( 𝐶 [,] 𝐷 ) )
34 ovolicc ⊢ ( ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ∧ 𝐶 ≤ 𝐷 ) → ( vol* ‘ ( 𝐶 [,] 𝐷 ) ) = ( 𝐷 − 𝐶 ) )
35 3 4 6 34 mp3an ⊢ ( vol* ‘ ( 𝐶 [,] 𝐷 ) ) = ( 𝐷 − 𝐶 )
36 33 35 eqtri ⊢ ( vol ‘ ( 𝐶 [,] 𝐷 ) ) = ( 𝐷 − 𝐶 )
37 29 36 eqtrdi ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = ( 𝐷 − 𝐶 ) )
38 15 37 eqtr4d ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) = ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) )
39 iffalse ⊢ ( ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) = 0 )
40 20 fveq2d ⊢ ( ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( vol ‘ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ ) ) = ( vol ‘ ∅ ) )
41 27 40 syl5eq ⊢ ( ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = ( vol ‘ ∅ ) )
42 0mbl ⊢ ∅ ∈ dom vol
43 mblvol ⊢ ( ∅ ∈ dom vol → ( vol ‘ ∅ ) = ( vol* ‘ ∅ ) )
44 42 43 ax-mp ⊢ ( vol ‘ ∅ ) = ( vol* ‘ ∅ )
45 ovol0 ⊢ ( vol* ‘ ∅ ) = 0
46 44 45 eqtri ⊢ ( vol ‘ ∅ ) = 0
47 41 46 eqtrdi ⊢ ( ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = 0 )
48 39 47 eqtr4d ⊢ ( ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) = ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) )
49 38 48 pm2.61i ⊢ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) = ( vol ‘ ( 𝑆 “ { 𝑥 } ) )
50 49 eqcomi ⊢ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 )
51 50 a1i ⊢ ( 𝑥 ∈ ℝ → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) )
52 4 3 resubcli ⊢ ( 𝐷 − 𝐶 ) ∈ ℝ
53 0re ⊢ 0 ∈ ℝ
54 52 53 ifcli ⊢ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) ∈ ℝ
55 51 54 eqeltrdi ⊢ ( 𝑥 ∈ ℝ → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ∈ ℝ )
56 volf ⊢ vol : dom vol ⟶ ( 0 [,] +∞ )
57 ffun ⊢ ( vol : dom vol ⟶ ( 0 [,] +∞ ) → Fun vol )
58 56 57 ax-mp ⊢ Fun vol
59 31 42 ifcli ⊢ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐶 [,] 𝐷 ) , ∅ ) ∈ dom vol
60 26 59 eqeltri ⊢ ( 𝑆 “ { 𝑥 } ) ∈ dom vol
61 fvimacnv ⊢ ( ( Fun vol ∧ ( 𝑆 “ { 𝑥 } ) ∈ dom vol ) → ( ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ∈ ℝ ↔ ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ) )
62 58 60 61 mp2an ⊢ ( ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ∈ ℝ ↔ ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) )
63 55 62 sylib ⊢ ( 𝑥 ∈ ℝ → ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) )
64 63 rgen ⊢ ∀ 𝑥 ∈ ℝ ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ )
65 9 a1i ⊢ ( 0 ∈ ℝ → ( 𝐴 [,] 𝐵 ) ⊆ ℝ )
66 rembl ⊢ ℝ ∈ dom vol
67 66 a1i ⊢ ( 0 ∈ ℝ → ℝ ∈ dom vol )
68 37 52 eqeltrdi ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ∈ ℝ )
69 68 adantl ⊢ ( ( 0 ∈ ℝ ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ∈ ℝ )
70 eldifn ⊢ ( 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) → ¬ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
71 70 47 syl ⊢ ( 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = 0 )
72 71 adantl ⊢ ( ( 0 ∈ ℝ ∧ 𝑥 ∈ ( ℝ ∖ ( 𝐴 [,] 𝐵 ) ) ) → ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = 0 )
73 37 mpteq2ia ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐷 − 𝐶 ) )
74 52 recni ⊢ ( 𝐷 − 𝐶 ) ∈ ℂ
75 ax-resscn ⊢ ℝ ⊆ ℂ
76 9 75 sstri ⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℂ
77 ssid ⊢ ℂ ⊆ ℂ
78 cncfmptc ⊢ ( ( ( 𝐷 − 𝐶 ) ∈ ℂ ∧ ( 𝐴 [,] 𝐵 ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐷 − 𝐶 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
79 74 76 77 78 mp3an ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐷 − 𝐶 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ )
80 cniccibl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐷 − 𝐶 ) ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐷 − 𝐶 ) ) ∈ 𝐿1 )
81 1 2 79 80 mp3an ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( 𝐷 − 𝐶 ) ) ∈ 𝐿1
82 73 81 eqeltri ⊢ ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ) ∈ 𝐿1
83 82 a1i ⊢ ( 0 ∈ ℝ → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ) ∈ 𝐿1 )
84 65 67 69 72 83 iblss2 ⊢ ( 0 ∈ ℝ → ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ) ∈ 𝐿1 )
85 53 84 ax-mp ⊢ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ) ∈ 𝐿1
86 dmarea ⊢ ( 𝑆 ∈ dom area ↔ ( 𝑆 ⊆ ( ℝ × ℝ ) ∧ ∀ 𝑥 ∈ ℝ ( 𝑆 “ { 𝑥 } ) ∈ ( ◡ vol “ ℝ ) ∧ ( 𝑥 ∈ ℝ ↦ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) ) ∈ 𝐿1 ) )
87 14 64 85 86 mpbir3an ⊢ 𝑆 ∈ dom area
88 areaval ⊢ ( 𝑆 ∈ dom area → ( area ‘ 𝑆 ) = ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) d 𝑥 )
89 87 88 ax-mp ⊢ ( area ‘ 𝑆 ) = ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) d 𝑥
90 itgeq2 ⊢ ( ∀ 𝑥 ∈ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) = if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) → ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) d 𝑥 = ∫ ℝ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) d 𝑥 )
91 90 51 mprg ⊢ ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) d 𝑥 = ∫ ℝ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) d 𝑥
92 iccmbl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 [,] 𝐵 ) ∈ dom vol )
93 1 2 92 mp2an ⊢ ( 𝐴 [,] 𝐵 ) ∈ dom vol
94 mblvol ⊢ ( ( 𝐴 [,] 𝐵 ) ∈ dom vol → ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) )
95 93 94 ax-mp ⊢ ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( vol* ‘ ( 𝐴 [,] 𝐵 ) )
96 ovolicc ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ≤ 𝐵 ) → ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵 − 𝐴 ) )
97 1 2 5 96 mp3an ⊢ ( vol* ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵 − 𝐴 )
98 95 97 eqtri ⊢ ( vol ‘ ( 𝐴 [,] 𝐵 ) ) = ( 𝐵 − 𝐴 )
99 2 1 resubcli ⊢ ( 𝐵 − 𝐴 ) ∈ ℝ
100 98 99 eqeltri ⊢ ( vol ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ
101 itgconst ⊢ ( ( ( 𝐴 [,] 𝐵 ) ∈ dom vol ∧ ( vol ‘ ( 𝐴 [,] 𝐵 ) ) ∈ ℝ ∧ ( 𝐷 − 𝐶 ) ∈ ℂ ) → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐷 − 𝐶 ) d 𝑥 = ( ( 𝐷 − 𝐶 ) · ( vol ‘ ( 𝐴 [,] 𝐵 ) ) ) )
102 93 100 74 101 mp3an ⊢ ∫ ( 𝐴 [,] 𝐵 ) ( 𝐷 − 𝐶 ) d 𝑥 = ( ( 𝐷 − 𝐶 ) · ( vol ‘ ( 𝐴 [,] 𝐵 ) ) )
103 itgss2 ⊢ ( ( 𝐴 [,] 𝐵 ) ⊆ ℝ → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐷 − 𝐶 ) d 𝑥 = ∫ ℝ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) d 𝑥 )
104 9 103 ax-mp ⊢ ∫ ( 𝐴 [,] 𝐵 ) ( 𝐷 − 𝐶 ) d 𝑥 = ∫ ℝ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) d 𝑥
105 98 oveq2i ⊢ ( ( 𝐷 − 𝐶 ) · ( vol ‘ ( 𝐴 [,] 𝐵 ) ) ) = ( ( 𝐷 − 𝐶 ) · ( 𝐵 − 𝐴 ) )
106 102 104 105 3eqtr3i ⊢ ∫ ℝ if ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) , ( 𝐷 − 𝐶 ) , 0 ) d 𝑥 = ( ( 𝐷 − 𝐶 ) · ( 𝐵 − 𝐴 ) )
107 91 106 eqtri ⊢ ∫ ℝ ( vol ‘ ( 𝑆 “ { 𝑥 } ) ) d 𝑥 = ( ( 𝐷 − 𝐶 ) · ( 𝐵 − 𝐴 ) )
108 99 recni ⊢ ( 𝐵 − 𝐴 ) ∈ ℂ
109 74 108 mulcomi ⊢ ( ( 𝐷 − 𝐶 ) · ( 𝐵 − 𝐴 ) ) = ( ( 𝐵 − 𝐴 ) · ( 𝐷 − 𝐶 ) )
110 89 107 109 3eqtri ⊢ ( area ‘ 𝑆 ) = ( ( 𝐵 − 𝐴 ) · ( 𝐷 − 𝐶 ) )