Step | Hyp | Ref
| Expression |
1 | | fvex 6905 |
. . . 4
β’ ((π·β(π΄βπ))β(πΈ / (2βπ))) β V |
2 | | nnenom 13945 |
. . . 4
β’ β
β Ο |
3 | 1, 2 | axcc3 10433 |
. . 3
β’
βπ(π Fn β β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
4 | | simprl 770 |
. . . . . 6
β’ ((π β§ (π Fn β β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))))) β π Fn β) |
5 | | nfv 1918 |
. . . . . . . . 9
β’
β²ππ |
6 | | nfra1 3282 |
. . . . . . . . 9
β’
β²πβπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
7 | 5, 6 | nfan 1903 |
. . . . . . . 8
β’
β²π(π β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
8 | | rspa 3246 |
. . . . . . . . . . 11
β’
((βπ β
β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π β β) β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
9 | 8 | adantll 713 |
. . . . . . . . . 10
β’ (((π β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β§ π β β) β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
10 | | ovnsubaddlem2.x |
. . . . . . . . . . . . . . . . 17
β’ (π β π β Fin) |
11 | 10 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β Fin) |
12 | | ovnsubaddlem2.n0 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β
) |
13 | 12 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β π β β
) |
14 | | ovnsubaddlem2.a |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π΄:ββΆπ« (β
βm π)) |
15 | 14 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π΄:ββΆπ« (β
βm π)) |
16 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β β) |
17 | 15, 16 | ffvelcdmd 7088 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (π΄βπ) β π« (β
βm π)) |
18 | | elpwi 4610 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄βπ) β π« (β
βm π)
β (π΄βπ) β (β
βm π)) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (π΄βπ) β (β βm π)) |
20 | | ovnsubaddlem2.e |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΈ β
β+) |
21 | 20 | adantr 482 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β πΈ β
β+) |
22 | | nnnn0 12479 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β0) |
23 | | 2nn 12285 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ 2 β
β |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β 2 β β) |
25 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β0
β π β
β0) |
26 | | nnexpcl 14040 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((2
β β β§ π
β β0) β (2βπ) β β) |
27 | 24, 25, 26 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β0
β (2βπ) β
β) |
28 | | nnrp 12985 |
. . . . . . . . . . . . . . . . . . . 20
β’
((2βπ) β
β β (2βπ)
β β+) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β0
β (2βπ) β
β+) |
30 | 22, 29 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (π β β β
(2βπ) β
β+) |
31 | 30 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (2βπ) β
β+) |
32 | 21, 31 | rpdivcld 13033 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (πΈ / (2βπ)) β
β+) |
33 | | ovnsubaddlem2.c |
. . . . . . . . . . . . . . . 16
β’ πΆ = (π β π« (β βm
π) β¦ {π β (((β Γ
β) βm π) βm β) β£ π β βͺ π β β Xπ β π (([,) β (πβπ))βπ)}) |
34 | | ovnsubaddlem2.l |
. . . . . . . . . . . . . . . 16
β’ πΏ = (β β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
β)βπ))) |
35 | | ovnsubaddlem2.d |
. . . . . . . . . . . . . . . 16
β’ π· = (π β π« (β βm
π) β¦ (π β β+
β¦ {π β (πΆβπ) β£
(Ξ£^β(π β β β¦ (πΏβ(πβπ)))) β€ (((voln*βπ)βπ) +π π)})) |
36 | 11, 13, 19, 32, 33, 34, 35 | ovncvrrp 45280 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β βπ π β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
37 | | n0 4347 |
. . . . . . . . . . . . . . 15
β’ (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β βπ π β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
38 | 36, 37 | sylibr 233 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((π·β(π΄βπ))β(πΈ / (2βπ))) β β
) |
39 | 38 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β ((π·β(π΄βπ))β(πΈ / (2βπ))) β β
) |
40 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β) β§ (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
41 | 39, 40 | mpd 15 |
. . . . . . . . . . . 12
β’ (((π β§ π β β) β§ (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
42 | 41 | ex 414 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
43 | 42 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β§ π β β) β ((((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
44 | 9, 43 | mpd 15 |
. . . . . . . . 9
β’ (((π β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β§ π β β) β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
45 | 44 | ex 414 |
. . . . . . . 8
β’ ((π β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β (π β β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
46 | 7, 45 | ralrimi 3255 |
. . . . . . 7
β’ ((π β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
47 | 46 | adantrl 715 |
. . . . . 6
β’ ((π β§ (π Fn β β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))))) β βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
48 | 4, 47 | jca 513 |
. . . . 5
β’ ((π β§ (π Fn β β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))))) β (π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
49 | 48 | ex 414 |
. . . 4
β’ (π β ((π Fn β β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β (π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))))) |
50 | 49 | eximdv 1921 |
. . 3
β’ (π β (βπ(π Fn β β§ βπ β β (((π·β(π΄βπ))β(πΈ / (2βπ))) β β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β βπ(π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))))) |
51 | 3, 50 | mpi 20 |
. 2
β’ (π β βπ(π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
52 | | simpl 484 |
. . . . 5
β’ ((π β§ (π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β π) |
53 | | simprl 770 |
. . . . 5
β’ ((π β§ (π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β π Fn β) |
54 | | simprr 772 |
. . . . 5
β’ ((π β§ (π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
55 | | nnf1oxpnn 43894 |
. . . . . 6
β’
βπ π:ββ1-1-ontoβ(β Γ β) |
56 | | simpl1 1192 |
. . . . . . . . 9
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β π) |
57 | | simpl2 1193 |
. . . . . . . . 9
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β π Fn β) |
58 | | fveq2 6892 |
. . . . . . . . . . . . . 14
β’ (π = π β (πβπ) = (πβπ)) |
59 | | 2fveq3 6897 |
. . . . . . . . . . . . . . 15
β’ (π = π β (π·β(π΄βπ)) = (π·β(π΄βπ))) |
60 | | oveq2 7417 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (2βπ) = (2βπ)) |
61 | 60 | oveq2d 7425 |
. . . . . . . . . . . . . . 15
β’ (π = π β (πΈ / (2βπ)) = (πΈ / (2βπ))) |
62 | 59, 61 | fveq12d 6899 |
. . . . . . . . . . . . . 14
β’ (π = π β ((π·β(π΄βπ))β(πΈ / (2βπ))) = ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
63 | 58, 62 | eleq12d 2828 |
. . . . . . . . . . . . 13
β’ (π = π β ((πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))) β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) |
64 | 63 | cbvralvw 3235 |
. . . . . . . . . . . 12
β’
(βπ β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))) β βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
65 | 64 | biimpri 227 |
. . . . . . . . . . 11
β’
(βπ β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))) β βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
66 | 65 | 3ad2ant3 1136 |
. . . . . . . . . 10
β’ ((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
67 | 66 | adantr 482 |
. . . . . . . . 9
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β
βπ β β
(πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
68 | | simpr 486 |
. . . . . . . . 9
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β π:ββ1-1-ontoβ(β Γ β)) |
69 | 10 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π:ββ1-1-ontoβ(β Γ β)) β π β Fin) |
70 | 69 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β π β Fin) |
71 | 12 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π:ββ1-1-ontoβ(β Γ β)) β π β β
) |
72 | 71 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β π β β
) |
73 | 14 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π:ββ1-1-ontoβ(β Γ β)) β π΄:ββΆπ«
(β βm π)) |
74 | 73 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β π΄:ββΆπ«
(β βm π)) |
75 | 20 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π:ββ1-1-ontoβ(β Γ β)) β πΈ β
β+) |
76 | 75 | 3ad2antl1 1186 |
. . . . . . . . . 10
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β πΈ β
β+) |
77 | | ovnsubaddlem2.z |
. . . . . . . . . 10
β’ π = (π β π« (β βm
π) β¦ {π§ β β*
β£ βπ β
(((β Γ β) βm π) βm β)(π β βͺ π β β Xπ β π (([,) β (πβπ))βπ) β§ π§ =
(Ξ£^β(π β β β¦ βπ β π (volβ(([,) β (πβπ))βπ)))))}) |
78 | | coeq2 5859 |
. . . . . . . . . . . . . . 15
β’ (β = π β ([,) β β) = ([,) β π)) |
79 | 78 | fveq1d 6894 |
. . . . . . . . . . . . . 14
β’ (β = π β (([,) β β)βπ) = (([,) β π)βπ)) |
80 | 79 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ (β = π β (volβ(([,) β β)βπ)) = (volβ(([,) β π)βπ))) |
81 | 80 | prodeq2ad 44308 |
. . . . . . . . . . . 12
β’ (β = π β βπ β π (volβ(([,) β β)βπ)) = βπ β π (volβ(([,) β π)βπ))) |
82 | 81 | cbvmptv 5262 |
. . . . . . . . . . 11
β’ (β β ((β Γ
β) βm π) β¦ βπ β π (volβ(([,) β β)βπ))) = (π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ))) |
83 | 34, 82 | eqtri 2761 |
. . . . . . . . . 10
β’ πΏ = (π β ((β Γ β)
βm π)
β¦ βπ β
π (volβ(([,) β
π)βπ))) |
84 | 64 | biimpi 215 |
. . . . . . . . . . . . 13
β’
(βπ β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))) β βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
85 | 84 | 3ad2ant3 1136 |
. . . . . . . . . . . 12
β’ ((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
86 | 85 | ad2antrr 725 |
. . . . . . . . . . 11
β’ ((((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β§ π β β) β
βπ β β
(πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
87 | | simpr 486 |
. . . . . . . . . . 11
β’ ((((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β§ π β β) β π β
β) |
88 | | rspa 3246 |
. . . . . . . . . . 11
β’
((βπ β
β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))) β§ π β β) β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
89 | 86, 87, 88 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β§ π β β) β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) |
90 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β π:ββ1-1-ontoβ(β Γ β)) |
91 | | 2fveq3 6897 |
. . . . . . . . . . . . 13
β’ (π = π β (1st β(πβπ)) = (1st β(πβπ))) |
92 | 91 | fveq2d 6896 |
. . . . . . . . . . . 12
β’ (π = π β (πβ(1st β(πβπ))) = (πβ(1st β(πβπ)))) |
93 | | 2fveq3 6897 |
. . . . . . . . . . . 12
β’ (π = π β (2nd β(πβπ)) = (2nd β(πβπ))) |
94 | 92, 93 | fveq12d 6899 |
. . . . . . . . . . 11
β’ (π = π β ((πβ(1st β(πβπ)))β(2nd β(πβπ))) = ((πβ(1st β(πβπ)))β(2nd β(πβπ)))) |
95 | 94 | cbvmptv 5262 |
. . . . . . . . . 10
β’ (π β β β¦ ((πβ(1st
β(πβπ)))β(2nd
β(πβπ)))) = (π β β β¦ ((πβ(1st β(πβπ)))β(2nd β(πβπ)))) |
96 | 70, 72, 74, 76, 77, 33, 83, 35, 89, 90, 95 | ovnsubaddlem1 45286 |
. . . . . . . . 9
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β
((voln*βπ)ββͺ
π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) |
97 | 56, 57, 67, 68, 96 | syl31anc 1374 |
. . . . . . . 8
β’ (((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β§ π:ββ1-1-ontoβ(β Γ β)) β
((voln*βπ)ββͺ
π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) |
98 | 97 | ex 414 |
. . . . . . 7
β’ ((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β (π:ββ1-1-ontoβ(β Γ β) β
((voln*βπ)ββͺ
π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ))) |
99 | 98 | exlimdv 1937 |
. . . . . 6
β’ ((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β (βπ π:ββ1-1-ontoβ(β Γ β) β
((voln*βπ)ββͺ
π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ))) |
100 | 55, 99 | mpi 20 |
. . . . 5
β’ ((π β§ π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β ((voln*βπ)ββͺ
π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) |
101 | 52, 53, 54, 100 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ))))) β ((voln*βπ)ββͺ
π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) |
102 | 101 | ex 414 |
. . 3
β’ (π β ((π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β ((voln*βπ)ββͺ
π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ))) |
103 | 102 | exlimdv 1937 |
. 2
β’ (π β (βπ(π Fn β β§ βπ β β (πβπ) β ((π·β(π΄βπ))β(πΈ / (2βπ)))) β ((voln*βπ)ββͺ
π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ))) |
104 | 51, 103 | mpd 15 |
1
β’ (π β ((voln*βπ)ββͺ π β β (π΄βπ)) β€
((Ξ£^β(π β β β¦ ((voln*βπ)β(π΄βπ)))) +π πΈ)) |