Step | Hyp | Ref
| Expression |
1 | | ovolsca.1 |
. . . . . 6
โข (๐ โ ๐ด โ โ) |
2 | 1 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ+) โ ๐ด โ
โ) |
3 | | ovolsca.4 |
. . . . . 6
โข (๐ โ (vol*โ๐ด) โ
โ) |
4 | 3 | adantr 482 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ+) โ
(vol*โ๐ด) โ
โ) |
5 | | ovolsca.2 |
. . . . . 6
โข (๐ โ ๐ถ โ
โ+) |
6 | | rpmulcl 12943 |
. . . . . 6
โข ((๐ถ โ โ+
โง ๐ฆ โ
โ+) โ (๐ถ ยท ๐ฆ) โ
โ+) |
7 | 5, 6 | sylan 581 |
. . . . 5
โข ((๐ โง ๐ฆ โ โ+) โ (๐ถ ยท ๐ฆ) โ
โ+) |
8 | | eqid 2733 |
. . . . . 6
โข seq1( + ,
((abs โ โ ) โ ๐)) = seq1( + , ((abs โ โ )
โ ๐)) |
9 | 8 | ovolgelb 24860 |
. . . . 5
โข ((๐ด โ โ โง
(vol*โ๐ด) โ
โ โง (๐ถ ยท
๐ฆ) โ
โ+) โ โ๐ โ (( โค โฉ (โ ร
โ)) โm โ)(๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ)))) |
10 | 2, 4, 7, 9 | syl3anc 1372 |
. . . 4
โข ((๐ โง ๐ฆ โ โ+) โ
โ๐ โ (( โค
โฉ (โ ร โ)) โm โ)(๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ)))) |
11 | 1 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ+) โง (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โง (๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ))))) โ ๐ด โ โ) |
12 | 5 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ+) โง (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โง (๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ))))) โ ๐ถ โ
โ+) |
13 | | ovolsca.3 |
. . . . . 6
โข (๐ โ ๐ต = {๐ฅ โ โ โฃ (๐ถ ยท ๐ฅ) โ ๐ด}) |
14 | 13 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ+) โง (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โง (๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ))))) โ ๐ต = {๐ฅ โ โ โฃ (๐ถ ยท ๐ฅ) โ ๐ด}) |
15 | 3 | ad2antrr 725 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ+) โง (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โง (๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ))))) โ (vol*โ๐ด) โ โ) |
16 | | 2fveq3 6848 |
. . . . . . . 8
โข (๐ = ๐ โ (1st โ(๐โ๐)) = (1st โ(๐โ๐))) |
17 | 16 | oveq1d 7373 |
. . . . . . 7
โข (๐ = ๐ โ ((1st โ(๐โ๐)) / ๐ถ) = ((1st โ(๐โ๐)) / ๐ถ)) |
18 | | 2fveq3 6848 |
. . . . . . . 8
โข (๐ = ๐ โ (2nd โ(๐โ๐)) = (2nd โ(๐โ๐))) |
19 | 18 | oveq1d 7373 |
. . . . . . 7
โข (๐ = ๐ โ ((2nd โ(๐โ๐)) / ๐ถ) = ((2nd โ(๐โ๐)) / ๐ถ)) |
20 | 17, 19 | opeq12d 4839 |
. . . . . 6
โข (๐ = ๐ โ โจ((1st โ(๐โ๐)) / ๐ถ), ((2nd โ(๐โ๐)) / ๐ถ)โฉ = โจ((1st
โ(๐โ๐)) / ๐ถ), ((2nd โ(๐โ๐)) / ๐ถ)โฉ) |
21 | 20 | cbvmptv 5219 |
. . . . 5
โข (๐ โ โ โฆ
โจ((1st โ(๐โ๐)) / ๐ถ), ((2nd โ(๐โ๐)) / ๐ถ)โฉ) = (๐ โ โ โฆ
โจ((1st โ(๐โ๐)) / ๐ถ), ((2nd โ(๐โ๐)) / ๐ถ)โฉ) |
22 | | elmapi 8790 |
. . . . . 6
โข (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โ ๐:โโถ( โค โฉ (โ ร
โ))) |
23 | 22 | ad2antrl 727 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ+) โง (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โง (๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ))))) โ ๐:โโถ( โค โฉ (โ ร
โ))) |
24 | | simprrl 780 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ+) โง (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โง (๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ))))) โ ๐ด โ โช ran
((,) โ ๐)) |
25 | | simplr 768 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ+) โง (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โง (๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ))))) โ ๐ฆ โ โ+) |
26 | | simprrr 781 |
. . . . 5
โข (((๐ โง ๐ฆ โ โ+) โง (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โง (๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ))))) โ sup(ran seq1( + , ((abs โ
โ ) โ ๐)),
โ*, < ) โค ((vol*โ๐ด) + (๐ถ ยท ๐ฆ))) |
27 | 11, 12, 14, 15, 8, 21, 23, 24, 25, 26 | ovolscalem1 24893 |
. . . 4
โข (((๐ โง ๐ฆ โ โ+) โง (๐ โ (( โค โฉ (โ
ร โ)) โm โ) โง (๐ด โ โช ran
((,) โ ๐) โง
sup(ran seq1( + , ((abs โ โ ) โ ๐)), โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐ฆ))))) โ (vol*โ๐ต) โค (((vol*โ๐ด) / ๐ถ) + ๐ฆ)) |
28 | 10, 27 | rexlimddv 3155 |
. . 3
โข ((๐ โง ๐ฆ โ โ+) โ
(vol*โ๐ต) โค
(((vol*โ๐ด) / ๐ถ) + ๐ฆ)) |
29 | 28 | ralrimiva 3140 |
. 2
โข (๐ โ โ๐ฆ โ โ+ (vol*โ๐ต) โค (((vol*โ๐ด) / ๐ถ) + ๐ฆ)) |
30 | | ssrab2 4038 |
. . . . 5
โข {๐ฅ โ โ โฃ (๐ถ ยท ๐ฅ) โ ๐ด} โ โ |
31 | 13, 30 | eqsstrdi 3999 |
. . . 4
โข (๐ โ ๐ต โ โ) |
32 | | ovolcl 24858 |
. . . 4
โข (๐ต โ โ โ
(vol*โ๐ต) โ
โ*) |
33 | 31, 32 | syl 17 |
. . 3
โข (๐ โ (vol*โ๐ต) โ
โ*) |
34 | 3, 5 | rerpdivcld 12993 |
. . 3
โข (๐ โ ((vol*โ๐ด) / ๐ถ) โ โ) |
35 | | xralrple 13130 |
. . 3
โข
(((vol*โ๐ต)
โ โ* โง ((vol*โ๐ด) / ๐ถ) โ โ) โ ((vol*โ๐ต) โค ((vol*โ๐ด) / ๐ถ) โ โ๐ฆ โ โ+ (vol*โ๐ต) โค (((vol*โ๐ด) / ๐ถ) + ๐ฆ))) |
36 | 33, 34, 35 | syl2anc 585 |
. 2
โข (๐ โ ((vol*โ๐ต) โค ((vol*โ๐ด) / ๐ถ) โ โ๐ฆ โ โ+ (vol*โ๐ต) โค (((vol*โ๐ด) / ๐ถ) + ๐ฆ))) |
37 | 29, 36 | mpbird 257 |
1
โข (๐ โ (vol*โ๐ต) โค ((vol*โ๐ด) / ๐ถ)) |