Step | Hyp | Ref
| Expression |
1 | | ovolsca.3 |
. . . 4
โข (๐ โ ๐ต = {๐ฅ โ โ โฃ (๐ถ ยท ๐ฅ) โ ๐ด}) |
2 | | ssrab2 4041 |
. . . 4
โข {๐ฅ โ โ โฃ (๐ถ ยท ๐ฅ) โ ๐ด} โ โ |
3 | 1, 2 | eqsstrdi 4002 |
. . 3
โข (๐ โ ๐ต โ โ) |
4 | | ovolcl 24865 |
. . 3
โข (๐ต โ โ โ
(vol*โ๐ต) โ
โ*) |
5 | 3, 4 | syl 17 |
. 2
โข (๐ โ (vol*โ๐ต) โ
โ*) |
6 | | ovolsca.7 |
. . . . . . . . . . . 12
โข (๐ โ ๐น:โโถ( โค โฉ (โ
ร โ))) |
7 | | ovolfcl 24853 |
. . . . . . . . . . . 12
โข ((๐น:โโถ( โค โฉ
(โ ร โ)) โง ๐ โ โ) โ ((1st
โ(๐นโ๐)) โ โ โง
(2nd โ(๐นโ๐)) โ โ โง (1st
โ(๐นโ๐)) โค (2nd
โ(๐นโ๐)))) |
8 | 6, 7 | sylan 581 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ ((1st
โ(๐นโ๐)) โ โ โง
(2nd โ(๐นโ๐)) โ โ โง (1st
โ(๐นโ๐)) โค (2nd
โ(๐นโ๐)))) |
9 | 8 | simp3d 1145 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (1st
โ(๐นโ๐)) โค (2nd
โ(๐นโ๐))) |
10 | 8 | simp1d 1143 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (1st
โ(๐นโ๐)) โ
โ) |
11 | 8 | simp2d 1144 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (2nd
โ(๐นโ๐)) โ
โ) |
12 | | ovolsca.2 |
. . . . . . . . . . . . 13
โข (๐ โ ๐ถ โ
โ+) |
13 | 12 | rpregt0d 12971 |
. . . . . . . . . . . 12
โข (๐ โ (๐ถ โ โ โง 0 < ๐ถ)) |
14 | 13 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (๐ถ โ โ โง 0 < ๐ถ)) |
15 | | lediv1 12028 |
. . . . . . . . . . 11
โข
(((1st โ(๐นโ๐)) โ โ โง (2nd
โ(๐นโ๐)) โ โ โง (๐ถ โ โ โง 0 <
๐ถ)) โ ((1st
โ(๐นโ๐)) โค (2nd
โ(๐นโ๐)) โ ((1st
โ(๐นโ๐)) / ๐ถ) โค ((2nd โ(๐นโ๐)) / ๐ถ))) |
16 | 10, 11, 14, 15 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ((1st
โ(๐นโ๐)) โค (2nd
โ(๐นโ๐)) โ ((1st
โ(๐นโ๐)) / ๐ถ) โค ((2nd โ(๐นโ๐)) / ๐ถ))) |
17 | 9, 16 | mpbid 231 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((1st
โ(๐นโ๐)) / ๐ถ) โค ((2nd โ(๐นโ๐)) / ๐ถ)) |
18 | | df-br 5110 |
. . . . . . . . 9
โข
(((1st โ(๐นโ๐)) / ๐ถ) โค ((2nd โ(๐นโ๐)) / ๐ถ) โ โจ((1st
โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ โ โค ) |
19 | 17, 18 | sylib 217 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ
โจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ โ โค ) |
20 | 12 | adantr 482 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ๐ถ โ
โ+) |
21 | 10, 20 | rerpdivcld 12996 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((1st
โ(๐นโ๐)) / ๐ถ) โ โ) |
22 | 11, 20 | rerpdivcld 12996 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ((2nd
โ(๐นโ๐)) / ๐ถ) โ โ) |
23 | 21, 22 | opelxpd 5675 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ
โจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ โ (โ ร
โ)) |
24 | 19, 23 | elind 4158 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ
โจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ โ ( โค โฉ (โ ร
โ))) |
25 | | ovolsca.6 |
. . . . . . 7
โข ๐บ = (๐ โ โ โฆ
โจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ) |
26 | 24, 25 | fmptd 7066 |
. . . . . 6
โข (๐ โ ๐บ:โโถ( โค โฉ (โ
ร โ))) |
27 | | eqid 2733 |
. . . . . . 7
โข ((abs
โ โ ) โ ๐บ) = ((abs โ โ ) โ ๐บ) |
28 | | eqid 2733 |
. . . . . . 7
โข seq1( + ,
((abs โ โ ) โ ๐บ)) = seq1( + , ((abs โ โ )
โ ๐บ)) |
29 | 27, 28 | ovolsf 24859 |
. . . . . 6
โข (๐บ:โโถ( โค โฉ
(โ ร โ)) โ seq1( + , ((abs โ โ ) โ
๐บ)):โโถ(0[,)+โ)) |
30 | 26, 29 | syl 17 |
. . . . 5
โข (๐ โ seq1( + , ((abs โ
โ ) โ ๐บ)):โโถ(0[,)+โ)) |
31 | 30 | frnd 6680 |
. . . 4
โข (๐ โ ran seq1( + , ((abs
โ โ ) โ ๐บ)) โ (0[,)+โ)) |
32 | | icossxr 13358 |
. . . 4
โข
(0[,)+โ) โ โ* |
33 | 31, 32 | sstrdi 3960 |
. . 3
โข (๐ โ ran seq1( + , ((abs
โ โ ) โ ๐บ)) โ
โ*) |
34 | | supxrcl 13243 |
. . 3
โข (ran
seq1( + , ((abs โ โ ) โ ๐บ)) โ โ* โ
sup(ran seq1( + , ((abs โ โ ) โ ๐บ)), โ*, < ) โ
โ*) |
35 | 33, 34 | syl 17 |
. 2
โข (๐ โ sup(ran seq1( + , ((abs
โ โ ) โ ๐บ)), โ*, < ) โ
โ*) |
36 | | ovolsca.4 |
. . . . 5
โข (๐ โ (vol*โ๐ด) โ
โ) |
37 | 36, 12 | rerpdivcld 12996 |
. . . 4
โข (๐ โ ((vol*โ๐ด) / ๐ถ) โ โ) |
38 | | ovolsca.9 |
. . . . 5
โข (๐ โ ๐
โ
โ+) |
39 | 38 | rpred 12965 |
. . . 4
โข (๐ โ ๐
โ โ) |
40 | 37, 39 | readdcld 11192 |
. . 3
โข (๐ โ (((vol*โ๐ด) / ๐ถ) + ๐
) โ โ) |
41 | 40 | rexrd 11213 |
. 2
โข (๐ โ (((vol*โ๐ด) / ๐ถ) + ๐
) โ
โ*) |
42 | 1 | eleq2d 2820 |
. . . . . . 7
โข (๐ โ (๐ฆ โ ๐ต โ ๐ฆ โ {๐ฅ โ โ โฃ (๐ถ ยท ๐ฅ) โ ๐ด})) |
43 | | oveq2 7369 |
. . . . . . . . 9
โข (๐ฅ = ๐ฆ โ (๐ถ ยท ๐ฅ) = (๐ถ ยท ๐ฆ)) |
44 | 43 | eleq1d 2819 |
. . . . . . . 8
โข (๐ฅ = ๐ฆ โ ((๐ถ ยท ๐ฅ) โ ๐ด โ (๐ถ ยท ๐ฆ) โ ๐ด)) |
45 | 44 | elrab 3649 |
. . . . . . 7
โข (๐ฆ โ {๐ฅ โ โ โฃ (๐ถ ยท ๐ฅ) โ ๐ด} โ (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) |
46 | 42, 45 | bitrdi 287 |
. . . . . 6
โข (๐ โ (๐ฆ โ ๐ต โ (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด))) |
47 | | breq2 5113 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ถ ยท ๐ฆ) โ ((1st โ(๐นโ๐)) < ๐ฅ โ (1st โ(๐นโ๐)) < (๐ถ ยท ๐ฆ))) |
48 | | breq1 5112 |
. . . . . . . . . . 11
โข (๐ฅ = (๐ถ ยท ๐ฆ) โ (๐ฅ < (2nd โ(๐นโ๐)) โ (๐ถ ยท ๐ฆ) < (2nd โ(๐นโ๐)))) |
49 | 47, 48 | anbi12d 632 |
. . . . . . . . . 10
โข (๐ฅ = (๐ถ ยท ๐ฆ) โ (((1st โ(๐นโ๐)) < ๐ฅ โง ๐ฅ < (2nd โ(๐นโ๐))) โ ((1st โ(๐นโ๐)) < (๐ถ ยท ๐ฆ) โง (๐ถ ยท ๐ฆ) < (2nd โ(๐นโ๐))))) |
50 | 49 | rexbidv 3172 |
. . . . . . . . 9
โข (๐ฅ = (๐ถ ยท ๐ฆ) โ (โ๐ โ โ ((1st
โ(๐นโ๐)) < ๐ฅ โง ๐ฅ < (2nd โ(๐นโ๐))) โ โ๐ โ โ ((1st
โ(๐นโ๐)) < (๐ถ ยท ๐ฆ) โง (๐ถ ยท ๐ฆ) < (2nd โ(๐นโ๐))))) |
51 | | ovolsca.8 |
. . . . . . . . . . 11
โข (๐ โ ๐ด โ โช ran
((,) โ ๐น)) |
52 | | ovolsca.1 |
. . . . . . . . . . . 12
โข (๐ โ ๐ด โ โ) |
53 | | ovolfioo 24854 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐น:โโถ( โค โฉ
(โ ร โ))) โ (๐ด โ โช ran
((,) โ ๐น) โ
โ๐ฅ โ ๐ด โ๐ โ โ ((1st
โ(๐นโ๐)) < ๐ฅ โง ๐ฅ < (2nd โ(๐นโ๐))))) |
54 | 52, 6, 53 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (๐ด โ โช ran
((,) โ ๐น) โ
โ๐ฅ โ ๐ด โ๐ โ โ ((1st
โ(๐นโ๐)) < ๐ฅ โง ๐ฅ < (2nd โ(๐นโ๐))))) |
55 | 51, 54 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ โ๐ฅ โ ๐ด โ๐ โ โ ((1st
โ(๐นโ๐)) < ๐ฅ โง ๐ฅ < (2nd โ(๐นโ๐)))) |
56 | 55 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โ โ๐ฅ โ ๐ด โ๐ โ โ ((1st
โ(๐นโ๐)) < ๐ฅ โง ๐ฅ < (2nd โ(๐นโ๐)))) |
57 | | simprr 772 |
. . . . . . . . 9
โข ((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โ (๐ถ ยท ๐ฆ) โ ๐ด) |
58 | 50, 56, 57 | rspcdva 3584 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โ โ๐ โ โ ((1st
โ(๐นโ๐)) < (๐ถ ยท ๐ฆ) โง (๐ถ ยท ๐ฆ) < (2nd โ(๐นโ๐)))) |
59 | | opex 5425 |
. . . . . . . . . . . . . . . 16
โข
โจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ โ V |
60 | 25 | fvmpt2 6963 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ โ โง
โจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ โ V) โ (๐บโ๐) = โจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ) |
61 | 59, 60 | mpan2 690 |
. . . . . . . . . . . . . . 15
โข (๐ โ โ โ (๐บโ๐) = โจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ) |
62 | 61 | fveq2d 6850 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(1st โ(๐บโ๐)) = (1st
โโจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ)) |
63 | | ovex 7394 |
. . . . . . . . . . . . . . 15
โข
((1st โ(๐นโ๐)) / ๐ถ) โ V |
64 | | ovex 7394 |
. . . . . . . . . . . . . . 15
โข
((2nd โ(๐นโ๐)) / ๐ถ) โ V |
65 | 63, 64 | op1st 7933 |
. . . . . . . . . . . . . 14
โข
(1st โโจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ) = ((1st โ(๐นโ๐)) / ๐ถ) |
66 | 62, 65 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(1st โ(๐บโ๐)) = ((1st โ(๐นโ๐)) / ๐ถ)) |
67 | 66 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ (1st
โ(๐บโ๐)) = ((1st
โ(๐นโ๐)) / ๐ถ)) |
68 | 67 | breq1d 5119 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ ((1st
โ(๐บโ๐)) < ๐ฆ โ ((1st โ(๐นโ๐)) / ๐ถ) < ๐ฆ)) |
69 | 10 | adantlr 714 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ (1st
โ(๐นโ๐)) โ
โ) |
70 | | simplrl 776 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ ๐ฆ โ โ) |
71 | 14 | adantlr 714 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ (๐ถ โ โ โง 0 < ๐ถ)) |
72 | | ltdivmul 12038 |
. . . . . . . . . . . 12
โข
(((1st โ(๐นโ๐)) โ โ โง ๐ฆ โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ (((1st
โ(๐นโ๐)) / ๐ถ) < ๐ฆ โ (1st โ(๐นโ๐)) < (๐ถ ยท ๐ฆ))) |
73 | 69, 70, 71, 72 | syl3anc 1372 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ (((1st
โ(๐นโ๐)) / ๐ถ) < ๐ฆ โ (1st โ(๐นโ๐)) < (๐ถ ยท ๐ฆ))) |
74 | 68, 73 | bitr2d 280 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ ((1st
โ(๐นโ๐)) < (๐ถ ยท ๐ฆ) โ (1st โ(๐บโ๐)) < ๐ฆ)) |
75 | 11 | adantlr 714 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ (2nd
โ(๐นโ๐)) โ
โ) |
76 | | ltmuldiv2 12037 |
. . . . . . . . . . . 12
โข ((๐ฆ โ โ โง
(2nd โ(๐นโ๐)) โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((๐ถ ยท ๐ฆ) < (2nd โ(๐นโ๐)) โ ๐ฆ < ((2nd โ(๐นโ๐)) / ๐ถ))) |
77 | 70, 75, 71, 76 | syl3anc 1372 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ ((๐ถ ยท ๐ฆ) < (2nd โ(๐นโ๐)) โ ๐ฆ < ((2nd โ(๐นโ๐)) / ๐ถ))) |
78 | 61 | fveq2d 6850 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ
(2nd โ(๐บโ๐)) = (2nd
โโจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ)) |
79 | 63, 64 | op2nd 7934 |
. . . . . . . . . . . . . 14
โข
(2nd โโจ((1st โ(๐นโ๐)) / ๐ถ), ((2nd โ(๐นโ๐)) / ๐ถ)โฉ) = ((2nd โ(๐นโ๐)) / ๐ถ) |
80 | 78, 79 | eqtrdi 2789 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ
(2nd โ(๐บโ๐)) = ((2nd โ(๐นโ๐)) / ๐ถ)) |
81 | 80 | adantl 483 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ (2nd
โ(๐บโ๐)) = ((2nd
โ(๐นโ๐)) / ๐ถ)) |
82 | 81 | breq2d 5121 |
. . . . . . . . . . 11
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ (๐ฆ < (2nd โ(๐บโ๐)) โ ๐ฆ < ((2nd โ(๐นโ๐)) / ๐ถ))) |
83 | 77, 82 | bitr4d 282 |
. . . . . . . . . 10
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ ((๐ถ ยท ๐ฆ) < (2nd โ(๐นโ๐)) โ ๐ฆ < (2nd โ(๐บโ๐)))) |
84 | 74, 83 | anbi12d 632 |
. . . . . . . . 9
โข (((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โง ๐ โ โ) โ (((1st
โ(๐นโ๐)) < (๐ถ ยท ๐ฆ) โง (๐ถ ยท ๐ฆ) < (2nd โ(๐นโ๐))) โ ((1st โ(๐บโ๐)) < ๐ฆ โง ๐ฆ < (2nd โ(๐บโ๐))))) |
85 | 84 | rexbidva 3170 |
. . . . . . . 8
โข ((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โ (โ๐ โ โ ((1st
โ(๐นโ๐)) < (๐ถ ยท ๐ฆ) โง (๐ถ ยท ๐ฆ) < (2nd โ(๐นโ๐))) โ โ๐ โ โ ((1st
โ(๐บโ๐)) < ๐ฆ โง ๐ฆ < (2nd โ(๐บโ๐))))) |
86 | 58, 85 | mpbid 231 |
. . . . . . 7
โข ((๐ โง (๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด)) โ โ๐ โ โ ((1st
โ(๐บโ๐)) < ๐ฆ โง ๐ฆ < (2nd โ(๐บโ๐)))) |
87 | 86 | ex 414 |
. . . . . 6
โข (๐ โ ((๐ฆ โ โ โง (๐ถ ยท ๐ฆ) โ ๐ด) โ โ๐ โ โ ((1st
โ(๐บโ๐)) < ๐ฆ โง ๐ฆ < (2nd โ(๐บโ๐))))) |
88 | 46, 87 | sylbid 239 |
. . . . 5
โข (๐ โ (๐ฆ โ ๐ต โ โ๐ โ โ ((1st
โ(๐บโ๐)) < ๐ฆ โง ๐ฆ < (2nd โ(๐บโ๐))))) |
89 | 88 | ralrimiv 3139 |
. . . 4
โข (๐ โ โ๐ฆ โ ๐ต โ๐ โ โ ((1st
โ(๐บโ๐)) < ๐ฆ โง ๐ฆ < (2nd โ(๐บโ๐)))) |
90 | | ovolfioo 24854 |
. . . . 5
โข ((๐ต โ โ โง ๐บ:โโถ( โค โฉ
(โ ร โ))) โ (๐ต โ โช ran
((,) โ ๐บ) โ
โ๐ฆ โ ๐ต โ๐ โ โ ((1st
โ(๐บโ๐)) < ๐ฆ โง ๐ฆ < (2nd โ(๐บโ๐))))) |
91 | 3, 26, 90 | syl2anc 585 |
. . . 4
โข (๐ โ (๐ต โ โช ran
((,) โ ๐บ) โ
โ๐ฆ โ ๐ต โ๐ โ โ ((1st
โ(๐บโ๐)) < ๐ฆ โง ๐ฆ < (2nd โ(๐บโ๐))))) |
92 | 89, 91 | mpbird 257 |
. . 3
โข (๐ โ ๐ต โ โช ran
((,) โ ๐บ)) |
93 | 28 | ovollb 24866 |
. . 3
โข ((๐บ:โโถ( โค โฉ
(โ ร โ)) โง ๐ต โ โช ran
((,) โ ๐บ)) โ
(vol*โ๐ต) โค sup(ran
seq1( + , ((abs โ โ ) โ ๐บ)), โ*, <
)) |
94 | 26, 92, 93 | syl2anc 585 |
. 2
โข (๐ โ (vol*โ๐ต) โค sup(ran seq1( + , ((abs
โ โ ) โ ๐บ)), โ*, <
)) |
95 | | fzfid 13887 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (1...๐) โ Fin) |
96 | 12 | rpcnd 12967 |
. . . . . . . . 9
โข (๐ โ ๐ถ โ โ) |
97 | 96 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ๐ถ โ โ) |
98 | | simpl 484 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ๐) |
99 | | elfznn 13479 |
. . . . . . . . . 10
โข (๐ โ (1...๐) โ ๐ โ โ) |
100 | 11, 10 | resubcld 11591 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ((2nd
โ(๐นโ๐)) โ (1st
โ(๐นโ๐))) โ
โ) |
101 | 98, 99, 100 | syl2an 597 |
. . . . . . . . 9
โข (((๐ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) โ โ) |
102 | 101 | recnd 11191 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ) โง ๐ โ (1...๐)) โ ((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) โ โ) |
103 | 12 | rpne0d 12970 |
. . . . . . . . 9
โข (๐ โ ๐ถ โ 0) |
104 | 103 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ๐ถ โ 0) |
105 | 95, 97, 102, 104 | fsumdivc 15679 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ (ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ) = ฮฃ๐ โ (1...๐)(((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ)) |
106 | 80, 66 | oveq12d 7379 |
. . . . . . . . . . 11
โข (๐ โ โ โ
((2nd โ(๐บโ๐)) โ (1st โ(๐บโ๐))) = (((2nd โ(๐นโ๐)) / ๐ถ) โ ((1st โ(๐นโ๐)) / ๐ถ))) |
107 | 106 | adantl 483 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ ((2nd
โ(๐บโ๐)) โ (1st
โ(๐บโ๐))) = (((2nd
โ(๐นโ๐)) / ๐ถ) โ ((1st โ(๐นโ๐)) / ๐ถ))) |
108 | 27 | ovolfsval 24857 |
. . . . . . . . . . 11
โข ((๐บ:โโถ( โค โฉ
(โ ร โ)) โง ๐ โ โ) โ (((abs โ
โ ) โ ๐บ)โ๐) = ((2nd โ(๐บโ๐)) โ (1st โ(๐บโ๐)))) |
109 | 26, 108 | sylan 581 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (((abs โ
โ ) โ ๐บ)โ๐) = ((2nd โ(๐บโ๐)) โ (1st โ(๐บโ๐)))) |
110 | 11 | recnd 11191 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (2nd
โ(๐นโ๐)) โ
โ) |
111 | 10 | recnd 11191 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (1st
โ(๐นโ๐)) โ
โ) |
112 | 12 | rpcnne0d 12974 |
. . . . . . . . . . . 12
โข (๐ โ (๐ถ โ โ โง ๐ถ โ 0)) |
113 | 112 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ (๐ถ โ โ โง ๐ถ โ 0)) |
114 | | divsubdir 11857 |
. . . . . . . . . . 11
โข
(((2nd โ(๐นโ๐)) โ โ โง (1st
โ(๐นโ๐)) โ โ โง (๐ถ โ โ โง ๐ถ โ 0)) โ
(((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ) = (((2nd โ(๐นโ๐)) / ๐ถ) โ ((1st โ(๐นโ๐)) / ๐ถ))) |
115 | 110, 111,
113, 114 | syl3anc 1372 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (((2nd
โ(๐นโ๐)) โ (1st
โ(๐นโ๐))) / ๐ถ) = (((2nd โ(๐นโ๐)) / ๐ถ) โ ((1st โ(๐นโ๐)) / ๐ถ))) |
116 | 107, 109,
115 | 3eqtr4d 2783 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (((abs โ
โ ) โ ๐บ)โ๐) = (((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ)) |
117 | 98, 99, 116 | syl2an 597 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((abs โ โ ) โ
๐บ)โ๐) = (((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ)) |
118 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ๐ โ โ) |
119 | | nnuz 12814 |
. . . . . . . . 9
โข โ =
(โคโฅโ1) |
120 | 118, 119 | eleqtrdi 2844 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ๐ โ
(โคโฅโ1)) |
121 | 100, 20 | rerpdivcld 12996 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ โ) โ (((2nd
โ(๐นโ๐)) โ (1st
โ(๐นโ๐))) / ๐ถ) โ โ) |
122 | 121 | recnd 11191 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ (((2nd
โ(๐นโ๐)) โ (1st
โ(๐นโ๐))) / ๐ถ) โ โ) |
123 | 98, 99, 122 | syl2an 597 |
. . . . . . . 8
โข (((๐ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ) โ โ) |
124 | 117, 120,
123 | fsumser 15623 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ฮฃ๐ โ (1...๐)(((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ) = (seq1( + , ((abs โ โ )
โ ๐บ))โ๐)) |
125 | 105, 124 | eqtrd 2773 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ) = (seq1( + , ((abs โ โ )
โ ๐บ))โ๐)) |
126 | | ovolsca.10 |
. . . . . . . . . . 11
โข (๐ โ sup(ran ๐, โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐
))) |
127 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
โข ((abs
โ โ ) โ ๐น) = ((abs โ โ ) โ ๐น) |
128 | | ovolsca.5 |
. . . . . . . . . . . . . . . 16
โข ๐ = seq1( + , ((abs โ
โ ) โ ๐น)) |
129 | 127, 128 | ovolsf 24859 |
. . . . . . . . . . . . . . 15
โข (๐น:โโถ( โค โฉ
(โ ร โ)) โ ๐:โโถ(0[,)+โ)) |
130 | 6, 129 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐:โโถ(0[,)+โ)) |
131 | 130 | frnd 6680 |
. . . . . . . . . . . . 13
โข (๐ โ ran ๐ โ (0[,)+โ)) |
132 | 131, 32 | sstrdi 3960 |
. . . . . . . . . . . 12
โข (๐ โ ran ๐ โ
โ*) |
133 | 12, 38 | rpmulcld 12981 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ถ ยท ๐
) โ
โ+) |
134 | 133 | rpred 12965 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ถ ยท ๐
) โ โ) |
135 | 36, 134 | readdcld 11192 |
. . . . . . . . . . . . 13
โข (๐ โ ((vol*โ๐ด) + (๐ถ ยท ๐
)) โ โ) |
136 | 135 | rexrd 11213 |
. . . . . . . . . . . 12
โข (๐ โ ((vol*โ๐ด) + (๐ถ ยท ๐
)) โ
โ*) |
137 | | supxrleub 13254 |
. . . . . . . . . . . 12
โข ((ran
๐ โ
โ* โง ((vol*โ๐ด) + (๐ถ ยท ๐
)) โ โ*) โ
(sup(ran ๐,
โ*, < ) โค ((vol*โ๐ด) + (๐ถ ยท ๐
)) โ โ๐ฅ โ ran ๐ ๐ฅ โค ((vol*โ๐ด) + (๐ถ ยท ๐
)))) |
138 | 132, 136,
137 | syl2anc 585 |
. . . . . . . . . . 11
โข (๐ โ (sup(ran ๐, โ*, < ) โค
((vol*โ๐ด) + (๐ถ ยท ๐
)) โ โ๐ฅ โ ran ๐ ๐ฅ โค ((vol*โ๐ด) + (๐ถ ยท ๐
)))) |
139 | 126, 138 | mpbid 231 |
. . . . . . . . . 10
โข (๐ โ โ๐ฅ โ ran ๐ ๐ฅ โค ((vol*โ๐ด) + (๐ถ ยท ๐
))) |
140 | 130 | ffnd 6673 |
. . . . . . . . . . 11
โข (๐ โ ๐ Fn โ) |
141 | | breq1 5112 |
. . . . . . . . . . . 12
โข (๐ฅ = (๐โ๐) โ (๐ฅ โค ((vol*โ๐ด) + (๐ถ ยท ๐
)) โ (๐โ๐) โค ((vol*โ๐ด) + (๐ถ ยท ๐
)))) |
142 | 141 | ralrn 7042 |
. . . . . . . . . . 11
โข (๐ Fn โ โ
(โ๐ฅ โ ran ๐ ๐ฅ โค ((vol*โ๐ด) + (๐ถ ยท ๐
)) โ โ๐ โ โ (๐โ๐) โค ((vol*โ๐ด) + (๐ถ ยท ๐
)))) |
143 | 140, 142 | syl 17 |
. . . . . . . . . 10
โข (๐ โ (โ๐ฅ โ ran ๐ ๐ฅ โค ((vol*โ๐ด) + (๐ถ ยท ๐
)) โ โ๐ โ โ (๐โ๐) โค ((vol*โ๐ด) + (๐ถ ยท ๐
)))) |
144 | 139, 143 | mpbid 231 |
. . . . . . . . 9
โข (๐ โ โ๐ โ โ (๐โ๐) โค ((vol*โ๐ด) + (๐ถ ยท ๐
))) |
145 | 144 | r19.21bi 3233 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (๐โ๐) โค ((vol*โ๐ด) + (๐ถ ยท ๐
))) |
146 | 6 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ โ) โ ๐น:โโถ( โค โฉ (โ
ร โ))) |
147 | 127 | ovolfsval 24857 |
. . . . . . . . . . 11
โข ((๐น:โโถ( โค โฉ
(โ ร โ)) โง ๐ โ โ) โ (((abs โ
โ ) โ ๐น)โ๐) = ((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐)))) |
148 | 146, 99, 147 | syl2an 597 |
. . . . . . . . . 10
โข (((๐ โง ๐ โ โ) โง ๐ โ (1...๐)) โ (((abs โ โ ) โ
๐น)โ๐) = ((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐)))) |
149 | 148, 120,
102 | fsumser 15623 |
. . . . . . . . 9
โข ((๐ โง ๐ โ โ) โ ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) = (seq1( + , ((abs โ โ )
โ ๐น))โ๐)) |
150 | 128 | fveq1i 6847 |
. . . . . . . . 9
โข (๐โ๐) = (seq1( + , ((abs โ โ )
โ ๐น))โ๐) |
151 | 149, 150 | eqtr4di 2791 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) = (๐โ๐)) |
152 | 37 | recnd 11191 |
. . . . . . . . . . 11
โข (๐ โ ((vol*โ๐ด) / ๐ถ) โ โ) |
153 | 38 | rpcnd 12967 |
. . . . . . . . . . 11
โข (๐ โ ๐
โ โ) |
154 | 96, 152, 153 | adddid 11187 |
. . . . . . . . . 10
โข (๐ โ (๐ถ ยท (((vol*โ๐ด) / ๐ถ) + ๐
)) = ((๐ถ ยท ((vol*โ๐ด) / ๐ถ)) + (๐ถ ยท ๐
))) |
155 | 36 | recnd 11191 |
. . . . . . . . . . . 12
โข (๐ โ (vol*โ๐ด) โ
โ) |
156 | 155, 96, 103 | divcan2d 11941 |
. . . . . . . . . . 11
โข (๐ โ (๐ถ ยท ((vol*โ๐ด) / ๐ถ)) = (vol*โ๐ด)) |
157 | 156 | oveq1d 7376 |
. . . . . . . . . 10
โข (๐ โ ((๐ถ ยท ((vol*โ๐ด) / ๐ถ)) + (๐ถ ยท ๐
)) = ((vol*โ๐ด) + (๐ถ ยท ๐
))) |
158 | 154, 157 | eqtrd 2773 |
. . . . . . . . 9
โข (๐ โ (๐ถ ยท (((vol*โ๐ด) / ๐ถ) + ๐
)) = ((vol*โ๐ด) + (๐ถ ยท ๐
))) |
159 | 158 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (๐ถ ยท (((vol*โ๐ด) / ๐ถ) + ๐
)) = ((vol*โ๐ด) + (๐ถ ยท ๐
))) |
160 | 145, 151,
159 | 3brtr4d 5141 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) โค (๐ถ ยท (((vol*โ๐ด) / ๐ถ) + ๐
))) |
161 | 95, 101 | fsumrecl 15627 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) โ โ) |
162 | 40 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (((vol*โ๐ด) / ๐ถ) + ๐
) โ โ) |
163 | 13 | adantr 482 |
. . . . . . . 8
โข ((๐ โง ๐ โ โ) โ (๐ถ โ โ โง 0 < ๐ถ)) |
164 | | ledivmul 12039 |
. . . . . . . 8
โข
((ฮฃ๐ โ
(1...๐)((2nd
โ(๐นโ๐)) โ (1st
โ(๐นโ๐))) โ โ โง
(((vol*โ๐ด) / ๐ถ) + ๐
) โ โ โง (๐ถ โ โ โง 0 < ๐ถ)) โ ((ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ) โค (((vol*โ๐ด) / ๐ถ) + ๐
) โ ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) โค (๐ถ ยท (((vol*โ๐ด) / ๐ถ) + ๐
)))) |
165 | 161, 162,
163, 164 | syl3anc 1372 |
. . . . . . 7
โข ((๐ โง ๐ โ โ) โ ((ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ) โค (((vol*โ๐ด) / ๐ถ) + ๐
) โ ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) โค (๐ถ ยท (((vol*โ๐ด) / ๐ถ) + ๐
)))) |
166 | 160, 165 | mpbird 257 |
. . . . . 6
โข ((๐ โง ๐ โ โ) โ (ฮฃ๐ โ (1...๐)((2nd โ(๐นโ๐)) โ (1st โ(๐นโ๐))) / ๐ถ) โค (((vol*โ๐ด) / ๐ถ) + ๐
)) |
167 | 125, 166 | eqbrtrrd 5133 |
. . . . 5
โข ((๐ โง ๐ โ โ) โ (seq1( + , ((abs
โ โ ) โ ๐บ))โ๐) โค (((vol*โ๐ด) / ๐ถ) + ๐
)) |
168 | 167 | ralrimiva 3140 |
. . . 4
โข (๐ โ โ๐ โ โ (seq1( + , ((abs โ
โ ) โ ๐บ))โ๐) โค (((vol*โ๐ด) / ๐ถ) + ๐
)) |
169 | 30 | ffnd 6673 |
. . . . 5
โข (๐ โ seq1( + , ((abs โ
โ ) โ ๐บ)) Fn
โ) |
170 | | breq1 5112 |
. . . . . 6
โข (๐ฆ = (seq1( + , ((abs โ
โ ) โ ๐บ))โ๐) โ (๐ฆ โค (((vol*โ๐ด) / ๐ถ) + ๐
) โ (seq1( + , ((abs โ โ )
โ ๐บ))โ๐) โค (((vol*โ๐ด) / ๐ถ) + ๐
))) |
171 | 170 | ralrn 7042 |
. . . . 5
โข (seq1( +
, ((abs โ โ ) โ ๐บ)) Fn โ โ (โ๐ฆ โ ran seq1( + , ((abs
โ โ ) โ ๐บ))๐ฆ โค (((vol*โ๐ด) / ๐ถ) + ๐
) โ โ๐ โ โ (seq1( + , ((abs โ
โ ) โ ๐บ))โ๐) โค (((vol*โ๐ด) / ๐ถ) + ๐
))) |
172 | 169, 171 | syl 17 |
. . . 4
โข (๐ โ (โ๐ฆ โ ran seq1( + , ((abs
โ โ ) โ ๐บ))๐ฆ โค (((vol*โ๐ด) / ๐ถ) + ๐
) โ โ๐ โ โ (seq1( + , ((abs โ
โ ) โ ๐บ))โ๐) โค (((vol*โ๐ด) / ๐ถ) + ๐
))) |
173 | 168, 172 | mpbird 257 |
. . 3
โข (๐ โ โ๐ฆ โ ran seq1( + , ((abs โ โ )
โ ๐บ))๐ฆ โค (((vol*โ๐ด) / ๐ถ) + ๐
)) |
174 | | supxrleub 13254 |
. . . 4
โข ((ran
seq1( + , ((abs โ โ ) โ ๐บ)) โ โ* โง
(((vol*โ๐ด) / ๐ถ) + ๐
) โ โ*) โ
(sup(ran seq1( + , ((abs โ โ ) โ ๐บ)), โ*, < ) โค
(((vol*โ๐ด) / ๐ถ) + ๐
) โ โ๐ฆ โ ran seq1( + , ((abs โ โ )
โ ๐บ))๐ฆ โค (((vol*โ๐ด) / ๐ถ) + ๐
))) |
175 | 33, 41, 174 | syl2anc 585 |
. . 3
โข (๐ โ (sup(ran seq1( + , ((abs
โ โ ) โ ๐บ)), โ*, < ) โค
(((vol*โ๐ด) / ๐ถ) + ๐
) โ โ๐ฆ โ ran seq1( + , ((abs โ โ )
โ ๐บ))๐ฆ โค (((vol*โ๐ด) / ๐ถ) + ๐
))) |
176 | 173, 175 | mpbird 257 |
. 2
โข (๐ โ sup(ran seq1( + , ((abs
โ โ ) โ ๐บ)), โ*, < ) โค
(((vol*โ๐ด) / ๐ถ) + ๐
)) |
177 | 5, 35, 41, 94, 176 | xrletrd 13090 |
1
โข (๐ โ (vol*โ๐ต) โค (((vol*โ๐ด) / ๐ถ) + ๐
)) |