Step | Hyp | Ref
| Expression |
1 | | lebnumlem1.u |
. . . . 5
β’ (π β π β Fin) |
2 | 1 | adantr 482 |
. . . 4
β’ ((π β§ π¦ β π) β π β Fin) |
3 | | lebnum.d |
. . . . . . . 8
β’ (π β π· β (Metβπ)) |
4 | 3 | ad2antrr 725 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π β π) β π· β (Metβπ)) |
5 | | difssd 4091 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π β π) β (π β π) β π) |
6 | | lebnum.s |
. . . . . . . . . . . 12
β’ (π β π β π½) |
7 | 6 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π¦ β π) β π β π½) |
8 | 7 | sselda 3943 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π) β§ π β π) β π β π½) |
9 | | elssuni 4897 |
. . . . . . . . . 10
β’ (π β π½ β π β βͺ π½) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ π β π) β π β βͺ π½) |
11 | | metxmet 23609 |
. . . . . . . . . . . 12
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
12 | 3, 11 | syl 17 |
. . . . . . . . . . 11
β’ (π β π· β (βMetβπ)) |
13 | | lebnum.j |
. . . . . . . . . . . 12
β’ π½ = (MetOpenβπ·) |
14 | 13 | mopnuni 23716 |
. . . . . . . . . . 11
β’ (π· β (βMetβπ) β π = βͺ π½) |
15 | 12, 14 | syl 17 |
. . . . . . . . . 10
β’ (π β π = βͺ π½) |
16 | 15 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ π β π) β π = βͺ π½) |
17 | 10, 16 | sseqtrrd 3984 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ π β π) β π β π) |
18 | | lebnumlem1.n |
. . . . . . . . . . . 12
β’ (π β Β¬ π β π) |
19 | | eleq1 2826 |
. . . . . . . . . . . . 13
β’ (π = π β (π β π β π β π)) |
20 | 19 | notbid 318 |
. . . . . . . . . . . 12
β’ (π = π β (Β¬ π β π β Β¬ π β π)) |
21 | 18, 20 | syl5ibrcom 247 |
. . . . . . . . . . 11
β’ (π β (π = π β Β¬ π β π)) |
22 | 21 | necon2ad 2957 |
. . . . . . . . . 10
β’ (π β (π β π β π β π)) |
23 | 22 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π¦ β π) β (π β π β π β π)) |
24 | 23 | imp 408 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ π β π) β π β π) |
25 | | pssdifn0 4324 |
. . . . . . . 8
β’ ((π β π β§ π β π) β (π β π) β β
) |
26 | 17, 24, 25 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π β π) β (π β π) β β
) |
27 | | eqid 2738 |
. . . . . . . 8
β’ (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )) = (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
28 | 27 | metdsre 24138 |
. . . . . . 7
β’ ((π· β (Metβπ) β§ (π β π) β π β§ (π β π) β β
) β (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆβ) |
29 | 4, 5, 26, 28 | syl3anc 1372 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ π β π) β (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆβ) |
30 | 27 | fmpt 7053 |
. . . . . 6
β’
(βπ¦ β
π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β β (π¦ β
π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆβ) |
31 | 29, 30 | sylibr 233 |
. . . . 5
β’ (((π β§ π¦ β π) β§ π β π) β βπ¦ β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β) |
32 | | simplr 768 |
. . . . 5
β’ (((π β§ π¦ β π) β§ π β π) β π¦ β π) |
33 | | rsp 3229 |
. . . . 5
β’
(βπ¦ β
π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β β (π¦ β
π β inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β)) |
34 | 31, 32, 33 | sylc 65 |
. . . 4
β’ (((π β§ π¦ β π) β§ π β π) β inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β) |
35 | 2, 34 | fsumrecl 15554 |
. . 3
β’ ((π β§ π¦ β π) β Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β) |
36 | | lebnum.u |
. . . . . . 7
β’ (π β π = βͺ π) |
37 | 36 | eleq2d 2824 |
. . . . . 6
β’ (π β (π¦ β π β π¦ β βͺ π)) |
38 | 37 | biimpa 478 |
. . . . 5
β’ ((π β§ π¦ β π) β π¦ β βͺ π) |
39 | | eluni2 4868 |
. . . . 5
β’ (π¦ β βͺ π
β βπ β
π π¦ β π) |
40 | 38, 39 | sylib 217 |
. . . 4
β’ ((π β§ π¦ β π) β βπ β π π¦ β π) |
41 | | 0red 11092 |
. . . . 5
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β 0 β β) |
42 | | simplr 768 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π¦ β π) |
43 | | eqid 2738 |
. . . . . . . 8
β’ (π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < )) = (π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, <
)) |
44 | 43 | metdsval 24132 |
. . . . . . 7
β’ (π¦ β π β ((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) = inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
45 | 42, 44 | syl 17 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β ((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) = inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
46 | 3 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π· β (Metβπ)) |
47 | | difssd 4091 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (π β π) β π) |
48 | 6 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π β π½) |
49 | | simprl 770 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π β π) |
50 | 48, 49 | sseldd 3944 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π β π½) |
51 | | elssuni 4897 |
. . . . . . . . . . 11
β’ (π β π½ β π β βͺ π½) |
52 | 50, 51 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π β βͺ π½) |
53 | 46, 11, 14 | 3syl 18 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π = βͺ π½) |
54 | 52, 53 | sseqtrrd 3984 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π β π) |
55 | | eleq1 2826 |
. . . . . . . . . . . . . 14
β’ (π = π β (π β π β π β π)) |
56 | 55 | notbid 318 |
. . . . . . . . . . . . 13
β’ (π = π β (Β¬ π β π β Β¬ π β π)) |
57 | 18, 56 | syl5ibrcom 247 |
. . . . . . . . . . . 12
β’ (π β (π = π β Β¬ π β π)) |
58 | 57 | necon2ad 2957 |
. . . . . . . . . . 11
β’ (π β (π β π β π β π)) |
59 | 58 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (π β π β π β π)) |
60 | 49, 59 | mpd 15 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π β π) |
61 | | pssdifn0 4324 |
. . . . . . . . 9
β’ ((π β π β§ π β π) β (π β π) β β
) |
62 | 54, 60, 61 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (π β π) β β
) |
63 | 43 | metdsre 24138 |
. . . . . . . 8
β’ ((π· β (Metβπ) β§ (π β π) β π β§ (π β π) β β
) β (π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < )):πβΆβ) |
64 | 46, 47, 62, 63 | syl3anc 1372 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < )):πβΆβ) |
65 | 64, 42 | ffvelcdmd 7031 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β ((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) β
β) |
66 | 45, 65 | eqeltrrd 2840 |
. . . . 5
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β) |
67 | 35 | adantr 482 |
. . . . 5
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β) |
68 | 12 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π· β (βMetβπ)) |
69 | 43 | metdsf 24133 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ (π β π) β π) β (π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < )):πβΆ(0[,]+β)) |
70 | 68, 47, 69 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < )):πβΆ(0[,]+β)) |
71 | 70, 42 | ffvelcdmd 7031 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β ((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) β
(0[,]+β)) |
72 | | elxrge0 13303 |
. . . . . . . . 9
β’ (((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) β (0[,]+β) β
(((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) β β*
β§ 0 β€ ((π€ β
π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦))) |
73 | 71, 72 | sylib 217 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) β β*
β§ 0 β€ ((π€ β
π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦))) |
74 | 73 | simprd 497 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β 0 β€ ((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦)) |
75 | | elndif 4087 |
. . . . . . . . . 10
β’ (π¦ β π β Β¬ π¦ β (π β π)) |
76 | 75 | ad2antll 728 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β Β¬ π¦ β (π β π)) |
77 | 53 | difeq1d 4080 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (π β π) = (βͺ π½ β π)) |
78 | 13 | mopntop 23715 |
. . . . . . . . . . . . 13
β’ (π· β (βMetβπ) β π½ β Top) |
79 | 68, 78 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π½ β Top) |
80 | | eqid 2738 |
. . . . . . . . . . . . 13
β’ βͺ π½ =
βͺ π½ |
81 | 80 | opncld 22306 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§ π β π½) β (βͺ π½ β π) β (Clsdβπ½)) |
82 | 79, 50, 81 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (βͺ π½ β π) β (Clsdβπ½)) |
83 | 77, 82 | eqeltrd 2839 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (π β π) β (Clsdβπ½)) |
84 | | cldcls 22315 |
. . . . . . . . . 10
β’ ((π β π) β (Clsdβπ½) β ((clsβπ½)β(π β π)) = (π β π)) |
85 | 83, 84 | syl 17 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β ((clsβπ½)β(π β π)) = (π β π)) |
86 | 76, 85 | neleqtrrd 2861 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β Β¬ π¦ β ((clsβπ½)β(π β π))) |
87 | 43, 13 | metdseq0 24139 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ (π β π) β π β§ π¦ β π) β (((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) = 0 β π¦ β ((clsβπ½)β(π β π)))) |
88 | 68, 47, 42, 87 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) = 0 β π¦ β ((clsβπ½)β(π β π)))) |
89 | 88 | necon3abid 2979 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β (((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) β 0 β Β¬ π¦ β ((clsβπ½)β(π β π)))) |
90 | 86, 89 | mpbird 257 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β ((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦) β 0) |
91 | 65, 74, 90 | ne0gt0d 11226 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β 0 < ((π€ β π β¦ inf(ran (π§ β (π β π) β¦ (π€π·π§)), β*, < ))βπ¦)) |
92 | 91, 45 | breqtrd 5130 |
. . . . 5
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β 0 < inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
93 | 1 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β π β Fin) |
94 | 34 | adantlr 714 |
. . . . . 6
β’ ((((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β§ π β π) β inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β) |
95 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ π¦ β π) β§ π β π) β π· β (βMetβπ)) |
96 | 27 | metdsf 24133 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ (π β π) β π) β (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆ(0[,]+β)) |
97 | 95, 5, 96 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β§ π¦ β π) β§ π β π) β (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆ(0[,]+β)) |
98 | 27 | fmpt 7053 |
. . . . . . . . . . 11
β’
(βπ¦ β
π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
(0[,]+β) β (π¦
β π β¦ inf(ran
(π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆ(0[,]+β)) |
99 | 97, 98 | sylibr 233 |
. . . . . . . . . 10
β’ (((π β§ π¦ β π) β§ π β π) β βπ¦ β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
(0[,]+β)) |
100 | | rsp 3229 |
. . . . . . . . . 10
β’
(βπ¦ β
π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
(0[,]+β) β (π¦
β π β inf(ran
(π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
(0[,]+β))) |
101 | 99, 32, 100 | sylc 65 |
. . . . . . . . 9
β’ (((π β§ π¦ β π) β§ π β π) β inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
(0[,]+β)) |
102 | | elxrge0 13303 |
. . . . . . . . 9
β’ (inf(ran
(π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
(0[,]+β) β (inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β* β§ 0 β€ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
))) |
103 | 101, 102 | sylib 217 |
. . . . . . . 8
β’ (((π β§ π¦ β π) β§ π β π) β (inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β* β§ 0 β€ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
))) |
104 | 103 | simprd 497 |
. . . . . . 7
β’ (((π β§ π¦ β π) β§ π β π) β 0 β€ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
105 | 104 | adantlr 714 |
. . . . . 6
β’ ((((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β§ π β π) β 0 β€ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
106 | | difeq2 4075 |
. . . . . . . . 9
β’ (π = π β (π β π) = (π β π)) |
107 | 106 | mpteq1d 5199 |
. . . . . . . 8
β’ (π = π β (π§ β (π β π) β¦ (π¦π·π§)) = (π§ β (π β π) β¦ (π¦π·π§))) |
108 | 107 | rneqd 5890 |
. . . . . . 7
β’ (π = π β ran (π§ β (π β π) β¦ (π¦π·π§)) = ran (π§ β (π β π) β¦ (π¦π·π§))) |
109 | 108 | infeq1d 9347 |
. . . . . 6
β’ (π = π β inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) = inf(ran
(π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
110 | 93, 94, 105, 109, 49 | fsumge1 15617 |
. . . . 5
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β€
Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
111 | 41, 66, 67, 92, 110 | ltletrd 11249 |
. . . 4
β’ (((π β§ π¦ β π) β§ (π β π β§ π¦ β π)) β 0 < Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
112 | 40, 111 | rexlimddv 3157 |
. . 3
β’ ((π β§ π¦ β π) β 0 < Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
113 | 35, 112 | elrpd 12883 |
. 2
β’ ((π β§ π¦ β π) β Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) β
β+) |
114 | | lebnumlem1.f |
. 2
β’ πΉ = (π¦ β π β¦ Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
115 | 113, 114 | fmptd 7057 |
1
β’ (π β πΉ:πβΆβ+) |