Step | Hyp | Ref
| Expression |
1 | | 2fveq3 6852 |
. . . . . . . 8
β’ (π = (π½βπ) β (πΉβ(1st βπ)) = (πΉβ(1st β(π½βπ)))) |
2 | | fveq2 6847 |
. . . . . . . 8
β’ (π = (π½βπ) β (2nd βπ) = (2nd
β(π½βπ))) |
3 | 1, 2 | fveq12d 6854 |
. . . . . . 7
β’ (π = (π½βπ) β ((πΉβ(1st βπ))β(2nd
βπ)) = ((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ)))) |
4 | 3 | fveq2d 6851 |
. . . . . 6
β’ (π = (π½βπ) β (2nd β((πΉβ(1st
βπ))β(2nd βπ))) = (2nd
β((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ))))) |
5 | 3 | fveq2d 6851 |
. . . . . 6
β’ (π = (π½βπ) β (1st β((πΉβ(1st
βπ))β(2nd βπ))) = (1st
β((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ))))) |
6 | 4, 5 | oveq12d 7380 |
. . . . 5
β’ (π = (π½βπ) β ((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) =
((2nd β((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))) β (1st β((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ)))))) |
7 | | fzfid 13885 |
. . . . 5
β’ (π β (1...πΎ) β Fin) |
8 | | ovoliun.j |
. . . . . . 7
β’ (π β π½:ββ1-1-ontoβ(β Γ β)) |
9 | | f1of1 6788 |
. . . . . . 7
β’ (π½:ββ1-1-ontoβ(β Γ β) β π½:ββ1-1β(β Γ β)) |
10 | 8, 9 | syl 17 |
. . . . . 6
β’ (π β π½:ββ1-1β(β Γ β)) |
11 | | fz1ssnn 13479 |
. . . . . 6
β’
(1...πΎ) β
β |
12 | | f1ores 6803 |
. . . . . 6
β’ ((π½:ββ1-1β(β Γ β) β§ (1...πΎ) β β) β (π½ βΎ (1...πΎ)):(1...πΎ)β1-1-ontoβ(π½ β (1...πΎ))) |
13 | 10, 11, 12 | sylancl 587 |
. . . . 5
β’ (π β (π½ βΎ (1...πΎ)):(1...πΎ)β1-1-ontoβ(π½ β (1...πΎ))) |
14 | | fvres 6866 |
. . . . . 6
β’ (π β (1...πΎ) β ((π½ βΎ (1...πΎ))βπ) = (π½βπ)) |
15 | 14 | adantl 483 |
. . . . 5
β’ ((π β§ π β (1...πΎ)) β ((π½ βΎ (1...πΎ))βπ) = (π½βπ)) |
16 | | ovoliun.f |
. . . . . . . . . . . . 13
β’ (π β πΉ:ββΆ(( β€ β© (β
Γ β)) βm β)) |
17 | 16 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π½ β (1...πΎ))) β πΉ:ββΆ(( β€ β© (β
Γ β)) βm β)) |
18 | | imassrn 6029 |
. . . . . . . . . . . . . . 15
β’ (π½ β (1...πΎ)) β ran π½ |
19 | | f1of 6789 |
. . . . . . . . . . . . . . . . 17
β’ (π½:ββ1-1-ontoβ(β Γ β) β π½:ββΆ(β Γ
β)) |
20 | 8, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π½:ββΆ(β Γ
β)) |
21 | 20 | frnd 6681 |
. . . . . . . . . . . . . . 15
β’ (π β ran π½ β (β Γ
β)) |
22 | 18, 21 | sstrid 3960 |
. . . . . . . . . . . . . 14
β’ (π β (π½ β (1...πΎ)) β (β Γ
β)) |
23 | 22 | sselda 3949 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (π½ β (1...πΎ))) β π β (β Γ
β)) |
24 | | xp1st 7958 |
. . . . . . . . . . . . 13
β’ (π β (β Γ
β) β (1st βπ) β β) |
25 | 23, 24 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (π½ β (1...πΎ))) β (1st βπ) β
β) |
26 | 17, 25 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’ ((π β§ π β (π½ β (1...πΎ))) β (πΉβ(1st βπ)) β (( β€ β© (β
Γ β)) βm β)) |
27 | | elovolmlem 24854 |
. . . . . . . . . . 11
β’ ((πΉβ(1st
βπ)) β (( β€
β© (β Γ β)) βm β) β (πΉβ(1st
βπ)):ββΆ(
β€ β© (β Γ β))) |
28 | 26, 27 | sylib 217 |
. . . . . . . . . 10
β’ ((π β§ π β (π½ β (1...πΎ))) β (πΉβ(1st βπ)):ββΆ( β€ β©
(β Γ β))) |
29 | | xp2nd 7959 |
. . . . . . . . . . 11
β’ (π β (β Γ
β) β (2nd βπ) β β) |
30 | 23, 29 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (π½ β (1...πΎ))) β (2nd βπ) β
β) |
31 | 28, 30 | ffvelcdmd 7041 |
. . . . . . . . 9
β’ ((π β§ π β (π½ β (1...πΎ))) β ((πΉβ(1st βπ))β(2nd
βπ)) β ( β€
β© (β Γ β))) |
32 | 31 | elin2d 4164 |
. . . . . . . 8
β’ ((π β§ π β (π½ β (1...πΎ))) β ((πΉβ(1st βπ))β(2nd
βπ)) β (β
Γ β)) |
33 | | xp2nd 7959 |
. . . . . . . 8
β’ (((πΉβ(1st
βπ))β(2nd βπ)) β (β Γ
β) β (2nd β((πΉβ(1st βπ))β(2nd
βπ))) β
β) |
34 | 32, 33 | syl 17 |
. . . . . . 7
β’ ((π β§ π β (π½ β (1...πΎ))) β (2nd β((πΉβ(1st
βπ))β(2nd βπ))) β
β) |
35 | | xp1st 7958 |
. . . . . . . 8
β’ (((πΉβ(1st
βπ))β(2nd βπ)) β (β Γ
β) β (1st β((πΉβ(1st βπ))β(2nd
βπ))) β
β) |
36 | 32, 35 | syl 17 |
. . . . . . 7
β’ ((π β§ π β (π½ β (1...πΎ))) β (1st β((πΉβ(1st
βπ))β(2nd βπ))) β
β) |
37 | 34, 36 | resubcld 11590 |
. . . . . 6
β’ ((π β§ π β (π½ β (1...πΎ))) β ((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) β
β) |
38 | 37 | recnd 11190 |
. . . . 5
β’ ((π β§ π β (π½ β (1...πΎ))) β ((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) β
β) |
39 | 6, 7, 13, 15, 38 | fsumf1o 15615 |
. . . 4
β’ (π β Ξ£π β (π½ β (1...πΎ))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) = Ξ£π β (1...πΎ)((2nd β((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))) β (1st β((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ)))))) |
40 | 16 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β πΉ:ββΆ(( β€ β© (β
Γ β)) βm β)) |
41 | 20 | ffvelcdmda 7040 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π½βπ) β (β Γ
β)) |
42 | | xp1st 7958 |
. . . . . . . . . . . 12
β’ ((π½βπ) β (β Γ β) β
(1st β(π½βπ)) β β) |
43 | 41, 42 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (1st
β(π½βπ)) β
β) |
44 | 40, 43 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΉβ(1st β(π½βπ))) β (( β€ β© (β Γ
β)) βm β)) |
45 | | elovolmlem 24854 |
. . . . . . . . . 10
β’ ((πΉβ(1st
β(π½βπ))) β (( β€ β©
(β Γ β)) βm β) β (πΉβ(1st
β(π½βπ))):ββΆ( β€ β©
(β Γ β))) |
46 | 44, 45 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΉβ(1st β(π½βπ))):ββΆ( β€ β© (β
Γ β))) |
47 | | xp2nd 7959 |
. . . . . . . . . 10
β’ ((π½βπ) β (β Γ β) β
(2nd β(π½βπ)) β β) |
48 | 41, 47 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β β) β (2nd
β(π½βπ)) β
β) |
49 | 46, 48 | ffvelcdmd 7041 |
. . . . . . . 8
β’ ((π β§ π β β) β ((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ))) β ( β€ β© (β Γ
β))) |
50 | | ovoliun.h |
. . . . . . . 8
β’ π» = (π β β β¦ ((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))) |
51 | 49, 50 | fmptd 7067 |
. . . . . . 7
β’ (π β π»:ββΆ( β€ β© (β
Γ β))) |
52 | | elfznn 13477 |
. . . . . . 7
β’ (π β (1...πΎ) β π β β) |
53 | | eqid 2737 |
. . . . . . . 8
β’ ((abs
β β ) β π») = ((abs β β ) β π») |
54 | 53 | ovolfsval 24850 |
. . . . . . 7
β’ ((π»:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (((abs β
β ) β π»)βπ) = ((2nd β(π»βπ)) β (1st β(π»βπ)))) |
55 | 51, 52, 54 | syl2an 597 |
. . . . . 6
β’ ((π β§ π β (1...πΎ)) β (((abs β β ) β
π»)βπ) = ((2nd β(π»βπ)) β (1st β(π»βπ)))) |
56 | 52 | adantl 483 |
. . . . . . . . 9
β’ ((π β§ π β (1...πΎ)) β π β β) |
57 | | 2fveq3 6852 |
. . . . . . . . . . . 12
β’ (π = π β (1st β(π½βπ)) = (1st β(π½βπ))) |
58 | 57 | fveq2d 6851 |
. . . . . . . . . . 11
β’ (π = π β (πΉβ(1st β(π½βπ))) = (πΉβ(1st β(π½βπ)))) |
59 | | 2fveq3 6852 |
. . . . . . . . . . 11
β’ (π = π β (2nd β(π½βπ)) = (2nd β(π½βπ))) |
60 | 58, 59 | fveq12d 6854 |
. . . . . . . . . 10
β’ (π = π β ((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ))) = ((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))) |
61 | | fvex 6860 |
. . . . . . . . . 10
β’ ((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ))) β V |
62 | 60, 50, 61 | fvmpt 6953 |
. . . . . . . . 9
β’ (π β β β (π»βπ) = ((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))) |
63 | 56, 62 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (1...πΎ)) β (π»βπ) = ((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))) |
64 | 63 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ π β (1...πΎ)) β (2nd β(π»βπ)) = (2nd β((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ))))) |
65 | 63 | fveq2d 6851 |
. . . . . . 7
β’ ((π β§ π β (1...πΎ)) β (1st β(π»βπ)) = (1st β((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ))))) |
66 | 64, 65 | oveq12d 7380 |
. . . . . 6
β’ ((π β§ π β (1...πΎ)) β ((2nd β(π»βπ)) β (1st β(π»βπ))) = ((2nd β((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ)))) β (1st
β((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))))) |
67 | 55, 66 | eqtrd 2777 |
. . . . 5
β’ ((π β§ π β (1...πΎ)) β (((abs β β ) β
π»)βπ) = ((2nd β((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ)))) β (1st
β((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))))) |
68 | | ovoliun.k |
. . . . . 6
β’ (π β πΎ β β) |
69 | | nnuz 12813 |
. . . . . 6
β’ β =
(β€β₯β1) |
70 | 68, 69 | eleqtrdi 2848 |
. . . . 5
β’ (π β πΎ β
(β€β₯β1)) |
71 | | ffvelcdm 7037 |
. . . . . . . . . . 11
β’ ((π»:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (π»βπ) β ( β€ β© (β Γ
β))) |
72 | 51, 52, 71 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ π β (1...πΎ)) β (π»βπ) β ( β€ β© (β Γ
β))) |
73 | 72 | elin2d 4164 |
. . . . . . . . 9
β’ ((π β§ π β (1...πΎ)) β (π»βπ) β (β Γ
β)) |
74 | | xp2nd 7959 |
. . . . . . . . 9
β’ ((π»βπ) β (β Γ β) β
(2nd β(π»βπ)) β β) |
75 | 73, 74 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (1...πΎ)) β (2nd β(π»βπ)) β β) |
76 | | xp1st 7958 |
. . . . . . . . 9
β’ ((π»βπ) β (β Γ β) β
(1st β(π»βπ)) β β) |
77 | 73, 76 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (1...πΎ)) β (1st β(π»βπ)) β β) |
78 | 75, 77 | resubcld 11590 |
. . . . . . 7
β’ ((π β§ π β (1...πΎ)) β ((2nd β(π»βπ)) β (1st β(π»βπ))) β β) |
79 | 78 | recnd 11190 |
. . . . . 6
β’ ((π β§ π β (1...πΎ)) β ((2nd β(π»βπ)) β (1st β(π»βπ))) β β) |
80 | 66, 79 | eqeltrrd 2839 |
. . . . 5
β’ ((π β§ π β (1...πΎ)) β ((2nd β((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ)))) β (1st
β((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ))))) β β) |
81 | 67, 70, 80 | fsumser 15622 |
. . . 4
β’ (π β Ξ£π β (1...πΎ)((2nd β((πΉβ(1st β(π½βπ)))β(2nd β(π½βπ)))) β (1st β((πΉβ(1st
β(π½βπ)))β(2nd
β(π½βπ))))) = (seq1( + , ((abs β
β ) β π»))βπΎ)) |
82 | 39, 81 | eqtrd 2777 |
. . 3
β’ (π β Ξ£π β (π½ β (1...πΎ))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) = (seq1( + ,
((abs β β ) β π»))βπΎ)) |
83 | | ovoliun.u |
. . . 4
β’ π = seq1( + , ((abs β
β ) β π»)) |
84 | 83 | fveq1i 6848 |
. . 3
β’ (πβπΎ) = (seq1( + , ((abs β β )
β π»))βπΎ) |
85 | 82, 84 | eqtr4di 2795 |
. 2
β’ (π β Ξ£π β (π½ β (1...πΎ))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) = (πβπΎ)) |
86 | | f1oeng 8918 |
. . . . . . 7
β’
(((1...πΎ) β Fin
β§ (π½ βΎ (1...πΎ)):(1...πΎ)β1-1-ontoβ(π½ β (1...πΎ))) β (1...πΎ) β (π½ β (1...πΎ))) |
87 | 7, 13, 86 | syl2anc 585 |
. . . . . 6
β’ (π β (1...πΎ) β (π½ β (1...πΎ))) |
88 | 87 | ensymd 8952 |
. . . . 5
β’ (π β (π½ β (1...πΎ)) β (1...πΎ)) |
89 | | enfii 9140 |
. . . . 5
β’
(((1...πΎ) β Fin
β§ (π½ β (1...πΎ)) β (1...πΎ)) β (π½ β (1...πΎ)) β Fin) |
90 | 7, 88, 89 | syl2anc 585 |
. . . 4
β’ (π β (π½ β (1...πΎ)) β Fin) |
91 | 90, 37 | fsumrecl 15626 |
. . 3
β’ (π β Ξ£π β (π½ β (1...πΎ))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) β
β) |
92 | | fzfid 13885 |
. . . . 5
β’ (π β (1...πΏ) β Fin) |
93 | | elfznn 13477 |
. . . . . 6
β’ (π β (1...πΏ) β π β β) |
94 | | ovoliun.v |
. . . . . 6
β’ ((π β§ π β β) β (vol*βπ΄) β
β) |
95 | 93, 94 | sylan2 594 |
. . . . 5
β’ ((π β§ π β (1...πΏ)) β (vol*βπ΄) β β) |
96 | 92, 95 | fsumrecl 15626 |
. . . 4
β’ (π β Ξ£π β (1...πΏ)(vol*βπ΄) β β) |
97 | | ovoliun.b |
. . . . . . 7
β’ (π β π΅ β
β+) |
98 | 97 | rpred 12964 |
. . . . . 6
β’ (π β π΅ β β) |
99 | | 2nn 12233 |
. . . . . . . 8
β’ 2 β
β |
100 | | nnnn0 12427 |
. . . . . . . 8
β’ (π β β β π β
β0) |
101 | | nnexpcl 13987 |
. . . . . . . 8
β’ ((2
β β β§ π
β β0) β (2βπ) β β) |
102 | 99, 100, 101 | sylancr 588 |
. . . . . . 7
β’ (π β β β
(2βπ) β
β) |
103 | 93, 102 | syl 17 |
. . . . . 6
β’ (π β (1...πΏ) β (2βπ) β β) |
104 | | nndivre 12201 |
. . . . . 6
β’ ((π΅ β β β§
(2βπ) β β)
β (π΅ / (2βπ)) β
β) |
105 | 98, 103, 104 | syl2an 597 |
. . . . 5
β’ ((π β§ π β (1...πΏ)) β (π΅ / (2βπ)) β β) |
106 | 92, 105 | fsumrecl 15626 |
. . . 4
β’ (π β Ξ£π β (1...πΏ)(π΅ / (2βπ)) β β) |
107 | 96, 106 | readdcld 11191 |
. . 3
β’ (π β (Ξ£π β (1...πΏ)(vol*βπ΄) + Ξ£π β (1...πΏ)(π΅ / (2βπ))) β β) |
108 | | ovoliun.r |
. . . 4
β’ (π β sup(ran π, β*, < ) β
β) |
109 | 108, 98 | readdcld 11191 |
. . 3
β’ (π β (sup(ran π, β*, < ) + π΅) β
β) |
110 | | relxp 5656 |
. . . . . . . . . . . . . . 15
β’ Rel
({π} Γ ((π½ β (1...πΎ)) β {π})) |
111 | | relres 5971 |
. . . . . . . . . . . . . . 15
β’ Rel
((π½ β (1...πΎ)) βΎ {π}) |
112 | | elsni 4608 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π₯ β {π} β π₯ = π) |
113 | 112 | opeq1d 4841 |
. . . . . . . . . . . . . . . . . . 19
β’ (π₯ β {π} β β¨π₯, π¦β© = β¨π, π¦β©) |
114 | 113 | eleq1d 2823 |
. . . . . . . . . . . . . . . . . 18
β’ (π₯ β {π} β (β¨π₯, π¦β© β (π½ β (1...πΎ)) β β¨π, π¦β© β (π½ β (1...πΎ)))) |
115 | | vex 3452 |
. . . . . . . . . . . . . . . . . . 19
β’ π β V |
116 | | vex 3452 |
. . . . . . . . . . . . . . . . . . 19
β’ π¦ β V |
117 | 115, 116 | elimasn 6046 |
. . . . . . . . . . . . . . . . . 18
β’ (π¦ β ((π½ β (1...πΎ)) β {π}) β β¨π, π¦β© β (π½ β (1...πΎ))) |
118 | 114, 117 | bitr4di 289 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β {π} β (β¨π₯, π¦β© β (π½ β (1...πΎ)) β π¦ β ((π½ β (1...πΎ)) β {π}))) |
119 | 118 | pm5.32i 576 |
. . . . . . . . . . . . . . . 16
β’ ((π₯ β {π} β§ β¨π₯, π¦β© β (π½ β (1...πΎ))) β (π₯ β {π} β§ π¦ β ((π½ β (1...πΎ)) β {π}))) |
120 | 116 | opelresi 5950 |
. . . . . . . . . . . . . . . 16
β’
(β¨π₯, π¦β© β ((π½ β (1...πΎ)) βΎ {π}) β (π₯ β {π} β§ β¨π₯, π¦β© β (π½ β (1...πΎ)))) |
121 | | opelxp 5674 |
. . . . . . . . . . . . . . . 16
β’
(β¨π₯, π¦β© β ({π} Γ ((π½ β (1...πΎ)) β {π})) β (π₯ β {π} β§ π¦ β ((π½ β (1...πΎ)) β {π}))) |
122 | 119, 120,
121 | 3bitr4ri 304 |
. . . . . . . . . . . . . . 15
β’
(β¨π₯, π¦β© β ({π} Γ ((π½ β (1...πΎ)) β {π})) β β¨π₯, π¦β© β ((π½ β (1...πΎ)) βΎ {π})) |
123 | 110, 111,
122 | eqrelriiv 5751 |
. . . . . . . . . . . . . 14
β’ ({π} Γ ((π½ β (1...πΎ)) β {π})) = ((π½ β (1...πΎ)) βΎ {π}) |
124 | | df-res 5650 |
. . . . . . . . . . . . . 14
β’ ((π½ β (1...πΎ)) βΎ {π}) = ((π½ β (1...πΎ)) β© ({π} Γ V)) |
125 | 123, 124 | eqtri 2765 |
. . . . . . . . . . . . 13
β’ ({π} Γ ((π½ β (1...πΎ)) β {π})) = ((π½ β (1...πΎ)) β© ({π} Γ V)) |
126 | 125 | a1i 11 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...πΏ)) β ({π} Γ ((π½ β (1...πΎ)) β {π})) = ((π½ β (1...πΎ)) β© ({π} Γ V))) |
127 | 126 | iuneq2dv 4983 |
. . . . . . . . . . 11
β’ (π β βͺ π β (1...πΏ)({π} Γ ((π½ β (1...πΎ)) β {π})) = βͺ
π β (1...πΏ)((π½ β (1...πΎ)) β© ({π} Γ V))) |
128 | | iunin2 5036 |
. . . . . . . . . . 11
β’ βͺ π β (1...πΏ)((π½ β (1...πΎ)) β© ({π} Γ V)) = ((π½ β (1...πΎ)) β© βͺ
π β (1...πΏ)({π} Γ V)) |
129 | 127, 128 | eqtrdi 2793 |
. . . . . . . . . 10
β’ (π β βͺ π β (1...πΏ)({π} Γ ((π½ β (1...πΎ)) β {π})) = ((π½ β (1...πΎ)) β© βͺ
π β (1...πΏ)({π} Γ V))) |
130 | | relxp 5656 |
. . . . . . . . . . . . . 14
β’ Rel
(β Γ β) |
131 | | relss 5742 |
. . . . . . . . . . . . . 14
β’ ((π½ β (1...πΎ)) β (β Γ β) β
(Rel (β Γ β) β Rel (π½ β (1...πΎ)))) |
132 | 22, 130, 131 | mpisyl 21 |
. . . . . . . . . . . . 13
β’ (π β Rel (π½ β (1...πΎ))) |
133 | | ovoliun.l2 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β βπ€ β (1...πΎ)(1st β(π½βπ€)) β€ πΏ) |
134 | 20 | ffnd 6674 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π½ Fn β) |
135 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π = (π½βπ€) β (1st βπ) = (1st
β(π½βπ€))) |
136 | 135 | breq1d 5120 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = (π½βπ€) β ((1st βπ) β€ πΏ β (1st β(π½βπ€)) β€ πΏ)) |
137 | 136 | ralima 7193 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π½ Fn β β§ (1...πΎ) β β) β
(βπ β (π½ β (1...πΎ))(1st βπ) β€ πΏ β βπ€ β (1...πΎ)(1st β(π½βπ€)) β€ πΏ)) |
138 | 134, 11, 137 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (βπ β (π½ β (1...πΎ))(1st βπ) β€ πΏ β βπ€ β (1...πΎ)(1st β(π½βπ€)) β€ πΏ)) |
139 | 133, 138 | mpbird 257 |
. . . . . . . . . . . . . . . . . 18
β’ (π β βπ β (π½ β (1...πΎ))(1st βπ) β€ πΏ) |
140 | 139 | r19.21bi 3237 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π½ β (1...πΎ))) β (1st βπ) β€ πΏ) |
141 | 25, 69 | eleqtrdi 2848 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π½ β (1...πΎ))) β (1st βπ) β
(β€β₯β1)) |
142 | | ovoliun.l1 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΏ β β€) |
143 | 142 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (π½ β (1...πΎ))) β πΏ β β€) |
144 | | elfz5 13440 |
. . . . . . . . . . . . . . . . . 18
β’
(((1st βπ) β (β€β₯β1)
β§ πΏ β β€)
β ((1st βπ) β (1...πΏ) β (1st βπ) β€ πΏ)) |
145 | 141, 143,
144 | syl2anc 585 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (π½ β (1...πΎ))) β ((1st βπ) β (1...πΏ) β (1st βπ) β€ πΏ)) |
146 | 140, 145 | mpbird 257 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (π½ β (1...πΎ))) β (1st βπ) β (1...πΏ)) |
147 | 146 | ralrimiva 3144 |
. . . . . . . . . . . . . . 15
β’ (π β βπ β (π½ β (1...πΎ))(1st βπ) β (1...πΏ)) |
148 | | vex 3452 |
. . . . . . . . . . . . . . . . . 18
β’ π₯ β V |
149 | 148, 116 | op1std 7936 |
. . . . . . . . . . . . . . . . 17
β’ (π = β¨π₯, π¦β© β (1st βπ) = π₯) |
150 | 149 | eleq1d 2823 |
. . . . . . . . . . . . . . . 16
β’ (π = β¨π₯, π¦β© β ((1st βπ) β (1...πΏ) β π₯ β (1...πΏ))) |
151 | 150 | rspccv 3581 |
. . . . . . . . . . . . . . 15
β’
(βπ β
(π½ β (1...πΎ))(1st βπ) β (1...πΏ) β (β¨π₯, π¦β© β (π½ β (1...πΎ)) β π₯ β (1...πΏ))) |
152 | 147, 151 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (β¨π₯, π¦β© β (π½ β (1...πΎ)) β π₯ β (1...πΏ))) |
153 | | opelxp 5674 |
. . . . . . . . . . . . . . 15
β’
(β¨π₯, π¦β© β (βͺ π β (1...πΏ){π} Γ V) β (π₯ β βͺ
π β (1...πΏ){π} β§ π¦ β V)) |
154 | 116 | biantru 531 |
. . . . . . . . . . . . . . 15
β’ (π₯ β βͺ π β (1...πΏ){π} β (π₯ β βͺ
π β (1...πΏ){π} β§ π¦ β V)) |
155 | | iunid 5025 |
. . . . . . . . . . . . . . . 16
β’ βͺ π β (1...πΏ){π} = (1...πΏ) |
156 | 155 | eleq2i 2830 |
. . . . . . . . . . . . . . 15
β’ (π₯ β βͺ π β (1...πΏ){π} β π₯ β (1...πΏ)) |
157 | 153, 154,
156 | 3bitr2i 299 |
. . . . . . . . . . . . . 14
β’
(β¨π₯, π¦β© β (βͺ π β (1...πΏ){π} Γ V) β π₯ β (1...πΏ)) |
158 | 152, 157 | syl6ibr 252 |
. . . . . . . . . . . . 13
β’ (π β (β¨π₯, π¦β© β (π½ β (1...πΎ)) β β¨π₯, π¦β© β (βͺ π β (1...πΏ){π} Γ V))) |
159 | 132, 158 | relssdv 5749 |
. . . . . . . . . . . 12
β’ (π β (π½ β (1...πΎ)) β (βͺ π β (1...πΏ){π} Γ V)) |
160 | | xpiundir 5708 |
. . . . . . . . . . . 12
β’ (βͺ π β (1...πΏ){π} Γ V) = βͺ π β (1...πΏ)({π} Γ V) |
161 | 159, 160 | sseqtrdi 3999 |
. . . . . . . . . . 11
β’ (π β (π½ β (1...πΎ)) β βͺ π β (1...πΏ)({π} Γ V)) |
162 | | df-ss 3932 |
. . . . . . . . . . 11
β’ ((π½ β (1...πΎ)) β βͺ π β (1...πΏ)({π} Γ V) β ((π½ β (1...πΎ)) β© βͺ
π β (1...πΏ)({π} Γ V)) = (π½ β (1...πΎ))) |
163 | 161, 162 | sylib 217 |
. . . . . . . . . 10
β’ (π β ((π½ β (1...πΎ)) β© βͺ
π β (1...πΏ)({π} Γ V)) = (π½ β (1...πΎ))) |
164 | 129, 163 | eqtrd 2777 |
. . . . . . . . 9
β’ (π β βͺ π β (1...πΏ)({π} Γ ((π½ β (1...πΎ)) β {π})) = (π½ β (1...πΎ))) |
165 | 164, 90 | eqeltrd 2838 |
. . . . . . . 8
β’ (π β βͺ π β (1...πΏ)({π} Γ ((π½ β (1...πΎ)) β {π})) β Fin) |
166 | | ssiun2 5012 |
. . . . . . . 8
β’ (π β (1...πΏ) β ({π} Γ ((π½ β (1...πΎ)) β {π})) β βͺ π β (1...πΏ)({π} Γ ((π½ β (1...πΎ)) β {π}))) |
167 | | ssfi 9124 |
. . . . . . . 8
β’
((βͺ π β (1...πΏ)({π} Γ ((π½ β (1...πΎ)) β {π})) β Fin β§ ({π} Γ ((π½ β (1...πΎ)) β {π})) β βͺ π β (1...πΏ)({π} Γ ((π½ β (1...πΎ)) β {π}))) β ({π} Γ ((π½ β (1...πΎ)) β {π})) β Fin) |
168 | 165, 166,
167 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π β (1...πΏ)) β ({π} Γ ((π½ β (1...πΎ)) β {π})) β Fin) |
169 | | 2ndconst 8038 |
. . . . . . . . . 10
β’ (π β V β (2nd
βΎ ({π} Γ
((π½ β (1...πΎ)) β {π}))):({π} Γ ((π½ β (1...πΎ)) β {π}))β1-1-ontoβ((π½ β (1...πΎ)) β {π})) |
170 | 169 | elv 3454 |
. . . . . . . . 9
β’
(2nd βΎ ({π} Γ ((π½ β (1...πΎ)) β {π}))):({π} Γ ((π½ β (1...πΎ)) β {π}))β1-1-ontoβ((π½ β (1...πΎ)) β {π}) |
171 | | f1oeng 8918 |
. . . . . . . . 9
β’ ((({π} Γ ((π½ β (1...πΎ)) β {π})) β Fin β§ (2nd βΎ
({π} Γ ((π½ β (1...πΎ)) β {π}))):({π} Γ ((π½ β (1...πΎ)) β {π}))β1-1-ontoβ((π½ β (1...πΎ)) β {π})) β ({π} Γ ((π½ β (1...πΎ)) β {π})) β ((π½ β (1...πΎ)) β {π})) |
172 | 168, 170,
171 | sylancl 587 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β ({π} Γ ((π½ β (1...πΎ)) β {π})) β ((π½ β (1...πΎ)) β {π})) |
173 | 172 | ensymd 8952 |
. . . . . . 7
β’ ((π β§ π β (1...πΏ)) β ((π½ β (1...πΎ)) β {π}) β ({π} Γ ((π½ β (1...πΎ)) β {π}))) |
174 | | enfii 9140 |
. . . . . . 7
β’ ((({π} Γ ((π½ β (1...πΎ)) β {π})) β Fin β§ ((π½ β (1...πΎ)) β {π}) β ({π} Γ ((π½ β (1...πΎ)) β {π}))) β ((π½ β (1...πΎ)) β {π}) β Fin) |
175 | 168, 173,
174 | syl2anc 585 |
. . . . . 6
β’ ((π β§ π β (1...πΏ)) β ((π½ β (1...πΎ)) β {π}) β Fin) |
176 | | ffvelcdm 7037 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆ(( β€ β©
(β Γ β)) βm β) β§ π β β) β (πΉβπ) β (( β€ β© (β Γ
β)) βm β)) |
177 | 16, 93, 176 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...πΏ)) β (πΉβπ) β (( β€ β© (β Γ
β)) βm β)) |
178 | | elovolmlem 24854 |
. . . . . . . . . . . . 13
β’ ((πΉβπ) β (( β€ β© (β Γ
β)) βm β) β (πΉβπ):ββΆ( β€ β© (β
Γ β))) |
179 | 177, 178 | sylib 217 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...πΏ)) β (πΉβπ):ββΆ( β€ β© (β
Γ β))) |
180 | 179 | adantrr 716 |
. . . . . . . . . . 11
β’ ((π β§ (π β (1...πΏ) β§ π β ((π½ β (1...πΎ)) β {π}))) β (πΉβπ):ββΆ( β€ β© (β
Γ β))) |
181 | | imassrn 6029 |
. . . . . . . . . . . . . 14
β’ ((π½ β (1...πΎ)) β {π}) β ran (π½ β (1...πΎ)) |
182 | 22 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...πΏ)) β (π½ β (1...πΎ)) β (β Γ
β)) |
183 | | rnss 5899 |
. . . . . . . . . . . . . . . 16
β’ ((π½ β (1...πΎ)) β (β Γ β) β
ran (π½ β (1...πΎ)) β ran (β Γ
β)) |
184 | 182, 183 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...πΏ)) β ran (π½ β (1...πΎ)) β ran (β Γ
β)) |
185 | | rnxpid 6130 |
. . . . . . . . . . . . . . 15
β’ ran
(β Γ β) = β |
186 | 184, 185 | sseqtrdi 3999 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...πΏ)) β ran (π½ β (1...πΎ)) β β) |
187 | 181, 186 | sstrid 3960 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...πΏ)) β ((π½ β (1...πΎ)) β {π}) β β) |
188 | 187 | sseld 3948 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...πΏ)) β (π β ((π½ β (1...πΎ)) β {π}) β π β β)) |
189 | 188 | impr 456 |
. . . . . . . . . . 11
β’ ((π β§ (π β (1...πΏ) β§ π β ((π½ β (1...πΎ)) β {π}))) β π β β) |
190 | 180, 189 | ffvelcdmd 7041 |
. . . . . . . . . 10
β’ ((π β§ (π β (1...πΏ) β§ π β ((π½ β (1...πΎ)) β {π}))) β ((πΉβπ)βπ) β ( β€ β© (β Γ
β))) |
191 | 190 | elin2d 4164 |
. . . . . . . . 9
β’ ((π β§ (π β (1...πΏ) β§ π β ((π½ β (1...πΎ)) β {π}))) β ((πΉβπ)βπ) β (β Γ
β)) |
192 | | xp2nd 7959 |
. . . . . . . . 9
β’ (((πΉβπ)βπ) β (β Γ β) β
(2nd β((πΉβπ)βπ)) β β) |
193 | 191, 192 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π β (1...πΏ) β§ π β ((π½ β (1...πΎ)) β {π}))) β (2nd β((πΉβπ)βπ)) β β) |
194 | | xp1st 7958 |
. . . . . . . . 9
β’ (((πΉβπ)βπ) β (β Γ β) β
(1st β((πΉβπ)βπ)) β β) |
195 | 191, 194 | syl 17 |
. . . . . . . 8
β’ ((π β§ (π β (1...πΏ) β§ π β ((π½ β (1...πΎ)) β {π}))) β (1st β((πΉβπ)βπ)) β β) |
196 | 193, 195 | resubcld 11590 |
. . . . . . 7
β’ ((π β§ (π β (1...πΏ) β§ π β ((π½ β (1...πΎ)) β {π}))) β ((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β β) |
197 | 196 | anassrs 469 |
. . . . . 6
β’ (((π β§ π β (1...πΏ)) β§ π β ((π½ β (1...πΎ)) β {π})) β ((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β β) |
198 | 175, 197 | fsumrecl 15626 |
. . . . 5
β’ ((π β§ π β (1...πΏ)) β Ξ£π β ((π½ β (1...πΎ)) β {π})((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β β) |
199 | 98, 102, 104 | syl2an 597 |
. . . . . . 7
β’ ((π β§ π β β) β (π΅ / (2βπ)) β β) |
200 | 94, 199 | readdcld 11191 |
. . . . . 6
β’ ((π β§ π β β) β ((vol*βπ΄) + (π΅ / (2βπ))) β β) |
201 | 93, 200 | sylan2 594 |
. . . . 5
β’ ((π β§ π β (1...πΏ)) β ((vol*βπ΄) + (π΅ / (2βπ))) β β) |
202 | | eqid 2737 |
. . . . . . . . . . . 12
β’ ((abs
β β ) β (πΉβπ)) = ((abs β β ) β (πΉβπ)) |
203 | | ovoliun.s |
. . . . . . . . . . . 12
β’ π = seq1( + , ((abs β
β ) β (πΉβπ))) |
204 | 202, 203 | ovolsf 24852 |
. . . . . . . . . . 11
β’ ((πΉβπ):ββΆ( β€ β© (β
Γ β)) β π:ββΆ(0[,)+β)) |
205 | 179, 204 | syl 17 |
. . . . . . . . . 10
β’ ((π β§ π β (1...πΏ)) β π:ββΆ(0[,)+β)) |
206 | 205 | frnd 6681 |
. . . . . . . . 9
β’ ((π β§ π β (1...πΏ)) β ran π β (0[,)+β)) |
207 | | icossxr 13356 |
. . . . . . . . 9
β’
(0[,)+β) β β* |
208 | 206, 207 | sstrdi 3961 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β ran π β
β*) |
209 | | supxrcl 13241 |
. . . . . . . 8
β’ (ran
π β
β* β sup(ran π, β*, < ) β
β*) |
210 | 208, 209 | syl 17 |
. . . . . . 7
β’ ((π β§ π β (1...πΏ)) β sup(ran π, β*, < ) β
β*) |
211 | | mnfxr 11219 |
. . . . . . . . 9
β’ -β
β β* |
212 | 211 | a1i 11 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β -β β
β*) |
213 | 95 | rexrd 11212 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β (vol*βπ΄) β
β*) |
214 | 95 | mnfltd 13052 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β -β < (vol*βπ΄)) |
215 | | ovoliun.x1 |
. . . . . . . . . 10
β’ ((π β§ π β β) β π΄ β βͺ ran
((,) β (πΉβπ))) |
216 | 93, 215 | sylan2 594 |
. . . . . . . . 9
β’ ((π β§ π β (1...πΏ)) β π΄ β βͺ ran
((,) β (πΉβπ))) |
217 | 203 | ovollb 24859 |
. . . . . . . . 9
β’ (((πΉβπ):ββΆ( β€ β© (β
Γ β)) β§ π΄
β βͺ ran ((,) β (πΉβπ))) β (vol*βπ΄) β€ sup(ran π, β*, <
)) |
218 | 179, 216,
217 | syl2anc 585 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β (vol*βπ΄) β€ sup(ran π, β*, <
)) |
219 | 212, 213,
210, 214, 218 | xrltletrd 13087 |
. . . . . . 7
β’ ((π β§ π β (1...πΏ)) β -β < sup(ran π, β*, <
)) |
220 | | ovoliun.x2 |
. . . . . . . 8
β’ ((π β§ π β β) β sup(ran π, β*, < )
β€ ((vol*βπ΄) +
(π΅ / (2βπ)))) |
221 | 93, 220 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β (1...πΏ)) β sup(ran π, β*, < ) β€
((vol*βπ΄) + (π΅ / (2βπ)))) |
222 | | xrre 13095 |
. . . . . . 7
β’
(((sup(ran π,
β*, < ) β β* β§ ((vol*βπ΄) + (π΅ / (2βπ))) β β) β§ (-β <
sup(ran π,
β*, < ) β§ sup(ran π, β*, < ) β€
((vol*βπ΄) + (π΅ / (2βπ))))) β sup(ran π, β*, < ) β
β) |
223 | 210, 201,
219, 221, 222 | syl22anc 838 |
. . . . . 6
β’ ((π β§ π β (1...πΏ)) β sup(ran π, β*, < ) β
β) |
224 | | 1zzd 12541 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β 1 β β€) |
225 | 202 | ovolfsval 24850 |
. . . . . . . . 9
β’ (((πΉβπ):ββΆ( β€ β© (β
Γ β)) β§ π
β β) β (((abs β β ) β (πΉβπ))βπ) = ((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ)))) |
226 | 179, 225 | sylan 581 |
. . . . . . . 8
β’ (((π β§ π β (1...πΏ)) β§ π β β) β (((abs β
β ) β (πΉβπ))βπ) = ((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ)))) |
227 | 202 | ovolfsf 24851 |
. . . . . . . . . . . . 13
β’ ((πΉβπ):ββΆ( β€ β© (β
Γ β)) β ((abs β β ) β (πΉβπ)):ββΆ(0[,)+β)) |
228 | 179, 227 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...πΏ)) β ((abs β β ) β
(πΉβπ)):ββΆ(0[,)+β)) |
229 | 228 | ffvelcdmda 7040 |
. . . . . . . . . . 11
β’ (((π β§ π β (1...πΏ)) β§ π β β) β (((abs β
β ) β (πΉβπ))βπ) β (0[,)+β)) |
230 | 226, 229 | eqeltrrd 2839 |
. . . . . . . . . 10
β’ (((π β§ π β (1...πΏ)) β§ π β β) β ((2nd
β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β (0[,)+β)) |
231 | | elrege0 13378 |
. . . . . . . . . 10
β’
(((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β (0[,)+β) β
(((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β β β§ 0 β€
((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))))) |
232 | 230, 231 | sylib 217 |
. . . . . . . . 9
β’ (((π β§ π β (1...πΏ)) β§ π β β) β (((2nd
β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β β β§ 0 β€
((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))))) |
233 | 232 | simpld 496 |
. . . . . . . 8
β’ (((π β§ π β (1...πΏ)) β§ π β β) β ((2nd
β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β β) |
234 | 232 | simprd 497 |
. . . . . . . 8
β’ (((π β§ π β (1...πΏ)) β§ π β β) β 0 β€
((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ)))) |
235 | | supxrub 13250 |
. . . . . . . . . . . . . . 15
β’ ((ran
π β
β* β§ π§
β ran π) β π§ β€ sup(ran π, β*, <
)) |
236 | 208, 235 | sylan 581 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...πΏ)) β§ π§ β ran π) β π§ β€ sup(ran π, β*, <
)) |
237 | 236 | ralrimiva 3144 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...πΏ)) β βπ§ β ran π π§ β€ sup(ran π, β*, <
)) |
238 | | brralrspcev 5170 |
. . . . . . . . . . . . 13
β’ ((sup(ran
π, β*,
< ) β β β§ βπ§ β ran π π§ β€ sup(ran π, β*, < )) β
βπ₯ β β
βπ§ β ran π π§ β€ π₯) |
239 | 223, 237,
238 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...πΏ)) β βπ₯ β β βπ§ β ran π π§ β€ π₯) |
240 | 205 | ffnd 6674 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...πΏ)) β π Fn β) |
241 | | breq1 5113 |
. . . . . . . . . . . . . . 15
β’ (π§ = (πβπ) β (π§ β€ π₯ β (πβπ) β€ π₯)) |
242 | 241 | ralrn 7043 |
. . . . . . . . . . . . . 14
β’ (π Fn β β
(βπ§ β ran π π§ β€ π₯ β βπ β β (πβπ) β€ π₯)) |
243 | 240, 242 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...πΏ)) β (βπ§ β ran π π§ β€ π₯ β βπ β β (πβπ) β€ π₯)) |
244 | 243 | rexbidv 3176 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...πΏ)) β (βπ₯ β β βπ§ β ran π π§ β€ π₯ β βπ₯ β β βπ β β (πβπ) β€ π₯)) |
245 | 239, 244 | mpbid 231 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...πΏ)) β βπ₯ β β βπ β β (πβπ) β€ π₯) |
246 | 69, 203, 224, 226, 233, 234, 245 | isumsup2 15738 |
. . . . . . . . . 10
β’ ((π β§ π β (1...πΏ)) β π β sup(ran π, β, < )) |
247 | 203, 246 | eqbrtrrid 5146 |
. . . . . . . . 9
β’ ((π β§ π β (1...πΏ)) β seq1( + , ((abs β β )
β (πΉβπ))) β sup(ran π, β, <
)) |
248 | | climrel 15381 |
. . . . . . . . . 10
β’ Rel
β |
249 | 248 | releldmi 5908 |
. . . . . . . . 9
β’ (seq1( +
, ((abs β β ) β (πΉβπ))) β sup(ran π, β, < ) β seq1( + , ((abs
β β ) β (πΉβπ))) β dom β ) |
250 | 247, 249 | syl 17 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β seq1( + , ((abs β β )
β (πΉβπ))) β dom β
) |
251 | 69, 224, 175, 187, 226, 233, 234, 250 | isumless 15737 |
. . . . . . 7
β’ ((π β§ π β (1...πΏ)) β Ξ£π β ((π½ β (1...πΎ)) β {π})((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β€ Ξ£π β β ((2nd
β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ)))) |
252 | 69, 203, 224, 226, 233, 234, 245 | isumsup 15739 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β Ξ£π β β ((2nd
β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) = sup(ran π, β, < )) |
253 | | rge0ssre 13380 |
. . . . . . . . . 10
β’
(0[,)+β) β β |
254 | 206, 253 | sstrdi 3961 |
. . . . . . . . 9
β’ ((π β§ π β (1...πΏ)) β ran π β β) |
255 | | 1nn 12171 |
. . . . . . . . . . . 12
β’ 1 β
β |
256 | 205 | fdmd 6684 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...πΏ)) β dom π = β) |
257 | 255, 256 | eleqtrrid 2845 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...πΏ)) β 1 β dom π) |
258 | 257 | ne0d 4300 |
. . . . . . . . . 10
β’ ((π β§ π β (1...πΏ)) β dom π β β
) |
259 | | dm0rn0 5885 |
. . . . . . . . . . 11
β’ (dom
π = β
β ran
π =
β
) |
260 | 259 | necon3bii 2997 |
. . . . . . . . . 10
β’ (dom
π β β
β ran
π β
β
) |
261 | 258, 260 | sylib 217 |
. . . . . . . . 9
β’ ((π β§ π β (1...πΏ)) β ran π β β
) |
262 | | supxrre 13253 |
. . . . . . . . 9
β’ ((ran
π β β β§ ran
π β β
β§
βπ₯ β β
βπ§ β ran π π§ β€ π₯) β sup(ran π, β*, < ) = sup(ran
π, β, <
)) |
263 | 254, 261,
239, 262 | syl3anc 1372 |
. . . . . . . 8
β’ ((π β§ π β (1...πΏ)) β sup(ran π, β*, < ) = sup(ran
π, β, <
)) |
264 | 252, 263 | eqtr4d 2780 |
. . . . . . 7
β’ ((π β§ π β (1...πΏ)) β Ξ£π β β ((2nd
β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) = sup(ran π, β*, <
)) |
265 | 251, 264 | breqtrd 5136 |
. . . . . 6
β’ ((π β§ π β (1...πΏ)) β Ξ£π β ((π½ β (1...πΎ)) β {π})((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β€ sup(ran π, β*, <
)) |
266 | 198, 223,
201, 265, 221 | letrd 11319 |
. . . . 5
β’ ((π β§ π β (1...πΏ)) β Ξ£π β ((π½ β (1...πΎ)) β {π})((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β€ ((vol*βπ΄) + (π΅ / (2βπ)))) |
267 | 92, 198, 201, 266 | fsumle 15691 |
. . . 4
β’ (π β Ξ£π β (1...πΏ)Ξ£π β ((π½ β (1...πΎ)) β {π})((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β€ Ξ£π β (1...πΏ)((vol*βπ΄) + (π΅ / (2βπ)))) |
268 | | vex 3452 |
. . . . . . . . . . 11
β’ π β V |
269 | 115, 268 | op1std 7936 |
. . . . . . . . . 10
β’ (π = β¨π, πβ© β (1st βπ) = π) |
270 | 269 | fveq2d 6851 |
. . . . . . . . 9
β’ (π = β¨π, πβ© β (πΉβ(1st βπ)) = (πΉβπ)) |
271 | 115, 268 | op2ndd 7937 |
. . . . . . . . 9
β’ (π = β¨π, πβ© β (2nd βπ) = π) |
272 | 270, 271 | fveq12d 6854 |
. . . . . . . 8
β’ (π = β¨π, πβ© β ((πΉβ(1st βπ))β(2nd
βπ)) = ((πΉβπ)βπ)) |
273 | 272 | fveq2d 6851 |
. . . . . . 7
β’ (π = β¨π, πβ© β (2nd β((πΉβ(1st
βπ))β(2nd βπ))) = (2nd
β((πΉβπ)βπ))) |
274 | 272 | fveq2d 6851 |
. . . . . . 7
β’ (π = β¨π, πβ© β (1st β((πΉβ(1st
βπ))β(2nd βπ))) = (1st
β((πΉβπ)βπ))) |
275 | 273, 274 | oveq12d 7380 |
. . . . . 6
β’ (π = β¨π, πβ© β ((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) =
((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ)))) |
276 | 196 | recnd 11190 |
. . . . . 6
β’ ((π β§ (π β (1...πΏ) β§ π β ((π½ β (1...πΎ)) β {π}))) β ((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) β β) |
277 | 275, 92, 175, 276 | fsum2d 15663 |
. . . . 5
β’ (π β Ξ£π β (1...πΏ)Ξ£π β ((π½ β (1...πΎ)) β {π})((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) = Ξ£π β βͺ
π β (1...πΏ)({π} Γ ((π½ β (1...πΎ)) β {π}))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ))))) |
278 | 164 | sumeq1d 15593 |
. . . . 5
β’ (π β Ξ£π β βͺ
π β (1...πΏ)({π} Γ ((π½ β (1...πΎ)) β {π}))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) = Ξ£π β (π½ β (1...πΎ))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ))))) |
279 | 277, 278 | eqtrd 2777 |
. . . 4
β’ (π β Ξ£π β (1...πΏ)Ξ£π β ((π½ β (1...πΎ)) β {π})((2nd β((πΉβπ)βπ)) β (1st β((πΉβπ)βπ))) = Ξ£π β (π½ β (1...πΎ))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ))))) |
280 | 95 | recnd 11190 |
. . . . 5
β’ ((π β§ π β (1...πΏ)) β (vol*βπ΄) β β) |
281 | 105 | recnd 11190 |
. . . . 5
β’ ((π β§ π β (1...πΏ)) β (π΅ / (2βπ)) β β) |
282 | 92, 280, 281 | fsumadd 15632 |
. . . 4
β’ (π β Ξ£π β (1...πΏ)((vol*βπ΄) + (π΅ / (2βπ))) = (Ξ£π β (1...πΏ)(vol*βπ΄) + Ξ£π β (1...πΏ)(π΅ / (2βπ)))) |
283 | 267, 279,
282 | 3brtr3d 5141 |
. . 3
β’ (π β Ξ£π β (π½ β (1...πΎ))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) β€
(Ξ£π β (1...πΏ)(vol*βπ΄) + Ξ£π β (1...πΏ)(π΅ / (2βπ)))) |
284 | | 1zzd 12541 |
. . . . . . . . 9
β’ (π β 1 β
β€) |
285 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β π β β) |
286 | | ovoliun.g |
. . . . . . . . . . . 12
β’ πΊ = (π β β β¦ (vol*βπ΄)) |
287 | 286 | fvmpt2 6964 |
. . . . . . . . . . 11
β’ ((π β β β§
(vol*βπ΄) β
β) β (πΊβπ) = (vol*βπ΄)) |
288 | 285, 94, 287 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (πΊβπ) = (vol*βπ΄)) |
289 | 288, 94 | eqeltrd 2838 |
. . . . . . . . 9
β’ ((π β§ π β β) β (πΊβπ) β β) |
290 | 69, 284, 289 | serfre 13944 |
. . . . . . . 8
β’ (π β seq1( + , πΊ):ββΆβ) |
291 | | ovoliun.t |
. . . . . . . . 9
β’ π = seq1( + , πΊ) |
292 | 291 | feq1i 6664 |
. . . . . . . 8
β’ (π:ββΆβ β
seq1( + , πΊ):ββΆβ) |
293 | 290, 292 | sylibr 233 |
. . . . . . 7
β’ (π β π:ββΆβ) |
294 | 293 | frnd 6681 |
. . . . . 6
β’ (π β ran π β β) |
295 | | ressxr 11206 |
. . . . . 6
β’ β
β β* |
296 | 294, 295 | sstrdi 3961 |
. . . . 5
β’ (π β ran π β
β*) |
297 | 93, 288 | sylan2 594 |
. . . . . . 7
β’ ((π β§ π β (1...πΏ)) β (πΊβπ) = (vol*βπ΄)) |
298 | | 1red 11163 |
. . . . . . . . . 10
β’ (π β 1 β
β) |
299 | | ffvelcdm 7037 |
. . . . . . . . . . . . 13
β’ ((π½:ββΆ(β Γ
β) β§ 1 β β) β (π½β1) β (β Γ
β)) |
300 | 20, 255, 299 | sylancl 587 |
. . . . . . . . . . . 12
β’ (π β (π½β1) β (β Γ
β)) |
301 | | xp1st 7958 |
. . . . . . . . . . . 12
β’ ((π½β1) β (β
Γ β) β (1st β(π½β1)) β β) |
302 | 300, 301 | syl 17 |
. . . . . . . . . . 11
β’ (π β (1st
β(π½β1)) β
β) |
303 | 302 | nnred 12175 |
. . . . . . . . . 10
β’ (π β (1st
β(π½β1)) β
β) |
304 | 142 | zred 12614 |
. . . . . . . . . 10
β’ (π β πΏ β β) |
305 | 302 | nnge1d 12208 |
. . . . . . . . . 10
β’ (π β 1 β€ (1st
β(π½β1))) |
306 | | 2fveq3 6852 |
. . . . . . . . . . . 12
β’ (π€ = 1 β (1st
β(π½βπ€)) = (1st
β(π½β1))) |
307 | 306 | breq1d 5120 |
. . . . . . . . . . 11
β’ (π€ = 1 β ((1st
β(π½βπ€)) β€ πΏ β (1st β(π½β1)) β€ πΏ)) |
308 | | eluzfz1 13455 |
. . . . . . . . . . . 12
β’ (πΎ β
(β€β₯β1) β 1 β (1...πΎ)) |
309 | 70, 308 | syl 17 |
. . . . . . . . . . 11
β’ (π β 1 β (1...πΎ)) |
310 | 307, 133,
309 | rspcdva 3585 |
. . . . . . . . . 10
β’ (π β (1st
β(π½β1)) β€
πΏ) |
311 | 298, 303,
304, 305, 310 | letrd 11319 |
. . . . . . . . 9
β’ (π β 1 β€ πΏ) |
312 | | elnnz1 12536 |
. . . . . . . . 9
β’ (πΏ β β β (πΏ β β€ β§ 1 β€
πΏ)) |
313 | 142, 311,
312 | sylanbrc 584 |
. . . . . . . 8
β’ (π β πΏ β β) |
314 | 313, 69 | eleqtrdi 2848 |
. . . . . . 7
β’ (π β πΏ β
(β€β₯β1)) |
315 | 297, 314,
280 | fsumser 15622 |
. . . . . 6
β’ (π β Ξ£π β (1...πΏ)(vol*βπ΄) = (seq1( + , πΊ)βπΏ)) |
316 | | seqfn 13925 |
. . . . . . . . 9
β’ (1 β
β€ β seq1( + , πΊ)
Fn (β€β₯β1)) |
317 | 284, 316 | syl 17 |
. . . . . . . 8
β’ (π β seq1( + , πΊ) Fn
(β€β₯β1)) |
318 | | fnfvelrn 7036 |
. . . . . . . 8
β’ ((seq1( +
, πΊ) Fn
(β€β₯β1) β§ πΏ β (β€β₯β1))
β (seq1( + , πΊ)βπΏ) β ran seq1( + , πΊ)) |
319 | 317, 314,
318 | syl2anc 585 |
. . . . . . 7
β’ (π β (seq1( + , πΊ)βπΏ) β ran seq1( + , πΊ)) |
320 | 291 | rneqi 5897 |
. . . . . . 7
β’ ran π = ran seq1( + , πΊ) |
321 | 319, 320 | eleqtrrdi 2849 |
. . . . . 6
β’ (π β (seq1( + , πΊ)βπΏ) β ran π) |
322 | 315, 321 | eqeltrd 2838 |
. . . . 5
β’ (π β Ξ£π β (1...πΏ)(vol*βπ΄) β ran π) |
323 | | supxrub 13250 |
. . . . 5
β’ ((ran
π β
β* β§ Ξ£π β (1...πΏ)(vol*βπ΄) β ran π) β Ξ£π β (1...πΏ)(vol*βπ΄) β€ sup(ran π, β*, <
)) |
324 | 296, 322,
323 | syl2anc 585 |
. . . 4
β’ (π β Ξ£π β (1...πΏ)(vol*βπ΄) β€ sup(ran π, β*, <
)) |
325 | 98 | recnd 11190 |
. . . . . 6
β’ (π β π΅ β β) |
326 | | geo2sum 15765 |
. . . . . 6
β’ ((πΏ β β β§ π΅ β β) β
Ξ£π β (1...πΏ)(π΅ / (2βπ)) = (π΅ β (π΅ / (2βπΏ)))) |
327 | 313, 325,
326 | syl2anc 585 |
. . . . 5
β’ (π β Ξ£π β (1...πΏ)(π΅ / (2βπ)) = (π΅ β (π΅ / (2βπΏ)))) |
328 | 313 | nnnn0d 12480 |
. . . . . . . . . 10
β’ (π β πΏ β
β0) |
329 | | nnexpcl 13987 |
. . . . . . . . . 10
β’ ((2
β β β§ πΏ
β β0) β (2βπΏ) β β) |
330 | 99, 328, 329 | sylancr 588 |
. . . . . . . . 9
β’ (π β (2βπΏ) β β) |
331 | 330 | nnrpd 12962 |
. . . . . . . 8
β’ (π β (2βπΏ) β
β+) |
332 | 97, 331 | rpdivcld 12981 |
. . . . . . 7
β’ (π β (π΅ / (2βπΏ)) β
β+) |
333 | 332 | rpge0d 12968 |
. . . . . 6
β’ (π β 0 β€ (π΅ / (2βπΏ))) |
334 | 98, 330 | nndivred 12214 |
. . . . . . 7
β’ (π β (π΅ / (2βπΏ)) β β) |
335 | 98, 334 | subge02d 11754 |
. . . . . 6
β’ (π β (0 β€ (π΅ / (2βπΏ)) β (π΅ β (π΅ / (2βπΏ))) β€ π΅)) |
336 | 333, 335 | mpbid 231 |
. . . . 5
β’ (π β (π΅ β (π΅ / (2βπΏ))) β€ π΅) |
337 | 327, 336 | eqbrtrd 5132 |
. . . 4
β’ (π β Ξ£π β (1...πΏ)(π΅ / (2βπ)) β€ π΅) |
338 | 96, 106, 108, 98, 324, 337 | le2addd 11781 |
. . 3
β’ (π β (Ξ£π β (1...πΏ)(vol*βπ΄) + Ξ£π β (1...πΏ)(π΅ / (2βπ))) β€ (sup(ran π, β*, < ) + π΅)) |
339 | 91, 107, 109, 283, 338 | letrd 11319 |
. 2
β’ (π β Ξ£π β (π½ β (1...πΎ))((2nd β((πΉβ(1st
βπ))β(2nd βπ))) β (1st
β((πΉβ(1st βπ))β(2nd
βπ)))) β€ (sup(ran
π, β*,
< ) + π΅)) |
340 | 85, 339 | eqbrtrrd 5134 |
1
β’ (π β (πβπΎ) β€ (sup(ran π, β*, < ) + π΅)) |