Step | Hyp | Ref
| Expression |
1 | | bcthlem.4 |
. . . 4
β’ (π β π· β (CMetβπ)) |
2 | | cmetmet 24653 |
. . . . . . 7
β’ (π· β (CMetβπ) β π· β (Metβπ)) |
3 | 1, 2 | syl 17 |
. . . . . 6
β’ (π β π· β (Metβπ)) |
4 | | metxmet 23690 |
. . . . . 6
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
5 | 3, 4 | syl 17 |
. . . . 5
β’ (π β π· β (βMetβπ)) |
6 | | bcthlem.9 |
. . . . 5
β’ (π β π:ββΆ(π Γ
β+)) |
7 | | bcth.2 |
. . . . . 6
β’ π½ = (MetOpenβπ·) |
8 | | bcthlem.5 |
. . . . . 6
β’ πΉ = (π β β, π§ β (π Γ β+) β¦
{β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) |
9 | | bcthlem.6 |
. . . . . 6
β’ (π β π:ββΆ(Clsdβπ½)) |
10 | | bcthlem.7 |
. . . . . 6
β’ (π β π
β
β+) |
11 | | bcthlem.8 |
. . . . . 6
β’ (π β πΆ β π) |
12 | | bcthlem.10 |
. . . . . 6
β’ (π β (πβ1) = β¨πΆ, π
β©) |
13 | | bcthlem.11 |
. . . . . 6
β’ (π β βπ β β (πβ(π + 1)) β (ππΉ(πβπ))) |
14 | 7, 1, 8, 9, 10, 11, 6, 12, 13 | bcthlem2 24692 |
. . . . 5
β’ (π β βπ β β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ))) |
15 | | elrp 12918 |
. . . . . . . . 9
β’ (π β β+
β (π β β
β§ 0 < π)) |
16 | | nnrecl 12412 |
. . . . . . . . 9
β’ ((π β β β§ 0 <
π) β βπ β β (1 / π) < π) |
17 | 15, 16 | sylbi 216 |
. . . . . . . 8
β’ (π β β+
β βπ β
β (1 / π) < π) |
18 | 17 | adantl 483 |
. . . . . . 7
β’ ((π β§ π β β+) β
βπ β β (1
/ π) < π) |
19 | | peano2nn 12166 |
. . . . . . . . . 10
β’ (π β β β (π + 1) β
β) |
20 | 19 | adantl 483 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π β β) β (π + 1) β
β) |
21 | | fvoveq1 7381 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (πβ(π + 1)) = (πβ(π + 1))) |
22 | | id 22 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β π = π) |
23 | | fveq2 6843 |
. . . . . . . . . . . . . . . . 17
β’ (π = π β (πβπ) = (πβπ)) |
24 | 22, 23 | oveq12d 7376 |
. . . . . . . . . . . . . . . 16
β’ (π = π β (ππΉ(πβπ)) = (ππΉ(πβπ))) |
25 | 21, 24 | eleq12d 2832 |
. . . . . . . . . . . . . . 15
β’ (π = π β ((πβ(π + 1)) β (ππΉ(πβπ)) β (πβ(π + 1)) β (ππΉ(πβπ)))) |
26 | 25 | rspccva 3581 |
. . . . . . . . . . . . . 14
β’
((βπ β
β (πβ(π + 1)) β (ππΉ(πβπ)) β§ π β β) β (πβ(π + 1)) β (ππΉ(πβπ))) |
27 | 13, 26 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (πβ(π + 1)) β (ππΉ(πβπ))) |
28 | 6 | ffvelcdmda 7036 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πβπ) β (π Γ
β+)) |
29 | 7, 1, 8 | bcthlem1 24691 |
. . . . . . . . . . . . . . 15
β’ ((π β§ (π β β β§ (πβπ) β (π Γ β+))) β
((πβ(π + 1)) β (ππΉ(πβπ)) β ((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ))))) |
30 | 29 | expr 458 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((πβπ) β (π Γ β+) β ((πβ(π + 1)) β (ππΉ(πβπ)) β ((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ)))))) |
31 | 28, 30 | mpd 15 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((πβ(π + 1)) β (ππΉ(πβπ)) β ((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ))))) |
32 | 27, 31 | mpbid 231 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((πβ(π + 1)) β (π Γ β+) β§
(2nd β(πβ(π + 1))) < (1 / π) β§ ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ)))) |
33 | 32 | simp2d 1144 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β (2nd
β(πβ(π + 1))) < (1 / π)) |
34 | 33 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β β) β
(2nd β(πβ(π + 1))) < (1 / π)) |
35 | 32 | simp1d 1143 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (πβ(π + 1)) β (π Γ
β+)) |
36 | | xp2nd 7955 |
. . . . . . . . . . . . . 14
β’ ((πβ(π + 1)) β (π Γ β+) β
(2nd β(πβ(π + 1))) β
β+) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β (2nd
β(πβ(π + 1))) β
β+) |
38 | 37 | rpred 12958 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β (2nd
β(πβ(π + 1))) β
β) |
39 | 38 | adantlr 714 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β β) β
(2nd β(πβ(π + 1))) β β) |
40 | | nnrecre 12196 |
. . . . . . . . . . . 12
β’ (π β β β (1 /
π) β
β) |
41 | 40 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β β) β (1 /
π) β
β) |
42 | | rpre 12924 |
. . . . . . . . . . . 12
β’ (π β β+
β π β
β) |
43 | 42 | ad2antlr 726 |
. . . . . . . . . . 11
β’ (((π β§ π β β+) β§ π β β) β π β
β) |
44 | | lttr 11232 |
. . . . . . . . . . 11
β’
(((2nd β(πβ(π + 1))) β β β§ (1 / π) β β β§ π β β) β
(((2nd β(πβ(π + 1))) < (1 / π) β§ (1 / π) < π) β (2nd β(πβ(π + 1))) < π)) |
45 | 39, 41, 43, 44 | syl3anc 1372 |
. . . . . . . . . 10
β’ (((π β§ π β β+) β§ π β β) β
(((2nd β(πβ(π + 1))) < (1 / π) β§ (1 / π) < π) β (2nd β(πβ(π + 1))) < π)) |
46 | 34, 45 | mpand 694 |
. . . . . . . . 9
β’ (((π β§ π β β+) β§ π β β) β ((1 /
π) < π β (2nd β(πβ(π + 1))) < π)) |
47 | | 2fveq3 6848 |
. . . . . . . . . . 11
β’ (π = (π + 1) β (2nd β(πβπ)) = (2nd β(πβ(π + 1)))) |
48 | 47 | breq1d 5116 |
. . . . . . . . . 10
β’ (π = (π + 1) β ((2nd β(πβπ)) < π β (2nd β(πβ(π + 1))) < π)) |
49 | 48 | rspcev 3582 |
. . . . . . . . 9
β’ (((π + 1) β β β§
(2nd β(πβ(π + 1))) < π) β βπ β β (2nd β(πβπ)) < π) |
50 | 20, 46, 49 | syl6an 683 |
. . . . . . . 8
β’ (((π β§ π β β+) β§ π β β) β ((1 /
π) < π β βπ β β (2nd β(πβπ)) < π)) |
51 | 50 | rexlimdva 3153 |
. . . . . . 7
β’ ((π β§ π β β+) β
(βπ β β (1
/ π) < π β βπ β β (2nd
β(πβπ)) < π)) |
52 | 18, 51 | mpd 15 |
. . . . . 6
β’ ((π β§ π β β+) β
βπ β β
(2nd β(πβπ)) < π) |
53 | 52 | ralrimiva 3144 |
. . . . 5
β’ (π β βπ β β+ βπ β β (2nd
β(πβπ)) < π) |
54 | 5, 6, 14, 53 | caubl 24675 |
. . . 4
β’ (π β (1st β
π) β (Cauβπ·)) |
55 | 7 | cmetcau 24656 |
. . . 4
β’ ((π· β (CMetβπ) β§ (1st β
π) β (Cauβπ·)) β (1st
β π) β dom
(βπ‘βπ½)) |
56 | 1, 54, 55 | syl2anc 585 |
. . 3
β’ (π β (1st β
π) β dom
(βπ‘βπ½)) |
57 | | fo1st 7942 |
. . . . . 6
β’
1st :VβontoβV |
58 | | fofun 6758 |
. . . . . 6
β’
(1st :VβontoβV β Fun 1st ) |
59 | 57, 58 | ax-mp 5 |
. . . . 5
β’ Fun
1st |
60 | | vex 3450 |
. . . . 5
β’ π β V |
61 | | cofunexg 7882 |
. . . . 5
β’ ((Fun
1st β§ π
β V) β (1st β π) β V) |
62 | 59, 60, 61 | mp2an 691 |
. . . 4
β’
(1st β π) β V |
63 | 62 | eldm 5857 |
. . 3
β’
((1st β π) β dom
(βπ‘βπ½) β βπ₯(1st β π)(βπ‘βπ½)π₯) |
64 | 56, 63 | sylib 217 |
. 2
β’ (π β βπ₯(1st β π)(βπ‘βπ½)π₯) |
65 | | 1nn 12165 |
. . . . . 6
β’ 1 β
β |
66 | 7, 1, 8, 9, 10, 11, 6, 12, 13 | bcthlem3 24693 |
. . . . . 6
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ 1 β β) β π₯ β ((ballβπ·)β(πβ1))) |
67 | 65, 66 | mp3an3 1451 |
. . . . 5
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯) β π₯ β ((ballβπ·)β(πβ1))) |
68 | 12 | fveq2d 6847 |
. . . . . . 7
β’ (π β ((ballβπ·)β(πβ1)) = ((ballβπ·)ββ¨πΆ, π
β©)) |
69 | | df-ov 7361 |
. . . . . . 7
β’ (πΆ(ballβπ·)π
) = ((ballβπ·)ββ¨πΆ, π
β©) |
70 | 68, 69 | eqtr4di 2795 |
. . . . . 6
β’ (π β ((ballβπ·)β(πβ1)) = (πΆ(ballβπ·)π
)) |
71 | 70 | adantr 482 |
. . . . 5
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯) β ((ballβπ·)β(πβ1)) = (πΆ(ballβπ·)π
)) |
72 | 67, 71 | eleqtrd 2840 |
. . . 4
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯) β π₯ β (πΆ(ballβπ·)π
)) |
73 | 7 | mopntop 23796 |
. . . . . . . . . . . . . 14
β’ (π· β (βMetβπ) β π½ β Top) |
74 | 5, 73 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β π½ β Top) |
75 | 74 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β π½ β Top) |
76 | 5 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β π· β (βMetβπ)) |
77 | | xp1st 7954 |
. . . . . . . . . . . . . . 15
β’ ((πβ(π + 1)) β (π Γ β+) β
(1st β(πβ(π + 1))) β π) |
78 | 35, 77 | syl 17 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (1st
β(πβ(π + 1))) β π) |
79 | 37 | rpxrd 12959 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β (2nd
β(πβ(π + 1))) β
β*) |
80 | | blssm 23774 |
. . . . . . . . . . . . . 14
β’ ((π· β (βMetβπ) β§ (1st
β(πβ(π + 1))) β π β§ (2nd β(πβ(π + 1))) β β*) β
((1st β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) β π) |
81 | 76, 78, 79, 80 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((1st
β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) β π) |
82 | | df-ov 7361 |
. . . . . . . . . . . . . 14
β’
((1st β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) = ((ballβπ·)ββ¨(1st β(πβ(π + 1))), (2nd β(πβ(π + 1)))β©) |
83 | | 1st2nd2 7961 |
. . . . . . . . . . . . . . . 16
β’ ((πβ(π + 1)) β (π Γ β+) β (πβ(π + 1)) = β¨(1st β(πβ(π + 1))), (2nd β(πβ(π + 1)))β©) |
84 | 35, 83 | syl 17 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β β) β (πβ(π + 1)) = β¨(1st β(πβ(π + 1))), (2nd β(πβ(π + 1)))β©) |
85 | 84 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β β) β ((ballβπ·)β(πβ(π + 1))) = ((ballβπ·)ββ¨(1st β(πβ(π + 1))), (2nd β(πβ(π + 1)))β©)) |
86 | 82, 85 | eqtr4id 2796 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β ((1st
β(πβ(π + 1)))(ballβπ·)(2nd β(πβ(π + 1)))) = ((ballβπ·)β(πβ(π + 1)))) |
87 | 7 | mopnuni 23797 |
. . . . . . . . . . . . . . 15
β’ (π· β (βMetβπ) β π = βͺ π½) |
88 | 5, 87 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π = βͺ π½) |
89 | 88 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ π β β) β π = βͺ π½) |
90 | 81, 86, 89 | 3sstr3d 3991 |
. . . . . . . . . . . 12
β’ ((π β§ π β β) β ((ballβπ·)β(πβ(π + 1))) β βͺ
π½) |
91 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ βͺ π½ =
βͺ π½ |
92 | 91 | sscls 22410 |
. . . . . . . . . . . 12
β’ ((π½ β Top β§
((ballβπ·)β(πβ(π + 1))) β βͺ
π½) β
((ballβπ·)β(πβ(π + 1))) β ((clsβπ½)β((ballβπ·)β(πβ(π + 1))))) |
93 | 75, 90, 92 | syl2anc 585 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((ballβπ·)β(πβ(π + 1))) β ((clsβπ½)β((ballβπ·)β(πβ(π + 1))))) |
94 | 32 | simp3d 1145 |
. . . . . . . . . . 11
β’ ((π β§ π β β) β ((clsβπ½)β((ballβπ·)β(πβ(π + 1)))) β (((ballβπ·)β(πβπ)) β (πβπ))) |
95 | 93, 94 | sstrd 3955 |
. . . . . . . . . 10
β’ ((π β§ π β β) β ((ballβπ·)β(πβ(π + 1))) β (((ballβπ·)β(πβπ)) β (πβπ))) |
96 | 95 | 3adant2 1132 |
. . . . . . . . 9
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ π β β) β ((ballβπ·)β(πβ(π + 1))) β (((ballβπ·)β(πβπ)) β (πβπ))) |
97 | 7, 1, 8, 9, 10, 11, 6, 12, 13 | bcthlem3 24693 |
. . . . . . . . . 10
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ (π + 1) β β) β π₯ β ((ballβπ·)β(πβ(π + 1)))) |
98 | 19, 97 | syl3an3 1166 |
. . . . . . . . 9
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ π β β) β π₯ β ((ballβπ·)β(πβ(π + 1)))) |
99 | 96, 98 | sseldd 3946 |
. . . . . . . 8
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ π β β) β π₯ β (((ballβπ·)β(πβπ)) β (πβπ))) |
100 | 99 | eldifbd 3924 |
. . . . . . 7
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯ β§ π β β) β Β¬ π₯ β (πβπ)) |
101 | 100 | 3expa 1119 |
. . . . . 6
β’ (((π β§ (1st β
π)(βπ‘βπ½)π₯) β§ π β β) β Β¬ π₯ β (πβπ)) |
102 | 101 | ralrimiva 3144 |
. . . . 5
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯) β βπ β β Β¬ π₯ β (πβπ)) |
103 | | eluni2 4870 |
. . . . . . . . 9
β’ (π₯ β βͺ ran π β βπ¦ β ran π π₯ β π¦) |
104 | 9 | ffnd 6670 |
. . . . . . . . . 10
β’ (π β π Fn β) |
105 | | eleq2 2827 |
. . . . . . . . . . 11
β’ (π¦ = (πβπ) β (π₯ β π¦ β π₯ β (πβπ))) |
106 | 105 | rexrn 7038 |
. . . . . . . . . 10
β’ (π Fn β β (βπ¦ β ran π π₯ β π¦ β βπ β β π₯ β (πβπ))) |
107 | 104, 106 | syl 17 |
. . . . . . . . 9
β’ (π β (βπ¦ β ran π π₯ β π¦ β βπ β β π₯ β (πβπ))) |
108 | 103, 107 | bitrid 283 |
. . . . . . . 8
β’ (π β (π₯ β βͺ ran
π β βπ β β π₯ β (πβπ))) |
109 | 108 | notbid 318 |
. . . . . . 7
β’ (π β (Β¬ π₯ β βͺ ran
π β Β¬ βπ β β π₯ β (πβπ))) |
110 | | ralnex 3076 |
. . . . . . 7
β’
(βπ β
β Β¬ π₯ β
(πβπ) β Β¬ βπ β β π₯ β (πβπ)) |
111 | 109, 110 | bitr4di 289 |
. . . . . 6
β’ (π β (Β¬ π₯ β βͺ ran
π β βπ β β Β¬ π₯ β (πβπ))) |
112 | 111 | biimpar 479 |
. . . . 5
β’ ((π β§ βπ β β Β¬ π₯ β (πβπ)) β Β¬ π₯ β βͺ ran
π) |
113 | 102, 112 | syldan 592 |
. . . 4
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯) β Β¬ π₯ β βͺ ran
π) |
114 | 72, 113 | eldifd 3922 |
. . 3
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯) β π₯ β ((πΆ(ballβπ·)π
) β βͺ ran
π)) |
115 | 114 | ne0d 4296 |
. 2
β’ ((π β§ (1st β
π)(βπ‘βπ½)π₯) β ((πΆ(ballβπ·)π
) β βͺ ran
π) β
β
) |
116 | 64, 115 | exlimddv 1939 |
1
β’ (π β ((πΆ(ballβπ·)π
) β βͺ ran
π) β
β
) |