Step | Hyp | Ref
| Expression |
1 | | fveq2 6847 |
. . . . . 6
β’ (π = β
β
(voln*βπ) =
(voln*ββ
)) |
2 | 1 | fveq1d 6849 |
. . . . 5
β’ (π = β
β
((voln*βπ)ββͺ
π β β (π΄βπ)) = ((voln*ββ
)ββͺ π β β (π΄βπ))) |
3 | 2 | adantl 483 |
. . . 4
β’ ((π β§ π = β
) β ((voln*βπ)ββͺ π β β (π΄βπ)) = ((voln*ββ
)ββͺ π β β (π΄βπ))) |
4 | | ovnsubadd.2 |
. . . . . . . . . . . 12
β’ (π β π΄:ββΆπ« (β
βm π)) |
5 | 4 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π΄:ββΆπ« (β
βm π)) |
6 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β) |
7 | 5, 6 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π΄βπ) β π« (β
βm π)) |
8 | | elpwi 4572 |
. . . . . . . . . 10
β’ ((π΄βπ) β π« (β
βm π)
β (π΄βπ) β (β
βm π)) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (π΄βπ) β (β βm π)) |
10 | 9 | ralrimiva 3144 |
. . . . . . . 8
β’ (π β βπ β β (π΄βπ) β (β βm π)) |
11 | | iunss 5010 |
. . . . . . . 8
β’ (βͺ π β β (π΄βπ) β (β βm π) β βπ β β (π΄βπ) β (β βm π)) |
12 | 10, 11 | sylibr 233 |
. . . . . . 7
β’ (π β βͺ π β β (π΄βπ) β (β βm π)) |
13 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ π = β
) β βͺ π β β (π΄βπ) β (β βm π)) |
14 | | oveq2 7370 |
. . . . . . 7
β’ (π = β
β (β
βm π) =
(β βm β
)) |
15 | 14 | adantl 483 |
. . . . . 6
β’ ((π β§ π = β
) β (β
βm π) =
(β βm β
)) |
16 | 13, 15 | sseqtrd 3989 |
. . . . 5
β’ ((π β§ π = β
) β βͺ π β β (π΄βπ) β (β βm
β
)) |
17 | 16 | ovn0val 44865 |
. . . 4
β’ ((π β§ π = β
) β
((voln*ββ
)ββͺ π β β (π΄βπ)) = 0) |
18 | 3, 17 | eqtrd 2777 |
. . 3
β’ ((π β§ π = β
) β ((voln*βπ)ββͺ π β β (π΄βπ)) = 0) |
19 | | nnex 12166 |
. . . . . 6
β’ β
β V |
20 | 19 | a1i 11 |
. . . . 5
β’ (π β β β
V) |
21 | | ovnsubadd.1 |
. . . . . . . 8
β’ (π β π β Fin) |
22 | 21 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β π β Fin) |
23 | 22, 9 | ovncl 44882 |
. . . . . 6
β’ ((π β§ π β β) β ((voln*βπ)β(π΄βπ)) β (0[,]+β)) |
24 | | eqid 2737 |
. . . . . 6
β’ (π β β β¦
((voln*βπ)β(π΄βπ))) = (π β β β¦ ((voln*βπ)β(π΄βπ))) |
25 | 23, 24 | fmptd 7067 |
. . . . 5
β’ (π β (π β β β¦ ((voln*βπ)β(π΄βπ))):ββΆ(0[,]+β)) |
26 | 20, 25 | sge0ge0 44699 |
. . . 4
β’ (π β 0 β€
(Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ))))) |
27 | 26 | adantr 482 |
. . 3
β’ ((π β§ π = β
) β 0 β€
(Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ))))) |
28 | 18, 27 | eqbrtrd 5132 |
. 2
β’ ((π β§ π = β
) β ((voln*βπ)ββͺ π β β (π΄βπ)) β€
(Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ))))) |
29 | 21, 12 | ovnxrcl 44884 |
. . . 4
β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β
β*) |
30 | 29 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π = β
) β ((voln*βπ)ββͺ π β β (π΄βπ)) β
β*) |
31 | 20, 25 | sge0xrcl 44700 |
. . . 4
β’ (π β
(Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) β
β*) |
32 | 31 | adantr 482 |
. . 3
β’ ((π β§ Β¬ π = β
) β
(Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) β
β*) |
33 | 21 | ad2antrr 725 |
. . . 4
β’ (((π β§ Β¬ π = β
) β§ π¦ β β+) β π β Fin) |
34 | | neqne 2952 |
. . . . 5
β’ (Β¬
π = β
β π β β
) |
35 | 34 | ad2antlr 726 |
. . . 4
β’ (((π β§ Β¬ π = β
) β§ π¦ β β+) β π β β
) |
36 | 4 | ad2antrr 725 |
. . . 4
β’ (((π β§ Β¬ π = β
) β§ π¦ β β+) β π΄:ββΆπ«
(β βm π)) |
37 | | simpr 486 |
. . . 4
β’ (((π β§ Β¬ π = β
) β§ π¦ β β+) β π¦ β
β+) |
38 | | eqid 2737 |
. . . 4
β’ (π β π« (β
βm π)
β¦ {π§ β
β* β£ βπ β (((β Γ β)
βm π)
βm β)(π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) = (π β π« (β βm
π) β¦ {π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)(π β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) |
39 | | sseq1 3974 |
. . . . . 6
β’ (π = π β (π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ) β π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ))) |
40 | 39 | rabbidv 3418 |
. . . . 5
β’ (π = π β {π β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)} = {π β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)}) |
41 | 40 | cbvmptv 5223 |
. . . 4
β’ (π β π« (β
βm π)
β¦ {π β
(((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) = (π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) |
42 | | eqid 2737 |
. . . 4
β’ (β β ((β Γ
β) βm π) β¦ βπ β π (volβ(([,) β β)βπ))) = (β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ))) |
43 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (πβπ) = (πβπ)) |
44 | 43 | coeq2d 5823 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β ([,) β (πβπ)) = ([,) β (πβπ))) |
45 | 44 | fveq1d 6849 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (([,) β (πβπ))βπ) = (([,) β (πβπ))βπ)) |
46 | 45 | ixpeq2dv 8858 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β Xπ β π (([,) β (πβπ))βπ) = Xπ β π (([,) β (πβπ))βπ)) |
47 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = π β (([,) β (πβπ))βπ) = (([,) β (πβπ))βπ)) |
48 | 47 | cbvixpv 8860 |
. . . . . . . . . . . . . . . . . 18
β’ Xπ β
π (([,) β (πβπ))βπ) = Xπ β π (([,) β (πβπ))βπ) |
49 | 46, 48 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β Xπ β π (([,) β (πβπ))βπ) = Xπ β π (([,) β (πβπ))βπ)) |
50 | 49 | cbviunv 5005 |
. . . . . . . . . . . . . . . 16
β’ βͺ π β β Xπ β π (([,) β (πβπ))βπ) = βͺ π β β Xπ β
π (([,) β (πβπ))βπ) |
51 | 50 | sseq2i 3978 |
. . . . . . . . . . . . . . 15
β’ (π β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)) |
52 | 51 | rabbii 3416 |
. . . . . . . . . . . . . 14
β’ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)} = {π β (((β Γ β)
βm π)
βm β) β£ π β βͺ
π β β Xπ β
π (([,) β (πβπ))βπ)} |
53 | 52 | mpteq2i 5215 |
. . . . . . . . . . . . 13
β’ (π β π« (β
βm π)
β¦ {π β
(((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) = (π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) |
54 | 53 | fveq1i 6848 |
. . . . . . . . . . . 12
β’ ((π β π« (β
βm π)
β¦ {π β
(((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) = ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) |
55 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) = ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ)) |
56 | 54, 55 | eqtrid 2789 |
. . . . . . . . . . 11
β’ (π = π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) = ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ)) |
57 | 56 | eleq2d 2824 |
. . . . . . . . . 10
β’ (π = π β (π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ))) |
58 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . 18
β’ (π = π β (volβ(([,) β β)βπ)) = (volβ(([,) β β)βπ))) |
59 | 58 | cbvprodv 15806 |
. . . . . . . . . . . . . . . . 17
β’
βπ β
π (volβ(([,) β
β)βπ)) = βπ β π (volβ(([,) β β)βπ)) |
60 | 59 | mpteq2i 5215 |
. . . . . . . . . . . . . . . 16
β’ (β β ((β Γ
β) βm π) β¦ βπ β π (volβ(([,) β β)βπ))) = (β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ))) |
61 | 60 | a1i 11 |
. . . . . . . . . . . . . . 15
β’ (π = π β (β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ))) = (β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))) |
62 | | fveq2 6847 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πβπ) = (πβπ)) |
63 | 61, 62 | fveq12d 6854 |
. . . . . . . . . . . . . 14
β’ (π = π β ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)) = ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ))) |
64 | 63 | cbvmptv 5223 |
. . . . . . . . . . . . 13
β’ (π β β β¦ ((β β ((β Γ
β) βm π) β¦ βπ β π (volβ(([,) β β)βπ)))β(πβπ))) = (π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ))) |
65 | 64 | fveq2i 6850 |
. . . . . . . . . . . 12
β’
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) =
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) |
66 | 65 | a1i 11 |
. . . . . . . . . . 11
β’ (π = π β
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) =
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ))))) |
67 | | fveq2 6847 |
. . . . . . . . . . . 12
β’ (π = π β ((voln*βπ)βπ) = ((voln*βπ)βπ)) |
68 | 67 | oveq1d 7377 |
. . . . . . . . . . 11
β’ (π = π β (((voln*βπ)βπ) +π π) = (((voln*βπ)βπ) +π π)) |
69 | 66, 68 | breq12d 5123 |
. . . . . . . . . 10
β’ (π = π β
((Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π) β
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π))) |
70 | 57, 69 | anbi12d 632 |
. . . . . . . . 9
β’ (π = π β ((π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β§
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)) β (π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β§
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)))) |
71 | 70 | rabbidva2 3412 |
. . . . . . . 8
β’ (π = π β {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)} = {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)}) |
72 | | fveq1 6846 |
. . . . . . . . . . . . 13
β’ (π = π β (πβπ) = (πβπ)) |
73 | 72 | fveq2d 6851 |
. . . . . . . . . . . 12
β’ (π = π β ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)) = ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ))) |
74 | 73 | mpteq2dv 5212 |
. . . . . . . . . . 11
β’ (π = π β (π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ))) = (π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) |
75 | 74 | fveq2d 6851 |
. . . . . . . . . 10
β’ (π = π β
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) =
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ))))) |
76 | 75 | breq1d 5120 |
. . . . . . . . 9
β’ (π = π β
((Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π) β
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π))) |
77 | 76 | cbvrabv 3420 |
. . . . . . . 8
β’ {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)} = {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)} |
78 | 71, 77 | eqtrdi 2793 |
. . . . . . 7
β’ (π = π β {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)} = {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)}) |
79 | 78 | mpteq2dv 5212 |
. . . . . 6
β’ (π = π β (π β β+ β¦ {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)}) = (π β β+ β¦ {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) |
80 | | oveq2 7370 |
. . . . . . . . 9
β’ (π = π β (((voln*βπ)βπ) +π π) = (((voln*βπ)βπ) +π π)) |
81 | 80 | breq2d 5122 |
. . . . . . . 8
β’ (π = π β
((Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π) β
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π))) |
82 | 81 | rabbidv 3418 |
. . . . . . 7
β’ (π = π β {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)} = {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)}) |
83 | 82 | cbvmptv 5223 |
. . . . . 6
β’ (π β β+
β¦ {π β ((π β π« (β
βm π)
β¦ {π β
(((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)}) = (π β β+ β¦ {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)}) |
84 | 79, 83 | eqtrdi 2793 |
. . . . 5
β’ (π = π β (π β β+ β¦ {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)}) = (π β β+ β¦ {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) |
85 | 84 | cbvmptv 5223 |
. . . 4
β’ (π β π« (β
βm π)
β¦ (π β
β+ β¦ {π β ((π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) = (π β π« (β βm
π) β¦ (π β β+
β¦ {π β ((π β π« (β
βm π)
β¦ {π β
(((β Γ β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)})βπ) β£
(Ξ£^β(π β β β¦ ((β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ)))β(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) |
86 | 33, 35, 36, 37, 38, 41, 42, 85 | ovnsubaddlem2 44886 |
. . 3
β’ (((π β§ Β¬ π = β
) β§ π¦ β β+) β
((voln*βπ)ββͺ
π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π π¦)) |
87 | 30, 32, 86 | xrlexaddrp 43660 |
. 2
β’ ((π β§ Β¬ π = β
) β ((voln*βπ)ββͺ π β β (π΄βπ)) β€
(Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ))))) |
88 | 28, 87 | pm2.61dan 812 |
1
β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β€
(Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ))))) |