Step | Hyp | Ref
| Expression |
1 | | rge0ssre 13382 |
. . 3
β’
(0[,)+β) β β |
2 | | hoidmvlelem4.l |
. . . 4
β’ πΏ = (π₯ β Fin β¦ (π β (β βm π₯), π β (β βm π₯) β¦ if(π₯ = β
, 0, βπ β π₯ (volβ((πβπ)[,)(πβπ)))))) |
3 | | hoidmvlelem4.x |
. . . . 5
β’ (π β π β Fin) |
4 | | hoidmvlelem4.w |
. . . . . 6
β’ π = (π βͺ {π}) |
5 | | hoidmvlelem4.y |
. . . . . . 7
β’ (π β π β π) |
6 | | hoidmvlelem4.z |
. . . . . . . . 9
β’ (π β π β (π β π)) |
7 | 6 | eldifad 3926 |
. . . . . . . 8
β’ (π β π β π) |
8 | | snssi 4772 |
. . . . . . . 8
β’ (π β π β {π} β π) |
9 | 7, 8 | syl 17 |
. . . . . . 7
β’ (π β {π} β π) |
10 | 5, 9 | unssd 4150 |
. . . . . 6
β’ (π β (π βͺ {π}) β π) |
11 | 4, 10 | eqsstrid 3996 |
. . . . 5
β’ (π β π β π) |
12 | | ssfi 9123 |
. . . . 5
β’ ((π β Fin β§ π β π) β π β Fin) |
13 | 3, 11, 12 | syl2anc 585 |
. . . 4
β’ (π β π β Fin) |
14 | | hoidmvlelem4.a |
. . . 4
β’ (π β π΄:πβΆβ) |
15 | | hoidmvlelem4.b |
. . . 4
β’ (π β π΅:πβΆβ) |
16 | 2, 13, 14, 15 | hoidmvcl 44913 |
. . 3
β’ (π β (π΄(πΏβπ)π΅) β (0[,)+β)) |
17 | 1, 16 | sselid 3946 |
. 2
β’ (π β (π΄(πΏβπ)π΅) β β) |
18 | | 1red 11164 |
. . . 4
β’ (π β 1 β
β) |
19 | | hoidmvlelem4.e |
. . . . 5
β’ (π β πΈ β
β+) |
20 | 19 | rpred 12965 |
. . . 4
β’ (π β πΈ β β) |
21 | 18, 20 | readdcld 11192 |
. . 3
β’ (π β (1 + πΈ) β β) |
22 | | nfv 1918 |
. . . . 5
β’
β²ππ |
23 | | nnex 12167 |
. . . . . 6
β’ β
β V |
24 | 23 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
25 | | icossicc 13362 |
. . . . . 6
β’
(0[,)+β) β (0[,]+β) |
26 | 13 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β Fin) |
27 | | hoidmvlelem4.c |
. . . . . . . . 9
β’ (π β πΆ:ββΆ(β βm
π)) |
28 | 27 | ffvelcdmda 7039 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΆβπ) β (β βm π)) |
29 | | elmapi 8793 |
. . . . . . . 8
β’ ((πΆβπ) β (β βm π) β (πΆβπ):πβΆβ) |
30 | 28, 29 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β (πΆβπ):πβΆβ) |
31 | | hoidmvlelem4.h |
. . . . . . . . 9
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) |
32 | | eleq1 2822 |
. . . . . . . . . . . . 13
β’ (π = β β (π β π β β β π)) |
33 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π = β β (πβπ) = (πββ)) |
34 | 33 | breq1d 5119 |
. . . . . . . . . . . . . 14
β’ (π = β β ((πβπ) β€ π₯ β (πββ) β€ π₯)) |
35 | 34, 33 | ifbieq1d 4514 |
. . . . . . . . . . . . 13
β’ (π = β β if((πβπ) β€ π₯, (πβπ), π₯) = if((πββ) β€ π₯, (πββ), π₯)) |
36 | 32, 33, 35 | ifbieq12d 4518 |
. . . . . . . . . . . 12
β’ (π = β β if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)) = if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯))) |
37 | 36 | cbvmptv 5222 |
. . . . . . . . . . 11
β’ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))) = (β β π β¦ if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯))) |
38 | 37 | mpteq2i 5214 |
. . . . . . . . . 10
β’ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯)))) = (π β (β βm π) β¦ (β β π β¦ if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯)))) |
39 | 38 | mpteq2i 5214 |
. . . . . . . . 9
β’ (π₯ β β β¦ (π β (β
βm π)
β¦ (π β π β¦ if(π β π, (πβπ), if((πβπ) β€ π₯, (πβπ), π₯))))) = (π₯ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯))))) |
40 | 31, 39 | eqtri 2761 |
. . . . . . . 8
β’ π» = (π₯ β β β¦ (π β (β βm π) β¦ (β β π β¦ if(β β π, (πββ), if((πββ) β€ π₯, (πββ), π₯))))) |
41 | | snidg 4624 |
. . . . . . . . . . . . 13
β’ (π β (π β π) β π β {π}) |
42 | 6, 41 | syl 17 |
. . . . . . . . . . . 12
β’ (π β π β {π}) |
43 | | elun2 4141 |
. . . . . . . . . . . 12
β’ (π β {π} β π β (π βͺ {π})) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β (π βͺ {π})) |
45 | 4 | a1i 11 |
. . . . . . . . . . . 12
β’ (π β π = (π βͺ {π})) |
46 | 45 | eqcomd 2739 |
. . . . . . . . . . 11
β’ (π β (π βͺ {π}) = π) |
47 | 44, 46 | eleqtrd 2836 |
. . . . . . . . . 10
β’ (π β π β π) |
48 | 15, 47 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ (π β (π΅βπ) β β) |
49 | 48 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β (π΅βπ) β β) |
50 | | hoidmvlelem4.d |
. . . . . . . . . 10
β’ (π β π·:ββΆ(β βm
π)) |
51 | 50 | ffvelcdmda 7039 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π·βπ) β (β βm π)) |
52 | | elmapi 8793 |
. . . . . . . . 9
β’ ((π·βπ) β (β βm π) β (π·βπ):πβΆβ) |
53 | 51, 52 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β β) β (π·βπ):πβΆβ) |
54 | 40, 49, 26, 53 | hsphoif 44907 |
. . . . . . 7
β’ ((π β§ π β β) β ((π»β(π΅βπ))β(π·βπ)):πβΆβ) |
55 | 2, 26, 30, 54 | hoidmvcl 44913 |
. . . . . 6
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))) β (0[,)+β)) |
56 | 25, 55 | sselid 3946 |
. . . . 5
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))) β (0[,]+β)) |
57 | 22, 24, 56 | sge0clmpt 44756 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) β (0[,]+β)) |
58 | 22, 24, 56 | sge0xrclmpt 44759 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) β
β*) |
59 | | pnfxr 11217 |
. . . . . 6
β’ +β
β β* |
60 | 59 | a1i 11 |
. . . . 5
β’ (π β +β β
β*) |
61 | | hoidmvlelem4.r |
. . . . . . 7
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
62 | 61 | rexrd 11213 |
. . . . . 6
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β
β*) |
63 | 2, 26, 30, 53 | hoidmvcl 44913 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,)+β)) |
64 | 25, 63 | sselid 3946 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)(π·βπ)) β (0[,]+β)) |
65 | 6 | eldifbd 3927 |
. . . . . . . . . 10
β’ (π β Β¬ π β π) |
66 | 47, 65 | eldifd 3925 |
. . . . . . . . 9
β’ (π β π β (π β π)) |
67 | 66 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β β) β π β (π β π)) |
68 | 2, 26, 67, 4, 49, 40, 30, 53 | hsphoidmvle 44917 |
. . . . . . 7
β’ ((π β§ π β β) β ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))) β€ ((πΆβπ)(πΏβπ)(π·βπ))) |
69 | 22, 24, 56, 64, 68 | sge0lempt 44741 |
. . . . . 6
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) β€
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) |
70 | 61 | ltpnfd 13050 |
. . . . . 6
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) < +β) |
71 | 58, 62, 60, 69, 70 | xrlelttrd 13088 |
. . . . 5
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) < +β) |
72 | 58, 60, 71 | xrltned 43682 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) β +β) |
73 | | ge0xrre 43859 |
. . . 4
β’
(((Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) β (0[,]+β) β§
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) β +β) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) β β) |
74 | 57, 72, 73 | syl2anc 585 |
. . 3
β’ (π β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) β β) |
75 | 21, 74 | remulcld 11193 |
. 2
β’ (π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ)))))) β β) |
76 | 21, 61 | remulcld 11193 |
. 2
β’ (π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ))))) β β) |
77 | | hoidmvlelem4.14 |
. . . . . . 7
β’ πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) |
78 | | hoidmvlelem4.u |
. . . . . . 7
β’ π = {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} |
79 | | hoidmvlelem4.s |
. . . . . . 7
β’ π = sup(π, β, < ) |
80 | 47 | ancli 550 |
. . . . . . . 8
β’ (π β (π β§ π β π)) |
81 | | eleq1 2822 |
. . . . . . . . . . 11
β’ (π = π β (π β π β π β π)) |
82 | 81 | anbi2d 630 |
. . . . . . . . . 10
β’ (π = π β ((π β§ π β π) β (π β§ π β π))) |
83 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π β (π΄βπ) = (π΄βπ)) |
84 | | fveq2 6846 |
. . . . . . . . . . 11
β’ (π = π β (π΅βπ) = (π΅βπ)) |
85 | 83, 84 | breq12d 5122 |
. . . . . . . . . 10
β’ (π = π β ((π΄βπ) < (π΅βπ) β (π΄βπ) < (π΅βπ))) |
86 | 82, 85 | imbi12d 345 |
. . . . . . . . 9
β’ (π = π β (((π β§ π β π) β (π΄βπ) < (π΅βπ)) β ((π β§ π β π) β (π΄βπ) < (π΅βπ)))) |
87 | | hoidmvlelem4.k |
. . . . . . . . 9
β’ ((π β§ π β π) β (π΄βπ) < (π΅βπ)) |
88 | 86, 87 | vtoclg 3527 |
. . . . . . . 8
β’ (π β π β ((π β§ π β π) β (π΄βπ) < (π΅βπ))) |
89 | 47, 80, 88 | sylc 65 |
. . . . . . 7
β’ (π β (π΄βπ) < (π΅βπ)) |
90 | 2, 3, 5, 6, 4, 14,
15, 27, 50, 61, 31, 77, 19, 78, 79, 89 | hoidmvlelem1 44926 |
. . . . . 6
β’ (π β π β π) |
91 | 48 | rexrd 11213 |
. . . . . . . 8
β’ (π β (π΅βπ) β
β*) |
92 | | iccssxr 13356 |
. . . . . . . . 9
β’ ((π΄βπ)[,](π΅βπ)) β
β* |
93 | | ssrab2 4041 |
. . . . . . . . . . 11
β’ {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β ((π΄βπ)[,](π΅βπ)) |
94 | 78, 93 | eqsstri 3982 |
. . . . . . . . . 10
β’ π β ((π΄βπ)[,](π΅βπ)) |
95 | 94, 90 | sselid 3946 |
. . . . . . . . 9
β’ (π β π β ((π΄βπ)[,](π΅βπ))) |
96 | 92, 95 | sselid 3946 |
. . . . . . . 8
β’ (π β π β
β*) |
97 | | simpl 484 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (π΅βπ) β€ π) β π) |
98 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (π΅βπ) β€ π) β Β¬ (π΅βπ) β€ π) |
99 | 14, 47 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄βπ) β β) |
100 | 99, 48 | iccssred 13360 |
. . . . . . . . . . . . . 14
β’ (π β ((π΄βπ)[,](π΅βπ)) β β) |
101 | 100, 95 | sseldd 3949 |
. . . . . . . . . . . . 13
β’ (π β π β β) |
102 | 101 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (π΅βπ) β€ π) β π β β) |
103 | 97, 48 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ Β¬ (π΅βπ) β€ π) β (π΅βπ) β β) |
104 | 102, 103 | ltnled 11310 |
. . . . . . . . . . 11
β’ ((π β§ Β¬ (π΅βπ) β€ π) β (π < (π΅βπ) β Β¬ (π΅βπ) β€ π)) |
105 | 98, 104 | mpbird 257 |
. . . . . . . . . 10
β’ ((π β§ Β¬ (π΅βπ) β€ π) β π < (π΅βπ)) |
106 | 3 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β π β Fin) |
107 | 5 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β π β π) |
108 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β π β (π β π)) |
109 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β π΄:πβΆβ) |
110 | 15 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β π΅:πβΆβ) |
111 | 87 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π < (π΅βπ)) β§ π β π) β (π΄βπ) < (π΅βπ)) |
112 | | eqid 2733 |
. . . . . . . . . . 11
β’ (π¦ β π β¦ 0) = (π¦ β π β¦ 0) |
113 | 27 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β πΆ:ββΆ(β βm
π)) |
114 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πΆβπ) = (πΆβπ)) |
115 | 114 | fveq1d 6848 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πΆβπ)βπ) = ((πΆβπ)βπ)) |
116 | | fveq2 6846 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (π·βπ) = (π·βπ)) |
117 | 116 | fveq1d 6848 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((π·βπ)βπ) = ((π·βπ)βπ)) |
118 | 115, 117 | oveq12d 7379 |
. . . . . . . . . . . . . 14
β’ (π = π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) = (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
119 | 118 | eleq2d 2820 |
. . . . . . . . . . . . 13
β’ (π = π β (π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ)))) |
120 | 114 | reseq1d 5940 |
. . . . . . . . . . . . 13
β’ (π = π β ((πΆβπ) βΎ π) = ((πΆβπ) βΎ π)) |
121 | 119, 120 | ifbieq1d 4514 |
. . . . . . . . . . . 12
β’ (π = π β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0))) |
122 | 121 | cbvmptv 5222 |
. . . . . . . . . . 11
β’ (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0))) = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0))) |
123 | 50 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β π·:ββΆ(β βm
π)) |
124 | 116 | reseq1d 5940 |
. . . . . . . . . . . . 13
β’ (π = π β ((π·βπ) βΎ π) = ((π·βπ) βΎ π)) |
125 | 119, 124 | ifbieq1d 4514 |
. . . . . . . . . . . 12
β’ (π = π β if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0))) |
126 | 125 | cbvmptv 5222 |
. . . . . . . . . . 11
β’ (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0))) = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0))) |
127 | 61 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))) β β) |
128 | 19 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β πΈ β
β+) |
129 | 90 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β π β π) |
130 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β π < (π΅βπ)) |
131 | | biid 261 |
. . . . . . . . . . . . . . . . 17
β’ (π β (((πΆβπ)βπ)[,)((π·βπ)βπ)) β π β (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
132 | | eqidd 2734 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = π¦ β 0 = 0) |
133 | 132 | cbvmptv 5222 |
. . . . . . . . . . . . . . . . 17
β’ (π€ β π β¦ 0) = (π¦ β π β¦ 0) |
134 | 131, 133 | ifbieq2i 4515 |
. . . . . . . . . . . . . . . 16
β’ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π€ β π β¦ 0)) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)) |
135 | 134 | mpteq2i 5214 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π€ β π β¦ 0))) = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0))) |
136 | 135 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π€ β π β¦ 0))) = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))) |
137 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π = π β π = π) |
138 | 136, 137 | fveq12d 6853 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π€ β π β¦ 0)))βπ) = ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)) |
139 | 131, 133 | ifbieq2i 4515 |
. . . . . . . . . . . . . . . 16
β’ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π€ β π β¦ 0)) = if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)) |
140 | 139 | mpteq2i 5214 |
. . . . . . . . . . . . . . 15
β’ (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π€ β π β¦ 0))) = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0))) |
141 | 140 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π€ β π β¦ 0))) = (π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))) |
142 | 141, 137 | fveq12d 6853 |
. . . . . . . . . . . . 13
β’ (π = π β ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π€ β π β¦ 0)))βπ) = ((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ)) |
143 | 138, 142 | oveq12d 7379 |
. . . . . . . . . . . 12
β’ (π = π β (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π€ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π€ β π β¦ 0)))βπ)) = (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ))) |
144 | 143 | cbvmptv 5222 |
. . . . . . . . . . 11
β’ (π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π€ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π€ β π β¦ 0)))βπ))) = (π β β β¦ (((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((πΆβπ) βΎ π), (π¦ β π β¦ 0)))βπ)(πΏβπ)((π β β β¦ if(π β (((πΆβπ)βπ)[,)((π·βπ)βπ)), ((π·βπ) βΎ π), (π¦ β π β¦ 0)))βπ))) |
145 | | hoidmvlelem4.i |
. . . . . . . . . . . 12
β’ (π β βπ β (β βm π)βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
146 | 145 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β βπ β (β βm π)βπ β (β βm π)βπ β ((β βm π) βm
β)ββ β
((β βm π) βm β)(Xπ β
π ((πβπ)[,)(πβπ)) β βͺ π β β Xπ β π (((πβπ)βπ)[,)((ββπ)βπ)) β (π(πΏβπ)π) β€
(Ξ£^β(π β β β¦ ((πβπ)(πΏβπ)(ββπ)))))) |
147 | | hoidmvlelem4.i2 |
. . . . . . . . . . . 12
β’ (π β Xπ β
π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
148 | 147 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π < (π΅βπ)) β Xπ β π ((π΄βπ)[,)(π΅βπ)) β βͺ π β β Xπ β π (((πΆβπ)βπ)[,)((π·βπ)βπ))) |
149 | | eqid 2733 |
. . . . . . . . . . . 12
β’ (π₯ β Xπ¦ β
π ((π΄βπ¦)[,)(π΅βπ¦)) β¦ (π¦ β π β¦ if(π¦ β π, (π₯βπ¦), π))) = (π₯ β Xπ¦ β π ((π΄βπ¦)[,)(π΅βπ¦)) β¦ (π¦ β π β¦ if(π¦ β π, (π₯βπ¦), π))) |
150 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (π΄βπ¦) = (π΄βπ)) |
151 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (π΅βπ¦) = (π΅βπ)) |
152 | 150, 151 | oveq12d 7379 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β ((π΄βπ¦)[,)(π΅βπ¦)) = ((π΄βπ)[,)(π΅βπ))) |
153 | 152 | cbvixpv 8859 |
. . . . . . . . . . . . 13
β’ Xπ¦ β
π ((π΄βπ¦)[,)(π΅βπ¦)) = Xπ β π ((π΄βπ)[,)(π΅βπ)) |
154 | | eleq1 2822 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (π¦ β π β π β π)) |
155 | | fveq2 6846 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π β (π₯βπ¦) = (π₯βπ)) |
156 | 154, 155 | ifbieq1d 4514 |
. . . . . . . . . . . . . 14
β’ (π¦ = π β if(π¦ β π, (π₯βπ¦), π) = if(π β π, (π₯βπ), π)) |
157 | 156 | cbvmptv 5222 |
. . . . . . . . . . . . 13
β’ (π¦ β π β¦ if(π¦ β π, (π₯βπ¦), π)) = (π β π β¦ if(π β π, (π₯βπ), π)) |
158 | 153, 157 | mpteq12i 5215 |
. . . . . . . . . . . 12
β’ (π₯ β Xπ¦ β
π ((π΄βπ¦)[,)(π΅βπ¦)) β¦ (π¦ β π β¦ if(π¦ β π, (π₯βπ¦), π))) = (π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ)) β¦ (π β π β¦ if(π β π, (π₯βπ), π))) |
159 | 149, 158 | eqtri 2761 |
. . . . . . . . . . 11
β’ (π₯ β Xπ¦ β
π ((π΄βπ¦)[,)(π΅βπ¦)) β¦ (π¦ β π β¦ if(π¦ β π, (π₯βπ¦), π))) = (π₯ β Xπ β π ((π΄βπ)[,)(π΅βπ)) β¦ (π β π β¦ if(π β π, (π₯βπ), π))) |
160 | 2, 106, 107, 108, 4, 109, 110, 111, 112, 113, 122, 123, 126, 127, 31, 77, 128, 78, 129, 130, 144, 146, 148, 159 | hoidmvlelem3 44928 |
. . . . . . . . . 10
β’ ((π β§ π < (π΅βπ)) β βπ’ β π π < π’) |
161 | 97, 105, 160 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ Β¬ (π΅βπ) β€ π) β βπ’ β π π < π’) |
162 | 94 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β ((π΄βπ)[,](π΅βπ))) |
163 | 162, 100 | sstrd 3958 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
164 | 163 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β π β β) |
165 | | ne0i 4298 |
. . . . . . . . . . . . . . . . 17
β’ (π’ β π β π β β
) |
166 | 165 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β π β β
) |
167 | 99 | rexrd 11213 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β (π΄βπ) β
β*) |
168 | 167 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β π) β (π΄βπ) β
β*) |
169 | 91 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β π) β (π΅βπ) β
β*) |
170 | 162 | sselda 3948 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π’ β π) β π’ β ((π΄βπ)[,](π΅βπ))) |
171 | | iccleub 13328 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ π’ β ((π΄βπ)[,](π΅βπ))) β π’ β€ (π΅βπ)) |
172 | 168, 169,
170, 171 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π’ β π) β π’ β€ (π΅βπ)) |
173 | 172 | ralrimiva 3140 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ’ β π π’ β€ (π΅βπ)) |
174 | | brralrspcev 5169 |
. . . . . . . . . . . . . . . . . 18
β’ (((π΅βπ) β β β§ βπ’ β π π’ β€ (π΅βπ)) β βπ¦ β β βπ’ β π π’ β€ π¦) |
175 | 48, 173, 174 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ (π β βπ¦ β β βπ’ β π π’ β€ π¦) |
176 | 175 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β βπ¦ β β βπ’ β π π’ β€ π¦) |
177 | | simpr 486 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π’ β π) β π’ β π) |
178 | | suprub 12124 |
. . . . . . . . . . . . . . . 16
β’ (((π β β β§ π β β
β§ βπ¦ β β βπ’ β π π’ β€ π¦) β§ π’ β π) β π’ β€ sup(π, β, < )) |
179 | 164, 166,
176, 177, 178 | syl31anc 1374 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β π’ β€ sup(π, β, < )) |
180 | 179, 79 | breqtrrdi 5151 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π) β π’ β€ π) |
181 | 180 | ralrimiva 3140 |
. . . . . . . . . . . . 13
β’ (π β βπ’ β π π’ β€ π) |
182 | 164, 177 | sseldd 3949 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β π’ β β) |
183 | 101 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π’ β π) β π β β) |
184 | 182, 183 | lenltd 11309 |
. . . . . . . . . . . . . 14
β’ ((π β§ π’ β π) β (π’ β€ π β Β¬ π < π’)) |
185 | 184 | ralbidva 3169 |
. . . . . . . . . . . . 13
β’ (π β (βπ’ β π π’ β€ π β βπ’ β π Β¬ π < π’)) |
186 | 181, 185 | mpbid 231 |
. . . . . . . . . . . 12
β’ (π β βπ’ β π Β¬ π < π’) |
187 | | ralnex 3072 |
. . . . . . . . . . . 12
β’
(βπ’ β
π Β¬ π < π’ β Β¬ βπ’ β π π < π’) |
188 | 186, 187 | sylib 217 |
. . . . . . . . . . 11
β’ (π β Β¬ βπ’ β π π < π’) |
189 | 188 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π < (π΅βπ)) β Β¬ βπ’ β π π < π’) |
190 | 97, 105, 189 | syl2anc 585 |
. . . . . . . . 9
β’ ((π β§ Β¬ (π΅βπ) β€ π) β Β¬ βπ’ β π π < π’) |
191 | 161, 190 | condan 817 |
. . . . . . . 8
β’ (π β (π΅βπ) β€ π) |
192 | | iccleub 13328 |
. . . . . . . . 9
β’ (((π΄βπ) β β* β§ (π΅βπ) β β* β§ π β ((π΄βπ)[,](π΅βπ))) β π β€ (π΅βπ)) |
193 | 167, 91, 95, 192 | syl3anc 1372 |
. . . . . . . 8
β’ (π β π β€ (π΅βπ)) |
194 | 91, 96, 191, 193 | xrletrid 13083 |
. . . . . . 7
β’ (π β (π΅βπ) = π) |
195 | 78 | eqcomi 2742 |
. . . . . . . 8
β’ {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} = π |
196 | 195 | a1i 11 |
. . . . . . 7
β’ (π β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} = π) |
197 | 194, 196 | eleq12d 2828 |
. . . . . 6
β’ (π β ((π΅βπ) β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β π β π)) |
198 | 90, 197 | mpbird 257 |
. . . . 5
β’ (π β (π΅βπ) β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))}) |
199 | | oveq1 7368 |
. . . . . . . 8
β’ (π§ = (π΅βπ) β (π§ β (π΄βπ)) = ((π΅βπ) β (π΄βπ))) |
200 | 199 | oveq2d 7377 |
. . . . . . 7
β’ (π§ = (π΅βπ) β (πΊ Β· (π§ β (π΄βπ))) = (πΊ Β· ((π΅βπ) β (π΄βπ)))) |
201 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π§ = (π΅βπ) β (π»βπ§) = (π»β(π΅βπ))) |
202 | 201 | fveq1d 6848 |
. . . . . . . . . . 11
β’ (π§ = (π΅βπ) β ((π»βπ§)β(π·βπ)) = ((π»β(π΅βπ))β(π·βπ))) |
203 | 202 | oveq2d 7377 |
. . . . . . . . . 10
β’ (π§ = (π΅βπ) β ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))) = ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ)))) |
204 | 203 | mpteq2dv 5211 |
. . . . . . . . 9
β’ (π§ = (π΅βπ) β (π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))) = (π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))) |
205 | 204 | fveq2d 6850 |
. . . . . . . 8
β’ (π§ = (π΅βπ) β
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))) =
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ)))))) |
206 | 205 | oveq2d 7377 |
. . . . . . 7
β’ (π§ = (π΅βπ) β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) = ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))))) |
207 | 200, 206 | breq12d 5122 |
. . . . . 6
β’ (π§ = (π΅βπ) β ((πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ)))))) β (πΊ Β· ((π΅βπ) β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ)))))))) |
208 | 207 | elrab 3649 |
. . . . 5
β’ ((π΅βπ) β {π§ β ((π΄βπ)[,](π΅βπ)) β£ (πΊ Β· (π§ β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»βπ§)β(π·βπ))))))} β ((π΅βπ) β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· ((π΅βπ) β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ)))))))) |
209 | 198, 208 | sylib 217 |
. . . 4
β’ (π β ((π΅βπ) β ((π΄βπ)[,](π΅βπ)) β§ (πΊ Β· ((π΅βπ) β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ)))))))) |
210 | 209 | simprd 497 |
. . 3
β’ (π β (πΊ Β· ((π΅βπ) β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))))) |
211 | 3, 5 | ssfid 9217 |
. . . . . 6
β’ (π β π β Fin) |
212 | | eqid 2733 |
. . . . . 6
β’
βπ β
π (volβ((π΄βπ)[,)(π΅βπ))) = βπ β π (volβ((π΄βπ)[,)(π΅βπ))) |
213 | 2, 211, 6, 65, 4, 14, 15, 212 | hoiprodp1 44919 |
. . . . 5
β’ (π β (π΄(πΏβπ)π΅) = (βπ β π (volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπ)[,)(π΅βπ))))) |
214 | | eqidd 2734 |
. . . . . . 7
β’ (π β βπ β π ((π΅βπ) β (π΄βπ)) = βπ β π ((π΅βπ) β (π΄βπ))) |
215 | 14 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π΄:πβΆβ) |
216 | | ssun1 4136 |
. . . . . . . . . . . 12
β’ π β (π βͺ {π}) |
217 | 4 | eqcomi 2742 |
. . . . . . . . . . . 12
β’ (π βͺ {π}) = π |
218 | 216, 217 | sseqtri 3984 |
. . . . . . . . . . 11
β’ π β π |
219 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β π) β π β π) |
220 | 218, 219 | sselid 3946 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π β π) |
221 | 215, 220 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π΄βπ) β β) |
222 | 15 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π) β π΅:πβΆβ) |
223 | 222, 220 | ffvelcdmd 7040 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π΅βπ) β β) |
224 | 220, 87 | syldan 592 |
. . . . . . . . 9
β’ ((π β§ π β π) β (π΄βπ) < (π΅βπ)) |
225 | 221, 223,
224 | volicon0 44906 |
. . . . . . . 8
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) = ((π΅βπ) β (π΄βπ))) |
226 | 225 | prodeq2dv 15814 |
. . . . . . 7
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = βπ β π ((π΅βπ) β (π΄βπ))) |
227 | 77 | a1i 11 |
. . . . . . . 8
β’ (π β πΊ = ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π))) |
228 | | hoidmvlelem4.n |
. . . . . . . . 9
β’ (π β π β β
) |
229 | 218 | a1i 11 |
. . . . . . . . . 10
β’ (π β π β π) |
230 | 14, 229 | fssresd 6713 |
. . . . . . . . 9
β’ (π β (π΄ βΎ π):πβΆβ) |
231 | 15, 229 | fssresd 6713 |
. . . . . . . . 9
β’ (π β (π΅ βΎ π):πβΆβ) |
232 | 2, 211, 228, 230, 231 | hoidmvn0val 44915 |
. . . . . . . 8
β’ (π β ((π΄ βΎ π)(πΏβπ)(π΅ βΎ π)) = βπ β π (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ)))) |
233 | | fvres 6865 |
. . . . . . . . . . . . 13
β’ (π β π β ((π΄ βΎ π)βπ) = (π΄βπ)) |
234 | | fvres 6865 |
. . . . . . . . . . . . 13
β’ (π β π β ((π΅ βΎ π)βπ) = (π΅βπ)) |
235 | 233, 234 | oveq12d 7379 |
. . . . . . . . . . . 12
β’ (π β π β (((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ)) = ((π΄βπ)[,)(π΅βπ))) |
236 | 235 | fveq2d 6850 |
. . . . . . . . . . 11
β’ (π β π β (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
237 | 236 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ))) = (volβ((π΄βπ)[,)(π΅βπ)))) |
238 | | volico 44314 |
. . . . . . . . . . 11
β’ (((π΄βπ) β β β§ (π΅βπ) β β) β (volβ((π΄βπ)[,)(π΅βπ))) = if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0)) |
239 | 221, 223,
238 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β π) β (volβ((π΄βπ)[,)(π΅βπ))) = if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0)) |
240 | 239, 225 | eqtr3d 2775 |
. . . . . . . . . 10
β’ ((π β§ π β π) β if((π΄βπ) < (π΅βπ), ((π΅βπ) β (π΄βπ)), 0) = ((π΅βπ) β (π΄βπ))) |
241 | 237, 239,
240 | 3eqtrd 2777 |
. . . . . . . . 9
β’ ((π β§ π β π) β (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ))) = ((π΅βπ) β (π΄βπ))) |
242 | 241 | prodeq2dv 15814 |
. . . . . . . 8
β’ (π β βπ β π (volβ(((π΄ βΎ π)βπ)[,)((π΅ βΎ π)βπ))) = βπ β π ((π΅βπ) β (π΄βπ))) |
243 | 227, 232,
242 | 3eqtrd 2777 |
. . . . . . 7
β’ (π β πΊ = βπ β π ((π΅βπ) β (π΄βπ))) |
244 | 214, 226,
243 | 3eqtr4d 2783 |
. . . . . 6
β’ (π β βπ β π (volβ((π΄βπ)[,)(π΅βπ))) = πΊ) |
245 | 99, 48, 89 | volicon0 44906 |
. . . . . 6
β’ (π β (volβ((π΄βπ)[,)(π΅βπ))) = ((π΅βπ) β (π΄βπ))) |
246 | 244, 245 | oveq12d 7379 |
. . . . 5
β’ (π β (βπ β π (volβ((π΄βπ)[,)(π΅βπ))) Β· (volβ((π΄βπ)[,)(π΅βπ)))) = (πΊ Β· ((π΅βπ) β (π΄βπ)))) |
247 | 213, 246 | eqtrd 2773 |
. . . 4
β’ (π β (π΄(πΏβπ)π΅) = (πΊ Β· ((π΅βπ) β (π΄βπ)))) |
248 | 247 | breq1d 5119 |
. . 3
β’ (π β ((π΄(πΏβπ)π΅) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ)))))) β (πΊ Β· ((π΅βπ) β (π΄βπ))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ)))))))) |
249 | 210, 248 | mpbird 257 |
. 2
β’ (π β (π΄(πΏβπ)π΅) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ))))))) |
250 | | 0le1 11686 |
. . . . 5
β’ 0 β€
1 |
251 | 250 | a1i 11 |
. . . 4
β’ (π β 0 β€ 1) |
252 | 19 | rpge0d 12969 |
. . . 4
β’ (π β 0 β€ πΈ) |
253 | 18, 20, 251, 252 | addge0d 11739 |
. . 3
β’ (π β 0 β€ (1 + πΈ)) |
254 | 74, 61, 21, 253, 69 | lemul2ad 12103 |
. 2
β’ (π β ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)((π»β(π΅βπ))β(π·βπ)))))) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))))) |
255 | 17, 75, 76, 249, 254 | letrd 11320 |
1
β’ (π β (π΄(πΏβπ)π΅) β€ ((1 + πΈ) Β·
(Ξ£^β(π β β β¦ ((πΆβπ)(πΏβπ)(π·βπ)))))) |