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 
|- A e. RR
arearect.2 
|- B e. RR
arearect.3 
|- C e. RR
arearect.4 
|- D e. RR
arearect.5 
|- A <_ B
arearect.6 
|- C <_ D
arearect.7 
|- S = ( ( A [,] B ) X. ( C [,] D ) )
Assertion arearect 
|- ( area ` S ) = ( ( B - A ) x. ( D - C ) )

Proof

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