Step | Hyp | Ref
| Expression |
1 | | 1rp 12975 |
. . . 4
β’ 1 β
β+ |
2 | 1 | ne0ii 4329 |
. . 3
β’
β+ β β
|
3 | | ral0 4504 |
. . . . 5
β’
βπ₯ β
β
βπ’ β
π (π₯(ballβπ·)π) β π’ |
4 | | simpr 484 |
. . . . . 6
β’ ((π β§ π = β
) β π = β
) |
5 | 4 | raleqdv 3317 |
. . . . 5
β’ ((π β§ π = β
) β (βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’ β βπ₯ β β
βπ’ β π (π₯(ballβπ·)π) β π’)) |
6 | 3, 5 | mpbiri 258 |
. . . 4
β’ ((π β§ π = β
) β βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
7 | 6 | ralrimivw 3142 |
. . 3
β’ ((π β§ π = β
) β βπ β β+
βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
8 | | r19.2z 4486 |
. . 3
β’
((β+ β β
β§ βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
9 | 2, 7, 8 | sylancr 586 |
. 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 24809 |
. . . . . 6
β’ (π β πΉ:πβΆβ+) |
19 | 18 | adantr 480 |
. . . . 5
β’ ((π β§ π β β
) β πΉ:πβΆβ+) |
20 | 19 | frnd 6715 |
. . . 4
β’ ((π β§ π β β
) β ran πΉ β
β+) |
21 | | eqid 2724 |
. . . . . . 7
β’ βͺ π½ =
βͺ π½ |
22 | | lebnumlem2.k |
. . . . . . 7
β’ πΎ = (topGenβran
(,)) |
23 | 12 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β β
) β π½ β Comp) |
24 | 10, 11, 12, 13, 14, 15, 16, 17, 22 | lebnumlem2 24810 |
. . . . . . . 8
β’ (π β πΉ β (π½ Cn πΎ)) |
25 | 24 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β β
) β πΉ β (π½ Cn πΎ)) |
26 | | metxmet 24162 |
. . . . . . . . . 10
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
27 | 10 | mopnuni 24269 |
. . . . . . . . . 10
β’ (π· β (βMetβπ) β π = βͺ π½) |
28 | 11, 26, 27 | 3syl 18 |
. . . . . . . . 9
β’ (π β π = βͺ π½) |
29 | 28 | neeq1d 2992 |
. . . . . . . 8
β’ (π β (π β β
β βͺ π½
β β
)) |
30 | 29 | biimpa 476 |
. . . . . . 7
β’ ((π β§ π β β
) β βͺ π½
β β
) |
31 | 21, 22, 23, 25, 30 | evth2 24808 |
. . . . . 6
β’ ((π β§ π β β
) β βπ€ β βͺ π½βπ₯ β βͺ π½(πΉβπ€) β€ (πΉβπ₯)) |
32 | 28 | adantr 480 |
. . . . . . 7
β’ ((π β§ π β β
) β π = βͺ π½) |
33 | | raleq 3314 |
. . . . . . . 8
β’ (π = βͺ
π½ β (βπ₯ β π (πΉβπ€) β€ (πΉβπ₯) β βπ₯ β βͺ π½(πΉβπ€) β€ (πΉβπ₯))) |
34 | 33 | rexeqbi1dv 3326 |
. . . . . . 7
β’ (π = βͺ
π½ β (βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯) β βπ€ β βͺ π½βπ₯ β βͺ π½(πΉβπ€) β€ (πΉβπ₯))) |
35 | 32, 34 | syl 17 |
. . . . . 6
β’ ((π β§ π β β
) β (βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯) β βπ€ β βͺ π½βπ₯ β βͺ π½(πΉβπ€) β€ (πΉβπ₯))) |
36 | 31, 35 | mpbird 257 |
. . . . 5
β’ ((π β§ π β β
) β βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯)) |
37 | | ffn 6707 |
. . . . . 6
β’ (πΉ:πβΆβ+ β πΉ Fn π) |
38 | | breq1 5141 |
. . . . . . . 8
β’ (π = (πΉβπ€) β (π β€ (πΉβπ₯) β (πΉβπ€) β€ (πΉβπ₯))) |
39 | 38 | ralbidv 3169 |
. . . . . . 7
β’ (π = (πΉβπ€) β (βπ₯ β π π β€ (πΉβπ₯) β βπ₯ β π (πΉβπ€) β€ (πΉβπ₯))) |
40 | 39 | rexrn 7078 |
. . . . . 6
β’ (πΉ Fn π β (βπ β ran πΉβπ₯ β π π β€ (πΉβπ₯) β βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯))) |
41 | 19, 37, 40 | 3syl 18 |
. . . . 5
β’ ((π β§ π β β
) β (βπ β ran πΉβπ₯ β π π β€ (πΉβπ₯) β βπ€ β π βπ₯ β π (πΉβπ€) β€ (πΉβπ₯))) |
42 | 36, 41 | mpbird 257 |
. . . 4
β’ ((π β§ π β β
) β βπ β ran πΉβπ₯ β π π β€ (πΉβπ₯)) |
43 | | ssrexv 4043 |
. . . 4
β’ (ran
πΉ β
β+ β (βπ β ran πΉβπ₯ β π π β€ (πΉβπ₯) β βπ β β+ βπ₯ β π π β€ (πΉβπ₯))) |
44 | 20, 42, 43 | sylc 65 |
. . 3
β’ ((π β§ π β β
) β βπ β β+
βπ₯ β π π β€ (πΉβπ₯)) |
45 | | simpr 484 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β β+) β π β
β+) |
46 | 14 | ad2antrr 723 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π β β+) β π = βͺ
π) |
47 | | simplr 766 |
. . . . . . . . . 10
β’ (((π β§ π β β
) β§ π β β+) β π β β
) |
48 | 46, 47 | eqnetrrd 3001 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ π β β+) β βͺ π
β β
) |
49 | | unieq 4910 |
. . . . . . . . . . 11
β’ (π = β
β βͺ π =
βͺ β
) |
50 | | uni0 4929 |
. . . . . . . . . . 11
β’ βͺ β
= β
|
51 | 49, 50 | eqtrdi 2780 |
. . . . . . . . . 10
β’ (π = β
β βͺ π =
β
) |
52 | 51 | necon3i 2965 |
. . . . . . . . 9
β’ (βͺ π
β β
β π β
β
) |
53 | 48, 52 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π β β+) β π β β
) |
54 | 15 | ad2antrr 723 |
. . . . . . . . 9
β’ (((π β§ π β β
) β§ π β β+) β π β Fin) |
55 | | hashnncl 14323 |
. . . . . . . . 9
β’ (π β Fin β
((β―βπ) β
β β π β
β
)) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
β’ (((π β§ π β β
) β§ π β β+) β
((β―βπ) β
β β π β
β
)) |
57 | 53, 56 | mpbird 257 |
. . . . . . 7
β’ (((π β§ π β β
) β§ π β β+) β
(β―βπ) β
β) |
58 | 57 | nnrpd 13011 |
. . . . . 6
β’ (((π β§ π β β
) β§ π β β+) β
(β―βπ) β
β+) |
59 | 45, 58 | rpdivcld 13030 |
. . . . 5
β’ (((π β§ π β β
) β§ π β β+) β (π / (β―βπ)) β
β+) |
60 | | ralnex 3064 |
. . . . . . . 8
β’
(βπ’ β
π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’ β Β¬ βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’) |
61 | 54 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β Fin) |
62 | 53 | adantr 480 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β β
) |
63 | | simprl 768 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π₯ β π) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π₯ β π) |
65 | | eqid 2724 |
. . . . . . . . . . . . . . 15
β’ (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )) = (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, <
)) |
66 | 65 | metdsval 24685 |
. . . . . . . . . . . . . 14
β’ (π₯ β π β ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) = inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
67 | 64, 66 | syl 17 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) = inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
68 | 11 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ π β β
) β§ π β β+) β π· β (Metβπ)) |
69 | 68 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π· β (Metβπ)) |
70 | | difssd 4124 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π β π) β π) |
71 | | elssuni 4931 |
. . . . . . . . . . . . . . . . . 18
β’ (π β π β π β βͺ π) |
72 | 71 | adantl 481 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π β βͺ π) |
73 | 46 | ad2antrr 723 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π = βͺ π) |
74 | 72, 73 | sseqtrrd 4015 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π β π) |
75 | | eleq1 2813 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π = π β (π β π β π β π)) |
76 | 75 | notbid 318 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π = π β (Β¬ π β π β Β¬ π β π)) |
77 | 16, 76 | syl5ibrcom 246 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (π = π β Β¬ π β π)) |
78 | 77 | necon2ad 2947 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (π β π β π β π)) |
79 | 78 | ad3antrrr 727 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (π β π β π β π)) |
80 | 79 | imp 406 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π β π) |
81 | | pssdifn0 4357 |
. . . . . . . . . . . . . . . 16
β’ ((π β π β§ π β π) β (π β π) β β
) |
82 | 74, 80, 81 | syl2anc 583 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π β π) β β
) |
83 | 65 | metdsre 24691 |
. . . . . . . . . . . . . . 15
β’ ((π· β (Metβπ) β§ (π β π) β π β§ (π β π) β β
) β (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆβ) |
84 | 69, 70, 82, 83 | syl3anc 1368 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < )):πβΆβ) |
85 | 84, 64 | ffvelcdmd 7077 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) β
β) |
86 | 67, 85 | eqeltrrd 2826 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, < ) β
β) |
87 | 59 | ad2antrr 723 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π / (β―βπ)) β
β+) |
88 | 87 | rpred 13013 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π / (β―βπ)) β β) |
89 | | simprr 770 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’) |
90 | | sseq2 4000 |
. . . . . . . . . . . . . . . . . 18
β’ (π’ = π β ((π₯(ballβπ·)(π / (β―βπ))) β π’ β (π₯(ballβπ·)(π / (β―βπ))) β π)) |
91 | 90 | notbid 318 |
. . . . . . . . . . . . . . . . 17
β’ (π’ = π β (Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’ β Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π)) |
92 | 91 | rspccva 3603 |
. . . . . . . . . . . . . . . 16
β’
((βπ’ β
π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’ β§ π β π) β Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π) |
93 | 89, 92 | sylan 579 |
. . . . . . . . . . . . . . 15
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π) |
94 | 69, 26 | syl 17 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β π· β (βMetβπ)) |
95 | 87 | rpxrd 13014 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π / (β―βπ)) β
β*) |
96 | 65 | metdsge 24687 |
. . . . . . . . . . . . . . . . 17
β’ (((π· β (βMetβπ) β§ (π β π) β π β§ π₯ β π) β§ (π / (β―βπ)) β β*) β
((π / (β―βπ)) β€ ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) β ((π β π) β© (π₯(ballβπ·)(π / (β―βπ)))) = β
)) |
97 | 94, 70, 64, 95, 96 | syl31anc 1370 |
. . . . . . . . . . . . . . . 16
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β ((π / (β―βπ)) β€ ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) β ((π β π) β© (π₯(ballβπ·)(π / (β―βπ)))) = β
)) |
98 | | blssm 24246 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β (βMetβπ) β§ π₯ β π β§ (π / (β―βπ)) β β*) β (π₯(ballβπ·)(π / (β―βπ))) β π) |
99 | 94, 64, 95, 98 | syl3anc 1368 |
. . . . . . . . . . . . . . . . 17
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (π₯(ballβπ·)(π / (β―βπ))) β π) |
100 | | difin0ss 4360 |
. . . . . . . . . . . . . . . . 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 11358 |
. . . . . . . . . . . . . 14
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β (((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) < (π / (β―βπ)) β Β¬ (π / (β―βπ)) β€ ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯))) |
105 | 103, 104 | mpbird 257 |
. . . . . . . . . . . . 13
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β ((π¦ β π β¦ inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ))βπ₯) < (π / (β―βπ))) |
106 | 67, 105 | eqbrtrrd 5162 |
. . . . . . . . . . . 12
β’
(((((π β§ π β β
) β§ π β β+)
β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β§ π β π) β inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, < ) < (π / (β―βπ))) |
107 | 61, 62, 86, 88, 106 | fsumlt 15743 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β Ξ£π β π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, < ) <
Ξ£π β π (π / (β―βπ))) |
108 | | oveq1 7408 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ = π₯ β (π¦π·π§) = (π₯π·π§)) |
109 | 108 | mpteq2dv 5240 |
. . . . . . . . . . . . . . . 16
β’ (π¦ = π₯ β (π§ β (π β π) β¦ (π¦π·π§)) = (π§ β (π β π) β¦ (π₯π·π§))) |
110 | 109 | rneqd 5927 |
. . . . . . . . . . . . . . 15
β’ (π¦ = π₯ β ran (π§ β (π β π) β¦ (π¦π·π§)) = ran (π§ β (π β π) β¦ (π₯π·π§))) |
111 | 110 | infeq1d 9468 |
. . . . . . . . . . . . . 14
β’ (π¦ = π₯ β inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) = inf(ran
(π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
112 | 111 | sumeq2sdv 15647 |
. . . . . . . . . . . . 13
β’ (π¦ = π₯ β Ξ£π β π inf(ran (π§ β (π β π) β¦ (π¦π·π§)), β*, < ) =
Ξ£π β π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
113 | | sumex 15631 |
. . . . . . . . . . . . 13
β’
Ξ£π β
π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, < ) β
V |
114 | 112, 17, 113 | fvmpt 6988 |
. . . . . . . . . . . 12
β’ (π₯ β π β (πΉβπ₯) = Ξ£π β π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
115 | 63, 114 | syl 17 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (πΉβπ₯) = Ξ£π β π inf(ran (π§ β (π β π) β¦ (π₯π·π§)), β*, <
)) |
116 | 59 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (π / (β―βπ)) β
β+) |
117 | 116 | rpcnd 13015 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (π / (β―βπ)) β β) |
118 | | fsumconst 15733 |
. . . . . . . . . . . . 13
β’ ((π β Fin β§ (π / (β―βπ)) β β) β
Ξ£π β π (π / (β―βπ)) = ((β―βπ) Β· (π / (β―βπ)))) |
119 | 61, 117, 118 | syl2anc 583 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β Ξ£π β π (π / (β―βπ)) = ((β―βπ) Β· (π / (β―βπ)))) |
120 | | simplr 766 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β β+) |
121 | 120 | rpcnd 13015 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β β) |
122 | 57 | adantr 480 |
. . . . . . . . . . . . . 14
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (β―βπ) β β) |
123 | 122 | nncnd 12225 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (β―βπ) β β) |
124 | 122 | nnne0d 12259 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (β―βπ) β 0) |
125 | 121, 123,
124 | divcan2d 11989 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β ((β―βπ) Β· (π / (β―βπ))) = π) |
126 | 119, 125 | eqtr2d 2765 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π = Ξ£π β π (π / (β―βπ))) |
127 | 107, 115,
126 | 3brtr4d 5170 |
. . . . . . . . . 10
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (πΉβπ₯) < π) |
128 | 19 | ad2antrr 723 |
. . . . . . . . . . . . 13
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β πΉ:πβΆβ+) |
129 | 128, 63 | ffvelcdmd 7077 |
. . . . . . . . . . . 12
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (πΉβπ₯) β
β+) |
130 | 129 | rpred 13013 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β (πΉβπ₯) β β) |
131 | 120 | rpred 13013 |
. . . . . . . . . . 11
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β π β β) |
132 | 130, 131 | ltnled 11358 |
. . . . . . . . . 10
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β ((πΉβπ₯) < π β Β¬ π β€ (πΉβπ₯))) |
133 | 127, 132 | mpbid 231 |
. . . . . . . . 9
β’ ((((π β§ π β β
) β§ π β β+) β§ (π₯ β π β§ βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’)) β Β¬ π β€ (πΉβπ₯)) |
134 | 133 | expr 456 |
. . . . . . . 8
β’ ((((π β§ π β β
) β§ π β β+) β§ π₯ β π) β (βπ’ β π Β¬ (π₯(ballβπ·)(π / (β―βπ))) β π’ β Β¬ π β€ (πΉβπ₯))) |
135 | 60, 134 | biimtrrid 242 |
. . . . . . 7
β’ ((((π β§ π β β
) β§ π β β+) β§ π₯ β π) β (Β¬ βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’ β Β¬ π β€ (πΉβπ₯))) |
136 | 135 | con4d 115 |
. . . . . 6
β’ ((((π β§ π β β
) β§ π β β+) β§ π₯ β π) β (π β€ (πΉβπ₯) β βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
137 | 136 | ralimdva 3159 |
. . . . 5
β’ (((π β§ π β β
) β§ π β β+) β
(βπ₯ β π π β€ (πΉβπ₯) β βπ₯ β π βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
138 | | oveq2 7409 |
. . . . . . . . 9
β’ (π = (π / (β―βπ)) β (π₯(ballβπ·)π) = (π₯(ballβπ·)(π / (β―βπ)))) |
139 | 138 | sseq1d 4005 |
. . . . . . . 8
β’ (π = (π / (β―βπ)) β ((π₯(ballβπ·)π) β π’ β (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
140 | 139 | rexbidv 3170 |
. . . . . . 7
β’ (π = (π / (β―βπ)) β (βπ’ β π (π₯(ballβπ·)π) β π’ β βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
141 | 140 | ralbidv 3169 |
. . . . . 6
β’ (π = (π / (β―βπ)) β (βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’ β βπ₯ β π βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’)) |
142 | 141 | rspcev 3604 |
. . . . 5
β’ (((π / (β―βπ)) β β+
β§ βπ₯ β
π βπ’ β π (π₯(ballβπ·)(π / (β―βπ))) β π’) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
143 | 59, 137, 142 | syl6an 681 |
. . . 4
β’ (((π β§ π β β
) β§ π β β+) β
(βπ₯ β π π β€ (πΉβπ₯) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’)) |
144 | 143 | rexlimdva 3147 |
. . 3
β’ ((π β§ π β β
) β (βπ β β+
βπ₯ β π π β€ (πΉβπ₯) β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’)) |
145 | 44, 144 | mpd 15 |
. 2
β’ ((π β§ π β β
) β βπ β β+
βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |
146 | 9, 145 | pm2.61dane 3021 |
1
β’ (π β βπ β β+ βπ₯ β π βπ’ β π (π₯(ballβπ·)π) β π’) |