Step | Hyp | Ref
| Expression |
1 | | bcthlem.11 |
. . . . . . 7
β’ (π β βπ β β (πβ(π + 1)) β (ππΉ(πβπ))) |
2 | | fvoveq1 7381 |
. . . . . . . . 9
β’ (π = π΄ β (πβ(π + 1)) = (πβ(π΄ + 1))) |
3 | | id 22 |
. . . . . . . . . 10
β’ (π = π΄ β π = π΄) |
4 | | fveq2 6843 |
. . . . . . . . . 10
β’ (π = π΄ β (πβπ) = (πβπ΄)) |
5 | 3, 4 | oveq12d 7376 |
. . . . . . . . 9
β’ (π = π΄ β (ππΉ(πβπ)) = (π΄πΉ(πβπ΄))) |
6 | 2, 5 | eleq12d 2832 |
. . . . . . . 8
β’ (π = π΄ β ((πβ(π + 1)) β (ππΉ(πβπ)) β (πβ(π΄ + 1)) β (π΄πΉ(πβπ΄)))) |
7 | 6 | rspccva 3581 |
. . . . . . 7
β’
((βπ β
β (πβ(π + 1)) β (ππΉ(πβπ)) β§ π΄ β β) β (πβ(π΄ + 1)) β (π΄πΉ(πβπ΄))) |
8 | 1, 7 | sylan 581 |
. . . . . 6
β’ ((π β§ π΄ β β) β (πβ(π΄ + 1)) β (π΄πΉ(πβπ΄))) |
9 | | bcthlem.9 |
. . . . . . . 8
β’ (π β π:ββΆ(π Γ
β+)) |
10 | 9 | ffvelcdmda 7036 |
. . . . . . 7
β’ ((π β§ π΄ β β) β (πβπ΄) β (π Γ
β+)) |
11 | | bcth.2 |
. . . . . . . . 9
β’ π½ = (MetOpenβπ·) |
12 | | bcthlem.4 |
. . . . . . . . 9
β’ (π β π· β (CMetβπ)) |
13 | | bcthlem.5 |
. . . . . . . . 9
β’ πΉ = (π β β, π§ β (π Γ β+) β¦
{β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) |
14 | 11, 12, 13 | bcthlem1 24691 |
. . . . . . . 8
β’ ((π β§ (π΄ β β β§ (πβπ΄) β (π Γ β+))) β
((πβ(π΄ + 1)) β (π΄πΉ(πβπ΄)) β ((πβ(π΄ + 1)) β (π Γ β+) β§
(2nd β(πβ(π΄ + 1))) < (1 / π΄) β§ ((clsβπ½)β((ballβπ·)β(πβ(π΄ + 1)))) β (((ballβπ·)β(πβπ΄)) β (πβπ΄))))) |
15 | 14 | expr 458 |
. . . . . . 7
β’ ((π β§ π΄ β β) β ((πβπ΄) β (π Γ β+) β ((πβ(π΄ + 1)) β (π΄πΉ(πβπ΄)) β ((πβ(π΄ + 1)) β (π Γ β+) β§
(2nd β(πβ(π΄ + 1))) < (1 / π΄) β§ ((clsβπ½)β((ballβπ·)β(πβ(π΄ + 1)))) β (((ballβπ·)β(πβπ΄)) β (πβπ΄)))))) |
16 | 10, 15 | mpd 15 |
. . . . . 6
β’ ((π β§ π΄ β β) β ((πβ(π΄ + 1)) β (π΄πΉ(πβπ΄)) β ((πβ(π΄ + 1)) β (π Γ β+) β§
(2nd β(πβ(π΄ + 1))) < (1 / π΄) β§ ((clsβπ½)β((ballβπ·)β(πβ(π΄ + 1)))) β (((ballβπ·)β(πβπ΄)) β (πβπ΄))))) |
17 | 8, 16 | mpbid 231 |
. . . . 5
β’ ((π β§ π΄ β β) β ((πβ(π΄ + 1)) β (π Γ β+) β§
(2nd β(πβ(π΄ + 1))) < (1 / π΄) β§ ((clsβπ½)β((ballβπ·)β(πβ(π΄ + 1)))) β (((ballβπ·)β(πβπ΄)) β (πβπ΄)))) |
18 | 17 | simp3d 1145 |
. . . 4
β’ ((π β§ π΄ β β) β ((clsβπ½)β((ballβπ·)β(πβ(π΄ + 1)))) β (((ballβπ·)β(πβπ΄)) β (πβπ΄))) |
19 | 18 | difss2d 4095 |
. . 3
β’ ((π β§ π΄ β β) β ((clsβπ½)β((ballβπ·)β(πβ(π΄ + 1)))) β ((ballβπ·)β(πβπ΄))) |
20 | 19 | 3adant2 1132 |
. 2
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ π΄ β β) β ((clsβπ½)β((ballβπ·)β(πβ(π΄ + 1)))) β ((ballβπ·)β(πβπ΄))) |
21 | | peano2nn 12166 |
. . 3
β’ (π΄ β β β (π΄ + 1) β
β) |
22 | | cmetmet 24653 |
. . . . 5
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
23 | | metxmet 23690 |
. . . . 5
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
24 | 12, 22, 23 | 3syl 18 |
. . . 4
β’ (π β π· β (βMetβπ)) |
25 | | bcthlem.6 |
. . . . 5
β’ (π β π:ββΆ(Clsdβπ½)) |
26 | | bcthlem.7 |
. . . . 5
β’ (π β π
β
β+) |
27 | | bcthlem.8 |
. . . . 5
β’ (π β πΆ β π) |
28 | | bcthlem.10 |
. . . . 5
β’ (π β (πβ1) = β¨πΆ, π
β©) |
29 | 11, 12, 13, 25, 26, 27, 9, 28, 1 | bcthlem2 24692 |
. . . 4
β’ (π β βπ β β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ))) |
30 | 24, 9, 29, 11 | caublcls 24676 |
. . 3
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ (π΄ + 1) β β) β π₯ β ((clsβπ½)β((ballβπ·)β(πβ(π΄ + 1))))) |
31 | 21, 30 | syl3an3 1166 |
. 2
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ π΄ β β) β π₯ β ((clsβπ½)β((ballβπ·)β(πβ(π΄ + 1))))) |
32 | 20, 31 | sseldd 3946 |
1
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ π΄ β β) β π₯ β ((ballβπ·)β(πβπ΄))) |