Step | Hyp | Ref
| Expression |
1 | | inss1 4189 |
. . 3
β’ (πΎ β© π΄) β πΎ |
2 | | uniioombl.k |
. . . . 5
β’ πΎ = βͺ
(((,) β πΊ) β
(1...π)) |
3 | | imassrn 6025 |
. . . . . 6
β’ (((,)
β πΊ) β
(1...π)) β ran ((,)
β πΊ) |
4 | 3 | unissi 4875 |
. . . . 5
β’ βͺ (((,) β πΊ) β (1...π)) β βͺ ran
((,) β πΊ) |
5 | 2, 4 | eqsstri 3979 |
. . . 4
β’ πΎ β βͺ ran ((,) β πΊ) |
6 | | uniioombl.g |
. . . . . . 7
β’ (π β πΊ:ββΆ( β€ β© (β
Γ β))) |
7 | 6 | uniiccdif 24958 |
. . . . . 6
β’ (π β (βͺ ran ((,) β πΊ) β βͺ ran
([,] β πΊ) β§
(vol*β(βͺ ran ([,] β πΊ) β βͺ ran
((,) β πΊ))) =
0)) |
8 | 7 | simpld 496 |
. . . . 5
β’ (π β βͺ ran ((,) β πΊ) β βͺ ran
([,] β πΊ)) |
9 | | ovolficcss 24849 |
. . . . . 6
β’ (πΊ:ββΆ( β€ β©
(β Γ β)) β βͺ ran ([,] β
πΊ) β
β) |
10 | 6, 9 | syl 17 |
. . . . 5
β’ (π β βͺ ran ([,] β πΊ) β β) |
11 | 8, 10 | sstrd 3955 |
. . . 4
β’ (π β βͺ ran ((,) β πΊ) β β) |
12 | 5, 11 | sstrid 3956 |
. . 3
β’ (π β πΎ β β) |
13 | | uniioombl.1 |
. . . . . 6
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
14 | | uniioombl.2 |
. . . . . 6
β’ (π β Disj π₯ β β
((,)β(πΉβπ₯))) |
15 | | uniioombl.3 |
. . . . . 6
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
16 | | uniioombl.a |
. . . . . 6
β’ π΄ = βͺ
ran ((,) β πΉ) |
17 | | uniioombl.e |
. . . . . 6
β’ (π β (vol*βπΈ) β
β) |
18 | | uniioombl.c |
. . . . . 6
β’ (π β πΆ β
β+) |
19 | | uniioombl.s |
. . . . . 6
β’ (π β πΈ β βͺ ran
((,) β πΊ)) |
20 | | uniioombl.t |
. . . . . 6
β’ π = seq1( + , ((abs β
β ) β πΊ)) |
21 | | uniioombl.v |
. . . . . 6
β’ (π β sup(ran π, β*, < ) β€
((vol*βπΈ) + πΆ)) |
22 | 13, 14, 15, 16, 17, 18, 6, 19, 20, 21 | uniioombllem1 24961 |
. . . . 5
β’ (π β sup(ran π, β*, < ) β
β) |
23 | | ssid 3967 |
. . . . . 6
β’ βͺ ran ((,) β πΊ) β βͺ ran
((,) β πΊ) |
24 | 20 | ovollb 24859 |
. . . . . 6
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ βͺ ran ((,) β
πΊ) β βͺ ran ((,) β πΊ)) β (vol*ββͺ ran ((,) β πΊ)) β€ sup(ran π, β*, <
)) |
25 | 6, 23, 24 | sylancl 587 |
. . . . 5
β’ (π β (vol*ββͺ ran ((,) β πΊ)) β€ sup(ran π, β*, <
)) |
26 | | ovollecl 24863 |
. . . . 5
β’ ((βͺ ran ((,) β πΊ) β β β§ sup(ran π, β*, < )
β β β§ (vol*ββͺ ran ((,) β
πΊ)) β€ sup(ran π, β*, < ))
β (vol*ββͺ ran ((,) β πΊ)) β
β) |
27 | 11, 22, 25, 26 | syl3anc 1372 |
. . . 4
β’ (π β (vol*ββͺ ran ((,) β πΊ)) β β) |
28 | | ovolsscl 24866 |
. . . 4
β’ ((πΎ β βͺ ran ((,) β πΊ) β§ βͺ ran
((,) β πΊ) β
β β§ (vol*ββͺ ran ((,) β πΊ)) β β) β
(vol*βπΎ) β
β) |
29 | 5, 11, 27, 28 | mp3an2i 1467 |
. . 3
β’ (π β (vol*βπΎ) β
β) |
30 | | ovolsscl 24866 |
. . 3
β’ (((πΎ β© π΄) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*β(πΎ β© π΄)) β
β) |
31 | 1, 12, 29, 30 | mp3an2i 1467 |
. 2
β’ (π β (vol*β(πΎ β© π΄)) β β) |
32 | | inss1 4189 |
. . . 4
β’ (πΎ β© πΏ) β πΎ |
33 | | ovolsscl 24866 |
. . . 4
β’ (((πΎ β© πΏ) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*β(πΎ β© πΏ)) β
β) |
34 | 32, 12, 29, 33 | mp3an2i 1467 |
. . 3
β’ (π β (vol*β(πΎ β© πΏ)) β β) |
35 | | ssun2 4134 |
. . . . . 6
β’ βͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β ((πΎ β© πΏ) βͺ βͺ
π β (1...π)βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) |
36 | | nnuz 12811 |
. . . . . . . . . . . . . 14
β’ β =
(β€β₯β1) |
37 | | uniioombl.n |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
38 | 37 | peano2nnd 12175 |
. . . . . . . . . . . . . . . 16
β’ (π β (π + 1) β β) |
39 | 38, 36 | eleqtrdi 2844 |
. . . . . . . . . . . . . . 15
β’ (π β (π + 1) β
(β€β₯β1)) |
40 | | uzsplit 13519 |
. . . . . . . . . . . . . . 15
β’ ((π + 1) β
(β€β₯β1) β (β€β₯β1) =
((1...((π + 1) β 1))
βͺ (β€β₯β(π + 1)))) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β1) = ((1...((π + 1) β 1)) βͺ
(β€β₯β(π + 1)))) |
42 | 36, 41 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ (π β β = ((1...((π + 1) β 1)) βͺ
(β€β₯β(π + 1)))) |
43 | 37 | nncnd 12174 |
. . . . . . . . . . . . . . . 16
β’ (π β π β β) |
44 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . 16
β’ 1 β
β |
45 | | pncan 11412 |
. . . . . . . . . . . . . . . 16
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
46 | 43, 44, 45 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β ((π + 1) β 1) = π) |
47 | 46 | oveq2d 7374 |
. . . . . . . . . . . . . 14
β’ (π β (1...((π + 1) β 1)) = (1...π)) |
48 | 47 | uneq1d 4123 |
. . . . . . . . . . . . 13
β’ (π β ((1...((π + 1) β 1)) βͺ
(β€β₯β(π + 1))) = ((1...π) βͺ (β€β₯β(π + 1)))) |
49 | 42, 48 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (π β β = ((1...π) βͺ
(β€β₯β(π + 1)))) |
50 | 49 | iuneq1d 4982 |
. . . . . . . . . . 11
β’ (π β βͺ π β β ((,)β(πΉβπ)) = βͺ
π β ((1...π) βͺ
(β€β₯β(π + 1)))((,)β(πΉβπ))) |
51 | | iunxun 5055 |
. . . . . . . . . . 11
β’ βͺ π β ((1...π) βͺ (β€β₯β(π + 1)))((,)β(πΉβπ)) = (βͺ
π β (1...π)((,)β(πΉβπ)) βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) |
52 | 50, 51 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π β βͺ π β β ((,)β(πΉβπ)) = (βͺ
π β (1...π)((,)β(πΉβπ)) βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) |
53 | | ioof 13370 |
. . . . . . . . . . . . . 14
β’
(,):(β* Γ β*)βΆπ«
β |
54 | | inss2 4190 |
. . . . . . . . . . . . . . . 16
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
55 | | rexpssxrxp 11205 |
. . . . . . . . . . . . . . . 16
β’ (β
Γ β) β (β* Γ
β*) |
56 | 54, 55 | sstri 3954 |
. . . . . . . . . . . . . . 15
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
57 | | fss 6686 |
. . . . . . . . . . . . . . 15
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΉ:ββΆ(β* Γ
β*)) |
58 | 13, 56, 57 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (π β πΉ:ββΆ(β* Γ
β*)) |
59 | | fco 6693 |
. . . . . . . . . . . . . 14
β’
(((,):(β* Γ β*)βΆπ«
β β§ πΉ:ββΆ(β* Γ
β*)) β ((,) β πΉ):ββΆπ«
β) |
60 | 53, 58, 59 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π β ((,) β πΉ):ββΆπ«
β) |
61 | | ffn 6669 |
. . . . . . . . . . . . 13
β’ (((,)
β πΉ):ββΆπ« β β
((,) β πΉ) Fn
β) |
62 | | fniunfv 7195 |
. . . . . . . . . . . . 13
β’ (((,)
β πΉ) Fn β
β βͺ π β β (((,) β πΉ)βπ) = βͺ ran ((,)
β πΉ)) |
63 | 60, 61, 62 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β βͺ π β β (((,) β πΉ)βπ) = βͺ ran ((,)
β πΉ)) |
64 | | fvco3 6941 |
. . . . . . . . . . . . . 14
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (((,) β πΉ)βπ) = ((,)β(πΉβπ))) |
65 | 13, 64 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (((,) β πΉ)βπ) = ((,)β(πΉβπ))) |
66 | 65 | iuneq2dv 4979 |
. . . . . . . . . . . 12
β’ (π β βͺ π β β (((,) β πΉ)βπ) = βͺ π β β
((,)β(πΉβπ))) |
67 | 63, 66 | eqtr3d 2775 |
. . . . . . . . . . 11
β’ (π β βͺ ran ((,) β πΉ) = βͺ
π β β
((,)β(πΉβπ))) |
68 | 16, 67 | eqtrid 2785 |
. . . . . . . . . 10
β’ (π β π΄ = βͺ π β β
((,)β(πΉβπ))) |
69 | | uniioombl.l |
. . . . . . . . . . . 12
β’ πΏ = βͺ
(((,) β πΉ) β
(1...π)) |
70 | | ffun 6672 |
. . . . . . . . . . . . . 14
β’ (((,)
β πΉ):ββΆπ« β β
Fun ((,) β πΉ)) |
71 | | funiunfv 7196 |
. . . . . . . . . . . . . 14
β’ (Fun ((,)
β πΉ) β βͺ π β (1...π)(((,) β πΉ)βπ) = βͺ (((,)
β πΉ) β
(1...π))) |
72 | 60, 70, 71 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β βͺ π β (1...π)(((,) β πΉ)βπ) = βͺ (((,)
β πΉ) β
(1...π))) |
73 | | elfznn 13476 |
. . . . . . . . . . . . . . 15
β’ (π β (1...π) β π β β) |
74 | 13, 73, 64 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (((,) β πΉ)βπ) = ((,)β(πΉβπ))) |
75 | 74 | iuneq2dv 4979 |
. . . . . . . . . . . . 13
β’ (π β βͺ π β (1...π)(((,) β πΉ)βπ) = βͺ π β (1...π)((,)β(πΉβπ))) |
76 | 72, 75 | eqtr3d 2775 |
. . . . . . . . . . . 12
β’ (π β βͺ (((,) β πΉ) β (1...π)) = βͺ
π β (1...π)((,)β(πΉβπ))) |
77 | 69, 76 | eqtrid 2785 |
. . . . . . . . . . 11
β’ (π β πΏ = βͺ π β (1...π)((,)β(πΉβπ))) |
78 | 77 | uneq1d 4123 |
. . . . . . . . . 10
β’ (π β (πΏ βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = (βͺ
π β (1...π)((,)β(πΉβπ)) βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) |
79 | 52, 68, 78 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ (π β π΄ = (πΏ βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) |
80 | 79 | ineq2d 4173 |
. . . . . . . 8
β’ (π β (πΎ β© π΄) = (πΎ β© (πΏ βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))))) |
81 | | indi 4234 |
. . . . . . . 8
β’ (πΎ β© (πΏ βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) = ((πΎ β© πΏ) βͺ (πΎ β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) |
82 | 80, 81 | eqtrdi 2789 |
. . . . . . 7
β’ (π β (πΎ β© π΄) = ((πΎ β© πΏ) βͺ (πΎ β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))))) |
83 | | fss 6686 |
. . . . . . . . . . . . . . 15
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΊ:ββΆ(β* Γ
β*)) |
84 | 6, 56, 83 | sylancl 587 |
. . . . . . . . . . . . . 14
β’ (π β πΊ:ββΆ(β* Γ
β*)) |
85 | | fco 6693 |
. . . . . . . . . . . . . 14
β’
(((,):(β* Γ β*)βΆπ«
β β§ πΊ:ββΆ(β* Γ
β*)) β ((,) β πΊ):ββΆπ«
β) |
86 | 53, 84, 85 | sylancr 588 |
. . . . . . . . . . . . 13
β’ (π β ((,) β πΊ):ββΆπ«
β) |
87 | | ffun 6672 |
. . . . . . . . . . . . 13
β’ (((,)
β πΊ):ββΆπ« β β
Fun ((,) β πΊ)) |
88 | | funiunfv 7196 |
. . . . . . . . . . . . 13
β’ (Fun ((,)
β πΊ) β βͺ π β (1...π)(((,) β πΊ)βπ) = βͺ (((,)
β πΊ) β
(1...π))) |
89 | 86, 87, 88 | 3syl 18 |
. . . . . . . . . . . 12
β’ (π β βͺ π β (1...π)(((,) β πΊ)βπ) = βͺ (((,)
β πΊ) β
(1...π))) |
90 | | elfznn 13476 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β π β β) |
91 | | fvco3 6941 |
. . . . . . . . . . . . . 14
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (((,) β πΊ)βπ) = ((,)β(πΊβπ))) |
92 | 6, 90, 91 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (((,) β πΊ)βπ) = ((,)β(πΊβπ))) |
93 | 92 | iuneq2dv 4979 |
. . . . . . . . . . . 12
β’ (π β βͺ π β (1...π)(((,) β πΊ)βπ) = βͺ π β (1...π)((,)β(πΊβπ))) |
94 | 89, 93 | eqtr3d 2775 |
. . . . . . . . . . 11
β’ (π β βͺ (((,) β πΊ) β (1...π)) = βͺ
π β (1...π)((,)β(πΊβπ))) |
95 | 2, 94 | eqtrid 2785 |
. . . . . . . . . 10
β’ (π β πΎ = βͺ π β (1...π)((,)β(πΊβπ))) |
96 | 95 | ineq2d 4173 |
. . . . . . . . 9
β’ (π β (βͺ π β (β€β₯β(π + 1))((,)β(πΉβπ)) β© πΎ) = (βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)) β© βͺ
π β (1...π)((,)β(πΊβπ)))) |
97 | | incom 4162 |
. . . . . . . . 9
β’ (πΎ β© βͺ π β (β€β₯β(π + 1))((,)β(πΉβπ))) = (βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)) β© πΎ) |
98 | | iunin2 5032 |
. . . . . . . . . . . . 13
β’ βͺ π β (β€β₯β(π + 1))(((,)β(πΊβπ)) β© ((,)β(πΉβπ))) = (((,)β(πΊβπ)) β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) |
99 | | incom 4162 |
. . . . . . . . . . . . . . 15
β’
(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = (((,)β(πΊβπ)) β© ((,)β(πΉβπ))) |
100 | 99 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β
(β€β₯β(π + 1)) β (((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = (((,)β(πΊβπ)) β© ((,)β(πΉβπ)))) |
101 | 100 | iuneq2i 4976 |
. . . . . . . . . . . . 13
β’ βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = βͺ
π β
(β€β₯β(π + 1))(((,)β(πΊβπ)) β© ((,)β(πΉβπ))) |
102 | | incom 4162 |
. . . . . . . . . . . . 13
β’ (βͺ π β (β€β₯β(π + 1))((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = (((,)β(πΊβπ)) β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) |
103 | 98, 101, 102 | 3eqtr4ri 2772 |
. . . . . . . . . . . 12
β’ (βͺ π β (β€β₯β(π + 1))((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = βͺ
π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) |
104 | 103 | a1i 11 |
. . . . . . . . . . 11
β’ (π β (1...π) β (βͺ π β (β€β₯β(π + 1))((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = βͺ
π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) |
105 | 104 | iuneq2i 4976 |
. . . . . . . . . 10
β’ βͺ π β (1...π)(βͺ π β
(β€β₯β(π + 1))((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = βͺ
π β (1...π)βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) |
106 | | iunin2 5032 |
. . . . . . . . . 10
β’ βͺ π β (1...π)(βͺ π β
(β€β₯β(π + 1))((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = (βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)) β© βͺ
π β (1...π)((,)β(πΊβπ))) |
107 | 105, 106 | eqtr3i 2763 |
. . . . . . . . 9
β’ βͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = (βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)) β© βͺ
π β (1...π)((,)β(πΊβπ))) |
108 | 96, 97, 107 | 3eqtr4g 2798 |
. . . . . . . 8
β’ (π β (πΎ β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = βͺ
π β (1...π)βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) |
109 | 108 | uneq2d 4124 |
. . . . . . 7
β’ (π β ((πΎ β© πΏ) βͺ (πΎ β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) = ((πΎ β© πΏ) βͺ βͺ
π β (1...π)βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
110 | 82, 109 | eqtrd 2773 |
. . . . . 6
β’ (π β (πΎ β© π΄) = ((πΎ β© πΏ) βͺ βͺ
π β (1...π)βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
111 | 35, 110 | sseqtrrid 3998 |
. . . . 5
β’ (π β βͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β (πΎ β© π΄)) |
112 | 111, 1 | sstrdi 3957 |
. . . 4
β’ (π β βͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β πΎ) |
113 | | ovolsscl 24866 |
. . . 4
β’
((βͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) |
114 | 112, 12, 29, 113 | syl3anc 1372 |
. . 3
β’ (π β (vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) |
115 | 34, 114 | readdcld 11189 |
. 2
β’ (π β ((vol*β(πΎ β© πΏ)) + (vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) β β) |
116 | 18 | rpred 12962 |
. . 3
β’ (π β πΆ β β) |
117 | 34, 116 | readdcld 11189 |
. 2
β’ (π β ((vol*β(πΎ β© πΏ)) + πΆ) β β) |
118 | 110 | fveq2d 6847 |
. . 3
β’ (π β (vol*β(πΎ β© π΄)) = (vol*β((πΎ β© πΏ) βͺ βͺ
π β (1...π)βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))))) |
119 | 32, 12 | sstrid 3956 |
. . . 4
β’ (π β (πΎ β© πΏ) β β) |
120 | 112, 12 | sstrd 3955 |
. . . 4
β’ (π β βͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β β) |
121 | | ovolun 24879 |
. . . 4
β’ ((((πΎ β© πΏ) β β β§ (vol*β(πΎ β© πΏ)) β β) β§ (βͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β β β§
(vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β)) β
(vol*β((πΎ β© πΏ) βͺ βͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) β€ ((vol*β(πΎ β© πΏ)) + (vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))))) |
122 | 119, 34, 120, 114, 121 | syl22anc 838 |
. . 3
β’ (π β (vol*β((πΎ β© πΏ) βͺ βͺ
π β (1...π)βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) β€ ((vol*β(πΎ β© πΏ)) + (vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))))) |
123 | 118, 122 | eqbrtrd 5128 |
. 2
β’ (π β (vol*β(πΎ β© π΄)) β€ ((vol*β(πΎ β© πΏ)) + (vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))))) |
124 | | fzfid 13884 |
. . . . 5
β’ (π β (1...π) β Fin) |
125 | | iunss 5006 |
. . . . . . . 8
β’ (βͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β πΎ β βπ β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β πΎ) |
126 | 112, 125 | sylib 217 |
. . . . . . 7
β’ (π β βπ β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β πΎ) |
127 | 126 | r19.21bi 3233 |
. . . . . 6
β’ ((π β§ π β (1...π)) β βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β πΎ) |
128 | 12 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (1...π)) β πΎ β β) |
129 | 29 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (vol*βπΎ) β β) |
130 | | ovolsscl 24866 |
. . . . . 6
β’
((βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) |
131 | 127, 128,
129, 130 | syl3anc 1372 |
. . . . 5
β’ ((π β§ π β (1...π)) β (vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) |
132 | 124, 131 | fsumrecl 15624 |
. . . 4
β’ (π β Ξ£π β (1...π)(vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) |
133 | 127, 128 | sstrd 3955 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β β) |
134 | 133, 131 | jca 513 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β β β§
(vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β)) |
135 | 134 | ralrimiva 3140 |
. . . . 5
β’ (π β βπ β (1...π)(βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β β β§
(vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β)) |
136 | | ovolfiniun 24881 |
. . . . 5
β’
(((1...π) β Fin
β§ βπ β
(1...π)(βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β β β§
(vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β)) β
(vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β€ Ξ£π β (1...π)(vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
137 | 124, 135,
136 | syl2anc 585 |
. . . 4
β’ (π β (vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β€ Ξ£π β (1...π)(vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
138 | | uniioombl.m |
. . . . . . . 8
β’ (π β π β β) |
139 | 116, 138 | nndivred 12212 |
. . . . . . 7
β’ (π β (πΆ / π) β β) |
140 | 139 | adantr 482 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (πΆ / π) β β) |
141 | 77 | ineq2d 4173 |
. . . . . . . . . . . . 13
β’ (π β (((,)β(πΊβπ)) β© πΏ) = (((,)β(πΊβπ)) β© βͺ
π β (1...π)((,)β(πΉβπ)))) |
142 | 141 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (((,)β(πΊβπ)) β© πΏ) = (((,)β(πΊβπ)) β© βͺ
π β (1...π)((,)β(πΉβπ)))) |
143 | 99 | a1i 11 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β (((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = (((,)β(πΊβπ)) β© ((,)β(πΉβπ)))) |
144 | 143 | iuneq2i 4976 |
. . . . . . . . . . . . 13
β’ βͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = βͺ
π β (1...π)(((,)β(πΊβπ)) β© ((,)β(πΉβπ))) |
145 | | iunin2 5032 |
. . . . . . . . . . . . 13
β’ βͺ π β (1...π)(((,)β(πΊβπ)) β© ((,)β(πΉβπ))) = (((,)β(πΊβπ)) β© βͺ
π β (1...π)((,)β(πΉβπ))) |
146 | 144, 145 | eqtri 2761 |
. . . . . . . . . . . 12
β’ βͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = (((,)β(πΊβπ)) β© βͺ
π β (1...π)((,)β(πΉβπ))) |
147 | 142, 146 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (((,)β(πΊβπ)) β© πΏ) = βͺ
π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) |
148 | | fzfid 13884 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (1...π) β Fin) |
149 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΉ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΉβπ) β ( β€ β© (β Γ
β))) |
150 | 13, 73, 149 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...π)) β (πΉβπ) β ( β€ β© (β Γ
β))) |
151 | 150 | elin2d 4160 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (1...π)) β (πΉβπ) β (β Γ
β)) |
152 | | 1st2nd2 7961 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΉβπ) β (β Γ β) β
(πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β (πΉβπ) = β¨(1st β(πΉβπ)), (2nd β(πΉβπ))β©) |
154 | 153 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β ((,)β(πΉβπ)) = ((,)ββ¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β©)) |
155 | | df-ov 7361 |
. . . . . . . . . . . . . . . . 17
β’
((1st β(πΉβπ))(,)(2nd β(πΉβπ))) = ((,)ββ¨(1st
β(πΉβπ)), (2nd
β(πΉβπ))β©) |
156 | 154, 155 | eqtr4di 2791 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β ((,)β(πΉβπ)) = ((1st β(πΉβπ))(,)(2nd β(πΉβπ)))) |
157 | | ioombl 24945 |
. . . . . . . . . . . . . . . 16
β’
((1st β(πΉβπ))(,)(2nd β(πΉβπ))) β dom vol |
158 | 156, 157 | eqeltrdi 2842 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((,)β(πΉβπ)) β dom vol) |
159 | 158 | adantlr 714 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π)) β§ π β (1...π)) β ((,)β(πΉβπ)) β dom vol) |
160 | | ffvelcdm 7033 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΊβπ) β ( β€ β© (β Γ
β))) |
161 | 6, 90, 160 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...π)) β (πΊβπ) β ( β€ β© (β Γ
β))) |
162 | 161 | elin2d 4160 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β (1...π)) β (πΊβπ) β (β Γ
β)) |
163 | | 1st2nd2 7961 |
. . . . . . . . . . . . . . . . . . 19
β’ ((πΊβπ) β (β Γ β) β
(πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
164 | 162, 163 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β (1...π)) β (πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
165 | 164 | fveq2d 6847 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) = ((,)ββ¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©)) |
166 | | df-ov 7361 |
. . . . . . . . . . . . . . . . 17
β’
((1st β(πΊβπ))(,)(2nd β(πΊβπ))) = ((,)ββ¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©) |
167 | 165, 166 | eqtr4di 2791 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) = ((1st β(πΊβπ))(,)(2nd β(πΊβπ)))) |
168 | | ioombl 24945 |
. . . . . . . . . . . . . . . 16
β’
((1st β(πΊβπ))(,)(2nd β(πΊβπ))) β dom vol |
169 | 167, 168 | eqeltrdi 2842 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) β dom vol) |
170 | 169 | adantr 482 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π)) β§ π β (1...π)) β ((,)β(πΊβπ)) β dom vol) |
171 | | inmbl 24922 |
. . . . . . . . . . . . . 14
β’
((((,)β(πΉβπ)) β dom vol β§ ((,)β(πΊβπ)) β dom vol) β (((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol) |
172 | 159, 170,
171 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ π β (1...π)) β (((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol) |
173 | 172 | ralrimiva 3140 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β βπ β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol) |
174 | | finiunmbl 24924 |
. . . . . . . . . . . 12
β’
(((1...π) β Fin
β§ βπ β
(1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol) β βͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol) |
175 | 148, 173,
174 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β βͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol) |
176 | 147, 175 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (((,)β(πΊβπ)) β© πΏ) β dom vol) |
177 | | inss2 4190 |
. . . . . . . . . . 11
β’
(((,)β(πΊβπ)) β© π΄) β π΄ |
178 | 13 | uniiccdif 24958 |
. . . . . . . . . . . . . . 15
β’ (π β (βͺ ran ((,) β πΉ) β βͺ ran
([,] β πΉ) β§
(vol*β(βͺ ran ([,] β πΉ) β βͺ ran
((,) β πΉ))) =
0)) |
179 | 178 | simpld 496 |
. . . . . . . . . . . . . 14
β’ (π β βͺ ran ((,) β πΉ) β βͺ ran
([,] β πΉ)) |
180 | | ovolficcss 24849 |
. . . . . . . . . . . . . . 15
β’ (πΉ:ββΆ( β€ β©
(β Γ β)) β βͺ ran ([,] β
πΉ) β
β) |
181 | 13, 180 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β βͺ ran ([,] β πΉ) β β) |
182 | 179, 181 | sstrd 3955 |
. . . . . . . . . . . . 13
β’ (π β βͺ ran ((,) β πΉ) β β) |
183 | 16, 182 | eqsstrid 3993 |
. . . . . . . . . . . 12
β’ (π β π΄ β β) |
184 | 183 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β π΄ β β) |
185 | 177, 184 | sstrid 3956 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (((,)β(πΊβπ)) β© π΄) β β) |
186 | | inss1 4189 |
. . . . . . . . . . 11
β’
(((,)β(πΊβπ)) β© π΄) β ((,)β(πΊβπ)) |
187 | | ioossre 13331 |
. . . . . . . . . . . 12
β’
((1st β(πΊβπ))(,)(2nd β(πΊβπ))) β β |
188 | 167, 187 | eqsstrdi 3999 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) β β) |
189 | 167 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) = (vol*β((1st
β(πΊβπ))(,)(2nd
β(πΊβπ))))) |
190 | | ovolfcl 24846 |
. . . . . . . . . . . . . . 15
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ((1st
β(πΊβπ)) β β β§
(2nd β(πΊβπ)) β β β§ (1st
β(πΊβπ)) β€ (2nd
β(πΊβπ)))) |
191 | 6, 90, 190 | syl2an 597 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β ((1st β(πΊβπ)) β β β§ (2nd
β(πΊβπ)) β β β§
(1st β(πΊβπ)) β€ (2nd β(πΊβπ)))) |
192 | | ovolioo 24948 |
. . . . . . . . . . . . . 14
β’
(((1st β(πΊβπ)) β β β§ (2nd
β(πΊβπ)) β β β§
(1st β(πΊβπ)) β€ (2nd β(πΊβπ))) β (vol*β((1st
β(πΊβπ))(,)(2nd
β(πΊβπ)))) = ((2nd
β(πΊβπ)) β (1st
β(πΊβπ)))) |
193 | 191, 192 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (vol*β((1st
β(πΊβπ))(,)(2nd
β(πΊβπ)))) = ((2nd
β(πΊβπ)) β (1st
β(πΊβπ)))) |
194 | 189, 193 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) = ((2nd β(πΊβπ)) β (1st β(πΊβπ)))) |
195 | 191 | simp2d 1144 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (2nd β(πΊβπ)) β β) |
196 | 191 | simp1d 1143 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (1st β(πΊβπ)) β β) |
197 | 195, 196 | resubcld 11588 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
198 | 194, 197 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) β β) |
199 | | ovolsscl 24866 |
. . . . . . . . . . 11
β’
(((((,)β(πΊβπ)) β© π΄) β ((,)β(πΊβπ)) β§ ((,)β(πΊβπ)) β β β§
(vol*β((,)β(πΊβπ))) β β) β
(vol*β(((,)β(πΊβπ)) β© π΄)) β β) |
200 | 186, 188,
198, 199 | mp3an2i 1467 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (vol*β(((,)β(πΊβπ)) β© π΄)) β β) |
201 | | mblsplit 24912 |
. . . . . . . . . 10
β’
(((((,)β(πΊβπ)) β© πΏ) β dom vol β§ (((,)β(πΊβπ)) β© π΄) β β β§
(vol*β(((,)β(πΊβπ)) β© π΄)) β β) β
(vol*β(((,)β(πΊβπ)) β© π΄)) = ((vol*β((((,)β(πΊβπ)) β© π΄) β© (((,)β(πΊβπ)) β© πΏ))) + (vol*β((((,)β(πΊβπ)) β© π΄) β (((,)β(πΊβπ)) β© πΏ))))) |
202 | 176, 185,
200, 201 | syl3anc 1372 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (vol*β(((,)β(πΊβπ)) β© π΄)) = ((vol*β((((,)β(πΊβπ)) β© π΄) β© (((,)β(πΊβπ)) β© πΏ))) + (vol*β((((,)β(πΊβπ)) β© π΄) β (((,)β(πΊβπ)) β© πΏ))))) |
203 | | imassrn 6025 |
. . . . . . . . . . . . . . 15
β’ (((,)
β πΉ) β
(1...π)) β ran ((,)
β πΉ) |
204 | 203 | unissi 4875 |
. . . . . . . . . . . . . 14
β’ βͺ (((,) β πΉ) β (1...π)) β βͺ ran
((,) β πΉ) |
205 | 204, 69, 16 | 3sstr4i 3988 |
. . . . . . . . . . . . 13
β’ πΏ β π΄ |
206 | | sslin 4195 |
. . . . . . . . . . . . 13
β’ (πΏ β π΄ β (((,)β(πΊβπ)) β© πΏ) β (((,)β(πΊβπ)) β© π΄)) |
207 | 205, 206 | mp1i 13 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (((,)β(πΊβπ)) β© πΏ) β (((,)β(πΊβπ)) β© π΄)) |
208 | | sseqin2 4176 |
. . . . . . . . . . . 12
β’
((((,)β(πΊβπ)) β© πΏ) β (((,)β(πΊβπ)) β© π΄) β ((((,)β(πΊβπ)) β© π΄) β© (((,)β(πΊβπ)) β© πΏ)) = (((,)β(πΊβπ)) β© πΏ)) |
209 | 207, 208 | sylib 217 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β ((((,)β(πΊβπ)) β© π΄) β© (((,)β(πΊβπ)) β© πΏ)) = (((,)β(πΊβπ)) β© πΏ)) |
210 | 209 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (vol*β((((,)β(πΊβπ)) β© π΄) β© (((,)β(πΊβπ)) β© πΏ))) = (vol*β(((,)β(πΊβπ)) β© πΏ))) |
211 | | indifdir 4245 |
. . . . . . . . . . . . 13
β’ ((π΄ β πΏ) β© ((,)β(πΊβπ))) = ((π΄ β© ((,)β(πΊβπ))) β (πΏ β© ((,)β(πΊβπ)))) |
212 | | incom 4162 |
. . . . . . . . . . . . . 14
β’ (π΄ β© ((,)β(πΊβπ))) = (((,)β(πΊβπ)) β© π΄) |
213 | | incom 4162 |
. . . . . . . . . . . . . 14
β’ (πΏ β© ((,)β(πΊβπ))) = (((,)β(πΊβπ)) β© πΏ) |
214 | 212, 213 | difeq12i 4081 |
. . . . . . . . . . . . 13
β’ ((π΄ β© ((,)β(πΊβπ))) β (πΏ β© ((,)β(πΊβπ)))) = ((((,)β(πΊβπ)) β© π΄) β (((,)β(πΊβπ)) β© πΏ)) |
215 | 211, 214 | eqtri 2761 |
. . . . . . . . . . . 12
β’ ((π΄ β πΏ) β© ((,)β(πΊβπ))) = ((((,)β(πΊβπ)) β© π΄) β (((,)β(πΊβπ)) β© πΏ)) |
216 | 79 | eqcomd 2739 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΏ βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = π΄) |
217 | 77 | ineq1d 4172 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΏ β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = (βͺ
π β (1...π)((,)β(πΉβπ)) β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) |
218 | | 2fveq3 6848 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ = π β ((,)β(πΉβπ₯)) = ((,)β(πΉβπ))) |
219 | 218 | cbvdisjv 5082 |
. . . . . . . . . . . . . . . . . . . 20
β’
(Disj π₯
β β ((,)β(πΉβπ₯)) β Disj π β β ((,)β(πΉβπ))) |
220 | 14, 219 | sylib 217 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β Disj π β β
((,)β(πΉβπ))) |
221 | | fz1ssnn 13478 |
. . . . . . . . . . . . . . . . . . . 20
β’
(1...π) β
β |
222 | 221 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (1...π) β β) |
223 | | uzss 12791 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π + 1) β
(β€β₯β1) β (β€β₯β(π + 1)) β
(β€β₯β1)) |
224 | 39, 223 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β
(β€β₯β(π + 1)) β
(β€β₯β1)) |
225 | 224, 36 | sseqtrrdi 3996 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β
(β€β₯β(π + 1)) β β) |
226 | 47 | ineq1d 4172 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β ((1...((π + 1) β 1)) β©
(β€β₯β(π + 1))) = ((1...π) β© (β€β₯β(π + 1)))) |
227 | | uzdisj 13520 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1...((π + 1)
β 1)) β© (β€β₯β(π + 1))) = β
|
228 | 226, 227 | eqtr3di 2788 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β ((1...π) β© (β€β₯β(π + 1))) =
β
) |
229 | | disjiun 5093 |
. . . . . . . . . . . . . . . . . . 19
β’
((Disj π
β β ((,)β(πΉβπ)) β§ ((1...π) β β β§
(β€β₯β(π + 1)) β β β§ ((1...π) β©
(β€β₯β(π + 1))) = β
)) β (βͺ π β (1...π)((,)β(πΉβπ)) β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = β
) |
230 | 220, 222,
225, 228, 229 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (βͺ π β (1...π)((,)β(πΉβπ)) β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = β
) |
231 | 217, 230 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
β’ (π β (πΏ β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = β
) |
232 | | uneqdifeq 4451 |
. . . . . . . . . . . . . . . . 17
β’ ((πΏ β π΄ β§ (πΏ β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = β
) β ((πΏ βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = π΄ β (π΄ β πΏ) = βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) |
233 | 205, 231,
232 | sylancr 588 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΏ βͺ βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) = π΄ β (π΄ β πΏ) = βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) |
234 | 216, 233 | mpbid 231 |
. . . . . . . . . . . . . . 15
β’ (π β (π΄ β πΏ) = βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) |
235 | 234 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β (π΄ β πΏ) = βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) |
236 | 235 | ineq2d 4173 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (((,)β(πΊβπ)) β© (π΄ β πΏ)) = (((,)β(πΊβπ)) β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ)))) |
237 | | incom 4162 |
. . . . . . . . . . . . 13
β’ ((π΄ β πΏ) β© ((,)β(πΊβπ))) = (((,)β(πΊβπ)) β© (π΄ β πΏ)) |
238 | 101, 98 | eqtri 2761 |
. . . . . . . . . . . . 13
β’ βͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) = (((,)β(πΊβπ)) β© βͺ
π β
(β€β₯β(π + 1))((,)β(πΉβπ))) |
239 | 236, 237,
238 | 3eqtr4g 2798 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β ((π΄ β πΏ) β© ((,)β(πΊβπ))) = βͺ
π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) |
240 | 215, 239 | eqtr3id 2787 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β ((((,)β(πΊβπ)) β© π΄) β (((,)β(πΊβπ)) β© πΏ)) = βͺ
π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) |
241 | 240 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (vol*β((((,)β(πΊβπ)) β© π΄) β (((,)β(πΊβπ)) β© πΏ))) = (vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
242 | 210, 241 | oveq12d 7376 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β ((vol*β((((,)β(πΊβπ)) β© π΄) β© (((,)β(πΊβπ)) β© πΏ))) + (vol*β((((,)β(πΊβπ)) β© π΄) β (((,)β(πΊβπ)) β© πΏ)))) = ((vol*β(((,)β(πΊβπ)) β© πΏ)) + (vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))))) |
243 | 202, 242 | eqtrd 2773 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (vol*β(((,)β(πΊβπ)) β© π΄)) = ((vol*β(((,)β(πΊβπ)) β© πΏ)) + (vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))))) |
244 | 200, 140 | resubcld 11588 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β ((vol*β(((,)β(πΊβπ)) β© π΄)) β (πΆ / π)) β β) |
245 | | inss2 4190 |
. . . . . . . . . . . . 13
β’
(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β ((,)β(πΊβπ)) |
246 | 188 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ π β (1...π)) β ((,)β(πΊβπ)) β β) |
247 | 198 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β (1...π)) β§ π β (1...π)) β (vol*β((,)β(πΊβπ))) β β) |
248 | | ovolsscl 24866 |
. . . . . . . . . . . . 13
β’
(((((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β ((,)β(πΊβπ)) β§ ((,)β(πΊβπ)) β β β§
(vol*β((,)β(πΊβπ))) β β) β
(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) |
249 | 245, 246,
247, 248 | mp3an2i 1467 |
. . . . . . . . . . . 12
β’ (((π β§ π β (1...π)) β§ π β (1...π)) β (vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) |
250 | 148, 249 | fsumrecl 15624 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) |
251 | | uniioombl.n2 |
. . . . . . . . . . . . . 14
β’ (π β βπ β (1...π)(absβ(Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β (vol*β(((,)β(πΊβπ)) β© π΄)))) < (πΆ / π)) |
252 | 251 | r19.21bi 3233 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (absβ(Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β (vol*β(((,)β(πΊβπ)) β© π΄)))) < (πΆ / π)) |
253 | 250, 200,
140 | absdifltd 15324 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β ((absβ(Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β (vol*β(((,)β(πΊβπ)) β© π΄)))) < (πΆ / π) β (((vol*β(((,)β(πΊβπ)) β© π΄)) β (πΆ / π)) < Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β§ Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) < ((vol*β(((,)β(πΊβπ)) β© π΄)) + (πΆ / π))))) |
254 | 252, 253 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (((vol*β(((,)β(πΊβπ)) β© π΄)) β (πΆ / π)) < Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β§ Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) < ((vol*β(((,)β(πΊβπ)) β© π΄)) + (πΆ / π)))) |
255 | 254 | simpld 496 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β ((vol*β(((,)β(πΊβπ)) β© π΄)) β (πΆ / π)) < Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
256 | 244, 250,
255 | ltled 11308 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β ((vol*β(((,)β(πΊβπ)) β© π΄)) β (πΆ / π)) β€ Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
257 | 147 | fveq2d 6847 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (vol*β(((,)β(πΊβπ)) β© πΏ)) = (vol*ββͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
258 | | mblvol 24910 |
. . . . . . . . . . . . . . . . 17
β’
((((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol β
(volβ(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) = (vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
259 | 172, 258 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β (1...π)) β§ π β (1...π)) β (volβ(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) = (vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
260 | 259, 249 | eqeltrd 2834 |
. . . . . . . . . . . . . . 15
β’ (((π β§ π β (1...π)) β§ π β (1...π)) β (volβ(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) |
261 | 172, 260 | jca 513 |
. . . . . . . . . . . . . 14
β’ (((π β§ π β (1...π)) β§ π β (1...π)) β ((((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol β§
(volβ(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β)) |
262 | 261 | ralrimiva 3140 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β βπ β (1...π)((((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol β§
(volβ(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β)) |
263 | | inss1 4189 |
. . . . . . . . . . . . . . . 16
β’
(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β ((,)β(πΉβπ)) |
264 | 263 | rgenw 3065 |
. . . . . . . . . . . . . . 15
β’
βπ β
β (((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β ((,)β(πΉβπ)) |
265 | 220 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β (1...π)) β Disj π β β ((,)β(πΉβπ))) |
266 | | disjss2 5074 |
. . . . . . . . . . . . . . 15
β’
(βπ β
β (((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β ((,)β(πΉβπ)) β (Disj π β β ((,)β(πΉβπ)) β Disj π β β (((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
267 | 264, 265,
266 | mpsyl 68 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β (1...π)) β Disj π β β (((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) |
268 | | disjss1 5077 |
. . . . . . . . . . . . . 14
β’
((1...π) β
β β (Disj π β β (((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β Disj π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
269 | 221, 267,
268 | mpsyl 68 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β Disj π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) |
270 | | volfiniun 24927 |
. . . . . . . . . . . . 13
β’
(((1...π) β Fin
β§ βπ β
(1...π)((((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol β§
(volβ(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β β) β§ Disj π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β (volββͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) = Ξ£π β (1...π)(volβ(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
271 | 148, 262,
269, 270 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (volββͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) = Ξ£π β (1...π)(volβ(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
272 | | mblvol 24910 |
. . . . . . . . . . . . 13
β’ (βͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))) β dom vol β (volββͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) = (vol*ββͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
273 | 175, 272 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (volββͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) = (vol*ββͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
274 | 259 | sumeq2dv 15593 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β Ξ£π β (1...π)(volβ(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) = Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
275 | 271, 273,
274 | 3eqtr3d 2781 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (vol*ββͺ π β (1...π)(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) = Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
276 | 257, 275 | eqtrd 2773 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (vol*β(((,)β(πΊβπ)) β© πΏ)) = Ξ£π β (1...π)(vol*β(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) |
277 | 256, 276 | breqtrrd 5134 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β ((vol*β(((,)β(πΊβπ)) β© π΄)) β (πΆ / π)) β€ (vol*β(((,)β(πΊβπ)) β© πΏ))) |
278 | 276, 250 | eqeltrd 2834 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β (vol*β(((,)β(πΊβπ)) β© πΏ)) β β) |
279 | 200, 140,
278 | lesubaddd 11757 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β (((vol*β(((,)β(πΊβπ)) β© π΄)) β (πΆ / π)) β€ (vol*β(((,)β(πΊβπ)) β© πΏ)) β (vol*β(((,)β(πΊβπ)) β© π΄)) β€ ((vol*β(((,)β(πΊβπ)) β© πΏ)) + (πΆ / π)))) |
280 | 277, 279 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β (vol*β(((,)β(πΊβπ)) β© π΄)) β€ ((vol*β(((,)β(πΊβπ)) β© πΏ)) + (πΆ / π))) |
281 | 243, 280 | eqbrtrrd 5130 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β ((vol*β(((,)β(πΊβπ)) β© πΏ)) + (vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) β€ ((vol*β(((,)β(πΊβπ)) β© πΏ)) + (πΆ / π))) |
282 | 131, 140,
278 | leadd2d 11755 |
. . . . . . 7
β’ ((π β§ π β (1...π)) β ((vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β€ (πΆ / π) β ((vol*β(((,)β(πΊβπ)) β© πΏ)) + (vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) β€ ((vol*β(((,)β(πΊβπ)) β© πΏ)) + (πΆ / π)))) |
283 | 281, 282 | mpbird 257 |
. . . . . 6
β’ ((π β§ π β (1...π)) β (vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β€ (πΆ / π)) |
284 | 124, 131,
140, 283 | fsumle 15689 |
. . . . 5
β’ (π β Ξ£π β (1...π)(vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β€ Ξ£π β (1...π)(πΆ / π)) |
285 | 139 | recnd 11188 |
. . . . . . 7
β’ (π β (πΆ / π) β β) |
286 | | fsumconst 15680 |
. . . . . . 7
β’
(((1...π) β Fin
β§ (πΆ / π) β β) β
Ξ£π β (1...π)(πΆ / π) = ((β―β(1...π)) Β· (πΆ / π))) |
287 | 124, 285,
286 | syl2anc 585 |
. . . . . 6
β’ (π β Ξ£π β (1...π)(πΆ / π) = ((β―β(1...π)) Β· (πΆ / π))) |
288 | | nnnn0 12425 |
. . . . . . . 8
β’ (π β β β π β
β0) |
289 | | hashfz1 14252 |
. . . . . . . 8
β’ (π β β0
β (β―β(1...π)) = π) |
290 | 138, 288,
289 | 3syl 18 |
. . . . . . 7
β’ (π β (β―β(1...π)) = π) |
291 | 290 | oveq1d 7373 |
. . . . . 6
β’ (π β ((β―β(1...π)) Β· (πΆ / π)) = (π Β· (πΆ / π))) |
292 | 116 | recnd 11188 |
. . . . . . 7
β’ (π β πΆ β β) |
293 | 138 | nncnd 12174 |
. . . . . . 7
β’ (π β π β β) |
294 | 138 | nnne0d 12208 |
. . . . . . 7
β’ (π β π β 0) |
295 | 292, 293,
294 | divcan2d 11938 |
. . . . . 6
β’ (π β (π Β· (πΆ / π)) = πΆ) |
296 | 287, 291,
295 | 3eqtrd 2777 |
. . . . 5
β’ (π β Ξ£π β (1...π)(πΆ / π) = πΆ) |
297 | 284, 296 | breqtrd 5132 |
. . . 4
β’ (π β Ξ£π β (1...π)(vol*ββͺ π β (β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β€ πΆ) |
298 | 114, 132,
116, 137, 297 | letrd 11317 |
. . 3
β’ (π β (vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ)))) β€ πΆ) |
299 | 114, 116,
34, 298 | leadd2dd 11775 |
. 2
β’ (π β ((vol*β(πΎ β© πΏ)) + (vol*ββͺ π β (1...π)βͺ π β
(β€β₯β(π + 1))(((,)β(πΉβπ)) β© ((,)β(πΊβπ))))) β€ ((vol*β(πΎ β© πΏ)) + πΆ)) |
300 | 31, 115, 117, 123, 299 | letrd 11317 |
1
β’ (π β (vol*β(πΎ β© π΄)) β€ ((vol*β(πΎ β© πΏ)) + πΆ)) |