Step | Hyp | Ref
| Expression |
1 | | oms.m |
. . 3
β’ π = (toOMeasβπ
) |
2 | 1 | fveq1i 6848 |
. 2
β’ (πββ
) =
((toOMeasβπ
)ββ
) |
3 | | oms.o |
. . . 4
β’ (π β π β π) |
4 | | oms.r |
. . . 4
β’ (π β π
:πβΆ(0[,]+β)) |
5 | | 0ss 4361 |
. . . . 5
β’ β
β βͺ dom π
|
6 | 4 | fdmd 6684 |
. . . . . 6
β’ (π β dom π
= π) |
7 | 6 | unieqd 4884 |
. . . . 5
β’ (π β βͺ dom π
= βͺ π) |
8 | 5, 7 | sseqtrid 4001 |
. . . 4
β’ (π β β
β βͺ π) |
9 | | omsfval 32934 |
. . . 4
β’ ((π β π β§ π
:πβΆ(0[,]+β) β§ β
β
βͺ π) β ((toOMeasβπ
)ββ
) = inf(ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)), (0[,]+β), < )) |
10 | 3, 4, 8, 9 | syl3anc 1372 |
. . 3
β’ (π β ((toOMeasβπ
)ββ
) = inf(ran
(π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)), (0[,]+β), < )) |
11 | | iccssxr 13354 |
. . . . . 6
β’
(0[,]+β) β β* |
12 | | xrltso 13067 |
. . . . . 6
β’ < Or
β* |
13 | | soss 5570 |
. . . . . 6
β’
((0[,]+β) β β* β ( < Or
β* β < Or (0[,]+β))) |
14 | 11, 12, 13 | mp2 9 |
. . . . 5
β’ < Or
(0[,]+β) |
15 | 14 | a1i 11 |
. . . 4
β’ (π β < Or
(0[,]+β)) |
16 | | 0e0iccpnf 13383 |
. . . . 5
β’ 0 β
(0[,]+β) |
17 | 16 | a1i 11 |
. . . 4
β’ (π β 0 β
(0[,]+β)) |
18 | | oms.d |
. . . . . . . . . 10
β’ (π β β
β dom π
) |
19 | 18 | snssd 4774 |
. . . . . . . . 9
β’ (π β {β
} β dom
π
) |
20 | | p0ex 5344 |
. . . . . . . . . 10
β’ {β
}
β V |
21 | 20 | elpw 4569 |
. . . . . . . . 9
β’
({β
} β π« dom π
β {β
} β dom π
) |
22 | 19, 21 | sylibr 233 |
. . . . . . . 8
β’ (π β {β
} β π«
dom π
) |
23 | | 0ss 4361 |
. . . . . . . . 9
β’ β
β βͺ {β
} |
24 | | 0ex 5269 |
. . . . . . . . . 10
β’ β
β V |
25 | | snct 31672 |
. . . . . . . . . 10
β’ (β
β V β {β
} βΌ Ο) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . 9
β’ {β
}
βΌ Ο |
27 | 23, 26 | pm3.2i 472 |
. . . . . . . 8
β’ (β
β βͺ {β
} β§ {β
} βΌ
Ο) |
28 | 22, 27 | jctir 522 |
. . . . . . 7
β’ (π β ({β
} β
π« dom π
β§
(β
β βͺ {β
} β§ {β
} βΌ
Ο))) |
29 | | unieq 4881 |
. . . . . . . . . 10
β’ (π§ = {β
} β βͺ π§ =
βͺ {β
}) |
30 | 29 | sseq2d 3981 |
. . . . . . . . 9
β’ (π§ = {β
} β (β
β βͺ π§ β β
β βͺ {β
})) |
31 | | breq1 5113 |
. . . . . . . . 9
β’ (π§ = {β
} β (π§ βΌ Ο β
{β
} βΌ Ο)) |
32 | 30, 31 | anbi12d 632 |
. . . . . . . 8
β’ (π§ = {β
} β ((β
β βͺ π§ β§ π§ βΌ Ο) β (β
β
βͺ {β
} β§ {β
} βΌ
Ο))) |
33 | 32 | elrab 3650 |
. . . . . . 7
β’
({β
} β {π§
β π« dom π
β£ (β
β βͺ π§ β§ π§ βΌ Ο)} β ({β
} β
π« dom π
β§
(β
β βͺ {β
} β§ {β
} βΌ
Ο))) |
34 | 28, 33 | sylibr 233 |
. . . . . 6
β’ (π β {β
} β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ
Ο)}) |
35 | | simpr 486 |
. . . . . . . . . 10
β’ ((π β§ π¦ = β
) β π¦ = β
) |
36 | 35 | fveq2d 6851 |
. . . . . . . . 9
β’ ((π β§ π¦ = β
) β (π
βπ¦) = (π
ββ
)) |
37 | | oms.0 |
. . . . . . . . . 10
β’ (π β (π
ββ
) = 0) |
38 | 37 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ = β
) β (π
ββ
) = 0) |
39 | 36, 38 | eqtrd 2777 |
. . . . . . . 8
β’ ((π β§ π¦ = β
) β (π
βπ¦) = 0) |
40 | 39, 18, 17 | esumsn 32704 |
. . . . . . 7
β’ (π β Ξ£*π¦ β {β
} (π
βπ¦) = 0) |
41 | 40 | eqcomd 2743 |
. . . . . 6
β’ (π β 0 =
Ξ£*π¦ β
{β
} (π
βπ¦)) |
42 | | esumeq1 32673 |
. . . . . . 7
β’ (π₯ = {β
} β
Ξ£*π¦ β
π₯(π
βπ¦) = Ξ£*π¦ β {β
} (π
βπ¦)) |
43 | 42 | rspceeqv 3600 |
. . . . . 6
β’
(({β
} β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β§ 0 = Ξ£*π¦ β {β
} (π
βπ¦)) β βπ₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}0
= Ξ£*π¦
β π₯(π
βπ¦)) |
44 | 34, 41, 43 | syl2anc 585 |
. . . . 5
β’ (π β βπ₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}0
= Ξ£*π¦
β π₯(π
βπ¦)) |
45 | | 0xr 11209 |
. . . . . 6
β’ 0 β
β* |
46 | | eqid 2737 |
. . . . . . 7
β’ (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) = (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) |
47 | 46 | elrnmpt 5916 |
. . . . . 6
β’ (0 β
β* β (0 β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) β βπ₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}0
= Ξ£*π¦
β π₯(π
βπ¦))) |
48 | 45, 47 | ax-mp 5 |
. . . . 5
β’ (0 β
ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) β βπ₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}0
= Ξ£*π¦
β π₯(π
βπ¦)) |
49 | 44, 48 | sylibr 233 |
. . . 4
β’ (π β 0 β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) |
50 | | nfv 1918 |
. . . . . . . 8
β’
β²π₯π |
51 | | nfmpt1 5218 |
. . . . . . . . . 10
β’
β²π₯(π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) |
52 | 51 | nfrn 5912 |
. . . . . . . . 9
β’
β²π₯ran
(π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) |
53 | 52 | nfcri 2895 |
. . . . . . . 8
β’
β²π₯ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) |
54 | 50, 53 | nfan 1903 |
. . . . . . 7
β’
β²π₯(π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) |
55 | | simpr 486 |
. . . . . . . 8
β’ ((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β π = Ξ£*π¦ β π₯(π
βπ¦)) |
56 | | vex 3452 |
. . . . . . . . 9
β’ π₯ β V |
57 | | nfv 1918 |
. . . . . . . . . . . . 13
β’
β²π¦π |
58 | | nfcv 2908 |
. . . . . . . . . . . . . . . 16
β’
β²π¦{π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ
Ο)} |
59 | | nfcv 2908 |
. . . . . . . . . . . . . . . . 17
β’
β²π¦π₯ |
60 | 59 | nfesum1 32679 |
. . . . . . . . . . . . . . . 16
β’
β²π¦Ξ£*π¦ β π₯(π
βπ¦) |
61 | 58, 60 | nfmpt 5217 |
. . . . . . . . . . . . . . 15
β’
β²π¦(π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) |
62 | 61 | nfrn 5912 |
. . . . . . . . . . . . . 14
β’
β²π¦ran
(π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) |
63 | 62 | nfcri 2895 |
. . . . . . . . . . . . 13
β’
β²π¦ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) |
64 | 57, 63 | nfan 1903 |
. . . . . . . . . . . 12
β’
β²π¦(π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) |
65 | | nfv 1918 |
. . . . . . . . . . . 12
β’
β²π¦ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ
Ο)} |
66 | 64, 65 | nfan 1903 |
. . . . . . . . . . 11
β’
β²π¦((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ
Ο)}) |
67 | 60 | nfeq2 2925 |
. . . . . . . . . . 11
β’
β²π¦ π = Ξ£*π¦ β π₯(π
βπ¦) |
68 | 66, 67 | nfan 1903 |
. . . . . . . . . 10
β’
β²π¦(((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) |
69 | 4 | ad4antr 731 |
. . . . . . . . . . . 12
β’
(((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β§ π¦ β π₯) β π
:πβΆ(0[,]+β)) |
70 | | ssrab2 4042 |
. . . . . . . . . . . . . . . 16
β’ {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β π« dom π
|
71 | | simpllr 775 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β§ π¦ β π₯) β π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ
Ο)}) |
72 | 70, 71 | sselid 3947 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β§ π¦ β π₯) β π₯ β π« dom π
) |
73 | 6 | pweqd 4582 |
. . . . . . . . . . . . . . . 16
β’ (π β π« dom π
= π« π) |
74 | 73 | ad4antr 731 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β§ π¦ β π₯) β π« dom π
= π« π) |
75 | 72, 74 | eleqtrd 2840 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β§ π¦ β π₯) β π₯ β π« π) |
76 | 75 | elpwid 4574 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β§ π¦ β π₯) β π₯ β π) |
77 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β§ π¦ β π₯) β π¦ β π₯) |
78 | 76, 77 | sseldd 3950 |
. . . . . . . . . . . 12
β’
(((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β§ π¦ β π₯) β π¦ β π) |
79 | 69, 78 | ffvelcdmd 7041 |
. . . . . . . . . . 11
β’
(((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β§ π¦ β π₯) β (π
βπ¦) β (0[,]+β)) |
80 | 79 | ex 414 |
. . . . . . . . . 10
β’ ((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β (π¦ β π₯ β (π
βπ¦) β (0[,]+β))) |
81 | 68, 80 | ralrimi 3243 |
. . . . . . . . 9
β’ ((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β βπ¦ β π₯ (π
βπ¦) β (0[,]+β)) |
82 | 59 | esumcl 32669 |
. . . . . . . . 9
β’ ((π₯ β V β§ βπ¦ β π₯ (π
βπ¦) β (0[,]+β)) β
Ξ£*π¦ β
π₯(π
βπ¦) β (0[,]+β)) |
83 | 56, 81, 82 | sylancr 588 |
. . . . . . . 8
β’ ((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β Ξ£*π¦ β π₯(π
βπ¦) β (0[,]+β)) |
84 | 55, 83 | eqeltrd 2838 |
. . . . . . 7
β’ ((((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β§ π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)})
β§ π =
Ξ£*π¦ β
π₯(π
βπ¦)) β π β (0[,]+β)) |
85 | | vex 3452 |
. . . . . . . . . 10
β’ π β V |
86 | 46 | elrnmpt 5916 |
. . . . . . . . . 10
β’ (π β V β (π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) β βπ₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ
Ο)}π =
Ξ£*π¦ β
π₯(π
βπ¦))) |
87 | 85, 86 | ax-mp 5 |
. . . . . . . . 9
β’ (π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) β βπ₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ
Ο)}π =
Ξ£*π¦ β
π₯(π
βπ¦)) |
88 | 87 | biimpi 215 |
. . . . . . . 8
β’ (π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)) β βπ₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ
Ο)}π =
Ξ£*π¦ β
π₯(π
βπ¦)) |
89 | 88 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β βπ₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ
Ο)}π =
Ξ£*π¦ β
π₯(π
βπ¦)) |
90 | 54, 84, 89 | r19.29af 3254 |
. . . . . 6
β’ ((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β π β (0[,]+β)) |
91 | | pnfxr 11216 |
. . . . . . 7
β’ +β
β β* |
92 | | iccgelb 13327 |
. . . . . . 7
β’ ((0
β β* β§ +β β β* β§
π β (0[,]+β))
β 0 β€ π) |
93 | 45, 91, 92 | mp3an12 1452 |
. . . . . 6
β’ (π β (0[,]+β) β 0
β€ π) |
94 | 90, 93 | syl 17 |
. . . . 5
β’ ((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β 0 β€ π) |
95 | 11, 90 | sselid 3947 |
. . . . . 6
β’ ((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β π β β*) |
96 | | xrlenlt 11227 |
. . . . . . 7
β’ ((0
β β* β§ π β β*) β (0 β€
π β Β¬ π < 0)) |
97 | 96 | bicomd 222 |
. . . . . 6
β’ ((0
β β* β§ π β β*) β (Β¬
π < 0 β 0 β€
π)) |
98 | 45, 95, 97 | sylancr 588 |
. . . . 5
β’ ((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β (Β¬ π < 0 β 0 β€ π)) |
99 | 94, 98 | mpbird 257 |
. . . 4
β’ ((π β§ π β ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦))) β Β¬ π < 0) |
100 | 15, 17, 49, 99 | infmin 9437 |
. . 3
β’ (π β inf(ran (π₯ β {π§ β π« dom π
β£ (β
β βͺ π§
β§ π§ βΌ Ο)}
β¦ Ξ£*π¦ β π₯(π
βπ¦)), (0[,]+β), < ) =
0) |
101 | 10, 100 | eqtrd 2777 |
. 2
β’ (π β ((toOMeasβπ
)ββ
) =
0) |
102 | 2, 101 | eqtrid 2789 |
1
β’ (π β (πββ
) = 0) |