Step | Hyp | Ref
| Expression |
1 | | hoidmv1lelem2.a |
. . . . . 6
β’ (π β π΄ β β) |
2 | | hoidmv1lelem2.b |
. . . . . 6
β’ (π β π΅ β β) |
3 | | hoidmv1lelem2.m |
. . . . . . . 8
β’ π = if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) |
4 | 3 | a1i 11 |
. . . . . . 7
β’ (π β π = if((π·βπΎ) β€ π΅, (π·βπΎ), π΅)) |
5 | | hoidmv1lelem2.d |
. . . . . . . . 9
β’ (π β π·:ββΆβ) |
6 | | hoidmv1lelem2.k |
. . . . . . . . 9
β’ (π β πΎ β β) |
7 | 5, 6 | ffvelcdmd 7042 |
. . . . . . . 8
β’ (π β (π·βπΎ) β β) |
8 | 7, 2 | ifcld 4538 |
. . . . . . 7
β’ (π β if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β β) |
9 | 4, 8 | eqeltrd 2833 |
. . . . . 6
β’ (π β π β β) |
10 | | hoidmv1lelem2.c |
. . . . . . . . . . 11
β’ (π β πΆ:ββΆβ) |
11 | 10, 6 | ffvelcdmd 7042 |
. . . . . . . . . 10
β’ (π β (πΆβπΎ) β β) |
12 | 7 | rexrd 11215 |
. . . . . . . . . 10
β’ (π β (π·βπΎ) β
β*) |
13 | | icossre 13356 |
. . . . . . . . . 10
β’ (((πΆβπΎ) β β β§ (π·βπΎ) β β*) β ((πΆβπΎ)[,)(π·βπΎ)) β β) |
14 | 11, 12, 13 | syl2anc 585 |
. . . . . . . . 9
β’ (π β ((πΆβπΎ)[,)(π·βπΎ)) β β) |
15 | | hoidmv1lelem2.s |
. . . . . . . . 9
β’ (π β π β ((πΆβπΎ)[,)(π·βπΎ))) |
16 | 14, 15 | sseldd 3949 |
. . . . . . . 8
β’ (π β π β β) |
17 | | hoidmv1lelem2.g |
. . . . . . . 8
β’ (π β π΄ β€ π) |
18 | 11 | rexrd 11215 |
. . . . . . . . . . . 12
β’ (π β (πΆβπΎ) β
β*) |
19 | | icoltub 43848 |
. . . . . . . . . . . 12
β’ (((πΆβπΎ) β β* β§ (π·βπΎ) β β* β§ π β ((πΆβπΎ)[,)(π·βπΎ))) β π < (π·βπΎ)) |
20 | 18, 12, 15, 19 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (π β π < (π·βπΎ)) |
21 | 16, 7, 20 | ltled 11313 |
. . . . . . . . . 10
β’ (π β π β€ (π·βπΎ)) |
22 | | hoidmv1lelem2.l |
. . . . . . . . . . 11
β’ (π β π < π΅) |
23 | 16, 2, 22 | ltled 11313 |
. . . . . . . . . 10
β’ (π β π β€ π΅) |
24 | 21, 23 | jca 513 |
. . . . . . . . 9
β’ (π β (π β€ (π·βπΎ) β§ π β€ π΅)) |
25 | | lemin 13122 |
. . . . . . . . . 10
β’ ((π β β β§ (π·βπΎ) β β β§ π΅ β β) β (π β€ if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β (π β€ (π·βπΎ) β§ π β€ π΅))) |
26 | 16, 7, 2, 25 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π β€ if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β (π β€ (π·βπΎ) β§ π β€ π΅))) |
27 | 24, 26 | mpbird 257 |
. . . . . . . 8
β’ (π β π β€ if((π·βπΎ) β€ π΅, (π·βπΎ), π΅)) |
28 | 1, 16, 8, 17, 27 | letrd 11322 |
. . . . . . 7
β’ (π β π΄ β€ if((π·βπΎ) β€ π΅, (π·βπΎ), π΅)) |
29 | 4 | eqcomd 2738 |
. . . . . . 7
β’ (π β if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) = π) |
30 | 28, 29 | breqtrd 5137 |
. . . . . 6
β’ (π β π΄ β€ π) |
31 | | min2 13120 |
. . . . . . . 8
β’ (((π·βπΎ) β β β§ π΅ β β) β if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β€ π΅) |
32 | 7, 2, 31 | syl2anc 585 |
. . . . . . 7
β’ (π β if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β€ π΅) |
33 | 4, 32 | eqbrtrd 5133 |
. . . . . 6
β’ (π β π β€ π΅) |
34 | 1, 2, 9, 30, 33 | eliccd 43844 |
. . . . 5
β’ (π β π β (π΄[,]π΅)) |
35 | 9 | recnd 11193 |
. . . . . . . 8
β’ (π β π β β) |
36 | 16 | recnd 11193 |
. . . . . . . 8
β’ (π β π β β) |
37 | 1 | recnd 11193 |
. . . . . . . 8
β’ (π β π΄ β β) |
38 | 35, 36, 37 | npncand 11546 |
. . . . . . 7
β’ (π β ((π β π) + (π β π΄)) = (π β π΄)) |
39 | 38 | eqcomd 2738 |
. . . . . 6
β’ (π β (π β π΄) = ((π β π) + (π β π΄))) |
40 | 9, 16 | resubcld 11593 |
. . . . . . . 8
β’ (π β (π β π) β β) |
41 | 16, 1 | resubcld 11593 |
. . . . . . . 8
β’ (π β (π β π΄) β β) |
42 | 40, 41 | readdcld 11194 |
. . . . . . 7
β’ (π β ((π β π) + (π β π΄)) β β) |
43 | | nnex 12169 |
. . . . . . . . . . . . 13
β’ β
β V |
44 | 43 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β β β
V) |
45 | | volf 24931 |
. . . . . . . . . . . . . . 15
β’ vol:dom
volβΆ(0[,]+β) |
46 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β vol:dom
volβΆ(0[,]+β)) |
47 | 10 | ffvelcdmda 7041 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΆβπ) β β) |
48 | 5 | ffvelcdmda 7041 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (π·βπ) β β) |
49 | 16 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β π β β) |
50 | 48, 49 | ifcld 4538 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β if((π·βπ) β€ π, (π·βπ), π) β β) |
51 | 50 | rexrd 11215 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β if((π·βπ) β€ π, (π·βπ), π) β
β*) |
52 | | icombl 24966 |
. . . . . . . . . . . . . . 15
β’ (((πΆβπ) β β β§ if((π·βπ) β€ π, (π·βπ), π) β β*) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol) |
53 | 47, 51, 52 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol) |
54 | 46, 53 | ffvelcdmd 7042 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β (0[,]+β)) |
55 | | eqid 2732 |
. . . . . . . . . . . . 13
β’ (π β β β¦
(volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) = (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) |
56 | 54, 55 | fmptd 7068 |
. . . . . . . . . . . 12
β’ (π β (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))):ββΆ(0[,]+β)) |
57 | 44, 56 | sge0xrcl 44728 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β
β*) |
58 | | pnfxr 11219 |
. . . . . . . . . . . 12
β’ +β
β β* |
59 | 58 | a1i 11 |
. . . . . . . . . . 11
β’ (π β +β β
β*) |
60 | | hoidmv1lelem2.r |
. . . . . . . . . . . . 13
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)(π·βπ))))) β β) |
61 | 60 | rexrd 11215 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)(π·βπ))))) β
β*) |
62 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²ππ |
63 | 48 | rexrd 11215 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (π·βπ) β
β*) |
64 | | icombl 24966 |
. . . . . . . . . . . . . . 15
β’ (((πΆβπ) β β β§ (π·βπ) β β*) β ((πΆβπ)[,)(π·βπ)) β dom vol) |
65 | 47, 63, 64 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πΆβπ)[,)(π·βπ)) β dom vol) |
66 | 46, 65 | ffvelcdmd 7042 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (volβ((πΆβπ)[,)(π·βπ))) β (0[,]+β)) |
67 | 47 | rexrd 11215 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΆβπ) β
β*) |
68 | 47 | leidd 11731 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πΆβπ) β€ (πΆβπ)) |
69 | | min1 13119 |
. . . . . . . . . . . . . . . 16
β’ (((π·βπ) β β β§ π β β) β if((π·βπ) β€ π, (π·βπ), π) β€ (π·βπ)) |
70 | 48, 49, 69 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β if((π·βπ) β€ π, (π·βπ), π) β€ (π·βπ)) |
71 | | icossico 13345 |
. . . . . . . . . . . . . . 15
β’ ((((πΆβπ) β β* β§ (π·βπ) β β*) β§ ((πΆβπ) β€ (πΆβπ) β§ if((π·βπ) β€ π, (π·βπ), π) β€ (π·βπ))) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β ((πΆβπ)[,)(π·βπ))) |
72 | 67, 63, 68, 70, 71 | syl22anc 838 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β ((πΆβπ)[,)(π·βπ))) |
73 | | volss 24935 |
. . . . . . . . . . . . . 14
β’ ((((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol β§ ((πΆβπ)[,)(π·βπ)) β dom vol β§ ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β ((πΆβπ)[,)(π·βπ))) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β€ (volβ((πΆβπ)[,)(π·βπ)))) |
74 | 53, 65, 72, 73 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β€ (volβ((πΆβπ)[,)(π·βπ)))) |
75 | 62, 44, 54, 66, 74 | sge0lempt 44753 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)(π·βπ)))))) |
76 | 60 | ltpnfd 13052 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)(π·βπ))))) < +β) |
77 | 57, 61, 59, 75, 76 | xrlelttrd 13090 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) < +β) |
78 | 57, 59, 77 | xrltned 43694 |
. . . . . . . . . 10
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β +β) |
79 | 78 | neneqd 2945 |
. . . . . . . . 9
β’ (π β Β¬
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) = +β) |
80 | 44, 56 | sge0repnf 44729 |
. . . . . . . . 9
β’ (π β
((Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β β Β¬
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) = +β)) |
81 | 79, 80 | mpbird 257 |
. . . . . . . 8
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β) |
82 | 40, 81 | readdcld 11194 |
. . . . . . 7
β’ (π β ((π β π) +
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) β β) |
83 | 9 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β β) |
84 | 48, 83 | ifcld 4538 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β if((π·βπ) β€ π, (π·βπ), π) β β) |
85 | 84 | rexrd 11215 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β if((π·βπ) β€ π, (π·βπ), π) β
β*) |
86 | | icombl 24966 |
. . . . . . . . . . . . . 14
β’ (((πΆβπ) β β β§ if((π·βπ) β€ π, (π·βπ), π) β β*) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol) |
87 | 47, 85, 86 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol) |
88 | 46, 87 | ffvelcdmd 7042 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β (0[,]+β)) |
89 | | eqid 2732 |
. . . . . . . . . . . 12
β’ (π β β β¦
(volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) = (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) |
90 | 88, 89 | fmptd 7068 |
. . . . . . . . . . 11
β’ (π β (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))):ββΆ(0[,]+β)) |
91 | 44, 90 | sge0xrcl 44728 |
. . . . . . . . . 10
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β
β*) |
92 | | min1 13119 |
. . . . . . . . . . . . . . 15
β’ (((π·βπ) β β β§ π β β) β if((π·βπ) β€ π, (π·βπ), π) β€ (π·βπ)) |
93 | 48, 83, 92 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β if((π·βπ) β€ π, (π·βπ), π) β€ (π·βπ)) |
94 | | icossico 13345 |
. . . . . . . . . . . . . 14
β’ ((((πΆβπ) β β* β§ (π·βπ) β β*) β§ ((πΆβπ) β€ (πΆβπ) β§ if((π·βπ) β€ π, (π·βπ), π) β€ (π·βπ))) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β ((πΆβπ)[,)(π·βπ))) |
95 | 67, 63, 68, 93, 94 | syl22anc 838 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β ((πΆβπ)[,)(π·βπ))) |
96 | | volss 24935 |
. . . . . . . . . . . . 13
β’ ((((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol β§ ((πΆβπ)[,)(π·βπ)) β dom vol β§ ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β ((πΆβπ)[,)(π·βπ))) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β€ (volβ((πΆβπ)[,)(π·βπ)))) |
97 | 87, 65, 95, 96 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β€ (volβ((πΆβπ)[,)(π·βπ)))) |
98 | 62, 44, 88, 66, 97 | sge0lempt 44753 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)(π·βπ)))))) |
99 | 91, 61, 59, 98, 76 | xrlelttrd 13090 |
. . . . . . . . . 10
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) < +β) |
100 | 91, 59, 99 | xrltned 43694 |
. . . . . . . . 9
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β +β) |
101 | 100 | neneqd 2945 |
. . . . . . . 8
β’ (π β Β¬
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) = +β) |
102 | 44, 90 | sge0repnf 44729 |
. . . . . . . 8
β’ (π β
((Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β β Β¬
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) = +β)) |
103 | 101, 102 | mpbird 257 |
. . . . . . 7
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β) |
104 | | hoidmv1lelem2.e |
. . . . . . . . . . 11
β’ (π β π β π) |
105 | | hoidmv1lelem2.u |
. . . . . . . . . . 11
β’ π = {π§ β (π΄[,]π΅) β£ (π§ β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))))} |
106 | 104, 105 | eleqtrdi 2843 |
. . . . . . . . . 10
β’ (π β π β {π§ β (π΄[,]π΅) β£ (π§ β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))))}) |
107 | | oveq1 7370 |
. . . . . . . . . . . 12
β’ (π§ = π β (π§ β π΄) = (π β π΄)) |
108 | | simpl 484 |
. . . . . . . . . . . . . . . . . 18
β’ ((π§ = π β§ π β β) β π§ = π) |
109 | 108 | breq2d 5123 |
. . . . . . . . . . . . . . . . 17
β’ ((π§ = π β§ π β β) β ((π·βπ) β€ π§ β (π·βπ) β€ π)) |
110 | 109, 108 | ifbieq2d 4518 |
. . . . . . . . . . . . . . . 16
β’ ((π§ = π β§ π β β) β if((π·βπ) β€ π§, (π·βπ), π§) = if((π·βπ) β€ π, (π·βπ), π)) |
111 | 110 | oveq2d 7379 |
. . . . . . . . . . . . . . 15
β’ ((π§ = π β§ π β β) β ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)) = ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) |
112 | 111 | fveq2d 6852 |
. . . . . . . . . . . . . 14
β’ ((π§ = π β§ π β β) β (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§))) = (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) |
113 | 112 | mpteq2dva 5211 |
. . . . . . . . . . . . 13
β’ (π§ = π β (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))) = (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) |
114 | 113 | fveq2d 6852 |
. . . . . . . . . . . 12
β’ (π§ = π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§))))) =
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
115 | 107, 114 | breq12d 5124 |
. . . . . . . . . . 11
β’ (π§ = π β ((π§ β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§))))) β (π β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
116 | 115 | elrab 3649 |
. . . . . . . . . 10
β’ (π β {π§ β (π΄[,]π΅) β£ (π§ β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))))} β (π β (π΄[,]π΅) β§ (π β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
117 | 106, 116 | sylib 217 |
. . . . . . . . 9
β’ (π β (π β (π΄[,]π΅) β§ (π β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
118 | 117 | simprd 497 |
. . . . . . . 8
β’ (π β (π β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
119 | 41, 81, 40, 118 | leadd2dd 11780 |
. . . . . . 7
β’ (π β ((π β π) + (π β π΄)) β€ ((π β π) +
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
120 | | difssd 4098 |
. . . . . . . . . 10
β’ (π β (β β {πΎ}) β
β) |
121 | 62, 44, 54, 81, 120 | sge0ssrempt 44748 |
. . . . . . . . 9
β’ (π β
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β) |
122 | | difexg 5290 |
. . . . . . . . . . . . . . 15
β’ (β
β V β (β β {πΎ}) β V) |
123 | 43, 122 | ax-mp 5 |
. . . . . . . . . . . . . 14
β’ (β
β {πΎ}) β
V |
124 | 123 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β (β β {πΎ}) β V) |
125 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β β {πΎ})) β vol:dom
volβΆ(0[,]+β)) |
126 | | simpl 484 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β β {πΎ})) β π) |
127 | | eldifi 4092 |
. . . . . . . . . . . . . . . . 17
β’ (π β (β β {πΎ}) β π β β) |
128 | 127 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (β β {πΎ})) β π β β) |
129 | 126, 128,
47 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β β {πΎ})) β (πΆβπ) β β) |
130 | 128, 85 | syldan 592 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (β β {πΎ})) β if((π·βπ) β€ π, (π·βπ), π) β
β*) |
131 | 129, 130,
86 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (β β {πΎ})) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol) |
132 | 125, 131 | ffvelcdmd 7042 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (β β {πΎ})) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β (0[,]+β)) |
133 | 62, 124, 132 | sge0xrclmpt 44771 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β
β*) |
134 | 44, 88, 120 | sge0lessmpt 44742 |
. . . . . . . . . . . . 13
β’ (π β
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
135 | 133, 91, 59, 134, 99 | xrlelttrd 13090 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) < +β) |
136 | 133, 59, 135 | xrltned 43694 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β +β) |
137 | 136 | neneqd 2945 |
. . . . . . . . . 10
β’ (π β Β¬
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) = +β) |
138 | 62, 124, 132 | sge0repnfmpt 44782 |
. . . . . . . . . 10
β’ (π β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β β Β¬
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) = +β)) |
139 | 137, 138 | mpbird 257 |
. . . . . . . . 9
β’ (π β
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β) |
140 | 9, 11 | resubcld 11593 |
. . . . . . . . 9
β’ (π β (π β (πΆβπΎ)) β β) |
141 | 128, 54 | syldan 592 |
. . . . . . . . . 10
β’ ((π β§ π β (β β {πΎ})) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β (0[,]+β)) |
142 | 128, 53 | syldan 592 |
. . . . . . . . . . 11
β’ ((π β§ π β (β β {πΎ})) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol) |
143 | 128, 67 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β β {πΎ})) β (πΆβπ) β
β*) |
144 | 128, 68 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β β {πΎ})) β (πΆβπ) β€ (πΆβπ)) |
145 | | iftrue 4498 |
. . . . . . . . . . . . . . . 16
β’ ((π·βπ) β€ π β if((π·βπ) β€ π, (π·βπ), π) = (π·βπ)) |
146 | 145 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β if((π·βπ) β€ π, (π·βπ), π) = (π·βπ)) |
147 | 48 | leidd 11731 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π·βπ) β€ (π·βπ)) |
148 | 147 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β (π·βπ) β€ (π·βπ)) |
149 | 48 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β (π·βπ) β β) |
150 | 83 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β π β β) |
151 | 49 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β π β β) |
152 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β (π·βπ) β€ π) |
153 | 20, 22 | jca 513 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π < (π·βπΎ) β§ π < π΅)) |
154 | | ltmin 13124 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ (π·βπΎ) β β β§ π΅ β β) β (π < if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β (π < (π·βπΎ) β§ π < π΅))) |
155 | 16, 7, 2, 154 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π < if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β (π < (π·βπΎ) β§ π < π΅))) |
156 | 153, 155 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β π < if((π·βπΎ) β€ π΅, (π·βπΎ), π΅)) |
157 | 156, 29 | breqtrd 5137 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π < π) |
158 | 157 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β π < π) |
159 | 149, 151,
150, 152, 158 | lelttrd 11323 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β (π·βπ) < π) |
160 | 149, 150,
159 | ltled 11313 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β (π·βπ) β€ π) |
161 | 148, 160 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β ((π·βπ) β€ (π·βπ) β§ (π·βπ) β€ π)) |
162 | | lemin 13122 |
. . . . . . . . . . . . . . . . 17
β’ (((π·βπ) β β β§ (π·βπ) β β β§ π β β) β ((π·βπ) β€ if((π·βπ) β€ π, (π·βπ), π) β ((π·βπ) β€ (π·βπ) β§ (π·βπ) β€ π))) |
163 | 149, 149,
150, 162 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β ((π·βπ) β€ if((π·βπ) β€ π, (π·βπ), π) β ((π·βπ) β€ (π·βπ) β§ (π·βπ) β€ π))) |
164 | 161, 163 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β (π·βπ) β€ if((π·βπ) β€ π, (π·βπ), π)) |
165 | 146, 164 | eqbrtrd 5133 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ (π·βπ) β€ π) β if((π·βπ) β€ π, (π·βπ), π) β€ if((π·βπ) β€ π, (π·βπ), π)) |
166 | | iffalse 4501 |
. . . . . . . . . . . . . . . 16
β’ (Β¬
(π·βπ) β€ π β if((π·βπ) β€ π, (π·βπ), π) = π) |
167 | 166 | adantl 483 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β if((π·βπ) β€ π, (π·βπ), π) = π) |
168 | 49 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β π β β) |
169 | 84 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β if((π·βπ) β€ π, (π·βπ), π) β β) |
170 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β Β¬ (π·βπ) β€ π) |
171 | 48 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β (π·βπ) β β) |
172 | 168, 171 | ltnled 11312 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β (π < (π·βπ) β Β¬ (π·βπ) β€ π)) |
173 | 170, 172 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β π < (π·βπ)) |
174 | 157 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β π < π) |
175 | 173, 174 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β (π < (π·βπ) β§ π < π)) |
176 | 83 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β π β β) |
177 | | ltmin 13124 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ (π·βπ) β β β§ π β β) β (π < if((π·βπ) β€ π, (π·βπ), π) β (π < (π·βπ) β§ π < π))) |
178 | 168, 171,
176, 177 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β (π < if((π·βπ) β€ π, (π·βπ), π) β (π < (π·βπ) β§ π < π))) |
179 | 175, 178 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β π < if((π·βπ) β€ π, (π·βπ), π)) |
180 | 168, 169,
179 | ltled 11313 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β π β€ if((π·βπ) β€ π, (π·βπ), π)) |
181 | 167, 180 | eqbrtrd 5133 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β) β§ Β¬ (π·βπ) β€ π) β if((π·βπ) β€ π, (π·βπ), π) β€ if((π·βπ) β€ π, (π·βπ), π)) |
182 | 165, 181 | pm2.61dan 812 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β if((π·βπ) β€ π, (π·βπ), π) β€ if((π·βπ) β€ π, (π·βπ), π)) |
183 | 128, 182 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ π β (β β {πΎ})) β if((π·βπ) β€ π, (π·βπ), π) β€ if((π·βπ) β€ π, (π·βπ), π)) |
184 | | icossico 13345 |
. . . . . . . . . . . 12
β’ ((((πΆβπ) β β* β§ if((π·βπ) β€ π, (π·βπ), π) β β*) β§ ((πΆβπ) β€ (πΆβπ) β§ if((π·βπ) β€ π, (π·βπ), π) β€ if((π·βπ) β€ π, (π·βπ), π))) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) |
185 | 143, 130,
144, 183, 184 | syl22anc 838 |
. . . . . . . . . . 11
β’ ((π β§ π β (β β {πΎ})) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) |
186 | | volss 24935 |
. . . . . . . . . . 11
β’ ((((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol β§ ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β dom vol β§ ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β€ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) |
187 | 142, 131,
185, 186 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π β (β β {πΎ})) β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) β€ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) |
188 | 62, 124, 141, 132, 187 | sge0lempt 44753 |
. . . . . . . . 9
β’ (π β
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β€
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
189 | 121, 139,
140, 188 | leadd2dd 11780 |
. . . . . . . 8
β’ (π β ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) β€ ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
190 | | difsnid 4776 |
. . . . . . . . . . . . . . . 16
β’ (πΎ β β β ((β
β {πΎ}) βͺ {πΎ}) = β) |
191 | 6, 190 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β ((β β {πΎ}) βͺ {πΎ}) = β) |
192 | 191 | eqcomd 2738 |
. . . . . . . . . . . . . 14
β’ (π β β = ((β
β {πΎ}) βͺ {πΎ})) |
193 | 192 | mpteq1d 5206 |
. . . . . . . . . . . . 13
β’ (π β (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) = (π β ((β β {πΎ}) βͺ {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) |
194 | 193 | fveq2d 6852 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) =
(Ξ£^β(π β ((β β {πΎ}) βͺ {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
195 | | neldifsnd 4759 |
. . . . . . . . . . . . 13
β’ (π β Β¬ πΎ β (β β {πΎ})) |
196 | | fveq2 6848 |
. . . . . . . . . . . . . . 15
β’ (π = πΎ β (πΆβπ) = (πΆβπΎ)) |
197 | | fveq2 6848 |
. . . . . . . . . . . . . . . . 17
β’ (π = πΎ β (π·βπ) = (π·βπΎ)) |
198 | 197 | breq1d 5121 |
. . . . . . . . . . . . . . . 16
β’ (π = πΎ β ((π·βπ) β€ π β (π·βπΎ) β€ π)) |
199 | 198, 197 | ifbieq1d 4516 |
. . . . . . . . . . . . . . 15
β’ (π = πΎ β if((π·βπ) β€ π, (π·βπ), π) = if((π·βπΎ) β€ π, (π·βπΎ), π)) |
200 | 196, 199 | oveq12d 7381 |
. . . . . . . . . . . . . 14
β’ (π = πΎ β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) = ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) |
201 | 200 | fveq2d 6852 |
. . . . . . . . . . . . 13
β’ (π = πΎ β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) = (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) |
202 | 45 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β vol:dom
volβΆ(0[,]+β)) |
203 | 7, 16 | ifcld 4538 |
. . . . . . . . . . . . . . . 16
β’ (π β if((π·βπΎ) β€ π, (π·βπΎ), π) β β) |
204 | 203 | rexrd 11215 |
. . . . . . . . . . . . . . 15
β’ (π β if((π·βπΎ) β€ π, (π·βπΎ), π) β
β*) |
205 | | icombl 24966 |
. . . . . . . . . . . . . . 15
β’ (((πΆβπΎ) β β β§ if((π·βπΎ) β€ π, (π·βπΎ), π) β β*) β ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)) β dom vol) |
206 | 11, 204, 205 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)) β dom vol) |
207 | 202, 206 | ffvelcdmd 7042 |
. . . . . . . . . . . . 13
β’ (π β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) β (0[,]+β)) |
208 | 62, 124, 6, 195, 141, 201, 207 | sge0splitsn 44784 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β ((β β {πΎ}) βͺ {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) =
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) +π
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))))) |
209 | | volicore 44924 |
. . . . . . . . . . . . . . 15
β’ (((πΆβπΎ) β β β§ if((π·βπΎ) β€ π, (π·βπΎ), π) β β) β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) β β) |
210 | 11, 203, 209 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ (π β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) β β) |
211 | | rexadd 13162 |
. . . . . . . . . . . . . 14
β’
(((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β β§
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) β β) β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) +π
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) =
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))))) |
212 | 121, 210,
211 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) +π
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) =
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))))) |
213 | | volico 44326 |
. . . . . . . . . . . . . . . 16
β’ (((πΆβπΎ) β β β§ if((π·βπΎ) β€ π, (π·βπΎ), π) β β) β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) = if((πΆβπΎ) < if((π·βπΎ) β€ π, (π·βπΎ), π), (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)), 0)) |
214 | 11, 203, 213 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) = if((πΆβπΎ) < if((π·βπΎ) β€ π, (π·βπΎ), π), (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)), 0)) |
215 | 16, 7 | ltnled 11312 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π < (π·βπΎ) β Β¬ (π·βπΎ) β€ π)) |
216 | 20, 215 | mpbid 231 |
. . . . . . . . . . . . . . . . . 18
β’ (π β Β¬ (π·βπΎ) β€ π) |
217 | 216 | iffalsed 4503 |
. . . . . . . . . . . . . . . . 17
β’ (π β if((π·βπΎ) β€ π, (π·βπΎ), π) = π) |
218 | 217 | breq2d 5123 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΆβπΎ) < if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ) < π)) |
219 | 218 | ifbid 4515 |
. . . . . . . . . . . . . . 15
β’ (π β if((πΆβπΎ) < if((π·βπΎ) β€ π, (π·βπΎ), π), (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)), 0) = if((πΆβπΎ) < π, (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)), 0)) |
220 | 217 | oveq1d 7378 |
. . . . . . . . . . . . . . . . 17
β’ (π β (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)) = (π β (πΆβπΎ))) |
221 | 220 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (πΆβπΎ) < π) β (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)) = (π β (πΆβπΎ))) |
222 | 217, 204 | eqeltrrd 2834 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β
β*) |
223 | 222 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ Β¬ (πΆβπΎ) < π) β π β
β*) |
224 | 18 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ Β¬ (πΆβπΎ) < π) β (πΆβπΎ) β
β*) |
225 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ Β¬ (πΆβπΎ) < π) β Β¬ (πΆβπΎ) < π) |
226 | 16 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ Β¬ (πΆβπΎ) < π) β π β β) |
227 | 11 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ Β¬ (πΆβπΎ) < π) β (πΆβπΎ) β β) |
228 | 226, 227 | lenltd 11311 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ Β¬ (πΆβπΎ) < π) β (π β€ (πΆβπΎ) β Β¬ (πΆβπΎ) < π)) |
229 | 225, 228 | mpbird 257 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ Β¬ (πΆβπΎ) < π) β π β€ (πΆβπΎ)) |
230 | | icogelb 13326 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((πΆβπΎ) β β* β§ (π·βπΎ) β β* β§ π β ((πΆβπΎ)[,)(π·βπΎ))) β (πΆβπΎ) β€ π) |
231 | 18, 12, 15, 230 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΆβπΎ) β€ π) |
232 | 231 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ Β¬ (πΆβπΎ) < π) β (πΆβπΎ) β€ π) |
233 | 223, 224,
229, 232 | xrletrid 13085 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ (πΆβπΎ) < π) β π = (πΆβπΎ)) |
234 | 233 | oveq1d 7378 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ (πΆβπΎ) < π) β (π β (πΆβπΎ)) = ((πΆβπΎ) β (πΆβπΎ))) |
235 | 227 | recnd 11193 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ Β¬ (πΆβπΎ) < π) β (πΆβπΎ) β β) |
236 | 235 | subidd 11510 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ Β¬ (πΆβπΎ) < π) β ((πΆβπΎ) β (πΆβπΎ)) = 0) |
237 | 234, 236 | eqtr2d 2773 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ (πΆβπΎ) < π) β 0 = (π β (πΆβπΎ))) |
238 | 221, 237 | ifeqda 4528 |
. . . . . . . . . . . . . . 15
β’ (π β if((πΆβπΎ) < π, (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)), 0) = (π β (πΆβπΎ))) |
239 | 214, 219,
238 | 3eqtrd 2776 |
. . . . . . . . . . . . . 14
β’ (π β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) = (π β (πΆβπΎ))) |
240 | 239 | oveq2d 7379 |
. . . . . . . . . . . . 13
β’ (π β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) =
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (π β (πΆβπΎ)))) |
241 | 121 | recnd 11193 |
. . . . . . . . . . . . . 14
β’ (π β
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β) |
242 | 11 | recnd 11193 |
. . . . . . . . . . . . . . 15
β’ (π β (πΆβπΎ) β β) |
243 | 36, 242 | subcld 11522 |
. . . . . . . . . . . . . 14
β’ (π β (π β (πΆβπΎ)) β β) |
244 | 241, 243 | addcomd 11367 |
. . . . . . . . . . . . 13
β’ (π β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (π β (πΆβπΎ))) = ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
245 | 212, 240,
244 | 3eqtrd 2776 |
. . . . . . . . . . . 12
β’ (π β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) +π
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) = ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
246 | 194, 208,
245 | 3eqtrd 2776 |
. . . . . . . . . . 11
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) = ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
247 | 246 | oveq2d 7379 |
. . . . . . . . . 10
β’ (π β ((π β π) +
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) = ((π β π) + ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))))) |
248 | 40 | recnd 11193 |
. . . . . . . . . . . 12
β’ (π β (π β π) β β) |
249 | 248, 243,
241 | addassd 11187 |
. . . . . . . . . . 11
β’ (π β (((π β π) + (π β (πΆβπΎ))) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) = ((π β π) + ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))))) |
250 | 249 | eqcomd 2738 |
. . . . . . . . . 10
β’ (π β ((π β π) + ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) = (((π β π) + (π β (πΆβπΎ))) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
251 | 35, 36, 242 | npncand 11546 |
. . . . . . . . . . 11
β’ (π β ((π β π) + (π β (πΆβπΎ))) = (π β (πΆβπΎ))) |
252 | 251 | oveq1d 7378 |
. . . . . . . . . 10
β’ (π β (((π β π) + (π β (πΆβπΎ))) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) = ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
253 | 247, 250,
252 | 3eqtrd 2776 |
. . . . . . . . 9
β’ (π β ((π β π) +
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) = ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
254 | 192 | mpteq1d 5206 |
. . . . . . . . . . 11
β’ (π β (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) = (π β ((β β {πΎ}) βͺ {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) |
255 | 254 | fveq2d 6852 |
. . . . . . . . . 10
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) =
(Ξ£^β(π β ((β β {πΎ}) βͺ {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
256 | 197 | breq1d 5121 |
. . . . . . . . . . . . . 14
β’ (π = πΎ β ((π·βπ) β€ π β (π·βπΎ) β€ π)) |
257 | 256, 197 | ifbieq1d 4516 |
. . . . . . . . . . . . 13
β’ (π = πΎ β if((π·βπ) β€ π, (π·βπ), π) = if((π·βπΎ) β€ π, (π·βπΎ), π)) |
258 | 196, 257 | oveq12d 7381 |
. . . . . . . . . . . 12
β’ (π = πΎ β ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)) = ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) |
259 | 258 | fveq2d 6852 |
. . . . . . . . . . 11
β’ (π = πΎ β (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) = (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) |
260 | 7, 9 | ifcld 4538 |
. . . . . . . . . . . . . 14
β’ (π β if((π·βπΎ) β€ π, (π·βπΎ), π) β β) |
261 | 260 | rexrd 11215 |
. . . . . . . . . . . . 13
β’ (π β if((π·βπΎ) β€ π, (π·βπΎ), π) β
β*) |
262 | | icombl 24966 |
. . . . . . . . . . . . 13
β’ (((πΆβπΎ) β β β§ if((π·βπΎ) β€ π, (π·βπΎ), π) β β*) β ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)) β dom vol) |
263 | 11, 261, 262 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)) β dom vol) |
264 | 202, 263 | ffvelcdmd 7042 |
. . . . . . . . . . 11
β’ (π β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) β (0[,]+β)) |
265 | 62, 124, 6, 195, 132, 259, 264 | sge0splitsn 44784 |
. . . . . . . . . 10
β’ (π β
(Ξ£^β(π β ((β β {πΎ}) βͺ {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) =
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) +π
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))))) |
266 | | volicore 44924 |
. . . . . . . . . . . . 13
β’ (((πΆβπΎ) β β β§ if((π·βπΎ) β€ π, (π·βπΎ), π) β β) β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) β β) |
267 | 11, 260, 266 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) β β) |
268 | | rexadd 13162 |
. . . . . . . . . . . 12
β’
(((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β β§
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) β β) β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) +π
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) =
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))))) |
269 | 139, 267,
268 | syl2anc 585 |
. . . . . . . . . . 11
β’ (π β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) +π
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) =
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))))) |
270 | | volico 44326 |
. . . . . . . . . . . . . 14
β’ (((πΆβπΎ) β β β§ if((π·βπΎ) β€ π, (π·βπΎ), π) β β) β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) = if((πΆβπΎ) < if((π·βπΎ) β€ π, (π·βπΎ), π), (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)), 0)) |
271 | 11, 260, 270 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (π β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) = if((πΆβπΎ) < if((π·βπΎ) β€ π, (π·βπΎ), π), (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)), 0)) |
272 | 20, 157 | jca 513 |
. . . . . . . . . . . . . . . 16
β’ (π β (π < (π·βπΎ) β§ π < π)) |
273 | | ltmin 13124 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ (π·βπΎ) β β β§ π β β) β (π < if((π·βπΎ) β€ π, (π·βπΎ), π) β (π < (π·βπΎ) β§ π < π))) |
274 | 16, 7, 9, 273 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β (π < if((π·βπΎ) β€ π, (π·βπΎ), π) β (π < (π·βπΎ) β§ π < π))) |
275 | 272, 274 | mpbird 257 |
. . . . . . . . . . . . . . 15
β’ (π β π < if((π·βπΎ) β€ π, (π·βπΎ), π)) |
276 | 11, 16, 260, 231, 275 | lelttrd 11323 |
. . . . . . . . . . . . . 14
β’ (π β (πΆβπΎ) < if((π·βπΎ) β€ π, (π·βπΎ), π)) |
277 | 276 | iftrued 4500 |
. . . . . . . . . . . . 13
β’ (π β if((πΆβπΎ) < if((π·βπΎ) β€ π, (π·βπΎ), π), (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)), 0) = (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ))) |
278 | | iftrue 4498 |
. . . . . . . . . . . . . . . . 17
β’ ((π·βπΎ) β€ π β if((π·βπΎ) β€ π, (π·βπΎ), π) = (π·βπΎ)) |
279 | 278 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π·βπΎ) β€ π) β if((π·βπΎ) β€ π, (π·βπΎ), π) = (π·βπΎ)) |
280 | 12 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π·βπΎ) β€ π) β (π·βπΎ) β
β*) |
281 | 9 | rexrd 11215 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β
β*) |
282 | 281 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π·βπΎ) β€ π) β π β
β*) |
283 | | simpr 486 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π·βπΎ) β€ π) β (π·βπΎ) β€ π) |
284 | | min1 13119 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π·βπΎ) β β β§ π΅ β β) β if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β€ (π·βπΎ)) |
285 | 7, 2, 284 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β if((π·βπΎ) β€ π΅, (π·βπΎ), π΅) β€ (π·βπΎ)) |
286 | 4, 285 | eqbrtrd 5133 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β€ (π·βπΎ)) |
287 | 286 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π·βπΎ) β€ π) β π β€ (π·βπΎ)) |
288 | 280, 282,
283, 287 | xrletrid 13085 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π·βπΎ) β€ π) β (π·βπΎ) = π) |
289 | 279, 288 | eqtrd 2772 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π·βπΎ) β€ π) β if((π·βπΎ) β€ π, (π·βπΎ), π) = π) |
290 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ Β¬ (π·βπΎ) β€ π) β Β¬ (π·βπΎ) β€ π) |
291 | 290 | iffalsed 4503 |
. . . . . . . . . . . . . . 15
β’ ((π β§ Β¬ (π·βπΎ) β€ π) β if((π·βπΎ) β€ π, (π·βπΎ), π) = π) |
292 | 289, 291 | pm2.61dan 812 |
. . . . . . . . . . . . . 14
β’ (π β if((π·βπΎ) β€ π, (π·βπΎ), π) = π) |
293 | 292 | oveq1d 7378 |
. . . . . . . . . . . . 13
β’ (π β (if((π·βπΎ) β€ π, (π·βπΎ), π) β (πΆβπΎ)) = (π β (πΆβπΎ))) |
294 | 271, 277,
293 | 3eqtrd 2776 |
. . . . . . . . . . . 12
β’ (π β (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π))) = (π β (πΆβπΎ))) |
295 | 294 | oveq2d 7379 |
. . . . . . . . . . 11
β’ (π β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) =
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (π β (πΆβπΎ)))) |
296 | 139 | recnd 11193 |
. . . . . . . . . . . 12
β’ (π β
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β β) |
297 | 35, 242 | subcld 11522 |
. . . . . . . . . . . 12
β’ (π β (π β (πΆβπΎ)) β β) |
298 | 296, 297 | addcomd 11367 |
. . . . . . . . . . 11
β’ (π β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) + (π β (πΆβπΎ))) = ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
299 | 269, 295,
298 | 3eqtrd 2776 |
. . . . . . . . . 10
β’ (π β
((Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) +π
(volβ((πΆβπΎ)[,)if((π·βπΎ) β€ π, (π·βπΎ), π)))) = ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
300 | 255, 265,
299 | 3eqtrd 2776 |
. . . . . . . . 9
β’ (π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) = ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
301 | 253, 300 | breq12d 5124 |
. . . . . . . 8
β’ (π β (((π β π) +
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) β ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) β€ ((π β (πΆβπΎ)) +
(Ξ£^β(π β (β β {πΎ}) β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))))) |
302 | 189, 301 | mpbird 257 |
. . . . . . 7
β’ (π β ((π β π) +
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
303 | 42, 82, 103, 119, 302 | letrd 11322 |
. . . . . 6
β’ (π β ((π β π) + (π β π΄)) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
304 | 39, 303 | eqbrtrd 5133 |
. . . . 5
β’ (π β (π β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
305 | 34, 304 | jca 513 |
. . . 4
β’ (π β (π β (π΄[,]π΅) β§ (π β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
306 | | oveq1 7370 |
. . . . . 6
β’ (π§ = π β (π§ β π΄) = (π β π΄)) |
307 | | breq2 5115 |
. . . . . . . . . . 11
β’ (π§ = π β ((π·βπ) β€ π§ β (π·βπ) β€ π)) |
308 | | id 22 |
. . . . . . . . . . 11
β’ (π§ = π β π§ = π) |
309 | 307, 308 | ifbieq2d 4518 |
. . . . . . . . . 10
β’ (π§ = π β if((π·βπ) β€ π§, (π·βπ), π§) = if((π·βπ) β€ π, (π·βπ), π)) |
310 | 309 | oveq2d 7379 |
. . . . . . . . 9
β’ (π§ = π β ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)) = ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))) |
311 | 310 | fveq2d 6852 |
. . . . . . . 8
β’ (π§ = π β (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§))) = (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))) |
312 | 311 | mpteq2dv 5213 |
. . . . . . 7
β’ (π§ = π β (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))) = (π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))) |
313 | 312 | fveq2d 6852 |
. . . . . 6
β’ (π§ = π β
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§))))) =
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π)))))) |
314 | 306, 313 | breq12d 5124 |
. . . . 5
β’ (π§ = π β ((π§ β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§))))) β (π β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
315 | 314 | elrab 3649 |
. . . 4
β’ (π β {π§ β (π΄[,]π΅) β£ (π§ β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))))} β (π β (π΄[,]π΅) β§ (π β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π, (π·βπ), π))))))) |
316 | 305, 315 | sylibr 233 |
. . 3
β’ (π β π β {π§ β (π΄[,]π΅) β£ (π§ β π΄) β€
(Ξ£^β(π β β β¦ (volβ((πΆβπ)[,)if((π·βπ) β€ π§, (π·βπ), π§)))))}) |
317 | 316, 105 | eleqtrrdi 2844 |
. 2
β’ (π β π β π) |
318 | 272 | simprd 497 |
. 2
β’ (π β π < π) |
319 | | breq2 5115 |
. . 3
β’ (π’ = π β (π < π’ β π < π)) |
320 | 319 | rspcev 3583 |
. 2
β’ ((π β π β§ π < π) β βπ’ β π π < π’) |
321 | 317, 318,
320 | syl2anc 585 |
1
β’ (π β βπ’ β π π < π’) |