Step | Hyp | Ref
| Expression |
1 | | bcthlem.11 |
. . . . 5
β’ (π β βπ β β (πβ(π + 1)) β (ππΉ(πβπ))) |
2 | | fvoveq1 7381 |
. . . . . . 7
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
3 | | id 22 |
. . . . . . . 8
β’ (π = π β π = π) |
4 | | fveq2 6843 |
. . . . . . . 8
β’ (π = π β (πβπ) = (πβπ)) |
5 | 3, 4 | oveq12d 7376 |
. . . . . . 7
β’ (π = π β (ππΉ(πβπ)) = (ππΉ(πβπ))) |
6 | 2, 5 | eleq12d 2832 |
. . . . . 6
β’ (π = π β ((πβ(π + 1)) β (ππΉ(πβπ)) β (πβ(π + 1)) β (ππΉ(πβπ)))) |
7 | 6 | rspccva 3581 |
. . . . 5
β’
((βπ β
β (πβ(π + 1)) β (ππΉ(πβπ)) β§ π β β) β (πβ(π + 1)) β (ππΉ(πβπ))) |
8 | 1, 7 | sylan 581 |
. . . 4
β’ ((π β§ π β β) β (πβ(π + 1)) β (ππΉ(πβπ))) |
9 | | bcthlem.9 |
. . . . . 6
β’ (π β π:ββΆ(π Γ
β+)) |
10 | 9 | ffvelcdmda 7036 |
. . . . 5
β’ ((π β§ π β β) β (πβπ) β (π Γ
β+)) |
11 | | bcth.2 |
. . . . . . 7
β’ π½ = (MetOpenβπ·) |
12 | | bcthlem.4 |
. . . . . . 7
β’ (π β π· β (CMetβπ)) |
13 | | bcthlem.5 |
. . . . . . 7
β’ πΉ = (π β β, π§ β (π Γ β+) β¦
{β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) |
14 | 11, 12, 13 | bcthlem1 24691 |
. . . . . 6
β’ ((π β§ (π β β β§ (πβπ) β (π Γ β+))) β
((πβ(π + 1)) β (ππΉ(πβπ)) β ((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ))))) |
15 | 14 | expr 458 |
. . . . 5
β’ ((π β§ π β β) β ((πβπ) β (π Γ β+) β ((πβ(π + 1)) β (ππΉ(πβπ)) β ((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ)))))) |
16 | 10, 15 | mpd 15 |
. . . 4
β’ ((π β§ π β β) β ((πβ(π + 1)) β (ππΉ(πβπ)) β ((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ))))) |
17 | 8, 16 | mpbid 231 |
. . 3
β’ ((π β§ π β β) β ((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ)))) |
18 | | cmetmet 24653 |
. . . . . . . . . . . 12
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
19 | 12, 18 | syl 17 |
. . . . . . . . . . 11
β’ (π β π· β (Metβπ)) |
20 | | metxmet 23690 |
. . . . . . . . . . 11
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
β’ (π β π· β (βMetβπ)) |
22 | 11 | mopntop 23796 |
. . . . . . . . . 10
β’ (π· β (βMetβπ) β π½ β Top) |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
β’ (π β π½ β Top) |
24 | | xp1st 7954 |
. . . . . . . . . . . 12
β’ ((πβ(π + 1)) β (π Γ β+) β
(1st β(πβ(π + 1))) β π) |
25 | | xp2nd 7955 |
. . . . . . . . . . . . 13
β’ ((πβ(π + 1)) β (π Γ β+) β
(2nd β(πβ(π + 1))) β
β+) |
26 | 25 | rpxrd 12959 |
. . . . . . . . . . . 12
β’ ((πβ(π + 1)) β (π Γ β+) β
(2nd β(πβ(π + 1))) β
β*) |
27 | 24, 26 | jca 513 |
. . . . . . . . . . 11
β’ ((πβ(π + 1)) β (π Γ β+) β
((1st β(πβ(π + 1))) β π β§ (2nd β(πβ(π + 1))) β
β*)) |
28 | | blssm 23774 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ (1st
β(πβ(π + 1))) β π β§ (2nd β(πβ(π + 1))) β β*) β
((1st β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) β π) |
29 | 28 | 3expb 1121 |
. . . . . . . . . . 11
β’ ((π· β (βMetβπ) β§ ((1st
β(πβ(π + 1))) β π β§ (2nd β(πβ(π + 1))) β β*)) β
((1st β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) β π) |
30 | 21, 27, 29 | syl2an 597 |
. . . . . . . . . 10
β’ ((π β§ (πβ(π + 1)) β (π Γ β+)) β
((1st β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) β π) |
31 | | df-ov 7361 |
. . . . . . . . . . . 12
β’
((1st β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) = ((ballβπ·)ββ¨(1st β(πβ(π + 1))), (2nd β(πβ(π + 1)))β©) |
32 | | 1st2nd2 7961 |
. . . . . . . . . . . . 13
β’ ((πβ(π + 1)) β (π Γ β+) β (πβ(π + 1)) = β¨(1st β(πβ(π + 1))), (2nd β(πβ(π + 1)))β©) |
33 | 32 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ ((πβ(π + 1)) β (π Γ β+) β
((ballβπ·)β(πβ(π + 1))) = ((ballβπ·)ββ¨(1st β(πβ(π + 1))), (2nd β(πβ(π + 1)))β©)) |
34 | 31, 33 | eqtr4id 2796 |
. . . . . . . . . . 11
β’ ((πβ(π + 1)) β (π Γ β+) β
((1st β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) = ((ballβπ·)β(πβ(π + 1)))) |
35 | 34 | adantl 483 |
. . . . . . . . . 10
β’ ((π β§ (πβ(π + 1)) β (π Γ β+)) β
((1st β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) = ((ballβπ·)β(πβ(π + 1)))) |
36 | 11 | mopnuni 23797 |
. . . . . . . . . . . 12
β’ (π· β (βMetβπ) β π = βͺ π½) |
37 | 21, 36 | syl 17 |
. . . . . . . . . . 11
β’ (π β π = βͺ π½) |
38 | 37 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (πβ(π + 1)) β (π Γ β+)) β π = βͺ
π½) |
39 | 30, 35, 38 | 3sstr3d 3991 |
. . . . . . . . 9
β’ ((π β§ (πβ(π + 1)) β (π Γ β+)) β
((ballβπ·)β(πβ(π + 1))) β βͺ
π½) |
40 | | eqid 2737 |
. . . . . . . . . 10
β’ βͺ π½ =
βͺ π½ |
41 | 40 | sscls 22410 |
. . . . . . . . 9
β’ ((π½ β Top β§
((ballβπ·)β(πβ(π + 1))) β βͺ
π½) β
((ballβπ·)β(πβ(π + 1))) β ((clsβπ½)β((ballβπ·)β(πβ(π + 1))))) |
42 | 23, 39, 41 | syl2an2r 684 |
. . . . . . . 8
β’ ((π β§ (πβ(π + 1)) β (π Γ β+)) β
((ballβπ·)β(πβ(π + 1))) β ((clsβπ½)β((ballβπ·)β(πβ(π + 1))))) |
43 | | difss2 4094 |
. . . . . . . 8
β’
(((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ)) β ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β ((ballβπ·)β(πβπ))) |
44 | | sstr2 3952 |
. . . . . . . 8
β’
(((ballβπ·)β(πβ(π + 1))) β ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β ((ballβπ·)β(πβπ)) β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ)))) |
45 | 42, 43, 44 | syl2im 40 |
. . . . . . 7
β’ ((π β§ (πβ(π + 1)) β (π Γ β+)) β
(((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ)) β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ)))) |
46 | 45 | a1d 25 |
. . . . . 6
β’ ((π β§ (πβ(π + 1)) β (π Γ β+)) β
((2nd β(πβ(π + 1))) < (1 / π) β (((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ)) β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ))))) |
47 | 46 | ex 414 |
. . . . 5
β’ (π β ((πβ(π + 1)) β (π Γ β+) β
((2nd β(πβ(π + 1))) < (1 / π) β (((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ)) β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ)))))) |
48 | 47 | 3impd 1349 |
. . . 4
β’ (π β (((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ))) β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ)))) |
49 | 48 | adantr 482 |
. . 3
β’ ((π β§ π β β) β (((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ))) β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ)))) |
50 | 17, 49 | mpd 15 |
. 2
β’ ((π β§ π β β) β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ))) |
51 | 50 | ralrimiva 3144 |
1
β’ (π β βπ β β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ))) |