Step | Hyp | Ref
| Expression |
1 | | 1rp 12924 |
. . . 4
β’ 1 β
β+ |
2 | 1 | ne0ii 4298 |
. . 3
β’
β+ β β
|
3 | | ral0 4471 |
. . . . 5
β’
βπ₯ β
β
βπ’ β
π (π₯(ballβπ·)π) β π’ |
4 | | simpr 486 |
. . . . . 6
β’ ((π β§ π = β
) β π = β
) |
5 | 4 | raleqdv 3312 |
. . . . 5
β’ ((π β§ π = β
) β (βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’ β βπ₯ β β
βπ’ β π (π₯(ballβπ·)π) β π’)) |
6 | 3, 5 | mpbiri 258 |
. . . 4
β’ ((π β§ π = β
) β βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
7 | 6 | ralrimivw 3144 |
. . 3
β’ ((π β§ π = β
) β βπ β β+
βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
8 | | r19.2z 4453 |
. . 3
β’
((β+ β β
β§ βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
9 | 2, 7, 8 | sylancr 588 |
. 2
β’ ((π β§ π = β
) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
10 | | lebnum.j |
. . . . . . 7
β’ π½ = (MetOpenβπ·) |
11 | | lebnum.d |
. . . . . . 7
β’ (π β π· β (Metβπ)) |
12 | | lebnum.c |
. . . . . . 7
β’ (π β π½ β Comp) |
13 | | lebnum.s |
. . . . . . 7
β’ (π β π β π½) |
14 | | lebnum.u |
. . . . . . 7
β’ (π β π = βͺ π) |
15 | | lebnumlem1.u |
. . . . . . 7
β’ (π β π β Fin) |
16 | | lebnumlem1.n |
. . . . . . 7
β’ (π β Β¬ π β π) |
17 | | lebnumlem1.f |
. . . . . . 7
β’ πΉ = (π¦ β π β¦ Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
18 | 10, 11, 12, 13, 14, 15, 16, 17 | lebnumlem1 24340 |
. . . . . 6
β’ (π β πΉ:πβΆβ+) |
19 | 18 | adantr 482 |
. . . . 5
β’ ((π β§ π β β
) β πΉ:πβΆβ+) |
20 | 19 | frnd 6677 |
. . . 4
β’ ((π β§ π β β
) β ran πΉ β
β+) |
21 | | eqid 2733 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
22 | | lebnumlem2.k |
. . . . . . 7
β’ πΎ = (topGenβran
(,)) |
23 | 12 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β
) β π½ β Comp) |
24 | 10, 11, 12, 13, 14, 15, 16, 17, 22 | lebnumlem2 24341 |
. . . . . . . 8
β’ (π β πΉ β (π½ Cn πΎ)) |
25 | 24 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β
) β πΉ β (π½ Cn πΎ)) |
26 | | metxmet 23703 |
. . . . . . . . . 10
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
27 | 10 | mopnuni 23810 |
. . . . . . . . . 10
β’ (π· β (βMetβπ) β π = βͺ π½) |
28 | 11, 26, 27 | 3syl 18 |
. . . . . . . . 9
β’ (π β π = βͺ π½) |
29 | 28 | neeq1d 3000 |
. . . . . . . 8
β’ (π β (π β β
β βͺ π½
β β
)) |
30 | 29 | biimpa 478 |
. . . . . . 7
β’ ((π β§ π β β
) β βͺ π½
β β
) |
31 | 21, 22, 23, 25, 30 | evth2 24339 |
. . . . . 6
β’ ((π β§ π β β
) β βπ€ β βͺ π½βπ₯ β βͺ π½(πΉβπ€) β€ (πΉβπ₯)) |
32 | 28 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β β
) β π = βͺ π½) |
33 | | raleq 3308 |
. . . . . . . 8
β’ (π = βͺ
π½ β (βπ₯ β π (πΉβπ€) β€ (πΉβπ₯) β βπ₯ β βͺ π½(πΉβπ€) β€ (πΉβπ₯))) |
34 | 33 | rexeqbi1dv 3307 |
. . . . . . 7
β’ (π = βͺ
π½ β (βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯) β βπ€ β βͺ π½βπ₯ β βͺ π½(πΉβπ€) β€ (πΉβπ₯))) |
35 | 32, 34 | syl 17 |
. . . . . 6
β’ ((π β§ π β β
) β (βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯) β βπ€ β βͺ π½βπ₯ β βͺ π½(πΉβπ€) β€ (πΉβπ₯))) |
36 | 31, 35 | mpbird 257 |
. . . . 5
β’ ((π β§ π β β
) β βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯)) |
37 | | ffn 6669 |
. . . . . 6
β’ (πΉ:πβΆβ+ β πΉ Fn π) |
38 | | breq1 5109 |
. . . . . . . 8
β’ (π = (πΉβπ€) β (π β€ (πΉβπ₯) β (πΉβπ€) β€ (πΉβπ₯))) |
39 | 38 | ralbidv 3171 |
. . . . . . 7
β’ (π = (πΉβπ€) β (βπ₯ β π π β€ (πΉβπ₯) β βπ₯ β π (πΉβπ€) β€ (πΉβπ₯))) |
40 | 39 | rexrn 7038 |
. . . . . 6
β’ (πΉ Fn π β (βπ β ran πΉβπ₯ β π π β€ (πΉβπ₯) β βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯))) |
41 | 19, 37, 40 | 3syl 18 |
. . . . 5
β’ ((π β§ π β β
) β (βπ β ran πΉβπ₯ β π π β€ (πΉβπ₯) β βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯))) |
42 | 36, 41 | mpbird 257 |
. . . 4
β’ ((π β§ π β β
) β βπ β ran πΉβπ₯ β π π β€ (πΉβπ₯)) |
43 | | ssrexv 4012 |
. . . 4
β’ (ran
πΉ β
β+ β (βπ β ran πΉβπ₯ β π π β€ (πΉβπ₯) β βπ β β+ βπ₯ β π π β€ (πΉβπ₯))) |
44 | 20, 42, 43 | sylc 65 |
. . 3
β’ ((π β§ π β β
) β βπ β β+
βπ₯ β π π β€ (πΉβπ₯)) |
45 | | simpr 486 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β β+) β π β
β+) |
46 | 14 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π β β+) β π = βͺ
π) |
47 | | simplr 768 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π β β+) β π β β
) |
48 | 46, 47 | eqnetrrd 3009 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ π β β+) β βͺ π
β β
) |
49 | | unieq 4877 |
. . . . . . . . . . 11
β’ (π = β
β βͺ π =
βͺ β
) |
50 | | uni0 4897 |
. . . . . . . . . . 11
β’ βͺ β
= β
|
51 | 49, 50 | eqtrdi 2789 |
. . . . . . . . . 10
β’ (π = β
β βͺ π =
β
) |
52 | 51 | necon3i 2973 |
. . . . . . . . 9
β’ (βͺ π
β β
β π β
β
) |
53 | 48, 52 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π β β+) β π β β
) |
54 | 15 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ π β β+) β π β Fin) |
55 | | hashnncl 14272 |
. . . . . . . . 9
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π β β+) β
((β―βπ) β
β β π β
β
)) |
57 | 53, 56 | mpbird 257 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β β+) β
(β―βπ) β
β) |
58 | 57 | nnrpd 12960 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β β+) β
(β―βπ) β
β+) |
59 | 45, 58 | rpdivcld 12979 |
. . . . 5
β’ (((π β§ π β β
) β§ π β β+) β (π / (β―βπ)) β
β+) |
60 | | ralnex 3072 |
. . . . . . . 8
β’
(βπ’ β
π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’ β Β¬ βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’) |
61 | 54 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β Fin) |
62 | 53 | adantr 482 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β β
) |
63 | | simprl 770 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π₯ β π) |
64 | 63 | adantr 482 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π₯ β π) |
65 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )) = (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
66 | 65 | metdsval 24226 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) = inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
67 | 64, 66 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) = inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
68 | 11 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ π β β+) β π· β (Metβπ)) |
69 | 68 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π· β (Metβπ)) |
70 | | difssd 4093 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π β π) β π) |
71 | | elssuni 4899 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β π β βͺ π) |
72 | 71 | adantl 483 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π β βͺ π) |
73 | 46 | ad2antrr 725 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π = βͺ π) |
74 | 72, 73 | sseqtrrd 3986 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π β π) |
75 | | eleq1 2822 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π β π β π β π)) |
76 | 75 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (Β¬ π β π β Β¬ π β π)) |
77 | 16, 76 | syl5ibrcom 247 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π = π β Β¬ π β π)) |
78 | 77 | necon2ad 2955 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π β π β π β π)) |
79 | 78 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (π β π β π β π)) |
80 | 79 | imp 408 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π β π) |
81 | | pssdifn0 4326 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β π) β (π β π) β β
) |
82 | 74, 80, 81 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π β π) β β
) |
83 | 65 | metdsre 24232 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Metβπ) β§ (π β π) β π β§ (π β π) β β
) β (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆβ) |
84 | 69, 70, 82, 83 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆβ) |
85 | 84, 64 | ffvelcdmd 7037 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) β
β) |
86 | 67, 85 | eqeltrrd 2835 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, < ) β
β) |
87 | 59 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π / (β―βπ)) β
β+) |
88 | 87 | rpred 12962 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π / (β―βπ)) β β) |
89 | | simprr 772 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’) |
90 | | sseq2 3971 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π β ((π₯(ballβπ·)(π / (β―βπ))) β π’ β (π₯(ballβπ·)(π / (β―βπ))) β π)) |
91 | 90 | notbid 318 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π β (Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’ β Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π)) |
92 | 91 | rspccva 3579 |
. . . . . . . . . . . . . . . 16
β’
((βπ’ β
π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’ β§ π β π) β Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π) |
93 | 89, 92 | sylan 581 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π) |
94 | 69, 26 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π· β (βMetβπ)) |
95 | 87 | rpxrd 12963 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π / (β―βπ)) β
β*) |
96 | 65 | metdsge 24228 |
. . . . . . . . . . . . . . . . 17
β’ (((π· β (βMetβπ) β§ (π β π) β π β§ π₯ β π) β§ (π / (β―βπ)) β β*) β
((π / (β―βπ)) β€ ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) β ((π β π) β© (π₯(ballβπ·)(π / (β―βπ)))) = β
)) |
97 | 94, 70, 64, 95, 96 | syl31anc 1374 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β ((π / (β―βπ)) β€ ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) β ((π β π) β© (π₯(ballβπ·)(π / (β―βπ)))) = β
)) |
98 | | blssm 23787 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (βMetβπ) β§ π₯ β π β§ (π / (β―βπ)) β β*) β (π₯(ballβπ·)(π / (β―βπ))) β π) |
99 | 94, 64, 95, 98 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π₯(ballβπ·)(π / (β―βπ))) β π) |
100 | | difin0ss 4329 |
. . . . . . . . . . . . . . . . 17
β’ (((π β π) β© (π₯(ballβπ·)(π / (β―βπ)))) = β
β ((π₯(ballβπ·)(π / (β―βπ))) β π β (π₯(ballβπ·)(π / (β―βπ))) β π)) |
101 | 99, 100 | syl5com 31 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (((π β π) β© (π₯(ballβπ·)(π / (β―βπ)))) = β
β (π₯(ballβπ·)(π / (β―βπ))) β π)) |
102 | 97, 101 | sylbid 239 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β ((π / (β―βπ)) β€ ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) β (π₯(ballβπ·)(π / (β―βπ))) β π)) |
103 | 93, 102 | mtod 197 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β Β¬ (π / (β―βπ)) β€ ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯)) |
104 | 85, 88 | ltnled 11307 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) < (π / (β―βπ)) β Β¬ (π / (β―βπ)) β€ ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯))) |
105 | 103, 104 | mpbird 257 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) < (π / (β―βπ))) |
106 | 67, 105 | eqbrtrrd 5130 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, < ) < (π / (β―βπ))) |
107 | 61, 62, 86, 88, 106 | fsumlt 15690 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β Ξ£π β π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, < ) <
Ξ£π β π (π / (β―βπ))) |
108 | | oveq1 7365 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β (π¦π·π§) = (π₯π·π§)) |
109 | 108 | mpteq2dv 5208 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β (π§ β (π β π) β¦ (π¦π·π§)) = (π§ β (π β π) β¦ (π₯π·π§))) |
110 | 109 | rneqd 5894 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β ran (π§ β (π β π) β¦ (π¦π·π§)) = ran (π§ β (π β π) β¦ (π₯π·π§))) |
111 | 110 | infeq1d 9418 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) = inf(ran
(π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
112 | 111 | sumeq2sdv 15594 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) =
Ξ£π β π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
113 | | sumex 15578 |
. . . . . . . . . . . . 13
β’
Ξ£π β
π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, < ) β
V |
114 | 112, 17, 113 | fvmpt 6949 |
. . . . . . . . . . . 12
β’ (π₯ β π β (πΉβπ₯) = Ξ£π β π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
115 | 63, 114 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (πΉβπ₯) = Ξ£π β π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
116 | 59 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (π / (β―βπ)) β
β+) |
117 | 116 | rpcnd 12964 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (π / (β―βπ)) β β) |
118 | | fsumconst 15680 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ (π / (β―βπ)) β β) β
Ξ£π β π (π / (β―βπ)) = ((β―βπ) Β· (π / (β―βπ)))) |
119 | 61, 117, 118 | syl2anc 585 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β Ξ£π β π (π / (β―βπ)) = ((β―βπ) Β· (π / (β―βπ)))) |
120 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β β+) |
121 | 120 | rpcnd 12964 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β β) |
122 | 57 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (β―βπ) β β) |
123 | 122 | nncnd 12174 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (β―βπ) β β) |
124 | 122 | nnne0d 12208 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (β―βπ) β 0) |
125 | 121, 123,
124 | divcan2d 11938 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β ((β―βπ) Β· (π / (β―βπ))) = π) |
126 | 119, 125 | eqtr2d 2774 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π = Ξ£π β π (π / (β―βπ))) |
127 | 107, 115,
126 | 3brtr4d 5138 |
. . . . . . . . . 10
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (πΉβπ₯) < π) |
128 | 19 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β πΉ:πβΆβ+) |
129 | 128, 63 | ffvelcdmd 7037 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (πΉβπ₯) β
β+) |
130 | 129 | rpred 12962 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (πΉβπ₯) β β) |
131 | 120 | rpred 12962 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β β) |
132 | 130, 131 | ltnled 11307 |
. . . . . . . . . 10
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β ((πΉβπ₯) < π β Β¬ π β€ (πΉβπ₯))) |
133 | 127, 132 | mpbid 231 |
. . . . . . . . 9
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β Β¬ π β€ (πΉβπ₯)) |
134 | 133 | expr 458 |
. . . . . . . 8
β’ ((((π β§ π β β
) β§ π β β+) β§ π₯ β π) β (βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’ β Β¬ π β€ (πΉβπ₯))) |
135 | 60, 134 | biimtrrid 242 |
. . . . . . 7
β’ ((((π β§ π β β
) β§ π β β+) β§ π₯ β π) β (Β¬ βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’ β Β¬ π β€ (πΉβπ₯))) |
136 | 135 | con4d 115 |
. . . . . 6
β’ ((((π β§ π β β
) β§ π β β+) β§ π₯ β π) β (π β€ (πΉβπ₯) β βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
137 | 136 | ralimdva 3161 |
. . . . 5
β’ (((π β§ π β β
) β§ π β β+) β
(βπ₯ β π π β€ (πΉβπ₯) β βπ₯ β π βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
138 | | oveq2 7366 |
. . . . . . . . 9
β’ (π = (π / (β―βπ)) β (π₯(ballβπ·)π) = (π₯(ballβπ·)(π / (β―βπ)))) |
139 | 138 | sseq1d 3976 |
. . . . . . . 8
β’ (π = (π / (β―βπ)) β ((π₯(ballβπ·)π) β π’ β (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
140 | 139 | rexbidv 3172 |
. . . . . . 7
β’ (π = (π / (β―βπ)) β (βπ’ β π (π₯(ballβπ·)π) β π’ β βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
141 | 140 | ralbidv 3171 |
. . . . . 6
β’ (π = (π / (β―βπ)) β (βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’ β βπ₯ β π βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
142 | 141 | rspcev 3580 |
. . . . 5
β’ (((π / (β―βπ)) β β+
β§ βπ₯ β
π βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
143 | 59, 137, 142 | syl6an 683 |
. . . 4
β’ (((π β§ π β β
) β§ π β β+) β
(βπ₯ β π π β€ (πΉβπ₯) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’)) |
144 | 143 | rexlimdva 3149 |
. . 3
β’ ((π β§ π β β
) β (βπ β β+
βπ₯ β π π β€ (πΉβπ₯) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’)) |
145 | 44, 144 | mpd 15 |
. 2
β’ ((π β§ π β β
) β βπ β β+
βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
146 | 9, 145 | pm2.61dane 3029 |
1
β’ (π β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |