Step | Hyp | Ref
| Expression |
1 | | nnnn0 12476 |
. . . . . 6
β’ (π β β β π β
β0) |
2 | | inss1 4228 |
. . . . . . . . 9
β’
(π« π β©
Fin) β π« π |
3 | | heibor.7 |
. . . . . . . . . 10
β’ (π β πΉ:β0βΆ(π« π β© Fin)) |
4 | 3 | ffvelcdmda 7084 |
. . . . . . . . 9
β’ ((π β§ π β β0) β (πΉβπ) β (π« π β© Fin)) |
5 | 2, 4 | sselid 3980 |
. . . . . . . 8
β’ ((π β§ π β β0) β (πΉβπ) β π« π) |
6 | 5 | elpwid 4611 |
. . . . . . 7
β’ ((π β§ π β β0) β (πΉβπ) β π) |
7 | | heibor.1 |
. . . . . . . . 9
β’ π½ = (MetOpenβπ·) |
8 | | heibor.3 |
. . . . . . . . 9
β’ πΎ = {π’ β£ Β¬ βπ£ β (π« π β© Fin)π’ β βͺ π£} |
9 | | heibor.4 |
. . . . . . . . 9
β’ πΊ = {β¨π¦, πβ© β£ (π β β0 β§ π¦ β (πΉβπ) β§ (π¦π΅π) β πΎ)} |
10 | | heibor.5 |
. . . . . . . . 9
β’ π΅ = (π§ β π, π β β0 β¦ (π§(ballβπ·)(1 / (2βπ)))) |
11 | | heibor.6 |
. . . . . . . . 9
β’ (π β π· β (CMetβπ)) |
12 | | heibor.8 |
. . . . . . . . 9
β’ (π β βπ β β0 π = βͺ π¦ β (πΉβπ)(π¦π΅π)) |
13 | | heibor.9 |
. . . . . . . . 9
β’ (π β βπ₯ β πΊ ((πβπ₯)πΊ((2nd βπ₯) + 1) β§ ((π΅βπ₯) β© ((πβπ₯)π΅((2nd βπ₯) + 1))) β πΎ)) |
14 | | heibor.10 |
. . . . . . . . 9
β’ (π β πΆπΊ0) |
15 | | heibor.11 |
. . . . . . . . 9
β’ π = seq0(π, (π β β0 β¦ if(π = 0, πΆ, (π β 1)))) |
16 | 7, 8, 9, 10, 11, 3, 12, 13, 14, 15 | heiborlem4 36671 |
. . . . . . . 8
β’ ((π β§ π β β0) β (πβπ)πΊπ) |
17 | | fvex 6902 |
. . . . . . . . . 10
β’ (πβπ) β V |
18 | | vex 3479 |
. . . . . . . . . 10
β’ π β V |
19 | 7, 8, 9, 17, 18 | heiborlem2 36669 |
. . . . . . . . 9
β’ ((πβπ)πΊπ β (π β β0 β§ (πβπ) β (πΉβπ) β§ ((πβπ)π΅π) β πΎ)) |
20 | 19 | simp2bi 1147 |
. . . . . . . 8
β’ ((πβπ)πΊπ β (πβπ) β (πΉβπ)) |
21 | 16, 20 | syl 17 |
. . . . . . 7
β’ ((π β§ π β β0) β (πβπ) β (πΉβπ)) |
22 | 6, 21 | sseldd 3983 |
. . . . . 6
β’ ((π β§ π β β0) β (πβπ) β π) |
23 | 1, 22 | sylan2 594 |
. . . . 5
β’ ((π β§ π β β) β (πβπ) β π) |
24 | 23 | ralrimiva 3147 |
. . . 4
β’ (π β βπ β β (πβπ) β π) |
25 | | fveq2 6889 |
. . . . . 6
β’ (π = π β (πβπ) = (πβπ)) |
26 | 25 | eleq1d 2819 |
. . . . 5
β’ (π = π β ((πβπ) β π β (πβπ) β π)) |
27 | 26 | cbvralvw 3235 |
. . . 4
β’
(βπ β
β (πβπ) β π β βπ β β (πβπ) β π) |
28 | 24, 27 | sylib 217 |
. . 3
β’ (π β βπ β β (πβπ) β π) |
29 | | 3re 12289 |
. . . . . . 7
β’ 3 β
β |
30 | | 3pos 12314 |
. . . . . . 7
β’ 0 <
3 |
31 | 29, 30 | elrpii 12974 |
. . . . . 6
β’ 3 β
β+ |
32 | | 2nn 12282 |
. . . . . . . 8
β’ 2 β
β |
33 | | nnnn0 12476 |
. . . . . . . 8
β’ (π β β β π β
β0) |
34 | | nnexpcl 14037 |
. . . . . . . 8
β’ ((2
β β β§ π
β β0) β (2βπ) β β) |
35 | 32, 33, 34 | sylancr 588 |
. . . . . . 7
β’ (π β β β
(2βπ) β
β) |
36 | 35 | nnrpd 13011 |
. . . . . 6
β’ (π β β β
(2βπ) β
β+) |
37 | | rpdivcl 12996 |
. . . . . 6
β’ ((3
β β+ β§ (2βπ) β β+) β (3 /
(2βπ)) β
β+) |
38 | 31, 36, 37 | sylancr 588 |
. . . . 5
β’ (π β β β (3 /
(2βπ)) β
β+) |
39 | | opelxpi 5713 |
. . . . . 6
β’ (((πβπ) β π β§ (3 / (2βπ)) β β+) β
β¨(πβπ), (3 / (2βπ))β© β (π Γ
β+)) |
40 | 39 | expcom 415 |
. . . . 5
β’ ((3 /
(2βπ)) β
β+ β ((πβπ) β π β β¨(πβπ), (3 / (2βπ))β© β (π Γ
β+))) |
41 | 38, 40 | syl 17 |
. . . 4
β’ (π β β β ((πβπ) β π β β¨(πβπ), (3 / (2βπ))β© β (π Γ
β+))) |
42 | 41 | ralimia 3081 |
. . 3
β’
(βπ β
β (πβπ) β π β βπ β β β¨(πβπ), (3 / (2βπ))β© β (π Γ
β+)) |
43 | 28, 42 | syl 17 |
. 2
β’ (π β βπ β β β¨(πβπ), (3 / (2βπ))β© β (π Γ
β+)) |
44 | | heibor.12 |
. . 3
β’ π = (π β β β¦ β¨(πβπ), (3 / (2βπ))β©) |
45 | 44 | fmpt 7107 |
. 2
β’
(βπ β
β β¨(πβπ), (3 / (2βπ))β© β (π Γ β+) β π:ββΆ(π Γ
β+)) |
46 | 43, 45 | sylib 217 |
1
β’ (π β π:ββΆ(π Γ
β+)) |