Step | Hyp | Ref
| Expression |
1 | | rge0ssre 13382 |
. . . 4
β’
(0[,)+β) β β |
2 | | hspmbllem1.l |
. . . . 5
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
3 | | hspmbllem1.x |
. . . . 5
β’ (π β π β Fin) |
4 | | hspmbllem1.a |
. . . . 5
β’ (π β π΄:πβΆβ) |
5 | | hspmbllem1.t |
. . . . . 6
β’ π = (π¦ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β (π β {πΎ}), (πββ), if((πββ) β€ π¦, (πββ), π¦))))) |
6 | | hspmbllem1.y |
. . . . . 6
β’ (π β π β β) |
7 | | hspmbllem1.b |
. . . . . 6
β’ (π β π΅:πβΆβ) |
8 | 5, 6, 3, 7 | hsphoif 44907 |
. . . . 5
β’ (π β ((πβπ)βπ΅):πβΆβ) |
9 | 2, 3, 4, 8 | hoidmvcl 44913 |
. . . 4
β’ (π β (π΄(πΏβπ)((πβπ)βπ΅)) β (0[,)+β)) |
10 | 1, 9 | sselid 3946 |
. . 3
β’ (π β (π΄(πΏβπ)((πβπ)βπ΅)) β β) |
11 | | hspmbllem1.s |
. . . . . 6
β’ π = (π₯ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β = πΎ, if(π₯ β€ (πββ), (πββ), π₯), (πββ))))) |
12 | 11, 6, 3, 4 | hoidifhspf 44949 |
. . . . 5
β’ (π β ((πβπ)βπ΄):πβΆβ) |
13 | 2, 3, 12, 7 | hoidmvcl 44913 |
. . . 4
β’ (π β (((πβπ)βπ΄)(πΏβπ)π΅) β (0[,)+β)) |
14 | 1, 13 | sselid 3946 |
. . 3
β’ (π β (((πβπ)βπ΄)(πΏβπ)π΅) β β) |
15 | 10, 14 | rexaddd 13162 |
. 2
β’ (π β ((π΄(πΏβπ)((πβπ)βπ΅)) +π (((πβπ)βπ΄)(πΏβπ)π΅)) = ((π΄(πΏβπ)((πβπ)βπ΅)) + (((πβπ)βπ΄)(πΏβπ)π΅))) |
16 | | hspmbllem1.k |
. . . . . 6
β’ (π β πΎ β π) |
17 | 16 | ne0d 4299 |
. . . . 5
β’ (π β π β β
) |
18 | 2, 3, 17, 4, 8 | hoidmvn0val 44915 |
. . . 4
β’ (π β (π΄(πΏβπ)((πβπ)βπ΅)) = βπ β π (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ)))) |
19 | 2, 3, 17, 12, 7 | hoidmvn0val 44915 |
. . . 4
β’ (π β (((πβπ)βπ΄)(πΏβπ)π΅) = βπ β π (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ)))) |
20 | 18, 19 | oveq12d 7379 |
. . 3
β’ (π β ((π΄(πΏβπ)((πβπ)βπ΅)) + (((πβπ)βπ΄)(πΏβπ)π΅)) = (βπ β π (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) + βπ β π (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))))) |
21 | | uncom 4117 |
. . . . . . . . 9
β’ ((π β {πΎ}) βͺ {πΎ}) = ({πΎ} βͺ (π β {πΎ})) |
22 | 21 | a1i 11 |
. . . . . . . 8
β’ (π β ((π β {πΎ}) βͺ {πΎ}) = ({πΎ} βͺ (π β {πΎ}))) |
23 | 16 | snssd 4773 |
. . . . . . . . 9
β’ (π β {πΎ} β π) |
24 | | undif 4445 |
. . . . . . . . 9
β’ ({πΎ} β π β ({πΎ} βͺ (π β {πΎ})) = π) |
25 | 23, 24 | sylib 217 |
. . . . . . . 8
β’ (π β ({πΎ} βͺ (π β {πΎ})) = π) |
26 | 22, 25 | eqtrd 2773 |
. . . . . . 7
β’ (π β ((π β {πΎ}) βͺ {πΎ}) = π) |
27 | 26 | eqcomd 2739 |
. . . . . 6
β’ (π β π = ((π β {πΎ}) βͺ {πΎ})) |
28 | 27 | prodeq1d 15812 |
. . . . 5
β’ (π β βπ β π (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) = βπ β ((π β {πΎ}) βͺ {πΎ})(volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ)))) |
29 | | nfv 1918 |
. . . . . 6
β’
β²ππ |
30 | | nfcv 2904 |
. . . . . 6
β’
β²π(volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) |
31 | | difssd 4096 |
. . . . . . 7
β’ (π β (π β {πΎ}) β π) |
32 | 3, 31 | ssfid 9217 |
. . . . . 6
β’ (π β (π β {πΎ}) β Fin) |
33 | | neldifsnd 4757 |
. . . . . 6
β’ (π β Β¬ πΎ β (π β {πΎ})) |
34 | 4 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π β {πΎ})) β π΄:πβΆβ) |
35 | 31 | sselda 3948 |
. . . . . . . . 9
β’ ((π β§ π β (π β {πΎ})) β π β π) |
36 | 34, 35 | ffvelcdmd 7040 |
. . . . . . . 8
β’ ((π β§ π β (π β {πΎ})) β (π΄βπ) β β) |
37 | 6 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π β {πΎ})) β π β β) |
38 | 3 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π β {πΎ})) β π β Fin) |
39 | 7 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β (π β {πΎ})) β π΅:πβΆβ) |
40 | 5, 37, 38, 39 | hsphoif 44907 |
. . . . . . . . 9
β’ ((π β§ π β (π β {πΎ})) β ((πβπ)βπ΅):πβΆβ) |
41 | 40, 35 | ffvelcdmd 7040 |
. . . . . . . 8
β’ ((π β§ π β (π β {πΎ})) β (((πβπ)βπ΅)βπ) β β) |
42 | | volicore 44912 |
. . . . . . . 8
β’ (((π΄βπ) β β β§ (((πβπ)βπ΅)βπ) β β) β (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) β β) |
43 | 36, 41, 42 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β (π β {πΎ})) β (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) β β) |
44 | 43 | recnd 11191 |
. . . . . 6
β’ ((π β§ π β (π β {πΎ})) β (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) β β) |
45 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (π΄βπ) = (π΄βπΎ)) |
46 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (((πβπ)βπ΅)βπ) = (((πβπ)βπ΅)βπΎ)) |
47 | 45, 46 | oveq12d 7379 |
. . . . . . 7
β’ (π = πΎ β ((π΄βπ)[,)(((πβπ)βπ΅)βπ)) = ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) |
48 | 47 | fveq2d 6850 |
. . . . . 6
β’ (π = πΎ β (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) = (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ)))) |
49 | 4, 16 | ffvelcdmd 7040 |
. . . . . . . 8
β’ (π β (π΄βπΎ) β β) |
50 | 8, 16 | ffvelcdmd 7040 |
. . . . . . . 8
β’ (π β (((πβπ)βπ΅)βπΎ) β β) |
51 | | volicore 44912 |
. . . . . . . 8
β’ (((π΄βπΎ) β β β§ (((πβπ)βπ΅)βπΎ) β β) β (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) β β) |
52 | 49, 50, 51 | syl2anc 585 |
. . . . . . 7
β’ (π β (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) β β) |
53 | 52 | recnd 11191 |
. . . . . 6
β’ (π β (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) β β) |
54 | 29, 30, 32, 16, 33, 44, 48, 53 | fprodsplitsn 15880 |
. . . . 5
β’ (π β βπ β ((π β {πΎ}) βͺ {πΎ})(volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) = (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) Β· (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))))) |
55 | 5, 37, 38, 39, 35 | hsphoival 44910 |
. . . . . . . . . 10
β’ ((π β§ π β (π β {πΎ})) β (((πβπ)βπ΅)βπ) = if(π β (π β {πΎ}), (π΅βπ), if((π΅βπ) β€ π, (π΅βπ), π))) |
56 | | iftrue 4496 |
. . . . . . . . . . 11
β’ (π β (π β {πΎ}) β if(π β (π β {πΎ}), (π΅βπ), if((π΅βπ) β€ π, (π΅βπ), π)) = (π΅βπ)) |
57 | 56 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β (π β {πΎ})) β if(π β (π β {πΎ}), (π΅βπ), if((π΅βπ) β€ π, (π΅βπ), π)) = (π΅βπ)) |
58 | 55, 57 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ π β (π β {πΎ})) β (((πβπ)βπ΅)βπ) = (π΅βπ)) |
59 | 58 | oveq2d 7377 |
. . . . . . . 8
β’ ((π β§ π β (π β {πΎ})) β ((π΄βπ)[,)(((πβπ)βπ΅)βπ)) = ((π΄βπ)[,)(π΅βπ))) |
60 | 59 | fveq2d 6850 |
. . . . . . 7
β’ ((π β§ π β (π β {πΎ})) β (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
61 | 60 | prodeq2dv 15814 |
. . . . . 6
β’ (π β βπ β (π β {πΎ})(volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) = βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ)))) |
62 | 61 | oveq1d 7376 |
. . . . 5
β’ (π β (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) Β· (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ)))) = (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))))) |
63 | 28, 54, 62 | 3eqtrd 2777 |
. . . 4
β’ (π β βπ β π (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) = (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))))) |
64 | 27 | prodeq1d 15812 |
. . . . 5
β’ (π β βπ β π (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) = βπ β ((π β {πΎ}) βͺ {πΎ})(volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ)))) |
65 | | nfcv 2904 |
. . . . . 6
β’
β²π(volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))) |
66 | 12 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β (π β {πΎ})) β ((πβπ)βπ΄):πβΆβ) |
67 | 66, 35 | ffvelcdmd 7040 |
. . . . . . . 8
β’ ((π β§ π β (π β {πΎ})) β (((πβπ)βπ΄)βπ) β β) |
68 | 58, 41 | eqeltrrd 2835 |
. . . . . . . 8
β’ ((π β§ π β (π β {πΎ})) β (π΅βπ) β β) |
69 | | volicore 44912 |
. . . . . . . 8
β’
(((((πβπ)βπ΄)βπ) β β β§ (π΅βπ) β β) β (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) β β) |
70 | 67, 68, 69 | syl2anc 585 |
. . . . . . 7
β’ ((π β§ π β (π β {πΎ})) β (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) β β) |
71 | 70 | recnd 11191 |
. . . . . 6
β’ ((π β§ π β (π β {πΎ})) β (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) β β) |
72 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (((πβπ)βπ΄)βπ) = (((πβπ)βπ΄)βπΎ)) |
73 | | fveq2 6846 |
. . . . . . . 8
β’ (π = πΎ β (π΅βπ) = (π΅βπΎ)) |
74 | 72, 73 | oveq12d 7379 |
. . . . . . 7
β’ (π = πΎ β ((((πβπ)βπ΄)βπ)[,)(π΅βπ)) = ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))) |
75 | 74 | fveq2d 6850 |
. . . . . 6
β’ (π = πΎ β (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) = (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ)))) |
76 | 12, 16 | ffvelcdmd 7040 |
. . . . . . . 8
β’ (π β (((πβπ)βπ΄)βπΎ) β β) |
77 | 7, 16 | ffvelcdmd 7040 |
. . . . . . . 8
β’ (π β (π΅βπΎ) β β) |
78 | | volicore 44912 |
. . . . . . . 8
β’
(((((πβπ)βπ΄)βπΎ) β β β§ (π΅βπΎ) β β) β
(volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))) β β) |
79 | 76, 77, 78 | syl2anc 585 |
. . . . . . 7
β’ (π β (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))) β β) |
80 | 79 | recnd 11191 |
. . . . . 6
β’ (π β (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))) β β) |
81 | 29, 65, 32, 16, 33, 71, 75, 80 | fprodsplitsn 15880 |
. . . . 5
β’ (π β βπ β ((π β {πΎ}) βͺ {πΎ})(volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) = (βπ β (π β {πΎ})(volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) Β· (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))))) |
82 | 11, 37, 38, 34, 35 | hoidifhspval3 44950 |
. . . . . . . . 9
β’ ((π β§ π β (π β {πΎ})) β (((πβπ)βπ΄)βπ) = if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ))) |
83 | | eldifsni 4754 |
. . . . . . . . . . . 12
β’ (π β (π β {πΎ}) β π β πΎ) |
84 | | neneq 2946 |
. . . . . . . . . . . 12
β’ (π β πΎ β Β¬ π = πΎ) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
β’ (π β (π β {πΎ}) β Β¬ π = πΎ) |
86 | 85 | iffalsed 4501 |
. . . . . . . . . 10
β’ (π β (π β {πΎ}) β if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ)) = (π΄βπ)) |
87 | 86 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (π β {πΎ})) β if(π = πΎ, if(π β€ (π΄βπ), (π΄βπ), π), (π΄βπ)) = (π΄βπ)) |
88 | 82, 87 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π β (π β {πΎ})) β (((πβπ)βπ΄)βπ) = (π΄βπ)) |
89 | 88 | fvoveq1d 7383 |
. . . . . . 7
β’ ((π β§ π β (π β {πΎ})) β (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
90 | 89 | prodeq2dv 15814 |
. . . . . 6
β’ (π β βπ β (π β {πΎ})(volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) = βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ)))) |
91 | 90 | oveq1d 7376 |
. . . . 5
β’ (π β (βπ β (π β {πΎ})(volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) Β· (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ)))) = (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))))) |
92 | 64, 81, 91 | 3eqtrd 2777 |
. . . 4
β’ (π β βπ β π (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ))) = (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))))) |
93 | 63, 92 | oveq12d 7379 |
. . 3
β’ (π β (βπ β π (volβ((π΄βπ)[,)(((πβπ)βπ΅)βπ))) + βπ β π (volβ((((πβπ)βπ΄)βπ)[,)(π΅βπ)))) = ((βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ)))) + (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ)))))) |
94 | 27 | prodeq1d 15812 |
. . . . 5
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = βπ β ((π β {πΎ}) βͺ {πΎ})(volβ((π΄βπ)[,)(π΅βπ)))) |
95 | | nfcv 2904 |
. . . . . 6
β’
β²π(volβ((π΄βπΎ)[,)(π΅βπΎ))) |
96 | 60, 44 | eqeltrrd 2835 |
. . . . . 6
β’ ((π β§ π β (π β {πΎ})) β (volβ((π΄βπ)[,)(π΅βπ))) β β) |
97 | 45, 73 | oveq12d 7379 |
. . . . . . 7
β’ (π = πΎ β ((π΄βπ)[,)(π΅βπ)) = ((π΄βπΎ)[,)(π΅βπΎ))) |
98 | 97 | fveq2d 6850 |
. . . . . 6
β’ (π = πΎ β (volβ((π΄βπ)[,)(π΅βπ))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
99 | | volicore 44912 |
. . . . . . . 8
β’ (((π΄βπΎ) β β β§ (π΅βπΎ) β β) β (volβ((π΄βπΎ)[,)(π΅βπΎ))) β β) |
100 | 49, 77, 99 | syl2anc 585 |
. . . . . . 7
β’ (π β (volβ((π΄βπΎ)[,)(π΅βπΎ))) β β) |
101 | 100 | recnd 11191 |
. . . . . 6
β’ (π β (volβ((π΄βπΎ)[,)(π΅βπΎ))) β β) |
102 | 29, 95, 32, 16, 33, 96, 98, 101 | fprodsplitsn 15880 |
. . . . 5
β’ (π β βπ β ((π β {πΎ}) βͺ {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) = (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπΎ)[,)(π΅βπΎ))))) |
103 | 94, 102 | eqtrd 2773 |
. . . 4
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπΎ)[,)(π΅βπΎ))))) |
104 | 5, 6, 3, 7, 16 | hsphoival 44910 |
. . . . . . . . . 10
β’ (π β (((πβπ)βπ΅)βπΎ) = if(πΎ β (π β {πΎ}), (π΅βπΎ), if((π΅βπΎ) β€ π, (π΅βπΎ), π))) |
105 | 33 | iffalsed 4501 |
. . . . . . . . . 10
β’ (π β if(πΎ β (π β {πΎ}), (π΅βπΎ), if((π΅βπΎ) β€ π, (π΅βπΎ), π)) = if((π΅βπΎ) β€ π, (π΅βπΎ), π)) |
106 | 104, 105 | eqtrd 2773 |
. . . . . . . . 9
β’ (π β (((πβπ)βπ΅)βπΎ) = if((π΅βπΎ) β€ π, (π΅βπΎ), π)) |
107 | 106 | oveq2d 7377 |
. . . . . . . 8
β’ (π β ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ)) = ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) |
108 | 107 | fveq2d 6850 |
. . . . . . 7
β’ (π β (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) = (volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π)))) |
109 | 11, 6, 3, 4, 16 | hoidifhspval3 44950 |
. . . . . . . . 9
β’ (π β (((πβπ)βπ΄)βπΎ) = if(πΎ = πΎ, if(π β€ (π΄βπΎ), (π΄βπΎ), π), (π΄βπΎ))) |
110 | | eqid 2733 |
. . . . . . . . . . 11
β’ πΎ = πΎ |
111 | 110 | iftruei 4497 |
. . . . . . . . . 10
β’ if(πΎ = πΎ, if(π β€ (π΄βπΎ), (π΄βπΎ), π), (π΄βπΎ)) = if(π β€ (π΄βπΎ), (π΄βπΎ), π) |
112 | 111 | a1i 11 |
. . . . . . . . 9
β’ (π β if(πΎ = πΎ, if(π β€ (π΄βπΎ), (π΄βπΎ), π), (π΄βπΎ)) = if(π β€ (π΄βπΎ), (π΄βπΎ), π)) |
113 | 109, 112 | eqtrd 2773 |
. . . . . . . 8
β’ (π β (((πβπ)βπ΄)βπΎ) = if(π β€ (π΄βπΎ), (π΄βπΎ), π)) |
114 | 113 | fvoveq1d 7383 |
. . . . . . 7
β’ (π β (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))) = (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) |
115 | 108, 114 | oveq12d 7379 |
. . . . . 6
β’ (π β ((volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) + (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ)))) = ((volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ))))) |
116 | | iftrue 4496 |
. . . . . . . . . . . 12
β’ ((π΅βπΎ) β€ π β if((π΅βπΎ) β€ π, (π΅βπΎ), π) = (π΅βπΎ)) |
117 | 116 | oveq2d 7377 |
. . . . . . . . . . 11
β’ ((π΅βπΎ) β€ π β ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π)) = ((π΄βπΎ)[,)(π΅βπΎ))) |
118 | 117 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π΅βπΎ) β€ π β (volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
119 | 118 | oveq1d 7376 |
. . . . . . . . 9
β’ ((π΅βπΎ) β€ π β ((volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = ((volβ((π΄βπΎ)[,)(π΅βπΎ))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ))))) |
120 | 119 | adantl 483 |
. . . . . . . 8
β’ ((π β§ (π΅βπΎ) β€ π) β ((volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = ((volβ((π΄βπΎ)[,)(π΅βπΎ))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ))))) |
121 | | iftrue 4496 |
. . . . . . . . . . . . . . 15
β’ (π β€ (π΄βπΎ) β if(π β€ (π΄βπΎ), (π΄βπΎ), π) = (π΄βπΎ)) |
122 | 121 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’ (π β€ (π΄βπΎ) β (if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)) = ((π΄βπΎ)[,)(π΅βπΎ))) |
123 | 122 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β (if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)) = ((π΄βπΎ)[,)(π΅βπΎ))) |
124 | 77 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β (π΅βπΎ) β β) |
125 | 6 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β π β β) |
126 | 49 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β (π΄βπΎ) β β) |
127 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β (π΅βπΎ) β€ π) |
128 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β π β€ (π΄βπΎ)) |
129 | 124, 125,
126, 127, 128 | letrd 11320 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β (π΅βπΎ) β€ (π΄βπΎ)) |
130 | 126 | rexrd 11213 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β (π΄βπΎ) β
β*) |
131 | 124 | rexrd 11213 |
. . . . . . . . . . . . . . 15
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β (π΅βπΎ) β
β*) |
132 | | ico0 13319 |
. . . . . . . . . . . . . . 15
β’ (((π΄βπΎ) β β* β§ (π΅βπΎ) β β*) β
(((π΄βπΎ)[,)(π΅βπΎ)) = β
β (π΅βπΎ) β€ (π΄βπΎ))) |
133 | 130, 131,
132 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β (((π΄βπΎ)[,)(π΅βπΎ)) = β
β (π΅βπΎ) β€ (π΄βπΎ))) |
134 | 129, 133 | mpbird 257 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β ((π΄βπΎ)[,)(π΅βπΎ)) = β
) |
135 | 123, 134 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅βπΎ) β€ π) β§ π β€ (π΄βπΎ)) β (if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)) = β
) |
136 | | iffalse 4499 |
. . . . . . . . . . . . . . 15
β’ (Β¬
π β€ (π΄βπΎ) β if(π β€ (π΄βπΎ), (π΄βπΎ), π) = π) |
137 | 136 | oveq1d 7376 |
. . . . . . . . . . . . . 14
β’ (Β¬
π β€ (π΄βπΎ) β (if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)) = (π[,)(π΅βπΎ))) |
138 | 137 | adantl 483 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΅βπΎ) β€ π) β§ Β¬ π β€ (π΄βπΎ)) β (if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)) = (π[,)(π΅βπΎ))) |
139 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π΅βπΎ) β€ π) β (π΅βπΎ) β€ π) |
140 | 6 | rexrd 11213 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β
β*) |
141 | 140 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π΅βπΎ) β€ π) β π β
β*) |
142 | 77 | rexrd 11213 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π΅βπΎ) β
β*) |
143 | 142 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π΅βπΎ) β€ π) β (π΅βπΎ) β
β*) |
144 | | ico0 13319 |
. . . . . . . . . . . . . . . 16
β’ ((π β β*
β§ (π΅βπΎ) β β*)
β ((π[,)(π΅βπΎ)) = β
β (π΅βπΎ) β€ π)) |
145 | 141, 143,
144 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π΅βπΎ) β€ π) β ((π[,)(π΅βπΎ)) = β
β (π΅βπΎ) β€ π)) |
146 | 139, 145 | mpbird 257 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΅βπΎ) β€ π) β (π[,)(π΅βπΎ)) = β
) |
147 | 146 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ (π΅βπΎ) β€ π) β§ Β¬ π β€ (π΄βπΎ)) β (π[,)(π΅βπΎ)) = β
) |
148 | 138, 147 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π β§ (π΅βπΎ) β€ π) β§ Β¬ π β€ (π΄βπΎ)) β (if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)) = β
) |
149 | 135, 148 | pm2.61dan 812 |
. . . . . . . . . . 11
β’ ((π β§ (π΅βπΎ) β€ π) β (if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)) = β
) |
150 | 149 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ (π΅βπΎ) β€ π) β (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ))) = (volββ
)) |
151 | | vol0 44290 |
. . . . . . . . . . 11
β’
(volββ
) = 0 |
152 | 151 | a1i 11 |
. . . . . . . . . 10
β’ ((π β§ (π΅βπΎ) β€ π) β (volββ
) =
0) |
153 | 150, 152 | eqtrd 2773 |
. . . . . . . . 9
β’ ((π β§ (π΅βπΎ) β€ π) β (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ))) = 0) |
154 | 153 | oveq2d 7377 |
. . . . . . . 8
β’ ((π β§ (π΅βπΎ) β€ π) β ((volβ((π΄βπΎ)[,)(π΅βπΎ))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = ((volβ((π΄βπΎ)[,)(π΅βπΎ))) + 0)) |
155 | 101 | addridd 11363 |
. . . . . . . . 9
β’ (π β ((volβ((π΄βπΎ)[,)(π΅βπΎ))) + 0) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
156 | 155 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π΅βπΎ) β€ π) β ((volβ((π΄βπΎ)[,)(π΅βπΎ))) + 0) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
157 | 120, 154,
156 | 3eqtrd 2777 |
. . . . . . 7
β’ ((π β§ (π΅βπΎ) β€ π) β ((volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
158 | | iffalse 4499 |
. . . . . . . . . . . 12
β’ (Β¬
(π΅βπΎ) β€ π β if((π΅βπΎ) β€ π, (π΅βπΎ), π) = π) |
159 | 158 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (Β¬
(π΅βπΎ) β€ π β ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π)) = ((π΄βπΎ)[,)π)) |
160 | 159 | fveq2d 6850 |
. . . . . . . . . 10
β’ (Β¬
(π΅βπΎ) β€ π β (volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) = (volβ((π΄βπΎ)[,)π))) |
161 | 160 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β (volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) = (volβ((π΄βπΎ)[,)π))) |
162 | 161 | oveq1d 7376 |
. . . . . . . 8
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β ((volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = ((volβ((π΄βπΎ)[,)π)) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ))))) |
163 | | simpl 484 |
. . . . . . . . 9
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β π) |
164 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β Β¬ (π΅βπΎ) β€ π) |
165 | 163, 6 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β π β β) |
166 | 163, 77 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β (π΅βπΎ) β β) |
167 | 165, 166 | ltnled 11310 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β (π < (π΅βπΎ) β Β¬ (π΅βπΎ) β€ π)) |
168 | 164, 167 | mpbird 257 |
. . . . . . . . 9
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β π < (π΅βπΎ)) |
169 | 121 | fvoveq1d 7383 |
. . . . . . . . . . . . 13
β’ (π β€ (π΄βπΎ) β (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
170 | 169 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ (π β€ (π΄βπΎ) β ((volβ((π΄βπΎ)[,)π)) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = ((volβ((π΄βπΎ)[,)π)) + (volβ((π΄βπΎ)[,)(π΅βπΎ))))) |
171 | 170 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π < (π΅βπΎ)) β§ π β€ (π΄βπΎ)) β ((volβ((π΄βπΎ)[,)π)) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = ((volβ((π΄βπΎ)[,)π)) + (volβ((π΄βπΎ)[,)(π΅βπΎ))))) |
172 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β€ (π΄βπΎ)) β π β€ (π΄βπΎ)) |
173 | 49 | rexrd 11213 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π΄βπΎ) β
β*) |
174 | 173 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β€ (π΄βπΎ)) β (π΄βπΎ) β
β*) |
175 | 140 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β€ (π΄βπΎ)) β π β
β*) |
176 | | ico0 13319 |
. . . . . . . . . . . . . . . . 17
β’ (((π΄βπΎ) β β* β§ π β β*)
β (((π΄βπΎ)[,)π) = β
β π β€ (π΄βπΎ))) |
177 | 174, 175,
176 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β€ (π΄βπΎ)) β (((π΄βπΎ)[,)π) = β
β π β€ (π΄βπΎ))) |
178 | 172, 177 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β€ (π΄βπΎ)) β ((π΄βπΎ)[,)π) = β
) |
179 | 178 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β€ (π΄βπΎ)) β (volβ((π΄βπΎ)[,)π)) = (volββ
)) |
180 | 151 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β€ (π΄βπΎ)) β (volββ
) =
0) |
181 | 179, 180 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ ((π β§ π β€ (π΄βπΎ)) β (volβ((π΄βπΎ)[,)π)) = 0) |
182 | 181 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ ((π β§ π β€ (π΄βπΎ)) β ((volβ((π΄βπΎ)[,)π)) + (volβ((π΄βπΎ)[,)(π΅βπΎ)))) = (0 + (volβ((π΄βπΎ)[,)(π΅βπΎ))))) |
183 | 182 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π < (π΅βπΎ)) β§ π β€ (π΄βπΎ)) β ((volβ((π΄βπΎ)[,)π)) + (volβ((π΄βπΎ)[,)(π΅βπΎ)))) = (0 + (volβ((π΄βπΎ)[,)(π΅βπΎ))))) |
184 | 101 | addlidd 11364 |
. . . . . . . . . . . 12
β’ (π β (0 + (volβ((π΄βπΎ)[,)(π΅βπΎ)))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
185 | 184 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π < (π΅βπΎ)) β§ π β€ (π΄βπΎ)) β (0 + (volβ((π΄βπΎ)[,)(π΅βπΎ)))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
186 | 171, 183,
185 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ π < (π΅βπΎ)) β§ π β€ (π΄βπΎ)) β ((volβ((π΄βπΎ)[,)π)) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
187 | 136 | fvoveq1d 7383 |
. . . . . . . . . . . . 13
β’ (Β¬
π β€ (π΄βπΎ) β (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ))) = (volβ(π[,)(π΅βπΎ)))) |
188 | 187 | oveq2d 7377 |
. . . . . . . . . . . 12
β’ (Β¬
π β€ (π΄βπΎ) β ((volβ((π΄βπΎ)[,)π)) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = ((volβ((π΄βπΎ)[,)π)) + (volβ(π[,)(π΅βπΎ))))) |
189 | 188 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π < (π΅βπΎ)) β§ Β¬ π β€ (π΄βπΎ)) β ((volβ((π΄βπΎ)[,)π)) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = ((volβ((π΄βπΎ)[,)π)) + (volβ(π[,)(π΅βπΎ))))) |
190 | | simpl 484 |
. . . . . . . . . . . 12
β’ (((π β§ π < (π΅βπΎ)) β§ Β¬ π β€ (π΄βπΎ)) β (π β§ π < (π΅βπΎ))) |
191 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ π β€ (π΄βπΎ)) β Β¬ π β€ (π΄βπΎ)) |
192 | 49 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ π β€ (π΄βπΎ)) β (π΄βπΎ) β β) |
193 | 6 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ π β€ (π΄βπΎ)) β π β β) |
194 | 192, 193 | ltnled 11310 |
. . . . . . . . . . . . . 14
β’ ((π β§ Β¬ π β€ (π΄βπΎ)) β ((π΄βπΎ) < π β Β¬ π β€ (π΄βπΎ))) |
195 | 191, 194 | mpbird 257 |
. . . . . . . . . . . . 13
β’ ((π β§ Β¬ π β€ (π΄βπΎ)) β (π΄βπΎ) < π) |
196 | 195 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π < (π΅βπΎ)) β§ Β¬ π β€ (π΄βπΎ)) β (π΄βπΎ) < π) |
197 | 49 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π΄βπΎ) < π) β (π΄βπΎ) β β) |
198 | 6 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π΄βπΎ) < π) β π β β) |
199 | | volico 44314 |
. . . . . . . . . . . . . . . 16
β’ (((π΄βπΎ) β β β§ π β β) β (volβ((π΄βπΎ)[,)π)) = if((π΄βπΎ) < π, (π β (π΄βπΎ)), 0)) |
200 | 197, 198,
199 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π΄βπΎ) < π) β (volβ((π΄βπΎ)[,)π)) = if((π΄βπΎ) < π, (π β (π΄βπΎ)), 0)) |
201 | | iftrue 4496 |
. . . . . . . . . . . . . . . 16
β’ ((π΄βπΎ) < π β if((π΄βπΎ) < π, (π β (π΄βπΎ)), 0) = (π β (π΄βπΎ))) |
202 | 201 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π΄βπΎ) < π) β if((π΄βπΎ) < π, (π β (π΄βπΎ)), 0) = (π β (π΄βπΎ))) |
203 | 200, 202 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π β§ (π΄βπΎ) < π) β (volβ((π΄βπΎ)[,)π)) = (π β (π΄βπΎ))) |
204 | 203 | adantlr 714 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β (volβ((π΄βπΎ)[,)π)) = (π β (π΄βπΎ))) |
205 | 6 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π < (π΅βπΎ)) β π β β) |
206 | 77 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π < (π΅βπΎ)) β (π΅βπΎ) β β) |
207 | | volico 44314 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ (π΅βπΎ) β β) β (volβ(π[,)(π΅βπΎ))) = if(π < (π΅βπΎ), ((π΅βπΎ) β π), 0)) |
208 | 205, 206,
207 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΅βπΎ)) β (volβ(π[,)(π΅βπΎ))) = if(π < (π΅βπΎ), ((π΅βπΎ) β π), 0)) |
209 | | iftrue 4496 |
. . . . . . . . . . . . . . . 16
β’ (π < (π΅βπΎ) β if(π < (π΅βπΎ), ((π΅βπΎ) β π), 0) = ((π΅βπΎ) β π)) |
210 | 209 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π < (π΅βπΎ)) β if(π < (π΅βπΎ), ((π΅βπΎ) β π), 0) = ((π΅βπΎ) β π)) |
211 | 208, 210 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ ((π β§ π < (π΅βπΎ)) β (volβ(π[,)(π΅βπΎ))) = ((π΅βπΎ) β π)) |
212 | 211 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β (volβ(π[,)(π΅βπΎ))) = ((π΅βπΎ) β π)) |
213 | 204, 212 | oveq12d 7379 |
. . . . . . . . . . . 12
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β ((volβ((π΄βπΎ)[,)π)) + (volβ(π[,)(π΅βπΎ)))) = ((π β (π΄βπΎ)) + ((π΅βπΎ) β π))) |
214 | 190, 196,
213 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π < (π΅βπΎ)) β§ Β¬ π β€ (π΄βπΎ)) β ((volβ((π΄βπΎ)[,)π)) + (volβ(π[,)(π΅βπΎ)))) = ((π β (π΄βπΎ)) + ((π΅βπΎ) β π))) |
215 | 197 | adantlr 714 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β (π΄βπΎ) β β) |
216 | 205 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β π β β) |
217 | 206 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β (π΅βπΎ) β β) |
218 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β (π΄βπΎ) < π) |
219 | | simplr 768 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β π < (π΅βπΎ)) |
220 | 215, 216,
217, 218, 219 | lttrd 11324 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β (π΄βπΎ) < (π΅βπΎ)) |
221 | 220 | iftrued 4498 |
. . . . . . . . . . . . . 14
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β if((π΄βπΎ) < (π΅βπΎ), ((π΅βπΎ) β (π΄βπΎ)), 0) = ((π΅βπΎ) β (π΄βπΎ))) |
222 | 221 | eqcomd 2739 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β ((π΅βπΎ) β (π΄βπΎ)) = if((π΄βπΎ) < (π΅βπΎ), ((π΅βπΎ) β (π΄βπΎ)), 0)) |
223 | 6, 49 | resubcld 11591 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π β (π΄βπΎ)) β β) |
224 | 223 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ (π β (π β (π΄βπΎ)) β β) |
225 | 77, 6 | resubcld 11591 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((π΅βπΎ) β π) β β) |
226 | 225 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π΅βπΎ) β π) β β) |
227 | 224, 226 | addcomd 11365 |
. . . . . . . . . . . . . . 15
β’ (π β ((π β (π΄βπΎ)) + ((π΅βπΎ) β π)) = (((π΅βπΎ) β π) + (π β (π΄βπΎ)))) |
228 | 77 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΅βπΎ) β β) |
229 | 6 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
230 | 49 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ (π β (π΄βπΎ) β β) |
231 | 228, 229,
230 | npncand 11544 |
. . . . . . . . . . . . . . 15
β’ (π β (((π΅βπΎ) β π) + (π β (π΄βπΎ))) = ((π΅βπΎ) β (π΄βπΎ))) |
232 | 227, 231 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (π β ((π β (π΄βπΎ)) + ((π΅βπΎ) β π)) = ((π΅βπΎ) β (π΄βπΎ))) |
233 | 232 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β ((π β (π΄βπΎ)) + ((π΅βπΎ) β π)) = ((π΅βπΎ) β (π΄βπΎ))) |
234 | | volico 44314 |
. . . . . . . . . . . . . 14
β’ (((π΄βπΎ) β β β§ (π΅βπΎ) β β) β (volβ((π΄βπΎ)[,)(π΅βπΎ))) = if((π΄βπΎ) < (π΅βπΎ), ((π΅βπΎ) β (π΄βπΎ)), 0)) |
235 | 215, 217,
234 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β (volβ((π΄βπΎ)[,)(π΅βπΎ))) = if((π΄βπΎ) < (π΅βπΎ), ((π΅βπΎ) β (π΄βπΎ)), 0)) |
236 | 222, 233,
235 | 3eqtr4d 2783 |
. . . . . . . . . . . 12
β’ (((π β§ π < (π΅βπΎ)) β§ (π΄βπΎ) < π) β ((π β (π΄βπΎ)) + ((π΅βπΎ) β π)) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
237 | 190, 196,
236 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π < (π΅βπΎ)) β§ Β¬ π β€ (π΄βπΎ)) β ((π β (π΄βπΎ)) + ((π΅βπΎ) β π)) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
238 | 189, 214,
237 | 3eqtrd 2777 |
. . . . . . . . . 10
β’ (((π β§ π < (π΅βπΎ)) β§ Β¬ π β€ (π΄βπΎ)) β ((volβ((π΄βπΎ)[,)π)) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
239 | 186, 238 | pm2.61dan 812 |
. . . . . . . . 9
β’ ((π β§ π < (π΅βπΎ)) β ((volβ((π΄βπΎ)[,)π)) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
240 | 163, 168,
239 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β ((volβ((π΄βπΎ)[,)π)) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
241 | 162, 240 | eqtrd 2773 |
. . . . . . 7
β’ ((π β§ Β¬ (π΅βπΎ) β€ π) β ((volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
242 | 157, 241 | pm2.61dan 812 |
. . . . . 6
β’ (π β ((volβ((π΄βπΎ)[,)if((π΅βπΎ) β€ π, (π΅βπΎ), π))) + (volβ(if(π β€ (π΄βπΎ), (π΄βπΎ), π)[,)(π΅βπΎ)))) = (volβ((π΄βπΎ)[,)(π΅βπΎ)))) |
243 | 115, 242 | eqtr2d 2774 |
. . . . 5
β’ (π β (volβ((π΄βπΎ)[,)(π΅βπΎ))) = ((volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) + (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))))) |
244 | 243 | oveq2d 7377 |
. . . 4
β’ (π β (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπΎ)[,)(π΅βπΎ)))) = (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· ((volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) + (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ)))))) |
245 | 32, 96 | fprodcl 15843 |
. . . . 5
β’ (π β βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) β β) |
246 | 245, 53, 80 | adddid 11187 |
. . . 4
β’ (π β (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· ((volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ))) + (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))))) = ((βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ)))) + (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ)))))) |
247 | 103, 244,
246 | 3eqtrrd 2778 |
. . 3
β’ (π β ((βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπΎ)[,)(((πβπ)βπ΅)βπΎ)))) + (βπ β (π β {πΎ})(volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((((πβπ)βπ΄)βπΎ)[,)(π΅βπΎ))))) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
248 | 20, 93, 247 | 3eqtrd 2777 |
. 2
β’ (π β ((π΄(πΏβπ)((πβπ)βπ΅)) + (((πβπ)βπ΄)(πΏβπ)π΅)) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
249 | 2, 3, 17, 4, 7 | hoidmvn0val 44915 |
. . 3
β’ (π β (π΄(πΏβπ)π΅) = βπ β π (volβ((π΄βπ)[,)(π΅βπ)))) |
250 | 249 | eqcomd 2739 |
. 2
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = (π΄(πΏβπ)π΅)) |
251 | 15, 248, 250 | 3eqtrrd 2778 |
1
β’ (π β (π΄(πΏβπ)π΅) = ((π΄(πΏβπ)((πβπ)βπ΅)) +π (((πβπ)βπ΄)(πΏβπ)π΅))) |