Step | Hyp | Ref
| Expression |
1 | | ovoliun.a |
. . . . 5
β’ ((π β§ π β β) β π΄ β β) |
2 | 1 | ralrimiva 3147 |
. . . 4
β’ (π β βπ β β π΄ β β) |
3 | | iunss 5049 |
. . . 4
β’ (βͺ π β β π΄ β β β βπ β β π΄ β
β) |
4 | 2, 3 | sylibr 233 |
. . 3
β’ (π β βͺ π β β π΄ β β) |
5 | | ovolcl 24995 |
. . 3
β’ (βͺ π β β π΄ β β β (vol*ββͺ π β β π΄) β
β*) |
6 | 4, 5 | syl 17 |
. 2
β’ (π β (vol*ββͺ π β β π΄) β
β*) |
7 | | ovoliun.f |
. . . . . . . . . 10
β’ (π β πΉ:ββΆ(( β€ β© (β
Γ β)) βm β)) |
8 | 7 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β β) β πΉ:ββΆ(( β€ β© (β
Γ β)) βm β)) |
9 | | ovoliun.j |
. . . . . . . . . . . 12
β’ (π β π½:ββ1-1-ontoβ(β Γ β)) |
10 | | f1of 6834 |
. . . . . . . . . . . 12
β’ (π½:ββ1-1-ontoβ(β Γ β) β π½:ββΆ(β Γ
β)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
β’ (π β π½:ββΆ(β Γ
β)) |
12 | 11 | ffvelcdmda 7087 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (π½βπ) β (β Γ
β)) |
13 | | xp1st 8007 |
. . . . . . . . . 10
β’ ((π½βπ) β (β Γ β) β
(1st β(π½βπ)) β β) |
14 | 12, 13 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (1st
β(π½βπ)) β
β) |
15 | 8, 14 | ffvelcdmd 7088 |
. . . . . . . 8
β’ ((π β§ π β β) β (πΉβ(1st β(π½βπ))) β (( β€ β© (β Γ
β)) βm β)) |
16 | | elovolmlem 24991 |
. . . . . . . 8
β’ ((πΉβ(1st
β(π½βπ))) β (( β€ β©
(β Γ β)) βm β) β (πΉβ(1st
β(π½βπ))):ββΆ( β€ β©
(β Γ β))) |
17 | 15, 16 | sylib 217 |
. . . . . . 7
β’ ((π β§ π β β) β (πΉβ(1st β(π½βπ))):ββΆ( β€ β© (β
Γ β))) |
18 | | xp2nd 8008 |
. . . . . . . 8
β’ ((π½βπ) β (β Γ β) β
(2nd β(π½βπ)) β β) |
19 | 12, 18 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β) β (2nd
β(π½βπ)) β
β) |
20 | 17, 19 | ffvelcdmd 7088 |
. . . . . 6
β’ ((π β§ π β β) β ((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ))) β ( β€ β© (β Γ
β))) |
21 | | ovoliun.h |
. . . . . 6
β’ π» = (π β β β¦ ((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))) |
22 | 20, 21 | fmptd 7114 |
. . . . 5
β’ (π β π»:ββΆ( β€ β© (β
Γ β))) |
23 | | eqid 2733 |
. . . . . 6
β’ ((abs
β β ) β π») = ((abs β β ) β π») |
24 | | ovoliun.u |
. . . . . 6
β’ π = seq1( + , ((abs β
β ) β π»)) |
25 | 23, 24 | ovolsf 24989 |
. . . . 5
β’ (π»:ββΆ( β€ β©
(β Γ β)) β π:ββΆ(0[,)+β)) |
26 | | frn 6725 |
. . . . 5
β’ (π:ββΆ(0[,)+β)
β ran π β
(0[,)+β)) |
27 | 22, 25, 26 | 3syl 18 |
. . . 4
β’ (π β ran π β (0[,)+β)) |
28 | | icossxr 13409 |
. . . 4
β’
(0[,)+β) β β* |
29 | 27, 28 | sstrdi 3995 |
. . 3
β’ (π β ran π β
β*) |
30 | | supxrcl 13294 |
. . 3
β’ (ran
π β
β* β sup(ran π, β*, < ) β
β*) |
31 | 29, 30 | syl 17 |
. 2
β’ (π β sup(ran π, β*, < ) β
β*) |
32 | | ovoliun.r |
. . . 4
β’ (π β sup(ran π, β*, < ) β
β) |
33 | | ovoliun.b |
. . . . 5
β’ (π β π΅ β
β+) |
34 | 33 | rpred 13016 |
. . . 4
β’ (π β π΅ β β) |
35 | 32, 34 | readdcld 11243 |
. . 3
β’ (π β (sup(ran π, β*, < ) + π΅) β
β) |
36 | 35 | rexrd 11264 |
. 2
β’ (π β (sup(ran π, β*, < ) + π΅) β
β*) |
37 | | eliun 5002 |
. . . . . 6
β’ (π§ β βͺ π β β π΄ β βπ β β π§ β π΄) |
38 | | ovoliun.x1 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π΄ β βͺ ran
((,) β (πΉβπ))) |
39 | 38 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((π β§ π β β β§ π§ β π΄) β π΄ β βͺ ran
((,) β (πΉβπ))) |
40 | 1 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β§ π β β β§ π§ β π΄) β π΄ β β) |
41 | 7 | ffvelcdmda 7087 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πΉβπ) β (( β€ β© (β Γ
β)) βm β)) |
42 | | elovolmlem 24991 |
. . . . . . . . . . . . 13
β’ ((πΉβπ) β (( β€ β© (β Γ
β)) βm β) β (πΉβπ):ββΆ( β€ β© (β
Γ β))) |
43 | 41, 42 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΉβπ):ββΆ( β€ β© (β
Γ β))) |
44 | 43 | 3adant3 1133 |
. . . . . . . . . . 11
β’ ((π β§ π β β β§ π§ β π΄) β (πΉβπ):ββΆ( β€ β© (β
Γ β))) |
45 | | ovolfioo 24984 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ (πΉβπ):ββΆ( β€ β© (β
Γ β))) β (π΄ β βͺ ran
((,) β (πΉβπ)) β βπ§ β π΄ βπ β β ((1st
β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ))))) |
46 | 40, 44, 45 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β β β§ π§ β π΄) β (π΄ β βͺ ran
((,) β (πΉβπ)) β βπ§ β π΄ βπ β β ((1st
β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ))))) |
47 | 39, 46 | mpbid 231 |
. . . . . . . . 9
β’ ((π β§ π β β β§ π§ β π΄) β βπ§ β π΄ βπ β β ((1st
β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ)))) |
48 | | simp3 1139 |
. . . . . . . . 9
β’ ((π β§ π β β β§ π§ β π΄) β π§ β π΄) |
49 | | rsp 3245 |
. . . . . . . . 9
β’
(βπ§ β
π΄ βπ β β ((1st
β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ))) β (π§ β π΄ β βπ β β ((1st
β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ))))) |
50 | 47, 48, 49 | sylc 65 |
. . . . . . . 8
β’ ((π β§ π β β β§ π§ β π΄) β βπ β β ((1st
β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ)))) |
51 | | simpl1 1192 |
. . . . . . . . . . . 12
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β π) |
52 | | f1ocnv 6846 |
. . . . . . . . . . . 12
β’ (π½:ββ1-1-ontoβ(β Γ β) β β‘π½:(β Γ β)β1-1-ontoββ) |
53 | | f1of 6834 |
. . . . . . . . . . . 12
β’ (β‘π½:(β Γ β)β1-1-ontoββ β β‘π½:(β Γ
β)βΆβ) |
54 | 51, 9, 52, 53 | 4syl 19 |
. . . . . . . . . . 11
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β β‘π½:(β Γ
β)βΆβ) |
55 | | simpl2 1193 |
. . . . . . . . . . 11
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β π β β) |
56 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β π β β) |
57 | 54, 55, 56 | fovcdmd 7579 |
. . . . . . . . . 10
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (πβ‘π½π) β β) |
58 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (πβ‘π½π) β (1st β(π½βπ)) = (1st β(π½β(πβ‘π½π)))) |
59 | 58 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ‘π½π) β (πΉβ(1st β(π½βπ))) = (πΉβ(1st β(π½β(πβ‘π½π))))) |
60 | | 2fveq3 6897 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (πβ‘π½π) β (2nd β(π½βπ)) = (2nd β(π½β(πβ‘π½π)))) |
61 | 59, 60 | fveq12d 6899 |
. . . . . . . . . . . . . . . . 17
β’ (π = (πβ‘π½π) β ((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ))) = ((πΉβ(1st β(π½β(πβ‘π½π))))β(2nd β(π½β(πβ‘π½π))))) |
62 | | fvex 6905 |
. . . . . . . . . . . . . . . . 17
β’ ((πΉβ(1st
β(π½β(πβ‘π½π))))β(2nd β(π½β(πβ‘π½π)))) β V |
63 | 61, 21, 62 | fvmpt 6999 |
. . . . . . . . . . . . . . . 16
β’ ((πβ‘π½π) β β β (π»β(πβ‘π½π)) = ((πΉβ(1st β(π½β(πβ‘π½π))))β(2nd β(π½β(πβ‘π½π))))) |
64 | 57, 63 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (π»β(πβ‘π½π)) = ((πΉβ(1st β(π½β(πβ‘π½π))))β(2nd β(π½β(πβ‘π½π))))) |
65 | | df-ov 7412 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (πβ‘π½π) = (β‘π½ββ¨π, πβ©) |
66 | 65 | fveq2i 6895 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π½β(πβ‘π½π)) = (π½β(β‘π½ββ¨π, πβ©)) |
67 | 51, 9 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β π½:ββ1-1-ontoβ(β Γ β)) |
68 | 55, 56 | opelxpd 5716 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β β¨π, πβ© β (β Γ
β)) |
69 | | f1ocnvfv2 7275 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π½:ββ1-1-ontoβ(β Γ β) β§ β¨π, πβ© β (β Γ β))
β (π½β(β‘π½ββ¨π, πβ©)) = β¨π, πβ©) |
70 | 67, 68, 69 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (π½β(β‘π½ββ¨π, πβ©)) = β¨π, πβ©) |
71 | 66, 70 | eqtrid 2785 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (π½β(πβ‘π½π)) = β¨π, πβ©) |
72 | 71 | fveq2d 6896 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (1st
β(π½β(πβ‘π½π))) = (1st ββ¨π, πβ©)) |
73 | | vex 3479 |
. . . . . . . . . . . . . . . . . . 19
β’ π β V |
74 | | vex 3479 |
. . . . . . . . . . . . . . . . . . 19
β’ π β V |
75 | 73, 74 | op1st 7983 |
. . . . . . . . . . . . . . . . . 18
β’
(1st ββ¨π, πβ©) = π |
76 | 72, 75 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (1st
β(π½β(πβ‘π½π))) = π) |
77 | 76 | fveq2d 6896 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (πΉβ(1st β(π½β(πβ‘π½π)))) = (πΉβπ)) |
78 | 71 | fveq2d 6896 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (2nd
β(π½β(πβ‘π½π))) = (2nd ββ¨π, πβ©)) |
79 | 73, 74 | op2nd 7984 |
. . . . . . . . . . . . . . . . 17
β’
(2nd ββ¨π, πβ©) = π |
80 | 78, 79 | eqtrdi 2789 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (2nd
β(π½β(πβ‘π½π))) = π) |
81 | 77, 80 | fveq12d 6899 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β ((πΉβ(1st β(π½β(πβ‘π½π))))β(2nd β(π½β(πβ‘π½π)))) = ((πΉβπ)βπ)) |
82 | 64, 81 | eqtrd 2773 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (π»β(πβ‘π½π)) = ((πΉβπ)βπ)) |
83 | 82 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (1st
β(π»β(πβ‘π½π))) = (1st β((πΉβπ)βπ))) |
84 | 83 | breq1d 5159 |
. . . . . . . . . . . 12
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β ((1st
β(π»β(πβ‘π½π))) < π§ β (1st β((πΉβπ)βπ)) < π§)) |
85 | 82 | fveq2d 6896 |
. . . . . . . . . . . . 13
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (2nd
β(π»β(πβ‘π½π))) = (2nd β((πΉβπ)βπ))) |
86 | 85 | breq2d 5161 |
. . . . . . . . . . . 12
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (π§ < (2nd β(π»β(πβ‘π½π))) β π§ < (2nd β((πΉβπ)βπ)))) |
87 | 84, 86 | anbi12d 632 |
. . . . . . . . . . 11
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (((1st
β(π»β(πβ‘π½π))) < π§ β§ π§ < (2nd β(π»β(πβ‘π½π)))) β ((1st β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ))))) |
88 | 87 | biimprd 247 |
. . . . . . . . . 10
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (((1st
β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ))) β ((1st β(π»β(πβ‘π½π))) < π§ β§ π§ < (2nd β(π»β(πβ‘π½π)))))) |
89 | | 2fveq3 6897 |
. . . . . . . . . . . . 13
β’ (π = (πβ‘π½π) β (1st β(π»βπ)) = (1st β(π»β(πβ‘π½π)))) |
90 | 89 | breq1d 5159 |
. . . . . . . . . . . 12
β’ (π = (πβ‘π½π) β ((1st β(π»βπ)) < π§ β (1st β(π»β(πβ‘π½π))) < π§)) |
91 | | 2fveq3 6897 |
. . . . . . . . . . . . 13
β’ (π = (πβ‘π½π) β (2nd β(π»βπ)) = (2nd β(π»β(πβ‘π½π)))) |
92 | 91 | breq2d 5161 |
. . . . . . . . . . . 12
β’ (π = (πβ‘π½π) β (π§ < (2nd β(π»βπ)) β π§ < (2nd β(π»β(πβ‘π½π))))) |
93 | 90, 92 | anbi12d 632 |
. . . . . . . . . . 11
β’ (π = (πβ‘π½π) β (((1st β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))) β ((1st β(π»β(πβ‘π½π))) < π§ β§ π§ < (2nd β(π»β(πβ‘π½π)))))) |
94 | 93 | rspcev 3613 |
. . . . . . . . . 10
β’ (((πβ‘π½π) β β β§ ((1st
β(π»β(πβ‘π½π))) < π§ β§ π§ < (2nd β(π»β(πβ‘π½π))))) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ)))) |
95 | 57, 88, 94 | syl6an 683 |
. . . . . . . . 9
β’ (((π β§ π β β β§ π§ β π΄) β§ π β β) β (((1st
β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ))) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
96 | 95 | rexlimdva 3156 |
. . . . . . . 8
β’ ((π β§ π β β β§ π§ β π΄) β (βπ β β ((1st
β((πΉβπ)βπ)) < π§ β§ π§ < (2nd β((πΉβπ)βπ))) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
97 | 50, 96 | mpd 15 |
. . . . . . 7
β’ ((π β§ π β β β§ π§ β π΄) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ)))) |
98 | 97 | rexlimdv3a 3160 |
. . . . . 6
β’ (π β (βπ β β π§ β π΄ β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
99 | 37, 98 | biimtrid 241 |
. . . . 5
β’ (π β (π§ β βͺ
π β β π΄ β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
100 | 99 | ralrimiv 3146 |
. . . 4
β’ (π β βπ§ β βͺ
π β β π΄βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ)))) |
101 | | ovolfioo 24984 |
. . . . 5
β’
((βͺ π β β π΄ β β β§ π»:ββΆ( β€ β© (β
Γ β))) β (βͺ π β β π΄ β βͺ ran ((,) β π») β βπ§ β βͺ
π β β π΄βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
102 | 4, 22, 101 | syl2anc 585 |
. . . 4
β’ (π β (βͺ π β β π΄ β βͺ ran
((,) β π») β
βπ§ β βͺ π β β π΄βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
103 | 100, 102 | mpbird 257 |
. . 3
β’ (π β βͺ π β β π΄ β βͺ ran
((,) β π»)) |
104 | 24 | ovollb 24996 |
. . 3
β’ ((π»:ββΆ( β€ β©
(β Γ β)) β§ βͺ π β β π΄ β βͺ ran ((,) β π»)) β (vol*ββͺ π β β π΄) β€ sup(ran π, β*, <
)) |
105 | 22, 103, 104 | syl2anc 585 |
. 2
β’ (π β (vol*ββͺ π β β π΄) β€ sup(ran π, β*, <
)) |
106 | | fzfi 13937 |
. . . . . . 7
β’
(1...π) β
Fin |
107 | | elfznn 13530 |
. . . . . . . . . 10
β’ (π€ β (1...π) β π€ β β) |
108 | | ffvelcdm 7084 |
. . . . . . . . . . 11
β’ ((π½:ββΆ(β Γ
β) β§ π€ β
β) β (π½βπ€) β (β Γ
β)) |
109 | | xp1st 8007 |
. . . . . . . . . . 11
β’ ((π½βπ€) β (β Γ β) β
(1st β(π½βπ€)) β β) |
110 | | nnre 12219 |
. . . . . . . . . . 11
β’
((1st β(π½βπ€)) β β β (1st
β(π½βπ€)) β
β) |
111 | 108, 109,
110 | 3syl 18 |
. . . . . . . . . 10
β’ ((π½:ββΆ(β Γ
β) β§ π€ β
β) β (1st β(π½βπ€)) β β) |
112 | 11, 107, 111 | syl2an 597 |
. . . . . . . . 9
β’ ((π β§ π€ β (1...π)) β (1st β(π½βπ€)) β β) |
113 | 112 | ralrimiva 3147 |
. . . . . . . 8
β’ (π β βπ€ β (1...π)(1st β(π½βπ€)) β β) |
114 | 113 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β) β βπ€ β (1...π)(1st β(π½βπ€)) β β) |
115 | | fimaxre3 12160 |
. . . . . . 7
β’
(((1...π) β Fin
β§ βπ€ β
(1...π)(1st
β(π½βπ€)) β β) β
βπ₯ β β
βπ€ β (1...π)(1st β(π½βπ€)) β€ π₯) |
116 | 106, 114,
115 | sylancr 588 |
. . . . . 6
β’ ((π β§ π β β) β βπ₯ β β βπ€ β (1...π)(1st β(π½βπ€)) β€ π₯) |
117 | | fllep1 13766 |
. . . . . . . . . . . 12
β’ (π₯ β β β π₯ β€ ((ββπ₯) + 1)) |
118 | 117 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π€ β (1...π)) β π₯ β€ ((ββπ₯) + 1)) |
119 | 112 | adantlr 714 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π€ β (1...π)) β (1st β(π½βπ€)) β β) |
120 | | simplr 768 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π€ β (1...π)) β π₯ β β) |
121 | | flcl 13760 |
. . . . . . . . . . . . . . 15
β’ (π₯ β β β
(ββπ₯) β
β€) |
122 | 121 | peano2zd 12669 |
. . . . . . . . . . . . . 14
β’ (π₯ β β β
((ββπ₯) + 1)
β β€) |
123 | 122 | zred 12666 |
. . . . . . . . . . . . 13
β’ (π₯ β β β
((ββπ₯) + 1)
β β) |
124 | 123 | ad2antlr 726 |
. . . . . . . . . . . 12
β’ (((π β§ π₯ β β) β§ π€ β (1...π)) β ((ββπ₯) + 1) β β) |
125 | | letr 11308 |
. . . . . . . . . . . 12
β’
(((1st β(π½βπ€)) β β β§ π₯ β β β§ ((ββπ₯) + 1) β β) β
(((1st β(π½βπ€)) β€ π₯ β§ π₯ β€ ((ββπ₯) + 1)) β (1st β(π½βπ€)) β€ ((ββπ₯) + 1))) |
126 | 119, 120,
124, 125 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ π₯ β β) β§ π€ β (1...π)) β (((1st β(π½βπ€)) β€ π₯ β§ π₯ β€ ((ββπ₯) + 1)) β (1st β(π½βπ€)) β€ ((ββπ₯) + 1))) |
127 | 118, 126 | mpan2d 693 |
. . . . . . . . . 10
β’ (((π β§ π₯ β β) β§ π€ β (1...π)) β ((1st β(π½βπ€)) β€ π₯ β (1st β(π½βπ€)) β€ ((ββπ₯) + 1))) |
128 | 127 | ralimdva 3168 |
. . . . . . . . 9
β’ ((π β§ π₯ β β) β (βπ€ β (1...π)(1st β(π½βπ€)) β€ π₯ β βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) |
129 | 128 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β (βπ€ β (1...π)(1st β(π½βπ€)) β€ π₯ β βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) |
130 | | ovoliun.t |
. . . . . . . . . 10
β’ π = seq1( + , πΊ) |
131 | | ovoliun.g |
. . . . . . . . . 10
β’ πΊ = (π β β β¦ (vol*βπ΄)) |
132 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β π) |
133 | 132, 1 | sylan 581 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β§ π β β) β π΄ β β) |
134 | | ovoliun.v |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (vol*βπ΄) β
β) |
135 | 132, 134 | sylan 581 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β§ π β β) β (vol*βπ΄) β
β) |
136 | 132, 32 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β sup(ran π, β*, < ) β
β) |
137 | 132, 33 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β π΅ β
β+) |
138 | | ovoliun.s |
. . . . . . . . . 10
β’ π = seq1( + , ((abs β
β ) β (πΉβπ))) |
139 | 132, 9 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β π½:ββ1-1-ontoβ(β Γ β)) |
140 | 132, 7 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β πΉ:ββΆ(( β€ β© (β
Γ β)) βm β)) |
141 | 132, 38 | sylan 581 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β§ π β β) β π΄ β βͺ ran
((,) β (πΉβπ))) |
142 | | ovoliun.x2 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β sup(ran π, β*, < )
β€ ((vol*βπ΄) +
(π΅ / (2βπ)))) |
143 | 132, 142 | sylan 581 |
. . . . . . . . . 10
β’ ((((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β§ π β β) β sup(ran π, β*, < )
β€ ((vol*βπ΄) +
(π΅ / (2βπ)))) |
144 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β π β β) |
145 | 122 | ad2antrl 727 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β ((ββπ₯) + 1) β
β€) |
146 | | simprr 772 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1)) |
147 | 130, 131,
133, 135, 136, 137, 138, 24, 21, 139, 140, 141, 143, 144, 145, 146 | ovoliunlem1 25019 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π₯ β β β§ βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1))) β (πβπ) β€ (sup(ran π, β*, < ) + π΅)) |
148 | 147 | expr 458 |
. . . . . . . 8
β’ (((π β§ π β β) β§ π₯ β β) β (βπ€ β (1...π)(1st β(π½βπ€)) β€ ((ββπ₯) + 1) β (πβπ) β€ (sup(ran π, β*, < ) + π΅))) |
149 | 129, 148 | syld 47 |
. . . . . . 7
β’ (((π β§ π β β) β§ π₯ β β) β (βπ€ β (1...π)(1st β(π½βπ€)) β€ π₯ β (πβπ) β€ (sup(ran π, β*, < ) + π΅))) |
150 | 149 | rexlimdva 3156 |
. . . . . 6
β’ ((π β§ π β β) β (βπ₯ β β βπ€ β (1...π)(1st β(π½βπ€)) β€ π₯ β (πβπ) β€ (sup(ran π, β*, < ) + π΅))) |
151 | 116, 150 | mpd 15 |
. . . . 5
β’ ((π β§ π β β) β (πβπ) β€ (sup(ran π, β*, < ) + π΅)) |
152 | 151 | ralrimiva 3147 |
. . . 4
β’ (π β βπ β β (πβπ) β€ (sup(ran π, β*, < ) + π΅)) |
153 | | ffn 6718 |
. . . . 5
β’ (π:ββΆ(0[,)+β)
β π Fn
β) |
154 | | breq1 5152 |
. . . . . 6
β’ (π§ = (πβπ) β (π§ β€ (sup(ran π, β*, < ) + π΅) β (πβπ) β€ (sup(ran π, β*, < ) + π΅))) |
155 | 154 | ralrn 7090 |
. . . . 5
β’ (π Fn β β
(βπ§ β ran π π§ β€ (sup(ran π, β*, < ) + π΅) β βπ β β (πβπ) β€ (sup(ran π, β*, < ) + π΅))) |
156 | 22, 25, 153, 155 | 4syl 19 |
. . . 4
β’ (π β (βπ§ β ran π π§ β€ (sup(ran π, β*, < ) + π΅) β βπ β β (πβπ) β€ (sup(ran π, β*, < ) + π΅))) |
157 | 152, 156 | mpbird 257 |
. . 3
β’ (π β βπ§ β ran π π§ β€ (sup(ran π, β*, < ) + π΅)) |
158 | | supxrleub 13305 |
. . . 4
β’ ((ran
π β
β* β§ (sup(ran π, β*, < ) + π΅) β β*)
β (sup(ran π,
β*, < ) β€ (sup(ran π, β*, < ) + π΅) β βπ§ β ran π π§ β€ (sup(ran π, β*, < ) + π΅))) |
159 | 29, 36, 158 | syl2anc 585 |
. . 3
β’ (π β (sup(ran π, β*, < ) β€ (sup(ran
π, β*,
< ) + π΅) β
βπ§ β ran π π§ β€ (sup(ran π, β*, < ) + π΅))) |
160 | 157, 159 | mpbird 257 |
. 2
β’ (π β sup(ran π, β*, < ) β€ (sup(ran
π, β*,
< ) + π΅)) |
161 | 6, 31, 36, 105, 160 | xrletrd 13141 |
1
β’ (π β (vol*ββͺ π β β π΄) β€ (sup(ran π, β*, < ) + π΅)) |