Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . 4
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (volโ๐ด) โ
โ) โ ๐ด โ
dom vol) |
2 | | simpr 486 |
. . . 4
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (volโ๐ด) โ
โ) โ (volโ๐ด) โ โ) |
3 | | rpre 12852 |
. . . . . 6
โข (๐ต โ โ+
โ ๐ต โ
โ) |
4 | 3 | ad2antlr 726 |
. . . . 5
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (volโ๐ด) โ
โ) โ ๐ต โ
โ) |
5 | | rpge0 12857 |
. . . . . 6
โข (๐ต โ โ+
โ 0 โค ๐ต) |
6 | 5 | ad2antlr 726 |
. . . . 5
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (volโ๐ด) โ
โ) โ 0 โค ๐ต) |
7 | | elrege0 13300 |
. . . . 5
โข (๐ต โ (0[,)+โ) โ
(๐ต โ โ โง 0
โค ๐ต)) |
8 | 4, 6, 7 | sylanbrc 584 |
. . . 4
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (volโ๐ด) โ
โ) โ ๐ต โ
(0[,)+โ)) |
9 | | itg2const 25027 |
. . . 4
โข ((๐ด โ dom vol โง
(volโ๐ด) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) = (๐ต ยท (volโ๐ด))) |
10 | 1, 2, 8, 9 | syl3anc 1372 |
. . 3
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (volโ๐ด) โ
โ) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) = (๐ต ยท (volโ๐ด))) |
11 | 4, 2 | remulcld 11119 |
. . 3
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (volโ๐ด) โ
โ) โ (๐ต ยท
(volโ๐ด)) โ
โ) |
12 | 10, 11 | eqeltrd 2839 |
. 2
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (volโ๐ด) โ
โ) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) |
13 | | mblvol 24816 |
. . . 4
โข (๐ด โ dom vol โ
(volโ๐ด) =
(vol*โ๐ด)) |
14 | 13 | ad2antrr 725 |
. . 3
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
(volโ๐ด) =
(vol*โ๐ด)) |
15 | | mblss 24817 |
. . . . . 6
โข (๐ด โ dom vol โ ๐ด โ
โ) |
16 | 15 | ad3antrrr 729 |
. . . . 5
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(vol*โ๐ด) โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) โ ๐ด โ โ) |
17 | | peano2re 11262 |
. . . . . . . 8
โข
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ โ
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) โ โ) |
18 | 17 | adantl 483 |
. . . . . . 7
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) โ โ) |
19 | | simplr 768 |
. . . . . . 7
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ ๐ต โ
โ+) |
20 | 18, 19 | rerpdivcld 12917 |
. . . . . 6
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ โ) |
21 | 20 | adantr 482 |
. . . . 5
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(vol*โ๐ด) โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) โ (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ โ) |
22 | | simpr 486 |
. . . . 5
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(vol*โ๐ด) โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) โ (vol*โ๐ด) โค (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) |
23 | | ovollecl 24769 |
. . . . 5
โข ((๐ด โ โ โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ โ โง (vol*โ๐ด) โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) โ (vol*โ๐ด) โ โ) |
24 | 16, 21, 22, 23 | syl3anc 1372 |
. . . 4
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(vol*โ๐ด) โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) โ (vol*โ๐ด) โ โ) |
25 | | simplll 774 |
. . . . . . . 8
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ ๐ด โ dom vol) |
26 | 20 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ โ) |
27 | 26 | rexrd 11139 |
. . . . . . . . 9
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ
โ*) |
28 | | simpr 486 |
. . . . . . . . . . . . 13
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0))) โ โ) |
29 | 3 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ฅ โ โ)
โ ๐ต โ
โ) |
30 | 29 | rexrd 11139 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ฅ โ โ)
โ ๐ต โ
โ*) |
31 | 5 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ฅ โ โ)
โ 0 โค ๐ต) |
32 | | elxrge0 13303 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต โ (0[,]+โ) โ
(๐ต โ
โ* โง 0 โค ๐ต)) |
33 | 30, 31, 32 | sylanbrc 584 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ฅ โ โ)
โ ๐ต โ
(0[,]+โ)) |
34 | | 0e0iccpnf 13305 |
. . . . . . . . . . . . . . . . 17
โข 0 โ
(0[,]+โ) |
35 | | ifcl 4530 |
. . . . . . . . . . . . . . . . 17
โข ((๐ต โ (0[,]+โ) โง 0
โ (0[,]+โ)) โ if(๐ฅ โ ๐ด, ๐ต, 0) โ (0[,]+โ)) |
36 | 33, 34, 35 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ฅ โ โ)
โ if(๐ฅ โ ๐ด, ๐ต, 0) โ (0[,]+โ)) |
37 | 36 | fmpttd 7058 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ (๐ฅ โ โ
โฆ if(๐ฅ โ ๐ด, ๐ต,
0)):โโถ(0[,]+โ)) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . . 14
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต,
0)):โโถ(0[,]+โ)) |
39 | | itg2ge0 25022 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)):โโถ(0[,]+โ) โ 0
โค (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . 13
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ 0 โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0)))) |
41 | 28, 40 | ge0p1rpd 12916 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) โ
โ+) |
42 | 41, 19 | rpdivcld 12903 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ
โ+) |
43 | 42 | rpge0d 12890 |
. . . . . . . . . 10
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ 0 โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) |
44 | 43 | adantr 482 |
. . . . . . . . 9
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ 0 โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) |
45 | 14 | breq2d 5116 |
. . . . . . . . . 10
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
((((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (volโ๐ด) โ (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด))) |
46 | 45 | biimpar 479 |
. . . . . . . . 9
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (volโ๐ด)) |
47 | | 0xr 11136 |
. . . . . . . . . 10
โข 0 โ
โ* |
48 | | iccssxr 13276 |
. . . . . . . . . . . 12
โข
(0[,]+โ) โ โ* |
49 | | volf 24815 |
. . . . . . . . . . . . 13
โข vol:dom
volโถ(0[,]+โ) |
50 | 49 | ffvelcdmi 7029 |
. . . . . . . . . . . 12
โข (๐ด โ dom vol โ
(volโ๐ด) โ
(0[,]+โ)) |
51 | 48, 50 | sselid 3941 |
. . . . . . . . . . 11
โข (๐ด โ dom vol โ
(volโ๐ด) โ
โ*) |
52 | 25, 51 | syl 17 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ (volโ๐ด) โ
โ*) |
53 | | elicc1 13237 |
. . . . . . . . . 10
โข ((0
โ โ* โง (volโ๐ด) โ โ*) โ
((((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ (0[,](volโ๐ด)) โ ((((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ โ* โง 0 โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โง (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (volโ๐ด)))) |
54 | 47, 52, 53 | sylancr 588 |
. . . . . . . . 9
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ ((((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ (0[,](volโ๐ด)) โ ((((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ โ* โง 0 โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โง (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (volโ๐ด)))) |
55 | 27, 44, 46, 54 | mpbir3and 1343 |
. . . . . . . 8
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ (0[,](volโ๐ด))) |
56 | | volivth 24893 |
. . . . . . . 8
โข ((๐ด โ dom vol โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ (0[,](volโ๐ด))) โ โ๐ง โ dom vol(๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต))) |
57 | 25, 55, 56 | syl2anc 585 |
. . . . . . 7
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ โ๐ง โ dom vol(๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต))) |
58 | 57 | ex 414 |
. . . . . 6
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
((((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด) โ โ๐ง โ dom vol(๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) |
59 | | simprl 770 |
. . . . . . . . . . 11
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ ๐ง โ dom vol) |
60 | | simprrr 781 |
. . . . . . . . . . . 12
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) |
61 | 20 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ โ) |
62 | 60, 61 | eqeltrd 2839 |
. . . . . . . . . . 11
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (volโ๐ง) โ โ) |
63 | 3 | ad2antlr 726 |
. . . . . . . . . . . . 13
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ ๐ต โ
โ) |
64 | 63 | adantr 482 |
. . . . . . . . . . . 12
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ ๐ต โ โ) |
65 | 19 | adantr 482 |
. . . . . . . . . . . . 13
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ ๐ต โ
โ+) |
66 | 65 | rpge0d 12890 |
. . . . . . . . . . . 12
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ 0 โค ๐ต) |
67 | 64, 66, 7 | sylanbrc 584 |
. . . . . . . . . . 11
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ ๐ต โ (0[,)+โ)) |
68 | | itg2const 25027 |
. . . . . . . . . . 11
โข ((๐ง โ dom vol โง
(volโ๐ง) โ
โ โง ๐ต โ
(0[,)+โ)) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต, 0))) = (๐ต ยท (volโ๐ง))) |
69 | 59, 62, 67, 68 | syl3anc 1372 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต, 0))) = (๐ต ยท (volโ๐ง))) |
70 | 60 | oveq2d 7366 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (๐ต ยท (volโ๐ง)) = (๐ต ยท (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต))) |
71 | 18 | recnd 11117 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) โ โ) |
72 | 63 | recnd 11117 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ ๐ต โ
โ) |
73 | | rpne0 12860 |
. . . . . . . . . . . . 13
โข (๐ต โ โ+
โ ๐ต โ
0) |
74 | 73 | ad2antlr 726 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ ๐ต โ 0) |
75 | 71, 72, 74 | divcan2d 11867 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ (๐ต ยท
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) = ((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1)) |
76 | 75 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (๐ต ยท (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) = ((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1)) |
77 | 69, 70, 76 | 3eqtrd 2782 |
. . . . . . . . 9
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต, 0))) = ((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1)) |
78 | 3 | adantl 483 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ ๐ต โ
โ) |
79 | 78 | rexrd 11139 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ ๐ต โ
โ*) |
80 | 5 | adantl 483 |
. . . . . . . . . . . . . . 15
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ 0 โค ๐ต) |
81 | 79, 80, 32 | sylanbrc 584 |
. . . . . . . . . . . . . 14
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ ๐ต โ
(0[,]+โ)) |
82 | | ifcl 4530 |
. . . . . . . . . . . . . 14
โข ((๐ต โ (0[,]+โ) โง 0
โ (0[,]+โ)) โ if(๐ฅ โ ๐ง, ๐ต, 0) โ (0[,]+โ)) |
83 | 81, 34, 82 | sylancl 587 |
. . . . . . . . . . . . 13
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ if(๐ฅ โ ๐ง, ๐ต, 0) โ (0[,]+โ)) |
84 | 83 | adantr 482 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ฅ โ โ)
โ if(๐ฅ โ ๐ง, ๐ต, 0) โ (0[,]+โ)) |
85 | 84 | fmpttd 7058 |
. . . . . . . . . . 11
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ (๐ฅ โ โ
โฆ if(๐ฅ โ ๐ง, ๐ต,
0)):โโถ(0[,]+โ)) |
86 | 85 | ad2antrr 725 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต,
0)):โโถ(0[,]+โ)) |
87 | 38 | adantr 482 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต,
0)):โโถ(0[,]+โ)) |
88 | | simpl 484 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ (๐ด โ dom vol โง ๐ต โ
โ+)) |
89 | | simprl 770 |
. . . . . . . . . . 11
โข ((๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต))) โ ๐ง โ ๐ด) |
90 | 78 | ad3antrrr 729 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ dom
vol โง ๐ต โ
โ+) โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โง ๐ฅ โ ๐ง) โ ๐ต โ โ) |
91 | 90 | leidd 11655 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ dom
vol โง ๐ต โ
โ+) โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โง ๐ฅ โ ๐ง) โ ๐ต โค ๐ต) |
92 | | iftrue 4491 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ ๐ง โ if(๐ฅ โ ๐ง, ๐ต, 0) = ๐ต) |
93 | 92 | adantl 483 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ dom
vol โง ๐ต โ
โ+) โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โง ๐ฅ โ ๐ง) โ if(๐ฅ โ ๐ง, ๐ต, 0) = ๐ต) |
94 | | simplr 768 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โ ๐ง โ ๐ด) |
95 | 94 | sselda 3943 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ dom
vol โง ๐ต โ
โ+) โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โง ๐ฅ โ ๐ง) โ ๐ฅ โ ๐ด) |
96 | 95 | iftrued 4493 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ dom
vol โง ๐ต โ
โ+) โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โง ๐ฅ โ ๐ง) โ if(๐ฅ โ ๐ด, ๐ต, 0) = ๐ต) |
97 | 91, 93, 96 | 3brtr4d 5136 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ dom
vol โง ๐ต โ
โ+) โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โง ๐ฅ โ ๐ง) โ if(๐ฅ โ ๐ง, ๐ต, 0) โค if(๐ฅ โ ๐ด, ๐ต, 0)) |
98 | | iffalse 4494 |
. . . . . . . . . . . . . . . 16
โข (ยฌ
๐ฅ โ ๐ง โ if(๐ฅ โ ๐ง, ๐ต, 0) = 0) |
99 | 98 | adantl 483 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ dom
vol โง ๐ต โ
โ+) โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โง ยฌ ๐ฅ โ ๐ง) โ if(๐ฅ โ ๐ง, ๐ต, 0) = 0) |
100 | | 0le0 12188 |
. . . . . . . . . . . . . . . . 17
โข 0 โค
0 |
101 | | breq2 5108 |
. . . . . . . . . . . . . . . . . 18
โข (๐ต = if(๐ฅ โ ๐ด, ๐ต, 0) โ (0 โค ๐ต โ 0 โค if(๐ฅ โ ๐ด, ๐ต, 0))) |
102 | | breq2 5108 |
. . . . . . . . . . . . . . . . . 18
โข (0 =
if(๐ฅ โ ๐ด, ๐ต, 0) โ (0 โค 0 โ 0 โค if(๐ฅ โ ๐ด, ๐ต, 0))) |
103 | 101, 102 | ifboth 4524 |
. . . . . . . . . . . . . . . . 17
โข ((0 โค
๐ต โง 0 โค 0) โ 0
โค if(๐ฅ โ ๐ด, ๐ต, 0)) |
104 | 80, 100, 103 | sylancl 587 |
. . . . . . . . . . . . . . . 16
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ 0 โค if(๐ฅ โ
๐ด, ๐ต, 0)) |
105 | 104 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ dom
vol โง ๐ต โ
โ+) โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โง ยฌ ๐ฅ โ ๐ง) โ 0 โค if(๐ฅ โ ๐ด, ๐ต, 0)) |
106 | 99, 105 | eqbrtrd 5126 |
. . . . . . . . . . . . . 14
โข
(((((๐ด โ dom
vol โง ๐ต โ
โ+) โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โง ยฌ ๐ฅ โ ๐ง) โ if(๐ฅ โ ๐ง, ๐ต, 0) โค if(๐ฅ โ ๐ด, ๐ต, 0)) |
107 | 97, 106 | pm2.61dan 812 |
. . . . . . . . . . . . 13
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ง โ ๐ด) โง ๐ฅ โ โ) โ if(๐ฅ โ ๐ง, ๐ต, 0) โค if(๐ฅ โ ๐ด, ๐ต, 0)) |
108 | 107 | ralrimiva 3142 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ง โ ๐ด) โ โ๐ฅ โ โ if(๐ฅ โ ๐ง, ๐ต, 0) โค if(๐ฅ โ ๐ด, ๐ต, 0)) |
109 | | reex 11076 |
. . . . . . . . . . . . . . 15
โข โ
โ V |
110 | 109 | a1i 11 |
. . . . . . . . . . . . . 14
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ โ โ V) |
111 | | eqidd 2739 |
. . . . . . . . . . . . . 14
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ (๐ฅ โ โ
โฆ if(๐ฅ โ ๐ง, ๐ต, 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต, 0))) |
112 | | eqidd 2739 |
. . . . . . . . . . . . . 14
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ (๐ฅ โ โ
โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) = (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) |
113 | 110, 84, 36, 111, 112 | ofrfval2 7629 |
. . . . . . . . . . . . 13
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ ((๐ฅ โ โ
โฆ if(๐ฅ โ ๐ง, ๐ต, 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)) โ โ๐ฅ โ โ if(๐ฅ โ ๐ง, ๐ต, 0) โค if(๐ฅ โ ๐ด, ๐ต, 0))) |
114 | 113 | biimpar 479 |
. . . . . . . . . . . 12
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง โ๐ฅ โ
โ if(๐ฅ โ ๐ง, ๐ต, 0) โค if(๐ฅ โ ๐ด, ๐ต, 0)) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต, 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) |
115 | 108, 114 | syldan 592 |
. . . . . . . . . . 11
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง ๐ง โ ๐ด) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต, 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) |
116 | 88, 89, 115 | syl2an 597 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต, 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) |
117 | | itg2le 25026 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต, 0)):โโถ(0[,]+โ) โง
(๐ฅ โ โ โฆ
if(๐ฅ โ ๐ด, ๐ต, 0)):โโถ(0[,]+โ) โง
(๐ฅ โ โ โฆ
if(๐ฅ โ ๐ง, ๐ต, 0)) โr โค (๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ง, ๐ต, 0))) โค (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) |
118 | 86, 87, 116, 117 | syl3anc 1372 |
. . . . . . . . 9
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ง, ๐ต, 0))) โค (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0)))) |
119 | 77, 118 | eqbrtrrd 5128 |
. . . . . . . 8
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ ((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0)))) |
120 | | ltp1 11929 |
. . . . . . . . . 10
โข
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ โ
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0))) < ((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1)) |
121 | 120 | ad2antlr 726 |
. . . . . . . . 9
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) < ((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1)) |
122 | | simplr 768 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) |
123 | 17 | ad2antlr 726 |
. . . . . . . . . 10
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ ((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) โ โ) |
124 | 122, 123 | ltnled 11236 |
. . . . . . . . 9
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ ((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) < ((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) โ ยฌ
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0))))) |
125 | 121, 124 | mpbid 231 |
. . . . . . . 8
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ ยฌ
((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) โค
(โซ2โ(๐ฅ
โ โ โฆ if(๐ฅ
โ ๐ด, ๐ต, 0)))) |
126 | 119, 125 | pm2.21dd 194 |
. . . . . . 7
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง (๐ง โ dom vol โง (๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)))) โ (vol*โ๐ด) โ โ) |
127 | 126 | rexlimdvaa 3152 |
. . . . . 6
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ (โ๐ง โ dom vol(๐ง โ ๐ด โง (volโ๐ง) = (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต)) โ (vol*โ๐ด) โ โ)) |
128 | 58, 127 | syld 47 |
. . . . 5
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
((((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด) โ (vol*โ๐ด) โ โ)) |
129 | 128 | imp 408 |
. . . 4
โข ((((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โง
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด)) โ (vol*โ๐ด) โ โ) |
130 | 51 | ad2antrr 725 |
. . . . . 6
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
(volโ๐ด) โ
โ*) |
131 | 14, 130 | eqeltrrd 2840 |
. . . . 5
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
(vol*โ๐ด) โ
โ*) |
132 | 20 | rexrd 11139 |
. . . . 5
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ
โ*) |
133 | | xrletri 13001 |
. . . . 5
โข
(((vol*โ๐ด)
โ โ* โง (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โ โ*) โ
((vol*โ๐ด) โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โจ (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด))) |
134 | 131, 132,
133 | syl2anc 585 |
. . . 4
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
((vol*โ๐ด) โค
(((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โจ (((โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) + 1) / ๐ต) โค (vol*โ๐ด))) |
135 | 24, 129, 134 | mpjaodan 958 |
. . 3
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
(vol*โ๐ด) โ
โ) |
136 | 14, 135 | eqeltrd 2839 |
. 2
โข (((๐ด โ dom vol โง ๐ต โ โ+)
โง (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ) โ
(volโ๐ด) โ
โ) |
137 | 12, 136 | impbida 800 |
1
โข ((๐ด โ dom vol โง ๐ต โ โ+)
โ ((volโ๐ด)
โ โ โ (โซ2โ(๐ฅ โ โ โฆ if(๐ฅ โ ๐ด, ๐ต, 0))) โ โ)) |