Step | Hyp | Ref
| Expression |
1 | | arearect.7 |
. . . . 5
β’ π = ((π΄[,]π΅) Γ (πΆ[,]π·)) |
2 | | arearect.1 |
. . . . . . 7
β’ π΄ β β |
3 | | arearect.2 |
. . . . . . 7
β’ π΅ β β |
4 | | iccssre 13352 |
. . . . . . 7
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β β) |
5 | 2, 3, 4 | mp2an 691 |
. . . . . 6
β’ (π΄[,]π΅) β β |
6 | | arearect.3 |
. . . . . . 7
β’ πΆ β β |
7 | | arearect.4 |
. . . . . . 7
β’ π· β β |
8 | | iccssre 13352 |
. . . . . . 7
β’ ((πΆ β β β§ π· β β) β (πΆ[,]π·) β β) |
9 | 6, 7, 8 | mp2an 691 |
. . . . . 6
β’ (πΆ[,]π·) β β |
10 | | xpss12 5649 |
. . . . . 6
β’ (((π΄[,]π΅) β β β§ (πΆ[,]π·) β β) β ((π΄[,]π΅) Γ (πΆ[,]π·)) β (β Γ
β)) |
11 | 5, 9, 10 | mp2an 691 |
. . . . 5
β’ ((π΄[,]π΅) Γ (πΆ[,]π·)) β (β Γ
β) |
12 | 1, 11 | eqsstri 3979 |
. . . 4
β’ π β (β Γ
β) |
13 | | iftrue 4493 |
. . . . . . . . . . 11
β’ (π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π· β πΆ), 0) = (π· β πΆ)) |
14 | 1 | imaeq1i 6011 |
. . . . . . . . . . . . . . 15
β’ (π β {π₯}) = (((π΄[,]π΅) Γ (πΆ[,]π·)) β {π₯}) |
15 | | iftrue 4493 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (πΆ[,]π·), β
) = (πΆ[,]π·)) |
16 | | xpimasn 6138 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β (π΄[,]π΅) β (((π΄[,]π΅) Γ (πΆ[,]π·)) β {π₯}) = (πΆ[,]π·)) |
17 | 15, 16 | eqtr4d 2776 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (πΆ[,]π·), β
) = (((π΄[,]π΅) Γ (πΆ[,]π·)) β {π₯})) |
18 | | iffalse 4496 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (πΆ[,]π·), β
) = β
) |
19 | | disjsn 4673 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄[,]π΅) β© {π₯}) = β
β Β¬ π₯ β (π΄[,]π΅)) |
20 | | xpima1 6136 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΄[,]π΅) β© {π₯}) = β
β (((π΄[,]π΅) Γ (πΆ[,]π·)) β {π₯}) = β
) |
21 | 19, 20 | sylbir 234 |
. . . . . . . . . . . . . . . . 17
β’ (Β¬
π₯ β (π΄[,]π΅) β (((π΄[,]π΅) Γ (πΆ[,]π·)) β {π₯}) = β
) |
22 | 18, 21 | eqtr4d 2776 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (πΆ[,]π·), β
) = (((π΄[,]π΅) Γ (πΆ[,]π·)) β {π₯})) |
23 | 17, 22 | pm2.61i 182 |
. . . . . . . . . . . . . . 15
β’ if(π₯ β (π΄[,]π΅), (πΆ[,]π·), β
) = (((π΄[,]π΅) Γ (πΆ[,]π·)) β {π₯}) |
24 | 14, 23 | eqtr4i 2764 |
. . . . . . . . . . . . . 14
β’ (π β {π₯}) = if(π₯ β (π΄[,]π΅), (πΆ[,]π·), β
) |
25 | 24 | fveq2i 6846 |
. . . . . . . . . . . . 13
β’
(volβ(π
β {π₯})) =
(volβif(π₯ β
(π΄[,]π΅), (πΆ[,]π·), β
)) |
26 | 15 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (π₯ β (π΄[,]π΅) β (volβif(π₯ β (π΄[,]π΅), (πΆ[,]π·), β
)) = (volβ(πΆ[,]π·))) |
27 | 25, 26 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ (π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) = (volβ(πΆ[,]π·))) |
28 | | iccmbl 24946 |
. . . . . . . . . . . . . . 15
β’ ((πΆ β β β§ π· β β) β (πΆ[,]π·) β dom vol) |
29 | 6, 7, 28 | mp2an 691 |
. . . . . . . . . . . . . 14
β’ (πΆ[,]π·) β dom vol |
30 | | mblvol 24910 |
. . . . . . . . . . . . . 14
β’ ((πΆ[,]π·) β dom vol β (volβ(πΆ[,]π·)) = (vol*β(πΆ[,]π·))) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(volβ(πΆ[,]π·)) = (vol*β(πΆ[,]π·)) |
32 | | arearect.6 |
. . . . . . . . . . . . . 14
β’ πΆ β€ π· |
33 | | ovolicc 24903 |
. . . . . . . . . . . . . 14
β’ ((πΆ β β β§ π· β β β§ πΆ β€ π·) β (vol*β(πΆ[,]π·)) = (π· β πΆ)) |
34 | 6, 7, 32, 33 | mp3an 1462 |
. . . . . . . . . . . . 13
β’
(vol*β(πΆ[,]π·)) = (π· β πΆ) |
35 | 31, 34 | eqtri 2761 |
. . . . . . . . . . . 12
β’
(volβ(πΆ[,]π·)) = (π· β πΆ) |
36 | 27, 35 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) = (π· β πΆ)) |
37 | 13, 36 | eqtr4d 2776 |
. . . . . . . . . 10
β’ (π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π· β πΆ), 0) = (volβ(π β {π₯}))) |
38 | | iffalse 4496 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π· β πΆ), 0) = 0) |
39 | 18 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (Β¬
π₯ β (π΄[,]π΅) β (volβif(π₯ β (π΄[,]π΅), (πΆ[,]π·), β
)) =
(volββ
)) |
40 | 25, 39 | eqtrid 2785 |
. . . . . . . . . . . 12
β’ (Β¬
π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) = (volββ
)) |
41 | | 0mbl 24919 |
. . . . . . . . . . . . . 14
β’ β
β dom vol |
42 | | mblvol 24910 |
. . . . . . . . . . . . . 14
β’ (β
β dom vol β (volββ
) =
(vol*ββ
)) |
43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . . . 13
β’
(volββ
) = (vol*ββ
) |
44 | | ovol0 24873 |
. . . . . . . . . . . . 13
β’
(vol*ββ
) = 0 |
45 | 43, 44 | eqtri 2761 |
. . . . . . . . . . . 12
β’
(volββ
) = 0 |
46 | 40, 45 | eqtrdi 2789 |
. . . . . . . . . . 11
β’ (Β¬
π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) = 0) |
47 | 38, 46 | eqtr4d 2776 |
. . . . . . . . . 10
β’ (Β¬
π₯ β (π΄[,]π΅) β if(π₯ β (π΄[,]π΅), (π· β πΆ), 0) = (volβ(π β {π₯}))) |
48 | 37, 47 | pm2.61i 182 |
. . . . . . . . 9
β’ if(π₯ β (π΄[,]π΅), (π· β πΆ), 0) = (volβ(π β {π₯})) |
49 | 48 | eqcomi 2742 |
. . . . . . . 8
β’
(volβ(π
β {π₯})) = if(π₯ β (π΄[,]π΅), (π· β πΆ), 0) |
50 | 49 | a1i 11 |
. . . . . . 7
β’ (π₯ β β β
(volβ(π β
{π₯})) = if(π₯ β (π΄[,]π΅), (π· β πΆ), 0)) |
51 | 7, 6 | resubcli 11468 |
. . . . . . . 8
β’ (π· β πΆ) β β |
52 | | 0re 11162 |
. . . . . . . 8
β’ 0 β
β |
53 | 51, 52 | ifcli 4534 |
. . . . . . 7
β’ if(π₯ β (π΄[,]π΅), (π· β πΆ), 0) β β |
54 | 50, 53 | eqeltrdi 2842 |
. . . . . 6
β’ (π₯ β β β
(volβ(π β
{π₯})) β
β) |
55 | | volf 24909 |
. . . . . . . 8
β’ vol:dom
volβΆ(0[,]+β) |
56 | | ffun 6672 |
. . . . . . . 8
β’ (vol:dom
volβΆ(0[,]+β) β Fun vol) |
57 | 55, 56 | ax-mp 5 |
. . . . . . 7
β’ Fun
vol |
58 | 29, 41 | ifcli 4534 |
. . . . . . . 8
β’ if(π₯ β (π΄[,]π΅), (πΆ[,]π·), β
) β dom vol |
59 | 24, 58 | eqeltri 2830 |
. . . . . . 7
β’ (π β {π₯}) β dom vol |
60 | | fvimacnv 7004 |
. . . . . . 7
β’ ((Fun vol
β§ (π β {π₯}) β dom vol) β
((volβ(π β
{π₯})) β β β
(π β {π₯}) β (β‘vol β β))) |
61 | 57, 59, 60 | mp2an 691 |
. . . . . 6
β’
((volβ(π
β {π₯})) β
β β (π β
{π₯}) β (β‘vol β β)) |
62 | 54, 61 | sylib 217 |
. . . . 5
β’ (π₯ β β β (π β {π₯}) β (β‘vol β β)) |
63 | 62 | rgen 3063 |
. . . 4
β’
βπ₯ β
β (π β {π₯}) β (β‘vol β β) |
64 | 5 | a1i 11 |
. . . . . 6
β’ (0 β
β β (π΄[,]π΅) β
β) |
65 | | rembl 24920 |
. . . . . . 7
β’ β
β dom vol |
66 | 65 | a1i 11 |
. . . . . 6
β’ (0 β
β β β β dom vol) |
67 | 36, 51 | eqeltrdi 2842 |
. . . . . . 7
β’ (π₯ β (π΄[,]π΅) β (volβ(π β {π₯})) β β) |
68 | 67 | adantl 483 |
. . . . . 6
β’ ((0
β β β§ π₯
β (π΄[,]π΅)) β (volβ(π β {π₯})) β β) |
69 | | eldifn 4088 |
. . . . . . . 8
β’ (π₯ β (β β (π΄[,]π΅)) β Β¬ π₯ β (π΄[,]π΅)) |
70 | 69, 46 | syl 17 |
. . . . . . 7
β’ (π₯ β (β β (π΄[,]π΅)) β (volβ(π β {π₯})) = 0) |
71 | 70 | adantl 483 |
. . . . . 6
β’ ((0
β β β§ π₯
β (β β (π΄[,]π΅))) β (volβ(π β {π₯})) = 0) |
72 | 36 | mpteq2ia 5209 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β¦ (volβ(π β {π₯}))) = (π₯ β (π΄[,]π΅) β¦ (π· β πΆ)) |
73 | 51 | recni 11174 |
. . . . . . . . . 10
β’ (π· β πΆ) β β |
74 | | ax-resscn 11113 |
. . . . . . . . . . 11
β’ β
β β |
75 | 5, 74 | sstri 3954 |
. . . . . . . . . 10
β’ (π΄[,]π΅) β β |
76 | | ssid 3967 |
. . . . . . . . . 10
β’ β
β β |
77 | | cncfmptc 24291 |
. . . . . . . . . 10
β’ (((π· β πΆ) β β β§ (π΄[,]π΅) β β β§ β β
β) β (π₯ β
(π΄[,]π΅) β¦ (π· β πΆ)) β ((π΄[,]π΅)βcnββ)) |
78 | 73, 75, 76, 77 | mp3an 1462 |
. . . . . . . . 9
β’ (π₯ β (π΄[,]π΅) β¦ (π· β πΆ)) β ((π΄[,]π΅)βcnββ) |
79 | | cniccibl 25221 |
. . . . . . . . 9
β’ ((π΄ β β β§ π΅ β β β§ (π₯ β (π΄[,]π΅) β¦ (π· β πΆ)) β ((π΄[,]π΅)βcnββ)) β (π₯ β (π΄[,]π΅) β¦ (π· β πΆ)) β
πΏ1) |
80 | 2, 3, 78, 79 | mp3an 1462 |
. . . . . . . 8
β’ (π₯ β (π΄[,]π΅) β¦ (π· β πΆ)) β
πΏ1 |
81 | 72, 80 | eqeltri 2830 |
. . . . . . 7
β’ (π₯ β (π΄[,]π΅) β¦ (volβ(π β {π₯}))) β
πΏ1 |
82 | 81 | a1i 11 |
. . . . . 6
β’ (0 β
β β (π₯ β
(π΄[,]π΅) β¦ (volβ(π β {π₯}))) β
πΏ1) |
83 | 64, 66, 68, 71, 82 | iblss2 25186 |
. . . . 5
β’ (0 β
β β (π₯ β
β β¦ (volβ(π β {π₯}))) β
πΏ1) |
84 | 52, 83 | ax-mp 5 |
. . . 4
β’ (π₯ β β β¦
(volβ(π β
{π₯}))) β
πΏ1 |
85 | | dmarea 26323 |
. . . 4
β’ (π β dom area β (π β (β Γ
β) β§ βπ₯
β β (π β
{π₯}) β (β‘vol β β) β§ (π₯ β β β¦
(volβ(π β
{π₯}))) β
πΏ1)) |
86 | 12, 63, 84, 85 | mpbir3an 1342 |
. . 3
β’ π β dom
area |
87 | | areaval 26330 |
. . 3
β’ (π β dom area β
(areaβπ) =
β«β(volβ(π
β {π₯})) dπ₯) |
88 | 86, 87 | ax-mp 5 |
. 2
β’
(areaβπ) =
β«β(volβ(π
β {π₯})) dπ₯ |
89 | | itgeq2 25158 |
. . . 4
β’
(βπ₯ β
β (volβ(π
β {π₯})) = if(π₯ β (π΄[,]π΅), (π· β πΆ), 0) β β«β(volβ(π β {π₯})) dπ₯ = β«βif(π₯ β (π΄[,]π΅), (π· β πΆ), 0) dπ₯) |
90 | 89, 50 | mprg 3067 |
. . 3
β’
β«β(volβ(π β {π₯})) dπ₯ = β«βif(π₯ β (π΄[,]π΅), (π· β πΆ), 0) dπ₯ |
91 | | iccmbl 24946 |
. . . . . 6
β’ ((π΄ β β β§ π΅ β β) β (π΄[,]π΅) β dom vol) |
92 | 2, 3, 91 | mp2an 691 |
. . . . 5
β’ (π΄[,]π΅) β dom vol |
93 | | mblvol 24910 |
. . . . . . . 8
β’ ((π΄[,]π΅) β dom vol β (volβ(π΄[,]π΅)) = (vol*β(π΄[,]π΅))) |
94 | 92, 93 | ax-mp 5 |
. . . . . . 7
β’
(volβ(π΄[,]π΅)) = (vol*β(π΄[,]π΅)) |
95 | | arearect.5 |
. . . . . . . 8
β’ π΄ β€ π΅ |
96 | | ovolicc 24903 |
. . . . . . . 8
β’ ((π΄ β β β§ π΅ β β β§ π΄ β€ π΅) β (vol*β(π΄[,]π΅)) = (π΅ β π΄)) |
97 | 2, 3, 95, 96 | mp3an 1462 |
. . . . . . 7
β’
(vol*β(π΄[,]π΅)) = (π΅ β π΄) |
98 | 94, 97 | eqtri 2761 |
. . . . . 6
β’
(volβ(π΄[,]π΅)) = (π΅ β π΄) |
99 | 3, 2 | resubcli 11468 |
. . . . . 6
β’ (π΅ β π΄) β β |
100 | 98, 99 | eqeltri 2830 |
. . . . 5
β’
(volβ(π΄[,]π΅)) β β |
101 | | itgconst 25199 |
. . . . 5
β’ (((π΄[,]π΅) β dom vol β§ (volβ(π΄[,]π΅)) β β β§ (π· β πΆ) β β) β β«(π΄[,]π΅)(π· β πΆ) dπ₯ = ((π· β πΆ) Β· (volβ(π΄[,]π΅)))) |
102 | 92, 100, 73, 101 | mp3an 1462 |
. . . 4
β’
β«(π΄[,]π΅)(π· β πΆ) dπ₯ = ((π· β πΆ) Β· (volβ(π΄[,]π΅))) |
103 | | itgss2 25193 |
. . . . 5
β’ ((π΄[,]π΅) β β β β«(π΄[,]π΅)(π· β πΆ) dπ₯ = β«βif(π₯ β (π΄[,]π΅), (π· β πΆ), 0) dπ₯) |
104 | 5, 103 | ax-mp 5 |
. . . 4
β’
β«(π΄[,]π΅)(π· β πΆ) dπ₯ = β«βif(π₯ β (π΄[,]π΅), (π· β πΆ), 0) dπ₯ |
105 | 98 | oveq2i 7369 |
. . . 4
β’ ((π· β πΆ) Β· (volβ(π΄[,]π΅))) = ((π· β πΆ) Β· (π΅ β π΄)) |
106 | 102, 104,
105 | 3eqtr3i 2769 |
. . 3
β’
β«βif(π₯
β (π΄[,]π΅), (π· β πΆ), 0) dπ₯ = ((π· β πΆ) Β· (π΅ β π΄)) |
107 | 90, 106 | eqtri 2761 |
. 2
β’
β«β(volβ(π β {π₯})) dπ₯ = ((π· β πΆ) Β· (π΅ β π΄)) |
108 | 99 | recni 11174 |
. . 3
β’ (π΅ β π΄) β β |
109 | 73, 108 | mulcomi 11168 |
. 2
β’ ((π· β πΆ) Β· (π΅ β π΄)) = ((π΅ β π΄) Β· (π· β πΆ)) |
110 | 88, 107, 109 | 3eqtri 2765 |
1
β’
(areaβπ) =
((π΅ β π΄) Β· (π· β πΆ)) |