Step | Hyp | Ref
| Expression |
1 | | inss1 4192 |
. . . . 5
β’ (πΈ β© π΄) β πΈ |
2 | 1 | a1i 11 |
. . . 4
β’ (π β (πΈ β© π΄) β πΈ) |
3 | | uniioombl.s |
. . . . 5
β’ (π β πΈ β βͺ ran
((,) β πΊ)) |
4 | | uniioombl.g |
. . . . . . . 8
β’ (π β πΊ:ββΆ( β€ β© (β
Γ β))) |
5 | 4 | uniiccdif 24965 |
. . . . . . 7
β’ (π β (βͺ ran ((,) β πΊ) β βͺ ran
([,] β πΊ) β§
(vol*β(βͺ ran ([,] β πΊ) β βͺ ran
((,) β πΊ))) =
0)) |
6 | 5 | simpld 496 |
. . . . . 6
β’ (π β βͺ ran ((,) β πΊ) β βͺ ran
([,] β πΊ)) |
7 | | ovolficcss 24856 |
. . . . . . 7
β’ (πΊ:ββΆ( β€ β©
(β Γ β)) β βͺ ran ([,] β
πΊ) β
β) |
8 | 4, 7 | syl 17 |
. . . . . 6
β’ (π β βͺ ran ([,] β πΊ) β β) |
9 | 6, 8 | sstrd 3958 |
. . . . 5
β’ (π β βͺ ran ((,) β πΊ) β β) |
10 | 3, 9 | sstrd 3958 |
. . . 4
β’ (π β πΈ β β) |
11 | | uniioombl.e |
. . . 4
β’ (π β (vol*βπΈ) β
β) |
12 | | ovolsscl 24873 |
. . . 4
β’ (((πΈ β© π΄) β πΈ β§ πΈ β β β§ (vol*βπΈ) β β) β
(vol*β(πΈ β© π΄)) β
β) |
13 | 2, 10, 11, 12 | syl3anc 1372 |
. . 3
β’ (π β (vol*β(πΈ β© π΄)) β β) |
14 | | difssd 4096 |
. . . 4
β’ (π β (πΈ β π΄) β πΈ) |
15 | | ovolsscl 24873 |
. . . 4
β’ (((πΈ β π΄) β πΈ β§ πΈ β β β§ (vol*βπΈ) β β) β
(vol*β(πΈ β
π΄)) β
β) |
16 | 14, 10, 11, 15 | syl3anc 1372 |
. . 3
β’ (π β (vol*β(πΈ β π΄)) β β) |
17 | | inss1 4192 |
. . . . . 6
β’ (πΎ β© π΄) β πΎ |
18 | 17 | a1i 11 |
. . . . 5
β’ (π β (πΎ β© π΄) β πΎ) |
19 | | uniioombl.1 |
. . . . . . . 8
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
20 | | uniioombl.2 |
. . . . . . . 8
β’ (π β Disj π₯ β β
((,)β(πΉβπ₯))) |
21 | | uniioombl.3 |
. . . . . . . 8
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
22 | | uniioombl.a |
. . . . . . . 8
β’ π΄ = βͺ
ran ((,) β πΉ) |
23 | | uniioombl.c |
. . . . . . . 8
β’ (π β πΆ β
β+) |
24 | | uniioombl.t |
. . . . . . . 8
β’ π = seq1( + , ((abs β
β ) β πΊ)) |
25 | | uniioombl.v |
. . . . . . . 8
β’ (π β sup(ran π, β*, < ) β€
((vol*βπΈ) + πΆ)) |
26 | | uniioombl.m |
. . . . . . . 8
β’ (π β π β β) |
27 | | uniioombl.m2 |
. . . . . . . 8
β’ (π β (absβ((πβπ) β sup(ran π, β*, < ))) < πΆ) |
28 | | uniioombl.k |
. . . . . . . 8
β’ πΎ = βͺ
(((,) β πΊ) β
(1...π)) |
29 | 19, 20, 21, 22, 11, 23, 4, 3, 24, 25, 26, 27, 28 | uniioombllem3a 24971 |
. . . . . . 7
β’ (π β (πΎ = βͺ π β (1...π)((,)β(πΊβπ)) β§ (vol*βπΎ) β β)) |
30 | 29 | simpld 496 |
. . . . . 6
β’ (π β πΎ = βͺ π β (1...π)((,)β(πΊβπ))) |
31 | | inss2 4193 |
. . . . . . . . . . . . 13
β’ ( β€
β© (β Γ β)) β (β Γ
β) |
32 | | elfznn 13479 |
. . . . . . . . . . . . . 14
β’ (π β (1...π) β π β β) |
33 | | ffvelcdm 7036 |
. . . . . . . . . . . . . 14
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (πΊβπ) β ( β€ β© (β Γ
β))) |
34 | 4, 32, 33 | syl2an 597 |
. . . . . . . . . . . . 13
β’ ((π β§ π β (1...π)) β (πΊβπ) β ( β€ β© (β Γ
β))) |
35 | 31, 34 | sselid 3946 |
. . . . . . . . . . . 12
β’ ((π β§ π β (1...π)) β (πΊβπ) β (β Γ
β)) |
36 | | 1st2nd2 7964 |
. . . . . . . . . . . 12
β’ ((πΊβπ) β (β Γ β) β
(πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π β (1...π)) β (πΊβπ) = β¨(1st β(πΊβπ)), (2nd β(πΊβπ))β©) |
38 | 37 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) = ((,)ββ¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©)) |
39 | | df-ov 7364 |
. . . . . . . . . 10
β’
((1st β(πΊβπ))(,)(2nd β(πΊβπ))) = ((,)ββ¨(1st
β(πΊβπ)), (2nd
β(πΊβπ))β©) |
40 | 38, 39 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) = ((1st β(πΊβπ))(,)(2nd β(πΊβπ)))) |
41 | | ioossre 13334 |
. . . . . . . . 9
β’
((1st β(πΊβπ))(,)(2nd β(πΊβπ))) β β |
42 | 40, 41 | eqsstrdi 4002 |
. . . . . . . 8
β’ ((π β§ π β (1...π)) β ((,)β(πΊβπ)) β β) |
43 | 42 | ralrimiva 3140 |
. . . . . . 7
β’ (π β βπ β (1...π)((,)β(πΊβπ)) β β) |
44 | | iunss 5009 |
. . . . . . 7
β’ (βͺ π β (1...π)((,)β(πΊβπ)) β β β βπ β (1...π)((,)β(πΊβπ)) β β) |
45 | 43, 44 | sylibr 233 |
. . . . . 6
β’ (π β βͺ π β (1...π)((,)β(πΊβπ)) β β) |
46 | 30, 45 | eqsstrd 3986 |
. . . . 5
β’ (π β πΎ β β) |
47 | 29 | simprd 497 |
. . . . 5
β’ (π β (vol*βπΎ) β
β) |
48 | | ovolsscl 24873 |
. . . . 5
β’ (((πΎ β© π΄) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*β(πΎ β© π΄)) β
β) |
49 | 18, 46, 47, 48 | syl3anc 1372 |
. . . 4
β’ (π β (vol*β(πΎ β© π΄)) β β) |
50 | 23 | rpred 12965 |
. . . 4
β’ (π β πΆ β β) |
51 | 49, 50 | readdcld 11192 |
. . 3
β’ (π β ((vol*β(πΎ β© π΄)) + πΆ) β β) |
52 | | difssd 4096 |
. . . . 5
β’ (π β (πΎ β π΄) β πΎ) |
53 | | ovolsscl 24873 |
. . . . 5
β’ (((πΎ β π΄) β πΎ β§ πΎ β β β§ (vol*βπΎ) β β) β
(vol*β(πΎ β
π΄)) β
β) |
54 | 52, 46, 47, 53 | syl3anc 1372 |
. . . 4
β’ (π β (vol*β(πΎ β π΄)) β β) |
55 | 54, 50 | readdcld 11192 |
. . 3
β’ (π β ((vol*β(πΎ β π΄)) + πΆ) β β) |
56 | | ssun2 4137 |
. . . . . . 7
β’ βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β (πΎ βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) |
57 | | ioof 13373 |
. . . . . . . . . . . . . . 15
β’
(,):(β* Γ β*)βΆπ«
β |
58 | | rexpssxrxp 11208 |
. . . . . . . . . . . . . . . . 17
β’ (β
Γ β) β (β* Γ
β*) |
59 | 31, 58 | sstri 3957 |
. . . . . . . . . . . . . . . 16
β’ ( β€
β© (β Γ β)) β (β* Γ
β*) |
60 | | fss 6689 |
. . . . . . . . . . . . . . . 16
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ ( β€ β© (β Γ β))
β (β* Γ β*)) β πΊ:ββΆ(β* Γ
β*)) |
61 | 4, 59, 60 | sylancl 587 |
. . . . . . . . . . . . . . 15
β’ (π β πΊ:ββΆ(β* Γ
β*)) |
62 | | fco 6696 |
. . . . . . . . . . . . . . 15
β’
(((,):(β* Γ β*)βΆπ«
β β§ πΊ:ββΆ(β* Γ
β*)) β ((,) β πΊ):ββΆπ«
β) |
63 | 57, 61, 62 | sylancr 588 |
. . . . . . . . . . . . . 14
β’ (π β ((,) β πΊ):ββΆπ«
β) |
64 | 63 | ffnd 6673 |
. . . . . . . . . . . . 13
β’ (π β ((,) β πΊ) Fn β) |
65 | | fnima 6635 |
. . . . . . . . . . . . 13
β’ (((,)
β πΊ) Fn β
β (((,) β πΊ)
β β) = ran ((,) β πΊ)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (((,) β πΊ) β β) = ran ((,)
β πΊ)) |
67 | | nnuz 12814 |
. . . . . . . . . . . . . . 15
β’ β =
(β€β₯β1) |
68 | 26 | peano2nnd 12178 |
. . . . . . . . . . . . . . . . 17
β’ (π β (π + 1) β β) |
69 | 68, 67 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . 16
β’ (π β (π + 1) β
(β€β₯β1)) |
70 | | uzsplit 13522 |
. . . . . . . . . . . . . . . 16
β’ ((π + 1) β
(β€β₯β1) β (β€β₯β1) =
((1...((π + 1) β 1))
βͺ (β€β₯β(π + 1)))) |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β
(β€β₯β1) = ((1...((π + 1) β 1)) βͺ
(β€β₯β(π + 1)))) |
72 | 67, 71 | eqtrid 2785 |
. . . . . . . . . . . . . 14
β’ (π β β = ((1...((π + 1) β 1)) βͺ
(β€β₯β(π + 1)))) |
73 | 26 | nncnd 12177 |
. . . . . . . . . . . . . . . . 17
β’ (π β π β β) |
74 | | ax-1cn 11117 |
. . . . . . . . . . . . . . . . 17
β’ 1 β
β |
75 | | pncan 11415 |
. . . . . . . . . . . . . . . . 17
β’ ((π β β β§ 1 β
β) β ((π + 1)
β 1) = π) |
76 | 73, 74, 75 | sylancl 587 |
. . . . . . . . . . . . . . . 16
β’ (π β ((π + 1) β 1) = π) |
77 | 76 | oveq2d 7377 |
. . . . . . . . . . . . . . 15
β’ (π β (1...((π + 1) β 1)) = (1...π)) |
78 | 77 | uneq1d 4126 |
. . . . . . . . . . . . . 14
β’ (π β ((1...((π + 1) β 1)) βͺ
(β€β₯β(π + 1))) = ((1...π) βͺ (β€β₯β(π + 1)))) |
79 | 72, 78 | eqtrd 2773 |
. . . . . . . . . . . . 13
β’ (π β β = ((1...π) βͺ
(β€β₯β(π + 1)))) |
80 | 79 | imaeq2d 6017 |
. . . . . . . . . . . 12
β’ (π β (((,) β πΊ) β β) = (((,)
β πΊ) β
((1...π) βͺ
(β€β₯β(π + 1))))) |
81 | 66, 80 | eqtr3d 2775 |
. . . . . . . . . . 11
β’ (π β ran ((,) β πΊ) = (((,) β πΊ) β ((1...π) βͺ
(β€β₯β(π + 1))))) |
82 | | imaundi 6106 |
. . . . . . . . . . 11
β’ (((,)
β πΊ) β
((1...π) βͺ
(β€β₯β(π + 1)))) = ((((,) β πΊ) β (1...π)) βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) |
83 | 81, 82 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π β ran ((,) β πΊ) = ((((,) β πΊ) β (1...π)) βͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) |
84 | 83 | unieqd 4883 |
. . . . . . . . 9
β’ (π β βͺ ran ((,) β πΊ) = βͺ ((((,)
β πΊ) β
(1...π)) βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) |
85 | | uniun 4895 |
. . . . . . . . 9
β’ βͺ ((((,) β πΊ) β (1...π)) βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) = (βͺ
(((,) β πΊ) β
(1...π)) βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) |
86 | 84, 85 | eqtrdi 2789 |
. . . . . . . 8
β’ (π β βͺ ran ((,) β πΊ) = (βͺ (((,)
β πΊ) β
(1...π)) βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) |
87 | 28 | uneq1i 4123 |
. . . . . . . 8
β’ (πΎ βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) = (βͺ
(((,) β πΊ) β
(1...π)) βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) |
88 | 86, 87 | eqtr4di 2791 |
. . . . . . 7
β’ (π β βͺ ran ((,) β πΊ) = (πΎ βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) |
89 | 56, 88 | sseqtrrid 4001 |
. . . . . 6
β’ (π β βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β βͺ
ran ((,) β πΊ)) |
90 | 19, 20, 21, 22, 11, 23, 4, 3, 24, 25 | uniioombllem1 24968 |
. . . . . . 7
β’ (π β sup(ran π, β*, < ) β
β) |
91 | | ssid 3970 |
. . . . . . . 8
β’ βͺ ran ((,) β πΊ) β βͺ ran
((,) β πΊ) |
92 | 24 | ovollb 24866 |
. . . . . . . 8
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ βͺ ran ((,) β
πΊ) β βͺ ran ((,) β πΊ)) β (vol*ββͺ ran ((,) β πΊ)) β€ sup(ran π, β*, <
)) |
93 | 4, 91, 92 | sylancl 587 |
. . . . . . 7
β’ (π β (vol*ββͺ ran ((,) β πΊ)) β€ sup(ran π, β*, <
)) |
94 | | ovollecl 24870 |
. . . . . . 7
β’ ((βͺ ran ((,) β πΊ) β β β§ sup(ran π, β*, < )
β β β§ (vol*ββͺ ran ((,) β
πΊ)) β€ sup(ran π, β*, < ))
β (vol*ββͺ ran ((,) β πΊ)) β
β) |
95 | 9, 90, 93, 94 | syl3anc 1372 |
. . . . . 6
β’ (π β (vol*ββͺ ran ((,) β πΊ)) β β) |
96 | | ovolsscl 24873 |
. . . . . 6
β’ ((βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β βͺ
ran ((,) β πΊ) β§
βͺ ran ((,) β πΊ) β β β§ (vol*ββͺ ran ((,) β πΊ)) β β) β (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β β) |
97 | 89, 9, 95, 96 | syl3anc 1372 |
. . . . 5
β’ (π β (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β β) |
98 | 49, 97 | readdcld 11192 |
. . . 4
β’ (π β ((vol*β(πΎ β© π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) β β) |
99 | | unss1 4143 |
. . . . . . . 8
β’ ((πΎ β© π΄) β πΎ β ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β (πΎ βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) |
100 | 17, 99 | ax-mp 5 |
. . . . . . 7
β’ ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β (πΎ βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) |
101 | 100, 88 | sseqtrrid 4001 |
. . . . . 6
β’ (π β ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β βͺ ran ((,) β πΊ)) |
102 | | ovolsscl 24873 |
. . . . . 6
β’ ((((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β βͺ ran ((,) β πΊ) β§ βͺ ran
((,) β πΊ) β
β β§ (vol*ββͺ ran ((,) β πΊ)) β β) β
(vol*β((πΎ β© π΄) βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) β β) |
103 | 101, 9, 95, 102 | syl3anc 1372 |
. . . . 5
β’ (π β (vol*β((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) β β) |
104 | 3, 88 | sseqtrd 3988 |
. . . . . . . 8
β’ (π β πΈ β (πΎ βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) |
105 | 104 | ssrind 4199 |
. . . . . . 7
β’ (π β (πΈ β© π΄) β ((πΎ βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β© π΄)) |
106 | | indir 4239 |
. . . . . . . 8
β’ ((πΎ βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β© π΄) = ((πΎ β© π΄) βͺ (βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) β© π΄)) |
107 | | inss1 4192 |
. . . . . . . . 9
β’ (βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β© π΄) β βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) |
108 | | unss2 4145 |
. . . . . . . . 9
β’ ((βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β© π΄) β βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) β ((πΎ β© π΄) βͺ (βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) β© π΄)) β ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) |
109 | 107, 108 | ax-mp 5 |
. . . . . . . 8
β’ ((πΎ β© π΄) βͺ (βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) β© π΄)) β ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) |
110 | 106, 109 | eqsstri 3982 |
. . . . . . 7
β’ ((πΎ βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β© π΄) β ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) |
111 | 105, 110 | sstrdi 3960 |
. . . . . 6
β’ (π β (πΈ β© π΄) β ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) |
112 | 101, 9 | sstrd 3958 |
. . . . . 6
β’ (π β ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β β) |
113 | | ovolss 24872 |
. . . . . 6
β’ (((πΈ β© π΄) β ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β§ ((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β β) β
(vol*β(πΈ β© π΄)) β€ (vol*β((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))))) |
114 | 111, 112,
113 | syl2anc 585 |
. . . . 5
β’ (π β (vol*β(πΈ β© π΄)) β€ (vol*β((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))))) |
115 | 18, 46 | sstrd 3958 |
. . . . . 6
β’ (π β (πΎ β© π΄) β β) |
116 | 89, 9 | sstrd 3958 |
. . . . . 6
β’ (π β βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β β) |
117 | | ovolun 24886 |
. . . . . 6
β’ ((((πΎ β© π΄) β β β§ (vol*β(πΎ β© π΄)) β β) β§ (βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β β β§
(vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β β)) β
(vol*β((πΎ β© π΄) βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) β€ ((vol*β(πΎ β© π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))))) |
118 | 115, 49, 116, 97, 117 | syl22anc 838 |
. . . . 5
β’ (π β (vol*β((πΎ β© π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) β€ ((vol*β(πΎ β© π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))))) |
119 | 13, 103, 98, 114, 118 | letrd 11320 |
. . . 4
β’ (π β (vol*β(πΈ β© π΄)) β€ ((vol*β(πΎ β© π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))))) |
120 | | rge0ssre 13382 |
. . . . . . . 8
β’
(0[,)+β) β β |
121 | | eqid 2733 |
. . . . . . . . . . 11
β’ ((abs
β β ) β πΊ) = ((abs β β ) β πΊ) |
122 | 121, 24 | ovolsf 24859 |
. . . . . . . . . 10
β’ (πΊ:ββΆ( β€ β©
(β Γ β)) β π:ββΆ(0[,)+β)) |
123 | 4, 122 | syl 17 |
. . . . . . . . 9
β’ (π β π:ββΆ(0[,)+β)) |
124 | 123, 26 | ffvelcdmd 7040 |
. . . . . . . 8
β’ (π β (πβπ) β (0[,)+β)) |
125 | 120, 124 | sselid 3946 |
. . . . . . 7
β’ (π β (πβπ) β β) |
126 | 90, 125 | resubcld 11591 |
. . . . . 6
β’ (π β (sup(ran π, β*, < ) β (πβπ)) β β) |
127 | 97 | rexrd 11213 |
. . . . . . 7
β’ (π β (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β
β*) |
128 | | id 22 |
. . . . . . . . . . . . . 14
β’ (π§ β β β π§ β
β) |
129 | | nnaddcl 12184 |
. . . . . . . . . . . . . 14
β’ ((π§ β β β§ π β β) β (π§ + π) β β) |
130 | 128, 26, 129 | syl2anr 598 |
. . . . . . . . . . . . 13
β’ ((π β§ π§ β β) β (π§ + π) β β) |
131 | 4 | ffvelcdmda 7039 |
. . . . . . . . . . . . 13
β’ ((π β§ (π§ + π) β β) β (πΊβ(π§ + π)) β ( β€ β© (β Γ
β))) |
132 | 130, 131 | syldan 592 |
. . . . . . . . . . . 12
β’ ((π β§ π§ β β) β (πΊβ(π§ + π)) β ( β€ β© (β Γ
β))) |
133 | 132 | fmpttd 7067 |
. . . . . . . . . . 11
β’ (π β (π§ β β β¦ (πΊβ(π§ + π))):ββΆ( β€ β© (β
Γ β))) |
134 | | eqid 2733 |
. . . . . . . . . . . 12
β’ ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π)))) = ((abs β β ) β
(π§ β β β¦
(πΊβ(π§ + π)))) |
135 | | eqid 2733 |
. . . . . . . . . . . 12
β’ seq1( + ,
((abs β β ) β (π§ β β β¦ (πΊβ(π§ + π))))) = seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π))))) |
136 | 134, 135 | ovolsf 24859 |
. . . . . . . . . . 11
β’ ((π§ β β β¦ (πΊβ(π§ + π))):ββΆ( β€ β© (β
Γ β)) β seq1( + , ((abs β β ) β (π§ β β β¦ (πΊβ(π§ + π))))):ββΆ(0[,)+β)) |
137 | 133, 136 | syl 17 |
. . . . . . . . . 10
β’ (π β seq1( + , ((abs β
β ) β (π§ β
β β¦ (πΊβ(π§ + π))))):ββΆ(0[,)+β)) |
138 | 137 | frnd 6680 |
. . . . . . . . 9
β’ (π β ran seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π))))) β
(0[,)+β)) |
139 | | icossxr 13358 |
. . . . . . . . 9
β’
(0[,)+β) β β* |
140 | 138, 139 | sstrdi 3960 |
. . . . . . . 8
β’ (π β ran seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π))))) β
β*) |
141 | | supxrcl 13243 |
. . . . . . . 8
β’ (ran
seq1( + , ((abs β β ) β (π§ β β β¦ (πΊβ(π§ + π))))) β β* β
sup(ran seq1( + , ((abs β β ) β (π§ β β β¦ (πΊβ(π§ + π))))), β*, < ) β
β*) |
142 | 140, 141 | syl 17 |
. . . . . . 7
β’ (π β sup(ran seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π))))), β*, < ) β
β*) |
143 | 126 | rexrd 11213 |
. . . . . . 7
β’ (π β (sup(ran π, β*, < ) β (πβπ)) β
β*) |
144 | | 1zzd 12542 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β 1 β
β€) |
145 | 26 | nnzd 12534 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β π β β€) |
146 | 145 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β π β β€) |
147 | | addcom 11349 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ 1 β
β) β (π + 1) =
(1 + π)) |
148 | 73, 74, 147 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β (π + 1) = (1 + π)) |
149 | 148 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β
(β€β₯β(π + 1)) = (β€β₯β(1 +
π))) |
150 | 149 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (π₯ β (β€β₯β(π + 1)) β π₯ β (β€β₯β(1 +
π)))) |
151 | 150 | biimpa 478 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β π₯ β
(β€β₯β(1 + π))) |
152 | | eluzsub 12801 |
. . . . . . . . . . . . . . . . . . 19
β’ ((1
β β€ β§ π
β β€ β§ π₯
β (β€β₯β(1 + π))) β (π₯ β π) β
(β€β₯β1)) |
153 | 144, 146,
151, 152 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β (π₯ β π) β
(β€β₯β1)) |
154 | 153, 67 | eleqtrrdi 2845 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β (π₯ β π) β β) |
155 | | eluzelz 12781 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π₯ β
(β€β₯β(π + 1)) β π₯ β β€) |
156 | 155 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β π₯ β
β€) |
157 | 156 | zcnd 12616 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β π₯ β
β) |
158 | 73 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β π β β) |
159 | 157, 158 | npcand 11524 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β ((π₯ β π) + π) = π₯) |
160 | 159 | eqcomd 2739 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β π₯ = ((π₯ β π) + π)) |
161 | | oveq1 7368 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ = (π₯ β π) β (π§ + π) = ((π₯ β π) + π)) |
162 | 161 | rspceeqv 3599 |
. . . . . . . . . . . . . . . . 17
β’ (((π₯ β π) β β β§ π₯ = ((π₯ β π) + π)) β βπ§ β β π₯ = (π§ + π)) |
163 | 154, 160,
162 | syl2anc 585 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β βπ§ β β π₯ = (π§ + π)) |
164 | | eqid 2733 |
. . . . . . . . . . . . . . . . . 18
β’ (π§ β β β¦ (π§ + π)) = (π§ β β β¦ (π§ + π)) |
165 | 164 | elrnmpt 5915 |
. . . . . . . . . . . . . . . . 17
β’ (π₯ β V β (π₯ β ran (π§ β β β¦ (π§ + π)) β βπ§ β β π₯ = (π§ + π))) |
166 | 165 | elv 3453 |
. . . . . . . . . . . . . . . 16
β’ (π₯ β ran (π§ β β β¦ (π§ + π)) β βπ§ β β π₯ = (π§ + π)) |
167 | 163, 166 | sylibr 233 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π₯ β (β€β₯β(π + 1))) β π₯ β ran (π§ β β β¦ (π§ + π))) |
168 | 167 | ex 414 |
. . . . . . . . . . . . . 14
β’ (π β (π₯ β (β€β₯β(π + 1)) β π₯ β ran (π§ β β β¦ (π§ + π)))) |
169 | 168 | ssrdv 3954 |
. . . . . . . . . . . . 13
β’ (π β
(β€β₯β(π + 1)) β ran (π§ β β β¦ (π§ + π))) |
170 | | imass2 6058 |
. . . . . . . . . . . . 13
β’
((β€β₯β(π + 1)) β ran (π§ β β β¦ (π§ + π)) β (πΊ β
(β€β₯β(π + 1))) β (πΊ β ran (π§ β β β¦ (π§ + π)))) |
171 | 169, 170 | syl 17 |
. . . . . . . . . . . 12
β’ (π β (πΊ β
(β€β₯β(π + 1))) β (πΊ β ran (π§ β β β¦ (π§ + π)))) |
172 | | rnco2 6209 |
. . . . . . . . . . . . 13
β’ ran
(πΊ β (π§ β β β¦ (π§ + π))) = (πΊ β ran (π§ β β β¦ (π§ + π))) |
173 | 4, 130 | cofmpt 7082 |
. . . . . . . . . . . . . 14
β’ (π β (πΊ β (π§ β β β¦ (π§ + π))) = (π§ β β β¦ (πΊβ(π§ + π)))) |
174 | 173 | rneqd 5897 |
. . . . . . . . . . . . 13
β’ (π β ran (πΊ β (π§ β β β¦ (π§ + π))) = ran (π§ β β β¦ (πΊβ(π§ + π)))) |
175 | 172, 174 | eqtr3id 2787 |
. . . . . . . . . . . 12
β’ (π β (πΊ β ran (π§ β β β¦ (π§ + π))) = ran (π§ β β β¦ (πΊβ(π§ + π)))) |
176 | 171, 175 | sseqtrd 3988 |
. . . . . . . . . . 11
β’ (π β (πΊ β
(β€β₯β(π + 1))) β ran (π§ β β β¦ (πΊβ(π§ + π)))) |
177 | | imass2 6058 |
. . . . . . . . . . 11
β’ ((πΊ β
(β€β₯β(π + 1))) β ran (π§ β β β¦ (πΊβ(π§ + π))) β ((,) β (πΊ β
(β€β₯β(π + 1)))) β ((,) β ran (π§ β β β¦ (πΊβ(π§ + π))))) |
178 | 176, 177 | syl 17 |
. . . . . . . . . 10
β’ (π β ((,) β (πΊ β
(β€β₯β(π + 1)))) β ((,) β ran (π§ β β β¦ (πΊβ(π§ + π))))) |
179 | | imaco 6207 |
. . . . . . . . . 10
β’ (((,)
β πΊ) β
(β€β₯β(π + 1))) = ((,) β (πΊ β
(β€β₯β(π + 1)))) |
180 | | rnco2 6209 |
. . . . . . . . . 10
β’ ran ((,)
β (π§ β β
β¦ (πΊβ(π§ + π)))) = ((,) β ran (π§ β β β¦ (πΊβ(π§ + π)))) |
181 | 178, 179,
180 | 3sstr4g 3993 |
. . . . . . . . 9
β’ (π β (((,) β πΊ) β
(β€β₯β(π + 1))) β ran ((,) β (π§ β β β¦ (πΊβ(π§ + π))))) |
182 | 181 | unissd 4879 |
. . . . . . . 8
β’ (π β βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β βͺ
ran ((,) β (π§ β
β β¦ (πΊβ(π§ + π))))) |
183 | 135 | ovollb 24866 |
. . . . . . . 8
β’ (((π§ β β β¦ (πΊβ(π§ + π))):ββΆ( β€ β© (β
Γ β)) β§ βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β βͺ
ran ((,) β (π§ β
β β¦ (πΊβ(π§ + π))))) β (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β€ sup(ran seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π))))), β*, <
)) |
184 | 133, 182,
183 | syl2anc 585 |
. . . . . . 7
β’ (π β (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β€ sup(ran seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π))))), β*, <
)) |
185 | 123 | frnd 6680 |
. . . . . . . . . . . . 13
β’ (π β ran π β (0[,)+β)) |
186 | 185, 139 | sstrdi 3960 |
. . . . . . . . . . . 12
β’ (π β ran π β
β*) |
187 | 24 | fveq1i 6847 |
. . . . . . . . . . . . . 14
β’ (πβ(π + π)) = (seq1( + , ((abs β β )
β πΊ))β(π + π)) |
188 | 26 | nnred 12176 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β π β β) |
189 | 188 | ltp1d 12093 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π < (π + 1)) |
190 | | fzdisj 13477 |
. . . . . . . . . . . . . . . . . 18
β’ (π < (π + 1) β ((1...π) β© ((π + 1)...(π + π))) = β
) |
191 | 189, 190 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’ (π β ((1...π) β© ((π + 1)...(π + π))) = β
) |
192 | 191 | adantr 482 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((1...π) β© ((π + 1)...(π + π))) = β
) |
193 | | nnnn0 12428 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β β β π β
β0) |
194 | | nn0addge1 12467 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β β β§ π β β0)
β π β€ (π + π)) |
195 | 188, 193,
194 | syl2an 597 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β€ (π + π)) |
196 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β π β β) |
197 | 196, 67 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
198 | | nnaddcl 12184 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β β β§ π β β) β (π + π) β β) |
199 | 26, 198 | sylan 581 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (π + π) β β) |
200 | 199 | nnzd 12534 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (π + π) β β€) |
201 | | elfz5 13442 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β
(β€β₯β1) β§ (π + π) β β€) β (π β (1...(π + π)) β π β€ (π + π))) |
202 | 197, 200,
201 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π β (1...(π + π)) β π β€ (π + π))) |
203 | 195, 202 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β π β (1...(π + π))) |
204 | | fzsplit 13476 |
. . . . . . . . . . . . . . . . 17
β’ (π β (1...(π + π)) β (1...(π + π)) = ((1...π) βͺ ((π + 1)...(π + π)))) |
205 | 203, 204 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (1...(π + π)) = ((1...π) βͺ ((π + 1)...(π + π)))) |
206 | | fzfid 13887 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (1...(π + π)) β Fin) |
207 | 4 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β πΊ:ββΆ( β€ β© (β
Γ β))) |
208 | | elfznn 13479 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...(π + π)) β π β β) |
209 | | ovolfcl 24853 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β ((1st
β(πΊβπ)) β β β§
(2nd β(πΊβπ)) β β β§ (1st
β(πΊβπ)) β€ (2nd
β(πΊβπ)))) |
210 | 207, 208,
209 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (1...(π + π))) β ((1st β(πΊβπ)) β β β§ (2nd
β(πΊβπ)) β β β§
(1st β(πΊβπ)) β€ (2nd β(πΊβπ)))) |
211 | 210 | simp2d 1144 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (1...(π + π))) β (2nd β(πΊβπ)) β β) |
212 | 210 | simp1d 1143 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (1...(π + π))) β (1st β(πΊβπ)) β β) |
213 | 211, 212 | resubcld 11591 |
. . . . . . . . . . . . . . . . 17
β’ (((π β§ π β β) β§ π β (1...(π + π))) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
214 | 213 | recnd 11191 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β (1...(π + π))) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
215 | 192, 205,
206, 214 | fsumsplit 15634 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β Ξ£π β (1...(π + π))((2nd β(πΊβπ)) β (1st β(πΊβπ))) = (Ξ£π β (1...π)((2nd β(πΊβπ)) β (1st β(πΊβπ))) + Ξ£π β ((π + 1)...(π + π))((2nd β(πΊβπ)) β (1st β(πΊβπ))))) |
216 | 121 | ovolfsval 24857 |
. . . . . . . . . . . . . . . . 17
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ π β β) β (((abs β
β ) β πΊ)βπ) = ((2nd β(πΊβπ)) β (1st β(πΊβπ)))) |
217 | 207, 208,
216 | syl2an 597 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β) β§ π β (1...(π + π))) β (((abs β β ) β
πΊ)βπ) = ((2nd β(πΊβπ)) β (1st β(πΊβπ)))) |
218 | 199, 67 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β (π + π) β
(β€β₯β1)) |
219 | 217, 218,
214 | fsumser 15623 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β Ξ£π β (1...(π + π))((2nd β(πΊβπ)) β (1st β(πΊβπ))) = (seq1( + , ((abs β β )
β πΊ))β(π + π))) |
220 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (1...π)) β πΊ:ββΆ( β€ β© (β
Γ β))) |
221 | 32 | adantl 483 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
222 | 220, 221,
216 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (1...π)) β (((abs β β ) β
πΊ)βπ) = ((2nd β(πΊβπ)) β (1st β(πΊβπ)))) |
223 | 4, 32, 209 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π β§ π β (1...π)) β ((1st β(πΊβπ)) β β β§ (2nd
β(πΊβπ)) β β β§
(1st β(πΊβπ)) β€ (2nd β(πΊβπ)))) |
224 | 223 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (1...π)) β (2nd β(πΊβπ)) β β) |
225 | 223 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β (1...π)) β (1st β(πΊβπ)) β β) |
226 | 224, 225 | resubcld 11591 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β (1...π)) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
227 | 226 | adantlr 714 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (1...π)) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
228 | 227 | recnd 11191 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (1...π)) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
229 | 222, 197,
228 | fsumser 15623 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β Ξ£π β (1...π)((2nd β(πΊβπ)) β (1st β(πΊβπ))) = (seq1( + , ((abs β β )
β πΊ))βπ)) |
230 | 24 | fveq1i 6847 |
. . . . . . . . . . . . . . . . 17
β’ (πβπ) = (seq1( + , ((abs β β )
β πΊ))βπ) |
231 | 229, 230 | eqtr4di 2791 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β Ξ£π β (1...π)((2nd β(πΊβπ)) β (1st β(πΊβπ))) = (πβπ)) |
232 | 196 | nnzd 12534 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β β€) |
233 | 232 | peano2zd 12618 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (π + 1) β β€) |
234 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β ((π + 1)...(π + π))) β πΊ:ββΆ( β€ β© (β
Γ β))) |
235 | 196 | peano2nnd 12178 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β§ π β β) β (π + 1) β β) |
236 | | elfzuz 13446 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π β ((π + 1)...(π + π)) β π β (β€β₯β(π + 1))) |
237 | | eluznn 12851 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π + 1) β β β§ π β
(β€β₯β(π + 1))) β π β β) |
238 | 235, 236,
237 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β ((π + 1)...(π + π))) β π β β) |
239 | 234, 238,
209 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ π β ((π + 1)...(π + π))) β ((1st β(πΊβπ)) β β β§ (2nd
β(πΊβπ)) β β β§
(1st β(πΊβπ)) β€ (2nd β(πΊβπ)))) |
240 | 239 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π β ((π + 1)...(π + π))) β (2nd β(πΊβπ)) β β) |
241 | 239 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π β ((π + 1)...(π + π))) β (1st β(πΊβπ)) β β) |
242 | 240, 241 | resubcld 11591 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β ((π + 1)...(π + π))) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
243 | 242 | recnd 11191 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β ((π + 1)...(π + π))) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) β β) |
244 | | 2fveq3 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + π) β (2nd β(πΊβπ)) = (2nd β(πΊβ(π + π)))) |
245 | | 2fveq3 6851 |
. . . . . . . . . . . . . . . . . . 19
β’ (π = (π + π) β (1st β(πΊβπ)) = (1st β(πΊβ(π + π)))) |
246 | 244, 245 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . 18
β’ (π = (π + π) β ((2nd β(πΊβπ)) β (1st β(πΊβπ))) = ((2nd β(πΊβ(π + π))) β (1st β(πΊβ(π + π))))) |
247 | 232, 233,
200, 243, 246 | fsumshftm 15674 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β Ξ£π β ((π + 1)...(π + π))((2nd β(πΊβπ)) β (1st β(πΊβπ))) = Ξ£π β (((π + 1) β π)...((π + π) β π))((2nd β(πΊβ(π + π))) β (1st β(πΊβ(π + π))))) |
248 | 196 | nncnd 12177 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β π β β) |
249 | | pncan2 11416 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β β β§ 1 β
β) β ((π + 1)
β π) =
1) |
250 | 248, 74, 249 | sylancl 587 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ((π + 1) β π) = 1) |
251 | | nncn 12169 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β β π β
β) |
252 | 251 | adantl 483 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β π β β) |
253 | 248, 252 | pncan2d 11522 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β ((π + π) β π) = π) |
254 | 250, 253 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (((π + 1) β π)...((π + π) β π)) = (1...π)) |
255 | 254 | sumeq1d 15594 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β Ξ£π β (((π + 1) β π)...((π + π) β π))((2nd β(πΊβ(π + π))) β (1st β(πΊβ(π + π)))) = Ξ£π β (1...π)((2nd β(πΊβ(π + π))) β (1st β(πΊβ(π + π))))) |
256 | 133 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β β) β (π§ β β β¦ (πΊβ(π§ + π))):ββΆ( β€ β© (β
Γ β))) |
257 | | elfznn 13479 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (1...π) β π β β) |
258 | 134 | ovolfsval 24857 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π§ β β β¦ (πΊβ(π§ + π))):ββΆ( β€ β© (β
Γ β)) β§ π
β β) β (((abs β β ) β (π§ β β β¦ (πΊβ(π§ + π))))βπ) = ((2nd β((π§ β β β¦ (πΊβ(π§ + π)))βπ)) β (1st β((π§ β β β¦ (πΊβ(π§ + π)))βπ)))) |
259 | 256, 257,
258 | syl2an 597 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (1...π)) β (((abs β β ) β
(π§ β β β¦
(πΊβ(π§ + π))))βπ) = ((2nd β((π§ β β β¦ (πΊβ(π§ + π)))βπ)) β (1st β((π§ β β β¦ (πΊβ(π§ + π)))βπ)))) |
260 | 257 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β (1...π)) β π β β) |
261 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ = π β (πΊβ(π§ + π)) = (πΊβ(π + π))) |
262 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (π§ β β β¦ (πΊβ(π§ + π))) = (π§ β β β¦ (πΊβ(π§ + π))) |
263 | | fvex 6859 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (πΊβ(π + π)) β V |
264 | 261, 262,
263 | fvmpt 6952 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (π β β β ((π§ β β β¦ (πΊβ(π§ + π)))βπ) = (πΊβ(π + π))) |
265 | 260, 264 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ π β (1...π)) β ((π§ β β β¦ (πΊβ(π§ + π)))βπ) = (πΊβ(π + π))) |
266 | 265 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π β (1...π)) β (2nd β((π§ β β β¦ (πΊβ(π§ + π)))βπ)) = (2nd β(πΊβ(π + π)))) |
267 | 265 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π β (1...π)) β (1st β((π§ β β β¦ (πΊβ(π§ + π)))βπ)) = (1st β(πΊβ(π + π)))) |
268 | 266, 267 | oveq12d 7379 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (1...π)) β ((2nd β((π§ β β β¦ (πΊβ(π§ + π)))βπ)) β (1st β((π§ β β β¦ (πΊβ(π§ + π)))βπ))) = ((2nd β(πΊβ(π + π))) β (1st β(πΊβ(π + π))))) |
269 | 259, 268 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (1...π)) β (((abs β β ) β
(π§ β β β¦
(πΊβ(π§ + π))))βπ) = ((2nd β(πΊβ(π + π))) β (1st β(πΊβ(π + π))))) |
270 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β π β β) |
271 | 270, 67 | eleqtrdi 2844 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β π β
(β€β₯β1)) |
272 | 4 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β (1...π)) β πΊ:ββΆ( β€ β© (β
Γ β))) |
273 | | nnaddcl 12184 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ ((π β β β§ π β β) β (π + π) β β) |
274 | 257, 196,
273 | syl2anr 598 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β β) β§ π β (1...π)) β (π + π) β β) |
275 | | ovolfcl 24853 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((πΊ:ββΆ( β€ β©
(β Γ β)) β§ (π + π) β β) β ((1st
β(πΊβ(π + π))) β β β§ (2nd
β(πΊβ(π + π))) β β β§ (1st
β(πΊβ(π + π))) β€ (2nd β(πΊβ(π + π))))) |
276 | 272, 274,
275 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ π β β) β§ π β (1...π)) β ((1st β(πΊβ(π + π))) β β β§ (2nd
β(πΊβ(π + π))) β β β§ (1st
β(πΊβ(π + π))) β€ (2nd β(πΊβ(π + π))))) |
277 | 276 | simp2d 1144 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π β (1...π)) β (2nd β(πΊβ(π + π))) β β) |
278 | 276 | simp1d 1143 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β§ π β β) β§ π β (1...π)) β (1st β(πΊβ(π + π))) β β) |
279 | 277, 278 | resubcld 11591 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β§ π β β) β§ π β (1...π)) β ((2nd β(πΊβ(π + π))) β (1st β(πΊβ(π + π)))) β β) |
280 | 279 | recnd 11191 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β§ π β β) β§ π β (1...π)) β ((2nd β(πΊβ(π + π))) β (1st β(πΊβ(π + π)))) β β) |
281 | 269, 271,
280 | fsumser 15623 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β Ξ£π β (1...π)((2nd β(πΊβ(π + π))) β (1st β(πΊβ(π + π)))) = (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ)) |
282 | 247, 255,
281 | 3eqtrd 2777 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β Ξ£π β ((π + 1)...(π + π))((2nd β(πΊβπ)) β (1st β(πΊβπ))) = (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ)) |
283 | 231, 282 | oveq12d 7379 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (Ξ£π β (1...π)((2nd β(πΊβπ)) β (1st β(πΊβπ))) + Ξ£π β ((π + 1)...(π + π))((2nd β(πΊβπ)) β (1st β(πΊβπ)))) = ((πβπ) + (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ))) |
284 | 215, 219,
283 | 3eqtr3d 2781 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β πΊ))β(π + π)) = ((πβπ) + (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ))) |
285 | 187, 284 | eqtrid 2785 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβ(π + π)) = ((πβπ) + (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ))) |
286 | 123 | ffnd 6673 |
. . . . . . . . . . . . . 14
β’ (π β π Fn β) |
287 | | fnfvelrn 7035 |
. . . . . . . . . . . . . 14
β’ ((π Fn β β§ (π + π) β β) β (πβ(π + π)) β ran π) |
288 | 286, 199,
287 | syl2an2r 684 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβ(π + π)) β ran π) |
289 | 285, 288 | eqeltrrd 2835 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((πβπ) + (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ)) β ran π) |
290 | | supxrub 13252 |
. . . . . . . . . . . 12
β’ ((ran
π β
β* β§ ((πβπ) + (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ)) β ran π) β ((πβπ) + (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ)) β€ sup(ran π, β*, <
)) |
291 | 186, 289,
290 | syl2an2r 684 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((πβπ) + (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ)) β€ sup(ran π, β*, <
)) |
292 | 125 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πβπ) β β) |
293 | 137 | ffvelcdmda 7039 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π)))))βπ) β (0[,)+β)) |
294 | 120, 293 | sselid 3946 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π)))))βπ) β β) |
295 | 90 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β sup(ran π, β*, < )
β β) |
296 | 292, 294,
295 | leaddsub2d 11765 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((πβπ) + (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ)) β€ sup(ran π, β*, < ) β (seq1(
+ , ((abs β β ) β (π§ β β β¦ (πΊβ(π§ + π)))))βπ) β€ (sup(ran π, β*, < ) β (πβπ)))) |
297 | 291, 296 | mpbid 231 |
. . . . . . . . . 10
β’ ((π β§ π β β) β (seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π)))))βπ) β€ (sup(ran π, β*, < ) β (πβπ))) |
298 | 297 | ralrimiva 3140 |
. . . . . . . . 9
β’ (π β βπ β β (seq1( + , ((abs β
β ) β (π§ β
β β¦ (πΊβ(π§ + π)))))βπ) β€ (sup(ran π, β*, < ) β (πβπ))) |
299 | 137 | ffnd 6673 |
. . . . . . . . . 10
β’ (π β seq1( + , ((abs β
β ) β (π§ β
β β¦ (πΊβ(π§ + π))))) Fn β) |
300 | | breq1 5112 |
. . . . . . . . . . 11
β’ (π₯ = (seq1( + , ((abs β
β ) β (π§ β
β β¦ (πΊβ(π§ + π)))))βπ) β (π₯ β€ (sup(ran π, β*, < ) β (πβπ)) β (seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))βπ) β€ (sup(ran π, β*, < ) β (πβπ)))) |
301 | 300 | ralrn 7042 |
. . . . . . . . . 10
β’ (seq1( +
, ((abs β β ) β (π§ β β β¦ (πΊβ(π§ + π))))) Fn β β (βπ₯ β ran seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π)))))π₯ β€ (sup(ran π, β*, < ) β (πβπ)) β βπ β β (seq1( + , ((abs β
β ) β (π§ β
β β¦ (πΊβ(π§ + π)))))βπ) β€ (sup(ran π, β*, < ) β (πβπ)))) |
302 | 299, 301 | syl 17 |
. . . . . . . . 9
β’ (π β (βπ₯ β ran seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π)))))π₯ β€ (sup(ran π, β*, < ) β (πβπ)) β βπ β β (seq1( + , ((abs β
β ) β (π§ β
β β¦ (πΊβ(π§ + π)))))βπ) β€ (sup(ran π, β*, < ) β (πβπ)))) |
303 | 298, 302 | mpbird 257 |
. . . . . . . 8
β’ (π β βπ₯ β ran seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))π₯ β€ (sup(ran π, β*, < ) β (πβπ))) |
304 | | supxrleub 13254 |
. . . . . . . . 9
β’ ((ran
seq1( + , ((abs β β ) β (π§ β β β¦ (πΊβ(π§ + π))))) β β* β§
(sup(ran π,
β*, < ) β (πβπ)) β β*) β
(sup(ran seq1( + , ((abs β β ) β (π§ β β β¦ (πΊβ(π§ + π))))), β*, < ) β€
(sup(ran π,
β*, < ) β (πβπ)) β βπ₯ β ran seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))π₯ β€ (sup(ran π, β*, < ) β (πβπ)))) |
305 | 140, 143,
304 | syl2anc 585 |
. . . . . . . 8
β’ (π β (sup(ran seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π))))), β*, < ) β€
(sup(ran π,
β*, < ) β (πβπ)) β βπ₯ β ran seq1( + , ((abs β β )
β (π§ β β
β¦ (πΊβ(π§ + π)))))π₯ β€ (sup(ran π, β*, < ) β (πβπ)))) |
306 | 303, 305 | mpbird 257 |
. . . . . . 7
β’ (π β sup(ran seq1( + , ((abs
β β ) β (π§ β β β¦ (πΊβ(π§ + π))))), β*, < ) β€
(sup(ran π,
β*, < ) β (πβπ))) |
307 | 127, 142,
143, 184, 306 | xrletrd 13090 |
. . . . . 6
β’ (π β (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β€ (sup(ran π, β*, < ) β (πβπ))) |
308 | 125, 90, 50 | absdifltd 15327 |
. . . . . . . . 9
β’ (π β ((absβ((πβπ) β sup(ran π, β*, < ))) < πΆ β ((sup(ran π, β*, < )
β πΆ) < (πβπ) β§ (πβπ) < (sup(ran π, β*, < ) + πΆ)))) |
309 | 27, 308 | mpbid 231 |
. . . . . . . 8
β’ (π β ((sup(ran π, β*, < )
β πΆ) < (πβπ) β§ (πβπ) < (sup(ran π, β*, < ) + πΆ))) |
310 | 309 | simpld 496 |
. . . . . . 7
β’ (π β (sup(ran π, β*, < ) β πΆ) < (πβπ)) |
311 | 90, 50, 125, 310 | ltsub23d 11768 |
. . . . . 6
β’ (π β (sup(ran π, β*, < ) β (πβπ)) < πΆ) |
312 | 97, 126, 50, 307, 311 | lelttrd 11321 |
. . . . 5
β’ (π β (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) < πΆ) |
313 | 97, 50, 49, 312 | ltadd2dd 11322 |
. . . 4
β’ (π β ((vol*β(πΎ β© π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) < ((vol*β(πΎ β© π΄)) + πΆ)) |
314 | 13, 98, 51, 119, 313 | lelttrd 11321 |
. . 3
β’ (π β (vol*β(πΈ β© π΄)) < ((vol*β(πΎ β© π΄)) + πΆ)) |
315 | 54, 97 | readdcld 11192 |
. . . 4
β’ (π β ((vol*β(πΎ β π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) β β) |
316 | | difss 4095 |
. . . . . . . 8
β’ (πΎ β π΄) β πΎ |
317 | | unss1 4143 |
. . . . . . . 8
β’ ((πΎ β π΄) β πΎ β ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β (πΎ βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) |
318 | 316, 317 | ax-mp 5 |
. . . . . . 7
β’ ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β (πΎ βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) |
319 | 318, 88 | sseqtrrid 4001 |
. . . . . 6
β’ (π β ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β βͺ ran ((,) β πΊ)) |
320 | | ovolsscl 24873 |
. . . . . 6
β’ ((((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β βͺ ran ((,) β πΊ) β§ βͺ ran
((,) β πΊ) β
β β§ (vol*ββͺ ran ((,) β πΊ)) β β) β
(vol*β((πΎ β
π΄) βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) β β) |
321 | 319, 9, 95, 320 | syl3anc 1372 |
. . . . 5
β’ (π β (vol*β((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) β β) |
322 | 104 | ssdifd 4104 |
. . . . . . 7
β’ (π β (πΈ β π΄) β ((πΎ βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β π΄)) |
323 | | difundir 4244 |
. . . . . . . 8
β’ ((πΎ βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β π΄) = ((πΎ β π΄) βͺ (βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) β π΄)) |
324 | | difss 4095 |
. . . . . . . . 9
β’ (βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β π΄) β βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) |
325 | | unss2 4145 |
. . . . . . . . 9
β’ ((βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β π΄) β βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) β ((πΎ β π΄) βͺ (βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) β π΄)) β ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) |
326 | 324, 325 | ax-mp 5 |
. . . . . . . 8
β’ ((πΎ β π΄) βͺ (βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))) β π΄)) β ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) |
327 | 323, 326 | eqsstri 3982 |
. . . . . . 7
β’ ((πΎ βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β π΄) β ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) |
328 | 322, 327 | sstrdi 3960 |
. . . . . 6
β’ (π β (πΈ β π΄) β ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) |
329 | 319, 9 | sstrd 3958 |
. . . . . 6
β’ (π β ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β β) |
330 | | ovolss 24872 |
. . . . . 6
β’ (((πΈ β π΄) β ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β§ ((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))) β β) β
(vol*β(πΈ β
π΄)) β€
(vol*β((πΎ β
π΄) βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1)))))) |
331 | 328, 329,
330 | syl2anc 585 |
. . . . 5
β’ (π β (vol*β(πΈ β π΄)) β€ (vol*β((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1)))))) |
332 | 52, 46 | sstrd 3958 |
. . . . . 6
β’ (π β (πΎ β π΄) β β) |
333 | | ovolun 24886 |
. . . . . 6
β’ ((((πΎ β π΄) β β β§ (vol*β(πΎ β π΄)) β β) β§ (βͺ (((,) β πΊ) β
(β€β₯β(π + 1))) β β β§
(vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))) β β)) β
(vol*β((πΎ β
π΄) βͺ βͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) β€ ((vol*β(πΎ β π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))))) |
334 | 332, 54, 116, 97, 333 | syl22anc 838 |
. . . . 5
β’ (π β (vol*β((πΎ β π΄) βͺ βͺ (((,)
β πΊ) β
(β€β₯β(π + 1))))) β€ ((vol*β(πΎ β π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))))) |
335 | 16, 321, 315, 331, 334 | letrd 11320 |
. . . 4
β’ (π β (vol*β(πΈ β π΄)) β€ ((vol*β(πΎ β π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1)))))) |
336 | 97, 50, 54, 312 | ltadd2dd 11322 |
. . . 4
β’ (π β ((vol*β(πΎ β π΄)) + (vol*ββͺ (((,) β πΊ) β
(β€β₯β(π + 1))))) < ((vol*β(πΎ β π΄)) + πΆ)) |
337 | 16, 315, 55, 335, 336 | lelttrd 11321 |
. . 3
β’ (π β (vol*β(πΈ β π΄)) < ((vol*β(πΎ β π΄)) + πΆ)) |
338 | 13, 16, 51, 55, 314, 337 | lt2addd 11786 |
. 2
β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) < (((vol*β(πΎ β© π΄)) + πΆ) + ((vol*β(πΎ β π΄)) + πΆ))) |
339 | 49 | recnd 11191 |
. . 3
β’ (π β (vol*β(πΎ β© π΄)) β β) |
340 | 50 | recnd 11191 |
. . 3
β’ (π β πΆ β β) |
341 | 54 | recnd 11191 |
. . 3
β’ (π β (vol*β(πΎ β π΄)) β β) |
342 | 339, 340,
341, 340 | add4d 11391 |
. 2
β’ (π β (((vol*β(πΎ β© π΄)) + πΆ) + ((vol*β(πΎ β π΄)) + πΆ)) = (((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) + (πΆ + πΆ))) |
343 | 338, 342 | breqtrd 5135 |
1
β’ (π β ((vol*β(πΈ β© π΄)) + (vol*β(πΈ β π΄))) < (((vol*β(πΎ β© π΄)) + (vol*β(πΎ β π΄))) + (πΆ + πΆ))) |