Step | Hyp | Ref
| Expression |
1 | | ovolun.a |
. . . . 5
β’ (π β (π΄ β β β§ (vol*βπ΄) β
β)) |
2 | 1 | simpld 496 |
. . . 4
β’ (π β π΄ β β) |
3 | | ovolun.b |
. . . . 5
β’ (π β (π΅ β β β§ (vol*βπ΅) β
β)) |
4 | 3 | simpld 496 |
. . . 4
β’ (π β π΅ β β) |
5 | 2, 4 | unssd 4147 |
. . 3
β’ (π β (π΄ βͺ π΅) β β) |
6 | | ovolun.g1 |
. . . . . . . . . . . 12
β’ (π β πΊ β (( β€ β© (β Γ
β)) βm β)) |
7 | | elovolmlem 24854 |
. . . . . . . . . . . 12
β’ (πΊ β (( β€ β© (β
Γ β)) βm β) β πΊ:ββΆ( β€ β© (β
Γ β))) |
8 | 6, 7 | sylib 217 |
. . . . . . . . . . 11
β’ (π β πΊ:ββΆ( β€ β© (β
Γ β))) |
9 | 8 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β β) β πΊ:ββΆ( β€ β© (β
Γ β))) |
10 | 9 | ffvelcdmda 7036 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ (π / 2) β β) β (πΊβ(π / 2)) β ( β€ β© (β Γ
β))) |
11 | | nneo 12592 |
. . . . . . . . . . . . 13
β’ (π β β β ((π / 2) β β β
Β¬ ((π + 1) / 2) β
β)) |
12 | 11 | adantl 483 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((π / 2) β β β Β¬ ((π + 1) / 2) β
β)) |
13 | 12 | con2bid 355 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (((π + 1) / 2) β β β Β¬ (π / 2) β
β)) |
14 | 13 | biimpar 479 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ Β¬ (π / 2) β β) β
((π + 1) / 2) β
β) |
15 | | ovolun.f1 |
. . . . . . . . . . . . 13
β’ (π β πΉ β (( β€ β© (β Γ
β)) βm β)) |
16 | | elovolmlem 24854 |
. . . . . . . . . . . . 13
β’ (πΉ β (( β€ β© (β
Γ β)) βm β) β πΉ:ββΆ( β€ β© (β
Γ β))) |
17 | 15, 16 | sylib 217 |
. . . . . . . . . . . 12
β’ (π β πΉ:ββΆ( β€ β© (β
Γ β))) |
18 | 17 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β πΉ:ββΆ( β€ β© (β
Γ β))) |
19 | 18 | ffvelcdmda 7036 |
. . . . . . . . . 10
β’ (((π β§ π β β) β§ ((π + 1) / 2) β β) β (πΉβ((π + 1) / 2)) β ( β€ β© (β
Γ β))) |
20 | 14, 19 | syldan 592 |
. . . . . . . . 9
β’ (((π β§ π β β) β§ Β¬ (π / 2) β β) β
(πΉβ((π + 1) / 2)) β ( β€ β©
(β Γ β))) |
21 | 10, 20 | ifclda 4522 |
. . . . . . . 8
β’ ((π β§ π β β) β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) β ( β€ β© (β
Γ β))) |
22 | | ovolun.h |
. . . . . . . 8
β’ π» = (π β β β¦ if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2)))) |
23 | 21, 22 | fmptd 7063 |
. . . . . . 7
β’ (π β π»:ββΆ( β€ β© (β
Γ β))) |
24 | | eqid 2733 |
. . . . . . . 8
β’ ((abs
β β ) β π») = ((abs β β ) β π») |
25 | | ovolun.u |
. . . . . . . 8
β’ π = seq1( + , ((abs β
β ) β π»)) |
26 | 24, 25 | ovolsf 24852 |
. . . . . . 7
β’ (π»:ββΆ( β€ β©
(β Γ β)) β π:ββΆ(0[,)+β)) |
27 | 23, 26 | syl 17 |
. . . . . 6
β’ (π β π:ββΆ(0[,)+β)) |
28 | | rge0ssre 13379 |
. . . . . 6
β’
(0[,)+β) β β |
29 | | fss 6686 |
. . . . . 6
β’ ((π:ββΆ(0[,)+β)
β§ (0[,)+β) β β) β π:ββΆβ) |
30 | 27, 28, 29 | sylancl 587 |
. . . . 5
β’ (π β π:ββΆβ) |
31 | 30 | frnd 6677 |
. . . 4
β’ (π β ran π β β) |
32 | | 1nn 12169 |
. . . . . . 7
β’ 1 β
β |
33 | | 1z 12538 |
. . . . . . . . . 10
β’ 1 β
β€ |
34 | | seqfn 13924 |
. . . . . . . . . 10
β’ (1 β
β€ β seq1( + , ((abs β β ) β π»)) Fn
(β€β₯β1)) |
35 | 33, 34 | mp1i 13 |
. . . . . . . . 9
β’ (π β seq1( + , ((abs β
β ) β π»)) Fn
(β€β₯β1)) |
36 | 25 | fneq1i 6600 |
. . . . . . . . . 10
β’ (π Fn β β seq1( + ,
((abs β β ) β π»)) Fn β) |
37 | | nnuz 12811 |
. . . . . . . . . . 11
β’ β =
(β€β₯β1) |
38 | 37 | fneq2i 6601 |
. . . . . . . . . 10
β’ (seq1( +
, ((abs β β ) β π»)) Fn β β seq1( + , ((abs β
β ) β π»)) Fn
(β€β₯β1)) |
39 | 36, 38 | bitri 275 |
. . . . . . . . 9
β’ (π Fn β β seq1( + ,
((abs β β ) β π»)) Fn
(β€β₯β1)) |
40 | 35, 39 | sylibr 233 |
. . . . . . . 8
β’ (π β π Fn β) |
41 | 40 | fndmd 6608 |
. . . . . . 7
β’ (π β dom π = β) |
42 | 32, 41 | eleqtrrid 2841 |
. . . . . 6
β’ (π β 1 β dom π) |
43 | 42 | ne0d 4296 |
. . . . 5
β’ (π β dom π β β
) |
44 | | dm0rn0 5881 |
. . . . . 6
β’ (dom
π = β
β ran
π =
β
) |
45 | 44 | necon3bii 2993 |
. . . . 5
β’ (dom
π β β
β ran
π β
β
) |
46 | 43, 45 | sylib 217 |
. . . 4
β’ (π β ran π β β
) |
47 | 1 | simprd 497 |
. . . . . . . 8
β’ (π β (vol*βπ΄) β
β) |
48 | 3 | simprd 497 |
. . . . . . . 8
β’ (π β (vol*βπ΅) β
β) |
49 | 47, 48 | readdcld 11189 |
. . . . . . 7
β’ (π β ((vol*βπ΄) + (vol*βπ΅)) β
β) |
50 | | ovolun.c |
. . . . . . . 8
β’ (π β πΆ β
β+) |
51 | 50 | rpred 12962 |
. . . . . . 7
β’ (π β πΆ β β) |
52 | 49, 51 | readdcld 11189 |
. . . . . 6
β’ (π β (((vol*βπ΄) + (vol*βπ΅)) + πΆ) β β) |
53 | | ovolun.s |
. . . . . . . . 9
β’ π = seq1( + , ((abs β
β ) β πΉ)) |
54 | | ovolun.t |
. . . . . . . . 9
β’ π = seq1( + , ((abs β
β ) β πΊ)) |
55 | | ovolun.f2 |
. . . . . . . . 9
β’ (π β π΄ β βͺ ran
((,) β πΉ)) |
56 | | ovolun.f3 |
. . . . . . . . 9
β’ (π β sup(ran π, β*, < ) β€
((vol*βπ΄) + (πΆ / 2))) |
57 | | ovolun.g2 |
. . . . . . . . 9
β’ (π β π΅ β βͺ ran
((,) β πΊ)) |
58 | | ovolun.g3 |
. . . . . . . . 9
β’ (π β sup(ran π, β*, < ) β€
((vol*βπ΅) + (πΆ / 2))) |
59 | 1, 3, 50, 53, 54, 25, 15, 55, 56, 6, 57, 58, 22 | ovolunlem1a 24876 |
. . . . . . . 8
β’ ((π β§ π β β) β (πβπ) β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ)) |
60 | 59 | ralrimiva 3140 |
. . . . . . 7
β’ (π β βπ β β (πβπ) β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ)) |
61 | | breq1 5109 |
. . . . . . . . 9
β’ (π§ = (πβπ) β (π§ β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ) β (πβπ) β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ))) |
62 | 61 | ralrn 7039 |
. . . . . . . 8
β’ (π Fn β β
(βπ§ β ran π π§ β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ) β βπ β β (πβπ) β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ))) |
63 | 40, 62 | syl 17 |
. . . . . . 7
β’ (π β (βπ§ β ran π π§ β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ) β βπ β β (πβπ) β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ))) |
64 | 60, 63 | mpbird 257 |
. . . . . 6
β’ (π β βπ§ β ran π π§ β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ)) |
65 | | brralrspcev 5166 |
. . . . . 6
β’
(((((vol*βπ΄) +
(vol*βπ΅)) + πΆ) β β β§
βπ§ β ran π π§ β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ)) β βπ β β βπ§ β ran π π§ β€ π) |
66 | 52, 64, 65 | syl2anc 585 |
. . . . 5
β’ (π β βπ β β βπ§ β ran π π§ β€ π) |
67 | | ressxr 11204 |
. . . . . . 7
β’ β
β β* |
68 | 31, 67 | sstrdi 3957 |
. . . . . 6
β’ (π β ran π β
β*) |
69 | | supxrbnd2 13247 |
. . . . . 6
β’ (ran
π β
β* β (βπ β β βπ§ β ran π π§ β€ π β sup(ran π, β*, < ) <
+β)) |
70 | 68, 69 | syl 17 |
. . . . 5
β’ (π β (βπ β β βπ§ β ran π π§ β€ π β sup(ran π, β*, < ) <
+β)) |
71 | 66, 70 | mpbid 231 |
. . . 4
β’ (π β sup(ran π, β*, < ) <
+β) |
72 | | supxrbnd 13253 |
. . . 4
β’ ((ran
π β β β§ ran
π β β
β§
sup(ran π,
β*, < ) < +β) β sup(ran π, β*, < ) β
β) |
73 | 31, 46, 71, 72 | syl3anc 1372 |
. . 3
β’ (π β sup(ran π, β*, < ) β
β) |
74 | | nncn 12166 |
. . . . . . . . . . . . . 14
β’ (π β β β π β
β) |
75 | 74 | adantl 483 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β) |
76 | | 1cnd 11155 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β 1 β
β) |
77 | 75 | 2timesd 12401 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (2 Β· π) = (π + π)) |
78 | 77 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((2 Β· π) β 1) = ((π + π) β 1)) |
79 | 75, 75, 76, 78 | assraddsubd 11574 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((2 Β· π) β 1) = (π + (π β 1))) |
80 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π β β) |
81 | | nnm1nn0 12459 |
. . . . . . . . . . . . 13
β’ (π β β β (π β 1) β
β0) |
82 | | nnnn0addcl 12448 |
. . . . . . . . . . . . 13
β’ ((π β β β§ (π β 1) β
β0) β (π + (π β 1)) β β) |
83 | 80, 81, 82 | syl2anc2 586 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π + (π β 1)) β β) |
84 | 79, 83 | eqeltrd 2834 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((2 Β· π) β 1) β
β) |
85 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π = ((2 Β· π) β 1) β (π / 2) = (((2 Β· π) β 1) /
2)) |
86 | 85 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π = ((2 Β· π) β 1) β ((π / 2) β β β (((2
Β· π) β 1) / 2)
β β)) |
87 | 85 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (π = ((2 Β· π) β 1) β (πΊβ(π / 2)) = (πΊβ(((2 Β· π) β 1) / 2))) |
88 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π = ((2 Β· π) β 1) β (π + 1) = (((2 Β· π) β 1) +
1)) |
89 | 88 | fvoveq1d 7380 |
. . . . . . . . . . . . . . 15
β’ (π = ((2 Β· π) β 1) β (πΉβ((π + 1) / 2)) = (πΉβ((((2 Β· π) β 1) + 1) / 2))) |
90 | 86, 87, 89 | ifbieq12d 4515 |
. . . . . . . . . . . . . 14
β’ (π = ((2 Β· π) β 1) β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) = if((((2 Β· π) β 1) / 2) β
β, (πΊβ(((2
Β· π) β 1) /
2)), (πΉβ((((2
Β· π) β 1) + 1)
/ 2)))) |
91 | | fvex 6856 |
. . . . . . . . . . . . . . 15
β’ (πΊβ(((2 Β· π) β 1) / 2)) β
V |
92 | | fvex 6856 |
. . . . . . . . . . . . . . 15
β’ (πΉβ((((2 Β· π) β 1) + 1) / 2)) β
V |
93 | 91, 92 | ifex 4537 |
. . . . . . . . . . . . . 14
β’ if((((2
Β· π) β 1) / 2)
β β, (πΊβ(((2 Β· π) β 1) / 2)), (πΉβ((((2 Β· π) β 1) + 1) / 2))) β
V |
94 | 90, 22, 93 | fvmpt 6949 |
. . . . . . . . . . . . 13
β’ (((2
Β· π) β 1)
β β β (π»β((2 Β· π) β 1)) = if((((2 Β· π) β 1) / 2) β
β, (πΊβ(((2
Β· π) β 1) /
2)), (πΉβ((((2
Β· π) β 1) + 1)
/ 2)))) |
95 | 84, 94 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π»β((2 Β· π) β 1)) = if((((2 Β· π) β 1) / 2) β
β, (πΊβ(((2
Β· π) β 1) /
2)), (πΉβ((((2
Β· π) β 1) + 1)
/ 2)))) |
96 | | 2nn 12231 |
. . . . . . . . . . . . . . . . . . . 20
β’ 2 β
β |
97 | | nnmulcl 12182 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((2
β β β§ π
β β) β (2 Β· π) β β) |
98 | 96, 80, 97 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π β§ π β β) β (2 Β· π) β
β) |
99 | 98 | nncnd 12174 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π β β) β (2 Β· π) β
β) |
100 | | ax-1cn 11114 |
. . . . . . . . . . . . . . . . . 18
β’ 1 β
β |
101 | | npcan 11415 |
. . . . . . . . . . . . . . . . . 18
β’ (((2
Β· π) β β
β§ 1 β β) β (((2 Β· π) β 1) + 1) = (2 Β· π)) |
102 | 99, 100, 101 | sylancl 587 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π β β) β (((2 Β· π) β 1) + 1) = (2 Β·
π)) |
103 | 102 | oveq1d 7373 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((((2 Β· π) β 1) + 1) / 2) = ((2
Β· π) /
2)) |
104 | | 2cn 12233 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
β |
105 | | 2ne0 12262 |
. . . . . . . . . . . . . . . . . 18
β’ 2 β
0 |
106 | | divcan3 11844 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β β β§ 2 β
β β§ 2 β 0) β ((2 Β· π) / 2) = π) |
107 | 104, 105,
106 | mp3an23 1454 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β ((2
Β· π) / 2) = π) |
108 | 75, 107 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β β) β ((2 Β· π) / 2) = π) |
109 | 103, 108 | eqtrd 2773 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((((2 Β· π) β 1) + 1) / 2) = π) |
110 | 109, 80 | eqeltrd 2834 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((((2 Β· π) β 1) + 1) / 2) β
β) |
111 | | nneo 12592 |
. . . . . . . . . . . . . . . 16
β’ (((2
Β· π) β 1)
β β β ((((2 Β· π) β 1) / 2) β β β Β¬
((((2 Β· π) β
1) + 1) / 2) β β)) |
112 | 84, 111 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β ((((2 Β· π) β 1) / 2) β β
β Β¬ ((((2 Β· π) β 1) + 1) / 2) β
β)) |
113 | 112 | con2bid 355 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (((((2 Β· π) β 1) + 1) / 2) β
β β Β¬ (((2 Β· π) β 1) / 2) β
β)) |
114 | 110, 113 | mpbid 231 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β Β¬ (((2 Β·
π) β 1) / 2) β
β) |
115 | 114 | iffalsed 4498 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β if((((2 Β·
π) β 1) / 2) β
β, (πΊβ(((2
Β· π) β 1) /
2)), (πΉβ((((2
Β· π) β 1) + 1)
/ 2))) = (πΉβ((((2
Β· π) β 1) + 1)
/ 2))) |
116 | 109 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΉβ((((2 Β· π) β 1) + 1) / 2)) = (πΉβπ)) |
117 | 95, 115, 116 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π»β((2 Β· π) β 1)) = (πΉβπ)) |
118 | | fveqeq2 6852 |
. . . . . . . . . . . 12
β’ (π = ((2 Β· π) β 1) β ((π»βπ) = (πΉβπ) β (π»β((2 Β· π) β 1)) = (πΉβπ))) |
119 | 118 | rspcev 3580 |
. . . . . . . . . . 11
β’ ((((2
Β· π) β 1)
β β β§ (π»β((2 Β· π) β 1)) = (πΉβπ)) β βπ β β (π»βπ) = (πΉβπ)) |
120 | 84, 117, 119 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β β) β βπ β β (π»βπ) = (πΉβπ)) |
121 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ ((π»βπ) = (πΉβπ) β (1st β(π»βπ)) = (1st β(πΉβπ))) |
122 | 121 | breq1d 5116 |
. . . . . . . . . . . . 13
β’ ((π»βπ) = (πΉβπ) β ((1st β(π»βπ)) < π§ β (1st β(πΉβπ)) < π§)) |
123 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ ((π»βπ) = (πΉβπ) β (2nd β(π»βπ)) = (2nd β(πΉβπ))) |
124 | 123 | breq2d 5118 |
. . . . . . . . . . . . 13
β’ ((π»βπ) = (πΉβπ) β (π§ < (2nd β(π»βπ)) β π§ < (2nd β(πΉβπ)))) |
125 | 122, 124 | anbi12d 632 |
. . . . . . . . . . . 12
β’ ((π»βπ) = (πΉβπ) β (((1st β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))) β ((1st β(πΉβπ)) < π§ β§ π§ < (2nd β(πΉβπ))))) |
126 | 125 | biimprcd 250 |
. . . . . . . . . . 11
β’
(((1st β(πΉβπ)) < π§ β§ π§ < (2nd β(πΉβπ))) β ((π»βπ) = (πΉβπ) β ((1st β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
127 | 126 | reximdv 3164 |
. . . . . . . . . 10
β’
(((1st β(πΉβπ)) < π§ β§ π§ < (2nd β(πΉβπ))) β (βπ β β (π»βπ) = (πΉβπ) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
128 | 120, 127 | syl5com 31 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((1st
β(πΉβπ)) < π§ β§ π§ < (2nd β(πΉβπ))) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
129 | 128 | rexlimdva 3149 |
. . . . . . . 8
β’ (π β (βπ β β ((1st
β(πΉβπ)) < π§ β§ π§ < (2nd β(πΉβπ))) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
130 | 129 | ralimdv 3163 |
. . . . . . 7
β’ (π β (βπ§ β π΄ βπ β β ((1st
β(πΉβπ)) < π§ β§ π§ < (2nd β(πΉβπ))) β βπ§ β π΄ βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
131 | | ovolfioo 24847 |
. . . . . . . 8
β’ ((π΄ β β β§ πΉ:ββΆ( β€ β©
(β Γ β))) β (π΄ β βͺ ran
((,) β πΉ) β
βπ§ β π΄ βπ β β ((1st
β(πΉβπ)) < π§ β§ π§ < (2nd β(πΉβπ))))) |
132 | 2, 17, 131 | syl2anc 585 |
. . . . . . 7
β’ (π β (π΄ β βͺ ran
((,) β πΉ) β
βπ§ β π΄ βπ β β ((1st
β(πΉβπ)) < π§ β§ π§ < (2nd β(πΉβπ))))) |
133 | | ovolfioo 24847 |
. . . . . . . 8
β’ ((π΄ β β β§ π»:ββΆ( β€ β©
(β Γ β))) β (π΄ β βͺ ran
((,) β π») β
βπ§ β π΄ βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
134 | 2, 23, 133 | syl2anc 585 |
. . . . . . 7
β’ (π β (π΄ β βͺ ran
((,) β π») β
βπ§ β π΄ βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
135 | 130, 132,
134 | 3imtr4d 294 |
. . . . . 6
β’ (π β (π΄ β βͺ ran
((,) β πΉ) β
π΄ β βͺ ran ((,) β π»))) |
136 | 55, 135 | mpd 15 |
. . . . 5
β’ (π β π΄ β βͺ ran
((,) β π»)) |
137 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π = (2 Β· π) β (π / 2) = ((2 Β· π) / 2)) |
138 | 137 | eleq1d 2819 |
. . . . . . . . . . . . . . 15
β’ (π = (2 Β· π) β ((π / 2) β β β ((2 Β·
π) / 2) β
β)) |
139 | 137 | fveq2d 6847 |
. . . . . . . . . . . . . . 15
β’ (π = (2 Β· π) β (πΊβ(π / 2)) = (πΊβ((2 Β· π) / 2))) |
140 | | oveq1 7365 |
. . . . . . . . . . . . . . . 16
β’ (π = (2 Β· π) β (π + 1) = ((2 Β· π) + 1)) |
141 | 140 | fvoveq1d 7380 |
. . . . . . . . . . . . . . 15
β’ (π = (2 Β· π) β (πΉβ((π + 1) / 2)) = (πΉβ(((2 Β· π) + 1) / 2))) |
142 | 138, 139,
141 | ifbieq12d 4515 |
. . . . . . . . . . . . . 14
β’ (π = (2 Β· π) β if((π / 2) β β, (πΊβ(π / 2)), (πΉβ((π + 1) / 2))) = if(((2 Β· π) / 2) β β, (πΊβ((2 Β· π) / 2)), (πΉβ(((2 Β· π) + 1) / 2)))) |
143 | | fvex 6856 |
. . . . . . . . . . . . . . 15
β’ (πΊβ((2 Β· π) / 2)) β
V |
144 | | fvex 6856 |
. . . . . . . . . . . . . . 15
β’ (πΉβ(((2 Β· π) + 1) / 2)) β
V |
145 | 143, 144 | ifex 4537 |
. . . . . . . . . . . . . 14
β’ if(((2
Β· π) / 2) β
β, (πΊβ((2
Β· π) / 2)), (πΉβ(((2 Β· π) + 1) / 2))) β
V |
146 | 142, 22, 145 | fvmpt 6949 |
. . . . . . . . . . . . 13
β’ ((2
Β· π) β β
β (π»β(2 Β·
π)) = if(((2 Β· π) / 2) β β, (πΊβ((2 Β· π) / 2)), (πΉβ(((2 Β· π) + 1) / 2)))) |
147 | 98, 146 | syl 17 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (π»β(2 Β· π)) = if(((2 Β· π) / 2) β β, (πΊβ((2 Β· π) / 2)), (πΉβ(((2 Β· π) + 1) / 2)))) |
148 | 108, 80 | eqeltrd 2834 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((2 Β· π) / 2) β
β) |
149 | 148 | iftrued 4495 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β if(((2 Β· π) / 2) β β, (πΊβ((2 Β· π) / 2)), (πΉβ(((2 Β· π) + 1) / 2))) = (πΊβ((2 Β· π) / 2))) |
150 | 108 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (πΊβ((2 Β· π) / 2)) = (πΊβπ)) |
151 | 147, 149,
150 | 3eqtrd 2777 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (π»β(2 Β· π)) = (πΊβπ)) |
152 | | fveqeq2 6852 |
. . . . . . . . . . . 12
β’ (π = (2 Β· π) β ((π»βπ) = (πΊβπ) β (π»β(2 Β· π)) = (πΊβπ))) |
153 | 152 | rspcev 3580 |
. . . . . . . . . . 11
β’ (((2
Β· π) β β
β§ (π»β(2 Β·
π)) = (πΊβπ)) β βπ β β (π»βπ) = (πΊβπ)) |
154 | 98, 151, 153 | syl2anc 585 |
. . . . . . . . . 10
β’ ((π β§ π β β) β βπ β β (π»βπ) = (πΊβπ)) |
155 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ ((π»βπ) = (πΊβπ) β (1st β(π»βπ)) = (1st β(πΊβπ))) |
156 | 155 | breq1d 5116 |
. . . . . . . . . . . . 13
β’ ((π»βπ) = (πΊβπ) β ((1st β(π»βπ)) < π§ β (1st β(πΊβπ)) < π§)) |
157 | | fveq2 6843 |
. . . . . . . . . . . . . 14
β’ ((π»βπ) = (πΊβπ) β (2nd β(π»βπ)) = (2nd β(πΊβπ))) |
158 | 157 | breq2d 5118 |
. . . . . . . . . . . . 13
β’ ((π»βπ) = (πΊβπ) β (π§ < (2nd β(π»βπ)) β π§ < (2nd β(πΊβπ)))) |
159 | 156, 158 | anbi12d 632 |
. . . . . . . . . . . 12
β’ ((π»βπ) = (πΊβπ) β (((1st β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))) β ((1st β(πΊβπ)) < π§ β§ π§ < (2nd β(πΊβπ))))) |
160 | 159 | biimprcd 250 |
. . . . . . . . . . 11
β’
(((1st β(πΊβπ)) < π§ β§ π§ < (2nd β(πΊβπ))) β ((π»βπ) = (πΊβπ) β ((1st β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
161 | 160 | reximdv 3164 |
. . . . . . . . . 10
β’
(((1st β(πΊβπ)) < π§ β§ π§ < (2nd β(πΊβπ))) β (βπ β β (π»βπ) = (πΊβπ) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
162 | 154, 161 | syl5com 31 |
. . . . . . . . 9
β’ ((π β§ π β β) β (((1st
β(πΊβπ)) < π§ β§ π§ < (2nd β(πΊβπ))) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
163 | 162 | rexlimdva 3149 |
. . . . . . . 8
β’ (π β (βπ β β ((1st
β(πΊβπ)) < π§ β§ π§ < (2nd β(πΊβπ))) β βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
164 | 163 | ralimdv 3163 |
. . . . . . 7
β’ (π β (βπ§ β π΅ βπ β β ((1st
β(πΊβπ)) < π§ β§ π§ < (2nd β(πΊβπ))) β βπ§ β π΅ βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
165 | | ovolfioo 24847 |
. . . . . . . 8
β’ ((π΅ β β β§ πΊ:ββΆ( β€ β©
(β Γ β))) β (π΅ β βͺ ran
((,) β πΊ) β
βπ§ β π΅ βπ β β ((1st
β(πΊβπ)) < π§ β§ π§ < (2nd β(πΊβπ))))) |
166 | 4, 8, 165 | syl2anc 585 |
. . . . . . 7
β’ (π β (π΅ β βͺ ran
((,) β πΊ) β
βπ§ β π΅ βπ β β ((1st
β(πΊβπ)) < π§ β§ π§ < (2nd β(πΊβπ))))) |
167 | | ovolfioo 24847 |
. . . . . . . 8
β’ ((π΅ β β β§ π»:ββΆ( β€ β©
(β Γ β))) β (π΅ β βͺ ran
((,) β π») β
βπ§ β π΅ βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
168 | 4, 23, 167 | syl2anc 585 |
. . . . . . 7
β’ (π β (π΅ β βͺ ran
((,) β π») β
βπ§ β π΅ βπ β β ((1st
β(π»βπ)) < π§ β§ π§ < (2nd β(π»βπ))))) |
169 | 164, 166,
168 | 3imtr4d 294 |
. . . . . 6
β’ (π β (π΅ β βͺ ran
((,) β πΊ) β
π΅ β βͺ ran ((,) β π»))) |
170 | 57, 169 | mpd 15 |
. . . . 5
β’ (π β π΅ β βͺ ran
((,) β π»)) |
171 | 136, 170 | unssd 4147 |
. . . 4
β’ (π β (π΄ βͺ π΅) β βͺ ran
((,) β π»)) |
172 | 25 | ovollb 24859 |
. . . 4
β’ ((π»:ββΆ( β€ β©
(β Γ β)) β§ (π΄ βͺ π΅) β βͺ ran
((,) β π»)) β
(vol*β(π΄ βͺ π΅)) β€ sup(ran π, β*, <
)) |
173 | 23, 171, 172 | syl2anc 585 |
. . 3
β’ (π β (vol*β(π΄ βͺ π΅)) β€ sup(ran π, β*, <
)) |
174 | | ovollecl 24863 |
. . 3
β’ (((π΄ βͺ π΅) β β β§ sup(ran π, β*, < )
β β β§ (vol*β(π΄ βͺ π΅)) β€ sup(ran π, β*, < )) β
(vol*β(π΄ βͺ π΅)) β
β) |
175 | 5, 73, 173, 174 | syl3anc 1372 |
. 2
β’ (π β (vol*β(π΄ βͺ π΅)) β β) |
176 | 52 | rexrd 11210 |
. . . 4
β’ (π β (((vol*βπ΄) + (vol*βπ΅)) + πΆ) β
β*) |
177 | | supxrleub 13251 |
. . . 4
β’ ((ran
π β
β* β§ (((vol*βπ΄) + (vol*βπ΅)) + πΆ) β β*) β
(sup(ran π,
β*, < ) β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ) β βπ§ β ran π π§ β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ))) |
178 | 68, 176, 177 | syl2anc 585 |
. . 3
β’ (π β (sup(ran π, β*, < ) β€
(((vol*βπ΄) +
(vol*βπ΅)) + πΆ) β βπ§ β ran π π§ β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ))) |
179 | 64, 178 | mpbird 257 |
. 2
β’ (π β sup(ran π, β*, < ) β€
(((vol*βπ΄) +
(vol*βπ΅)) + πΆ)) |
180 | 175, 73, 52, 173, 179 | letrd 11317 |
1
β’ (π β (vol*β(π΄ βͺ π΅)) β€ (((vol*βπ΄) + (vol*βπ΅)) + πΆ)) |