Step | Hyp | Ref
| Expression |
1 | | unieq 4881 |
. . . . . . . . 9
โข (๐ด = โ
โ โช ๐ด =
โช โ
) |
2 | | uni0 4901 |
. . . . . . . . 9
โข โช โ
= โ
|
3 | 1, 2 | eqtrdi 2793 |
. . . . . . . 8
โข (๐ด = โ
โ โช ๐ด =
โ
) |
4 | 3 | fveq2d 6851 |
. . . . . . 7
โข (๐ด = โ
โ
(vol*โโช ๐ด) = (vol*โโ
)) |
5 | | ovol0 24873 |
. . . . . . 7
โข
(vol*โโ
) = 0 |
6 | 4, 5 | eqtr2di 2794 |
. . . . . 6
โข (๐ด = โ
โ 0 =
(vol*โโช ๐ด)) |
7 | 6 | a1d 25 |
. . . . 5
โข (๐ด = โ
โ ((๐ด โผ โ โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ 0 = (vol*โโช ๐ด))) |
8 | | ovolge0 24861 |
. . . . . . . 8
โข (โช ๐ด
โ โ โ 0 โค (vol*โโช ๐ด)) |
9 | 8 | ad2antll 728 |
. . . . . . 7
โข (((๐ด โ โ
โง ๐ด โผ โ) โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ 0 โค (vol*โโช ๐ด)) |
10 | | reldom 8896 |
. . . . . . . . . . . 12
โข Rel
โผ |
11 | 10 | brrelex1i 5693 |
. . . . . . . . . . 11
โข (๐ด โผ โ โ ๐ด โ V) |
12 | | 0sdomg 9055 |
. . . . . . . . . . 11
โข (๐ด โ V โ (โ
โบ ๐ด โ ๐ด โ โ
)) |
13 | 11, 12 | syl 17 |
. . . . . . . . . 10
โข (๐ด โผ โ โ (โ
โบ ๐ด โ ๐ด โ โ
)) |
14 | 13 | biimparc 481 |
. . . . . . . . 9
โข ((๐ด โ โ
โง ๐ด โผ โ) โ โ
โบ ๐ด) |
15 | | fodomr 9079 |
. . . . . . . . 9
โข ((โ
โบ ๐ด โง ๐ด โผ โ) โ
โ๐ ๐:โโontoโ๐ด) |
16 | 14, 15 | sylancom 589 |
. . . . . . . 8
โข ((๐ด โ โ
โง ๐ด โผ โ) โ
โ๐ ๐:โโontoโ๐ด) |
17 | | unissb 4905 |
. . . . . . . . . . . 12
โข (โช ๐ด
โ โ โ โ๐ฅ โ ๐ด ๐ฅ โ โ) |
18 | 17 | anbi1i 625 |
. . . . . . . . . . 11
โข ((โช ๐ด
โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ (โ๐ฅ โ ๐ด ๐ฅ โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ)) |
19 | | r19.26 3115 |
. . . . . . . . . . 11
โข
(โ๐ฅ โ
๐ด (๐ฅ โ โ โง ๐ฅ โผ โ) โ (โ๐ฅ โ ๐ด ๐ฅ โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ)) |
20 | 18, 19 | bitr4i 278 |
. . . . . . . . . 10
โข ((โช ๐ด
โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง ๐ฅ โผ โ)) |
21 | | brdom2 8929 |
. . . . . . . . . . . . . 14
โข (๐ฅ โผ โ โ (๐ฅ โบ โ โจ ๐ฅ โ
โ)) |
22 | | nnenom 13892 |
. . . . . . . . . . . . . . . . 17
โข โ
โ ฯ |
23 | | sdomen2 9073 |
. . . . . . . . . . . . . . . . 17
โข (โ
โ ฯ โ (๐ฅ
โบ โ โ ๐ฅ
โบ ฯ)) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โบ โ โ ๐ฅ โบ
ฯ) |
25 | | isfinite 9595 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ โ Fin โ ๐ฅ โบ
ฯ) |
26 | 24, 25 | bitr4i 278 |
. . . . . . . . . . . . . . 15
โข (๐ฅ โบ โ โ ๐ฅ โ Fin) |
27 | 26 | orbi1i 913 |
. . . . . . . . . . . . . 14
โข ((๐ฅ โบ โ โจ ๐ฅ โ โ) โ (๐ฅ โ Fin โจ ๐ฅ โ
โ)) |
28 | 21, 27 | bitri 275 |
. . . . . . . . . . . . 13
โข (๐ฅ โผ โ โ (๐ฅ โ Fin โจ ๐ฅ โ
โ)) |
29 | | ovolfi 24874 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ Fin โง ๐ฅ โ โ) โ
(vol*โ๐ฅ) =
0) |
30 | 29 | expcom 415 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ (๐ฅ โ Fin โ
(vol*โ๐ฅ) =
0)) |
31 | | ovolctb 24870 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง ๐ฅ โ โ) โ
(vol*โ๐ฅ) =
0) |
32 | 31 | ex 414 |
. . . . . . . . . . . . . 14
โข (๐ฅ โ โ โ (๐ฅ โ โ โ
(vol*โ๐ฅ) =
0)) |
33 | 30, 32 | jaod 858 |
. . . . . . . . . . . . 13
โข (๐ฅ โ โ โ ((๐ฅ โ Fin โจ ๐ฅ โ โ) โ
(vol*โ๐ฅ) =
0)) |
34 | 28, 33 | biimtrid 241 |
. . . . . . . . . . . 12
โข (๐ฅ โ โ โ (๐ฅ โผ โ โ
(vol*โ๐ฅ) =
0)) |
35 | 34 | imdistani 570 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฅ โผ โ) โ (๐ฅ โ โ โง
(vol*โ๐ฅ) =
0)) |
36 | 35 | ralimi 3087 |
. . . . . . . . . 10
โข
(โ๐ฅ โ
๐ด (๐ฅ โ โ โง ๐ฅ โผ โ) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0)) |
37 | 20, 36 | sylbi 216 |
. . . . . . . . 9
โข ((โช ๐ด
โ โ โง โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0)) |
38 | 37 | ancoms 460 |
. . . . . . . 8
โข
((โ๐ฅ โ
๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0)) |
39 | | foima 6766 |
. . . . . . . . . . . . 13
โข (๐:โโontoโ๐ด โ (๐ โ โ) = ๐ด) |
40 | 39 | raleqdv 3316 |
. . . . . . . . . . . 12
โข (๐:โโontoโ๐ด โ (โ๐ฅ โ (๐ โ โ)(๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0))) |
41 | | fofn 6763 |
. . . . . . . . . . . . 13
โข (๐:โโontoโ๐ด โ ๐ Fn โ) |
42 | | ssid 3971 |
. . . . . . . . . . . . 13
โข โ
โ โ |
43 | | sseq1 3974 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐โ๐) โ (๐ฅ โ โ โ (๐โ๐) โ โ)) |
44 | | fveqeq2 6856 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = (๐โ๐) โ ((vol*โ๐ฅ) = 0 โ (vol*โ(๐โ๐)) = 0)) |
45 | 43, 44 | anbi12d 632 |
. . . . . . . . . . . . . 14
โข (๐ฅ = (๐โ๐) โ ((๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
46 | 45 | ralima 7193 |
. . . . . . . . . . . . 13
โข ((๐ Fn โ โง โ
โ โ) โ (โ๐ฅ โ (๐ โ โ)(๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
47 | 41, 42, 46 | sylancl 587 |
. . . . . . . . . . . 12
โข (๐:โโontoโ๐ด โ (โ๐ฅ โ (๐ โ โ)(๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
48 | 40, 47 | bitr3d 281 |
. . . . . . . . . . 11
โข (๐:โโontoโ๐ด โ (โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
49 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
50 | 49 | sseq1d 3980 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((๐โ๐) โ โ โ (๐โ๐) โ โ)) |
51 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = ๐ โ (vol*โ(๐โ๐)) = (vol*โ(๐โ๐))) |
52 | 51 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ ((vol*โ(๐โ๐)) = 0 โ (vol*โ(๐โ๐)) = 0)) |
53 | 50, 52 | anbi12d 632 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
54 | 53 | cbvralvw 3228 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) |
55 | | 0re 11164 |
. . . . . . . . . . . . . . . . . 18
โข 0 โ
โ |
56 | | eleq1a 2833 |
. . . . . . . . . . . . . . . . . 18
โข (0 โ
โ โ ((vol*โ(๐โ๐)) = 0 โ (vol*โ(๐โ๐)) โ โ)) |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
โข
((vol*โ(๐โ๐)) = 0 โ (vol*โ(๐โ๐)) โ โ) |
58 | 57 | anim2i 618 |
. . . . . . . . . . . . . . . 16
โข (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) โ โ)) |
59 | 58 | ralimi 3087 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) โ โ)) |
60 | 54, 59 | sylbi 216 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) โ โ)) |
61 | | ovoliunnfl.0 |
. . . . . . . . . . . . . 14
โข ((๐ Fn โ โง โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) โ โ)) โ
(vol*โโช ๐ โ โ (๐โ๐)) โค sup(ran seq1( + , (๐ โ โ โฆ (vol*โ(๐โ๐)))), โ*, <
)) |
62 | 41, 60, 61 | syl2an 597 |
. . . . . . . . . . . . 13
โข ((๐:โโontoโ๐ด โง โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) โ (vol*โโช ๐ โ โ (๐โ๐)) โค sup(ran seq1( + , (๐ โ โ โฆ (vol*โ(๐โ๐)))), โ*, <
)) |
63 | | fofun 6762 |
. . . . . . . . . . . . . . . . 17
โข (๐:โโontoโ๐ด โ Fun ๐) |
64 | | funiunfv 7200 |
. . . . . . . . . . . . . . . . 17
โข (Fun
๐ โ โช ๐ โ โ (๐โ๐) = โช (๐ โ
โ)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
โข (๐:โโontoโ๐ด โ โช
๐ โ โ (๐โ๐) = โช (๐ โ
โ)) |
66 | 39 | unieqd 4884 |
. . . . . . . . . . . . . . . 16
โข (๐:โโontoโ๐ด โ โช (๐ โ โ) = โช ๐ด) |
67 | 65, 66 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
โข (๐:โโontoโ๐ด โ โช
๐ โ โ (๐โ๐) = โช ๐ด) |
68 | 67 | fveq2d 6851 |
. . . . . . . . . . . . . 14
โข (๐:โโontoโ๐ด โ (vol*โโช ๐ โ โ (๐โ๐)) = (vol*โโช
๐ด)) |
69 | 68 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐:โโontoโ๐ด โง โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) โ (vol*โโช ๐ โ โ (๐โ๐)) = (vol*โโช
๐ด)) |
70 | | fveq2 6847 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = ๐ โ (๐โ๐) = (๐โ๐)) |
71 | 70 | sseq1d 3980 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = ๐ โ ((๐โ๐) โ โ โ (๐โ๐) โ โ)) |
72 | | 2fveq3 6852 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ = ๐ โ (vol*โ(๐โ๐)) = (vol*โ(๐โ๐))) |
73 | 72 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ = ๐ โ ((vol*โ(๐โ๐)) = 0 โ (vol*โ(๐โ๐)) = 0)) |
74 | 71, 73 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = ๐ โ (((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0))) |
75 | 74 | rspccva 3583 |
. . . . . . . . . . . . . . . . . . . 20
โข
((โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โง ๐ โ โ) โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) |
76 | 75 | simprd 497 |
. . . . . . . . . . . . . . . . . . 19
โข
((โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โง ๐ โ โ) โ (vol*โ(๐โ๐)) = 0) |
77 | 76 | mpteq2dva 5210 |
. . . . . . . . . . . . . . . . . 18
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ (๐ โ โ โฆ
(vol*โ(๐โ๐))) = (๐ โ โ โฆ 0)) |
78 | 77 | seqeq3d 13921 |
. . . . . . . . . . . . . . . . 17
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ seq1( + , (๐ โ โ โฆ
(vol*โ(๐โ๐)))) = seq1( + , (๐ โ โ โฆ
0))) |
79 | 78 | rneqd 5898 |
. . . . . . . . . . . . . . . 16
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ ran seq1( + ,
(๐ โ โ โฆ
(vol*โ(๐โ๐)))) = ran seq1( + , (๐ โ โ โฆ
0))) |
80 | 79 | supeq1d 9389 |
. . . . . . . . . . . . . . 15
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ sup(ran seq1( + ,
(๐ โ โ โฆ
(vol*โ(๐โ๐)))), โ*, <
) = sup(ran seq1( + , (๐
โ โ โฆ 0)), โ*, < )) |
81 | | 0cn 11154 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 0 โ
โ |
82 | | ser1const 13971 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((0
โ โ โง ๐
โ โ) โ (seq1( + , (โ ร {0}))โ๐) = (๐ ยท 0)) |
83 | 81, 82 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (seq1( +
, (โ ร {0}))โ๐) = (๐ ยท 0)) |
84 | | nncn 12168 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ โ ๐ โ
โ) |
85 | 84 | mul01d 11361 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ โ (๐ ยท 0) =
0) |
86 | 83, 85 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ (seq1( +
, (โ ร {0}))โ๐) = 0) |
87 | 86 | mpteq2ia 5213 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ โฆ (seq1( +
, (โ ร {0}))โ๐)) = (๐ โ โ โฆ 0) |
88 | | fconstmpt 5699 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (โ
ร {0}) = (๐ โ
โ โฆ 0) |
89 | | seqeq3 13918 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((โ
ร {0}) = (๐ โ
โ โฆ 0) โ seq1( + , (โ ร {0})) = seq1( + , (๐ โ โ โฆ
0))) |
90 | 88, 89 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . 21
โข seq1( + ,
(โ ร {0})) = seq1( + , (๐ โ โ โฆ 0)) |
91 | | 1z 12540 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข 1 โ
โค |
92 | | seqfn 13925 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (1 โ
โค โ seq1( + , (โ ร {0})) Fn
(โคโฅโ1)) |
93 | 91, 92 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
โข seq1( + ,
(โ ร {0})) Fn (โคโฅโ1) |
94 | | nnuz 12813 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข โ =
(โคโฅโ1) |
95 | 94 | fneq2i 6605 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (seq1( +
, (โ ร {0})) Fn โ โ seq1( + , (โ ร {0})) Fn
(โคโฅโ1)) |
96 | | dffn5 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (seq1( +
, (โ ร {0})) Fn โ โ seq1( + , (โ ร {0})) =
(๐ โ โ โฆ
(seq1( + , (โ ร {0}))โ๐))) |
97 | 95, 96 | bitr3i 277 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (seq1( +
, (โ ร {0})) Fn (โคโฅโ1) โ seq1( + ,
(โ ร {0})) = (๐
โ โ โฆ (seq1( + , (โ ร {0}))โ๐))) |
98 | 93, 97 | mpbi 229 |
. . . . . . . . . . . . . . . . . . . . 21
โข seq1( + ,
(โ ร {0})) = (๐
โ โ โฆ (seq1( + , (โ ร {0}))โ๐)) |
99 | 90, 98 | eqtr3i 2767 |
. . . . . . . . . . . . . . . . . . . 20
โข seq1( + ,
(๐ โ โ โฆ
0)) = (๐ โ โ
โฆ (seq1( + , (โ ร {0}))โ๐)) |
100 | | fconstmpt 5699 |
. . . . . . . . . . . . . . . . . . . 20
โข (โ
ร {0}) = (๐ โ
โ โฆ 0) |
101 | 87, 99, 100 | 3eqtr4i 2775 |
. . . . . . . . . . . . . . . . . . 19
โข seq1( + ,
(๐ โ โ โฆ
0)) = (โ ร {0}) |
102 | 101 | rneqi 5897 |
. . . . . . . . . . . . . . . . . 18
โข ran seq1(
+ , (๐ โ โ
โฆ 0)) = ran (โ ร {0}) |
103 | | 1nn 12171 |
. . . . . . . . . . . . . . . . . . 19
โข 1 โ
โ |
104 | | ne0i 4299 |
. . . . . . . . . . . . . . . . . . 19
โข (1 โ
โ โ โ โ โ
) |
105 | | rnxp 6127 |
. . . . . . . . . . . . . . . . . . 19
โข (โ
โ โ
โ ran (โ ร {0}) = {0}) |
106 | 103, 104,
105 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
โข ran
(โ ร {0}) = {0} |
107 | 102, 106 | eqtri 2765 |
. . . . . . . . . . . . . . . . 17
โข ran seq1(
+ , (๐ โ โ
โฆ 0)) = {0} |
108 | 107 | supeq1i 9390 |
. . . . . . . . . . . . . . . 16
โข sup(ran
seq1( + , (๐ โ โ
โฆ 0)), โ*, < ) = sup({0}, โ*, <
) |
109 | | xrltso 13067 |
. . . . . . . . . . . . . . . . 17
โข < Or
โ* |
110 | | 0xr 11209 |
. . . . . . . . . . . . . . . . 17
โข 0 โ
โ* |
111 | | supsn 9415 |
. . . . . . . . . . . . . . . . 17
โข (( <
Or โ* โง 0 โ โ*) โ sup({0},
โ*, < ) = 0) |
112 | 109, 110,
111 | mp2an 691 |
. . . . . . . . . . . . . . . 16
โข sup({0},
โ*, < ) = 0 |
113 | 108, 112 | eqtri 2765 |
. . . . . . . . . . . . . . 15
โข sup(ran
seq1( + , (๐ โ โ
โฆ 0)), โ*, < ) = 0 |
114 | 80, 113 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
โข
(โ๐ โ
โ ((๐โ๐) โ โ โง
(vol*โ(๐โ๐)) = 0) โ sup(ran seq1( + ,
(๐ โ โ โฆ
(vol*โ(๐โ๐)))), โ*, <
) = 0) |
115 | 114 | adantl 483 |
. . . . . . . . . . . . 13
โข ((๐:โโontoโ๐ด โง โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) โ sup(ran seq1( + , (๐ โ โ โฆ
(vol*โ(๐โ๐)))), โ*, <
) = 0) |
116 | 62, 69, 115 | 3brtr3d 5141 |
. . . . . . . . . . . 12
โข ((๐:โโontoโ๐ด โง โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0)) โ (vol*โโช ๐ด)
โค 0) |
117 | 116 | ex 414 |
. . . . . . . . . . 11
โข (๐:โโontoโ๐ด โ (โ๐ โ โ ((๐โ๐) โ โ โง (vol*โ(๐โ๐)) = 0) โ (vol*โโช ๐ด)
โค 0)) |
118 | 48, 117 | sylbid 239 |
. . . . . . . . . 10
โข (๐:โโontoโ๐ด โ (โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ (vol*โโช ๐ด)
โค 0)) |
119 | 118 | exlimiv 1934 |
. . . . . . . . 9
โข
(โ๐ ๐:โโontoโ๐ด โ (โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0) โ (vol*โโช ๐ด)
โค 0)) |
120 | 119 | imp 408 |
. . . . . . . 8
โข
((โ๐ ๐:โโontoโ๐ด โง โ๐ฅ โ ๐ด (๐ฅ โ โ โง (vol*โ๐ฅ) = 0)) โ (vol*โโช ๐ด)
โค 0) |
121 | 16, 38, 120 | syl2an 597 |
. . . . . . 7
โข (((๐ด โ โ
โง ๐ด โผ โ) โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ (vol*โโช ๐ด) โค 0) |
122 | | ovolcl 24858 |
. . . . . . . . 9
โข (โช ๐ด
โ โ โ (vol*โโช ๐ด) โ
โ*) |
123 | | xrletri3 13080 |
. . . . . . . . 9
โข ((0
โ โ* โง (vol*โโช ๐ด) โ โ*)
โ (0 = (vol*โโช ๐ด) โ (0 โค (vol*โโช ๐ด)
โง (vol*โโช ๐ด) โค 0))) |
124 | 110, 122,
123 | sylancr 588 |
. . . . . . . 8
โข (โช ๐ด
โ โ โ (0 = (vol*โโช ๐ด) โ (0 โค
(vol*โโช ๐ด) โง (vol*โโช ๐ด)
โค 0))) |
125 | 124 | ad2antll 728 |
. . . . . . 7
โข (((๐ด โ โ
โง ๐ด โผ โ) โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ (0 = (vol*โโช ๐ด) โ (0 โค
(vol*โโช ๐ด) โง (vol*โโช ๐ด)
โค 0))) |
126 | 9, 121, 125 | mpbir2and 712 |
. . . . . 6
โข (((๐ด โ โ
โง ๐ด โผ โ) โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ 0 = (vol*โโช ๐ด)) |
127 | 126 | expl 459 |
. . . . 5
โข (๐ด โ โ
โ ((๐ด โผ โ โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ 0 = (vol*โโช ๐ด))) |
128 | 7, 127 | pm2.61ine 3029 |
. . . 4
โข ((๐ด โผ โ โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ 0 = (vol*โโช ๐ด)) |
129 | | renepnf 11210 |
. . . . . . 7
โข (0 โ
โ โ 0 โ +โ) |
130 | 55, 129 | mp1i 13 |
. . . . . 6
โข (โช ๐ด =
โ โ 0 โ +โ) |
131 | | fveq2 6847 |
. . . . . . 7
โข (โช ๐ด =
โ โ (vol*โโช ๐ด) = (vol*โโ)) |
132 | | ovolre 24905 |
. . . . . . 7
โข
(vol*โโ) = +โ |
133 | 131, 132 | eqtrdi 2793 |
. . . . . 6
โข (โช ๐ด =
โ โ (vol*โโช ๐ด) = +โ) |
134 | 130, 133 | neeqtrrd 3019 |
. . . . 5
โข (โช ๐ด =
โ โ 0 โ (vol*โโช ๐ด)) |
135 | 134 | necon2i 2979 |
. . . 4
โข (0 =
(vol*โโช ๐ด) โ โช ๐ด โ โ) |
136 | 128, 135 | syl 17 |
. . 3
โข ((๐ด โผ โ โง
(โ๐ฅ โ ๐ด ๐ฅ โผ โ โง โช ๐ด
โ โ)) โ โช ๐ด โ โ) |
137 | 136 | expr 458 |
. 2
โข ((๐ด โผ โ โง
โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ (โช ๐ด
โ โ โ โช ๐ด โ โ)) |
138 | | eqimss 4005 |
. . 3
โข (โช ๐ด =
โ โ โช ๐ด โ โ) |
139 | 138 | necon3bi 2971 |
. 2
โข (ยฌ
โช ๐ด โ โ โ โช ๐ด
โ โ) |
140 | 137, 139 | pm2.61d1 180 |
1
โข ((๐ด โผ โ โง
โ๐ฅ โ ๐ด ๐ฅ โผ โ) โ โช ๐ด
โ โ) |