Step | Hyp | Ref
| Expression |
1 | | iscmet3.5 |
. . 3
β’ (π β πΉ β dom
(βπ‘βπ½)) |
2 | | eldmg 5899 |
. . . 4
β’ (πΉ β dom
(βπ‘βπ½) β (πΉ β dom
(βπ‘βπ½) β βπ₯ πΉ(βπ‘βπ½)π₯)) |
3 | 2 | ibi 267 |
. . 3
β’ (πΉ β dom
(βπ‘βπ½) β βπ₯ πΉ(βπ‘βπ½)π₯) |
4 | 1, 3 | syl 17 |
. 2
β’ (π β βπ₯ πΉ(βπ‘βπ½)π₯) |
5 | | iscmet3.4 |
. . . . . . 7
β’ (π β π· β (Metβπ)) |
6 | | metxmet 23840 |
. . . . . . 7
β’ (π· β (Metβπ) β π· β (βMetβπ)) |
7 | 5, 6 | syl 17 |
. . . . . 6
β’ (π β π· β (βMetβπ)) |
8 | | iscmet3.2 |
. . . . . . 7
β’ π½ = (MetOpenβπ·) |
9 | 8 | mopntopon 23945 |
. . . . . 6
β’ (π· β (βMetβπ) β π½ β (TopOnβπ)) |
10 | 7, 9 | syl 17 |
. . . . 5
β’ (π β π½ β (TopOnβπ)) |
11 | | lmcl 22801 |
. . . . 5
β’ ((π½ β (TopOnβπ) β§ πΉ(βπ‘βπ½)π₯) β π₯ β π) |
12 | 10, 11 | sylan 581 |
. . . 4
β’ ((π β§ πΉ(βπ‘βπ½)π₯) β π₯ β π) |
13 | 7 | adantr 482 |
. . . . . . 7
β’ ((π β§ πΉ(βπ‘βπ½)π₯) β π· β (βMetβπ)) |
14 | 8 | mopni2 24002 |
. . . . . . . 8
β’ ((π· β (βMetβπ) β§ π¦ β π½ β§ π₯ β π¦) β βπ β β+ (π₯(ballβπ·)π) β π¦) |
15 | 14 | 3expia 1122 |
. . . . . . 7
β’ ((π· β (βMetβπ) β§ π¦ β π½) β (π₯ β π¦ β βπ β β+ (π₯(ballβπ·)π) β π¦)) |
16 | 13, 15 | sylan 581 |
. . . . . 6
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π¦ β π½) β (π₯ β π¦ β βπ β β+ (π₯(ballβπ·)π) β π¦)) |
17 | | iscmet3.7 |
. . . . . . . . 9
β’ (π β πΊ β (Filβπ)) |
18 | 17 | ad3antrrr 729 |
. . . . . . . 8
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π¦ β π½) β§ (π β β+ β§ (π₯(ballβπ·)π) β π¦)) β πΊ β (Filβπ)) |
19 | | iscmet3.3 |
. . . . . . . . . . . 12
β’ (π β π β β€) |
20 | 19 | ad2antrr 725 |
. . . . . . . . . . 11
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β π β
β€) |
21 | | rphalfcl 13001 |
. . . . . . . . . . . 12
β’ (π β β+
β (π / 2) β
β+) |
22 | 21 | adantl 483 |
. . . . . . . . . . 11
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β (π / 2) β
β+) |
23 | | iscmet3.1 |
. . . . . . . . . . . 12
β’ π =
(β€β₯βπ) |
24 | 23 | iscmet3lem3 24807 |
. . . . . . . . . . 11
β’ ((π β β€ β§ (π / 2) β
β+) β βπ β π βπ β (β€β₯βπ)((1 / 2)βπ) < (π / 2)) |
25 | 20, 22, 24 | syl2anc 585 |
. . . . . . . . . 10
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β
βπ β π βπ β (β€β₯βπ)((1 / 2)βπ) < (π / 2)) |
26 | 13 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β π· β (βMetβπ)) |
27 | 12 | adantr 482 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β π₯ β π) |
28 | | blcntr 23919 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π₯ β π β§ (π / 2) β β+) β
π₯ β (π₯(ballβπ·)(π / 2))) |
29 | 26, 27, 22, 28 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β π₯ β (π₯(ballβπ·)(π / 2))) |
30 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β πΉ(βπ‘βπ½)π₯) |
31 | 22 | rpxrd 13017 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β (π / 2) β
β*) |
32 | 8 | blopn 24009 |
. . . . . . . . . . . 12
β’ ((π· β (βMetβπ) β§ π₯ β π β§ (π / 2) β β*) β
(π₯(ballβπ·)(π / 2)) β π½) |
33 | 26, 27, 31, 32 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β (π₯(ballβπ·)(π / 2)) β π½) |
34 | 23, 29, 20, 30, 33 | lmcvg 22766 |
. . . . . . . . . 10
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β
βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π₯(ballβπ·)(π / 2))) |
35 | 23 | rexanuz2 15296 |
. . . . . . . . . . 11
β’
(βπ β
π βπ β
(β€β₯βπ)(((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))) β (βπ β π βπ β (β€β₯βπ)((1 / 2)βπ) < (π / 2) β§ βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π₯(ballβπ·)(π / 2)))) |
36 | 23 | r19.2uz 15298 |
. . . . . . . . . . . 12
β’
(βπ β
π βπ β
(β€β₯βπ)(((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))) β βπ β π (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2)))) |
37 | 17 | ad3antrrr 729 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ (π β π β§ (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))))) β πΊ β (Filβπ)) |
38 | | iscmet3.8 |
. . . . . . . . . . . . . . . 16
β’ (π β π:β€βΆπΊ) |
39 | 38 | ad3antrrr 729 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ (π β π β§ (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))))) β π:β€βΆπΊ) |
40 | | eluzelz 12832 |
. . . . . . . . . . . . . . . . 17
β’ (π β
(β€β₯βπ) β π β β€) |
41 | 40, 23 | eleq2s 2852 |
. . . . . . . . . . . . . . . 16
β’ (π β π β π β β€) |
42 | 41 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ (π β π β§ (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))))) β π β β€) |
43 | | ffvelcdm 7084 |
. . . . . . . . . . . . . . 15
β’ ((π:β€βΆπΊ β§ π β β€) β (πβπ) β πΊ) |
44 | 39, 42, 43 | syl2anc 585 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ (π β π β§ (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))))) β (πβπ) β πΊ) |
45 | | rpxr 12983 |
. . . . . . . . . . . . . . . . 17
β’ (π β β+
β π β
β*) |
46 | 45 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β π β
β*) |
47 | | blssm 23924 |
. . . . . . . . . . . . . . . 16
β’ ((π· β (βMetβπ) β§ π₯ β π β§ π β β*) β (π₯(ballβπ·)π) β π) |
48 | 26, 27, 46, 47 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β (π₯(ballβπ·)π) β π) |
49 | 48 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ (π β π β§ (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))))) β (π₯(ballβπ·)π) β π) |
50 | 41 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β π β β€) |
51 | | 1rp 12978 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ 1 β
β+ |
52 | | rphalfcl 13001 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (1 β
β+ β (1 / 2) β β+) |
53 | 51, 52 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (1 / 2)
β β+ |
54 | | rpexpcl 14046 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((1 / 2)
β β+ β§ π β β€) β ((1 / 2)βπ) β
β+) |
55 | 53, 54 | mpan 689 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (π β β€ β ((1 /
2)βπ) β
β+) |
56 | 50, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β ((1 / 2)βπ) β
β+) |
57 | 56 | rpred 13016 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β ((1 / 2)βπ) β β) |
58 | 22 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (π / 2) β
β+) |
59 | 58 | rpred 13016 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (π / 2) β β) |
60 | | ltle 11302 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((1 /
2)βπ) β β
β§ (π / 2) β
β) β (((1 / 2)βπ) < (π / 2) β ((1 / 2)βπ) β€ (π / 2))) |
61 | 57, 59, 60 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (((1 / 2)βπ) < (π / 2) β ((1 / 2)βπ) β€ (π / 2))) |
62 | | fveq2 6892 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π = π β (πβπ) = (πβπ)) |
63 | 62 | eleq2d 2820 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π = π β ((πΉβπ) β (πβπ) β (πΉβπ) β (πβπ))) |
64 | | iscmet3.10 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β βπ β π βπ β (π...π)(πΉβπ) β (πβπ)) |
65 | 64 | r19.21bi 3249 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β π) β βπ β (π...π)(πΉβπ) β (πβπ)) |
66 | | eluzfz2 13509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
β’ (π β
(β€β₯βπ) β π β (π...π)) |
67 | 66, 23 | eleq2s 2852 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
β’ (π β π β π β (π...π)) |
68 | 67 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β π) β π β (π...π)) |
69 | 63, 65, 68 | rspcdva 3614 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β π) β (πΉβπ) β (πβπ)) |
70 | 69 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β (πΉβπ) β (πβπ)) |
71 | | simpr 486 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β π¦ β (πβπ)) |
72 | | iscmet3.9 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β βπ β β€ βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) |
73 | 72 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β βπ β β€ βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) |
74 | 41 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β π β β€) |
75 | | rsp 3245 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’
(βπ β
β€ βπ’ β
(πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ) β (π β β€ β βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ))) |
76 | 73, 74, 75 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) |
77 | | oveq1 7416 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π’ = (πΉβπ) β (π’π·π£) = ((πΉβπ)π·π£)) |
78 | 77 | breq1d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π’ = (πΉβπ) β ((π’π·π£) < ((1 / 2)βπ) β ((πΉβπ)π·π£) < ((1 / 2)βπ))) |
79 | | oveq2 7417 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π£ = π¦ β ((πΉβπ)π·π£) = ((πΉβπ)π·π¦)) |
80 | 79 | breq1d 5159 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π£ = π¦ β (((πΉβπ)π·π£) < ((1 / 2)βπ) β ((πΉβπ)π·π¦) < ((1 / 2)βπ))) |
81 | 78, 80 | rspc2va 3624 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ ((((πΉβπ) β (πβπ) β§ π¦ β (πβπ)) β§ βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) β ((πΉβπ)π·π¦) < ((1 / 2)βπ)) |
82 | 70, 71, 76, 81 | syl21anc 837 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β ((πΉβπ)π·π¦) < ((1 / 2)βπ)) |
83 | 7 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β π· β (βMetβπ)) |
84 | 41, 55 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β π β ((1 / 2)βπ) β
β+) |
85 | 84 | rpxrd 13017 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ (π β π β ((1 / 2)βπ) β
β*) |
86 | 85 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β ((1 / 2)βπ) β
β*) |
87 | | iscmet3.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ (π β πΉ:πβΆπ) |
88 | 87 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β π) β (πΉβπ) β π) |
89 | 88 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β (πΉβπ) β π) |
90 | 17 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β π) β πΊ β (Filβπ)) |
91 | 38, 41, 43 | syl2an 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((π β§ π β π) β (πβπ) β πΊ) |
92 | | filelss 23356 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
β’ ((πΊ β (Filβπ) β§ (πβπ) β πΊ) β (πβπ) β π) |
93 | 90, 91, 92 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
β’ ((π β§ π β π) β (πβπ) β π) |
94 | 93 | sselda 3983 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β π¦ β π) |
95 | | elbl2 23896 |
. . . . . . . . . . . . . . . . . . . . . . . 24
β’ (((π· β (βMetβπ) β§ ((1 / 2)βπ) β β*)
β§ ((πΉβπ) β π β§ π¦ β π)) β (π¦ β ((πΉβπ)(ballβπ·)((1 / 2)βπ)) β ((πΉβπ)π·π¦) < ((1 / 2)βπ))) |
96 | 83, 86, 89, 94, 95 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . . . . . 23
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β (π¦ β ((πΉβπ)(ballβπ·)((1 / 2)βπ)) β ((πΉβπ)π·π¦) < ((1 / 2)βπ))) |
97 | 82, 96 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ (((π β§ π β π) β§ π¦ β (πβπ)) β π¦ β ((πΉβπ)(ballβπ·)((1 / 2)βπ))) |
98 | 97 | ex 414 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π β§ π β π) β (π¦ β (πβπ) β π¦ β ((πΉβπ)(ballβπ·)((1 / 2)βπ)))) |
99 | 98 | ssrdv 3989 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β§ π β π) β (πβπ) β ((πΉβπ)(ballβπ·)((1 / 2)βπ))) |
100 | 99 | ad4ant14 751 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (πβπ) β ((πΉβπ)(ballβπ·)((1 / 2)βπ))) |
101 | 26 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β π· β (βMetβπ)) |
102 | 87 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β πΉ:πβΆπ) |
103 | 102 | ffvelcdmda 7087 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (πΉβπ) β π) |
104 | 56 | rpxrd 13017 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β ((1 / 2)βπ) β
β*) |
105 | 31 | adantr 482 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (π / 2) β
β*) |
106 | | ssbl 23929 |
. . . . . . . . . . . . . . . . . . . . 21
β’ (((π· β (βMetβπ) β§ (πΉβπ) β π) β§ (((1 / 2)βπ) β β* β§ (π / 2) β
β*) β§ ((1 / 2)βπ) β€ (π / 2)) β ((πΉβπ)(ballβπ·)((1 / 2)βπ)) β ((πΉβπ)(ballβπ·)(π / 2))) |
107 | 106 | 3expia 1122 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π· β (βMetβπ) β§ (πΉβπ) β π) β§ (((1 / 2)βπ) β β* β§ (π / 2) β
β*)) β (((1 / 2)βπ) β€ (π / 2) β ((πΉβπ)(ballβπ·)((1 / 2)βπ)) β ((πΉβπ)(ballβπ·)(π / 2)))) |
108 | 101, 103,
104, 105, 107 | syl22anc 838 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (((1 / 2)βπ) β€ (π / 2) β ((πΉβπ)(ballβπ·)((1 / 2)βπ)) β ((πΉβπ)(ballβπ·)(π / 2)))) |
109 | | sstr 3991 |
. . . . . . . . . . . . . . . . . . 19
β’ (((πβπ) β ((πΉβπ)(ballβπ·)((1 / 2)βπ)) β§ ((πΉβπ)(ballβπ·)((1 / 2)βπ)) β ((πΉβπ)(ballβπ·)(π / 2))) β (πβπ) β ((πΉβπ)(ballβπ·)(π / 2))) |
110 | 100, 108,
109 | syl6an 683 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (((1 / 2)βπ) β€ (π / 2) β (πβπ) β ((πΉβπ)(ballβπ·)(π / 2)))) |
111 | 61, 110 | syld 47 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (((1 / 2)βπ) < (π / 2) β (πβπ) β ((πΉβπ)(ballβπ·)(π / 2)))) |
112 | 111 | adantrd 493 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β ((((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))) β (πβπ) β ((πΉβπ)(ballβπ·)(π / 2)))) |
113 | 112 | impr 456 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ (π β π β§ (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))))) β (πβπ) β ((πΉβπ)(ballβπ·)(π / 2))) |
114 | 27 | adantr 482 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β π₯ β π) |
115 | | blcom 23900 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π· β (βMetβπ) β§ (π / 2) β β*) β§
(π₯ β π β§ (πΉβπ) β π)) β ((πΉβπ) β (π₯(ballβπ·)(π / 2)) β π₯ β ((πΉβπ)(ballβπ·)(π / 2)))) |
116 | 101, 105,
114, 103, 115 | syl22anc 838 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β ((πΉβπ) β (π₯(ballβπ·)(π / 2)) β π₯ β ((πΉβπ)(ballβπ·)(π / 2)))) |
117 | | rpre 12982 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β β+
β π β
β) |
118 | 117 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . 19
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β π β β) |
119 | | blhalf 23911 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π· β (βMetβπ) β§ (πΉβπ) β π) β§ (π β β β§ π₯ β ((πΉβπ)(ballβπ·)(π / 2)))) β ((πΉβπ)(ballβπ·)(π / 2)) β (π₯(ballβπ·)π)) |
120 | 119 | expr 458 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π· β (βMetβπ) β§ (πΉβπ) β π) β§ π β β) β (π₯ β ((πΉβπ)(ballβπ·)(π / 2)) β ((πΉβπ)(ballβπ·)(π / 2)) β (π₯(ballβπ·)π))) |
121 | 101, 103,
118, 120 | syl21anc 837 |
. . . . . . . . . . . . . . . . . 18
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β (π₯ β ((πΉβπ)(ballβπ·)(π / 2)) β ((πΉβπ)(ballβπ·)(π / 2)) β (π₯(ballβπ·)π))) |
122 | 116, 121 | sylbid 239 |
. . . . . . . . . . . . . . . . 17
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β ((πΉβπ) β (π₯(ballβπ·)(π / 2)) β ((πΉβπ)(ballβπ·)(π / 2)) β (π₯(ballβπ·)π))) |
123 | 122 | adantld 492 |
. . . . . . . . . . . . . . . 16
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ π β π) β ((((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))) β ((πΉβπ)(ballβπ·)(π / 2)) β (π₯(ballβπ·)π))) |
124 | 123 | impr 456 |
. . . . . . . . . . . . . . 15
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ (π β π β§ (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))))) β ((πΉβπ)(ballβπ·)(π / 2)) β (π₯(ballβπ·)π)) |
125 | 113, 124 | sstrd 3993 |
. . . . . . . . . . . . . 14
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ (π β π β§ (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))))) β (πβπ) β (π₯(ballβπ·)π)) |
126 | | filss 23357 |
. . . . . . . . . . . . . 14
β’ ((πΊ β (Filβπ) β§ ((πβπ) β πΊ β§ (π₯(ballβπ·)π) β π β§ (πβπ) β (π₯(ballβπ·)π))) β (π₯(ballβπ·)π) β πΊ) |
127 | 37, 44, 49, 125, 126 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β§ (π β π β§ (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))))) β (π₯(ballβπ·)π) β πΊ) |
128 | 127 | rexlimdvaa 3157 |
. . . . . . . . . . . 12
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β
(βπ β π (((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))) β (π₯(ballβπ·)π) β πΊ)) |
129 | 36, 128 | syl5 34 |
. . . . . . . . . . 11
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β
(βπ β π βπ β (β€β₯βπ)(((1 / 2)βπ) < (π / 2) β§ (πΉβπ) β (π₯(ballβπ·)(π / 2))) β (π₯(ballβπ·)π) β πΊ)) |
130 | 35, 129 | biimtrrid 242 |
. . . . . . . . . 10
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β
((βπ β π βπ β (β€β₯βπ)((1 / 2)βπ) < (π / 2) β§ βπ β π βπ β (β€β₯βπ)(πΉβπ) β (π₯(ballβπ·)(π / 2))) β (π₯(ballβπ·)π) β πΊ)) |
131 | 25, 34, 130 | mp2and 698 |
. . . . . . . . 9
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π β β+) β (π₯(ballβπ·)π) β πΊ) |
132 | 131 | ad2ant2r 746 |
. . . . . . . 8
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π¦ β π½) β§ (π β β+ β§ (π₯(ballβπ·)π) β π¦)) β (π₯(ballβπ·)π) β πΊ) |
133 | 10 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ πΉ(βπ‘βπ½)π₯) β π½ β (TopOnβπ)) |
134 | | toponss 22429 |
. . . . . . . . . 10
β’ ((π½ β (TopOnβπ) β§ π¦ β π½) β π¦ β π) |
135 | 133, 134 | sylan 581 |
. . . . . . . . 9
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π¦ β π½) β π¦ β π) |
136 | 135 | adantr 482 |
. . . . . . . 8
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π¦ β π½) β§ (π β β+ β§ (π₯(ballβπ·)π) β π¦)) β π¦ β π) |
137 | | simprr 772 |
. . . . . . . 8
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π¦ β π½) β§ (π β β+ β§ (π₯(ballβπ·)π) β π¦)) β (π₯(ballβπ·)π) β π¦) |
138 | | filss 23357 |
. . . . . . . 8
β’ ((πΊ β (Filβπ) β§ ((π₯(ballβπ·)π) β πΊ β§ π¦ β π β§ (π₯(ballβπ·)π) β π¦)) β π¦ β πΊ) |
139 | 18, 132, 136, 137, 138 | syl13anc 1373 |
. . . . . . 7
β’ ((((π β§ πΉ(βπ‘βπ½)π₯) β§ π¦ β π½) β§ (π β β+ β§ (π₯(ballβπ·)π) β π¦)) β π¦ β πΊ) |
140 | 139 | rexlimdvaa 3157 |
. . . . . 6
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π¦ β π½) β (βπ β β+ (π₯(ballβπ·)π) β π¦ β π¦ β πΊ)) |
141 | 16, 140 | syld 47 |
. . . . 5
β’ (((π β§ πΉ(βπ‘βπ½)π₯) β§ π¦ β π½) β (π₯ β π¦ β π¦ β πΊ)) |
142 | 141 | ralrimiva 3147 |
. . . 4
β’ ((π β§ πΉ(βπ‘βπ½)π₯) β βπ¦ β π½ (π₯ β π¦ β π¦ β πΊ)) |
143 | | flimopn 23479 |
. . . . . 6
β’ ((π½ β (TopOnβπ) β§ πΊ β (Filβπ)) β (π₯ β (π½ fLim πΊ) β (π₯ β π β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΊ)))) |
144 | 10, 17, 143 | syl2anc 585 |
. . . . 5
β’ (π β (π₯ β (π½ fLim πΊ) β (π₯ β π β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΊ)))) |
145 | 144 | adantr 482 |
. . . 4
β’ ((π β§ πΉ(βπ‘βπ½)π₯) β (π₯ β (π½ fLim πΊ) β (π₯ β π β§ βπ¦ β π½ (π₯ β π¦ β π¦ β πΊ)))) |
146 | 12, 142, 145 | mpbir2and 712 |
. . 3
β’ ((π β§ πΉ(βπ‘βπ½)π₯) β π₯ β (π½ fLim πΊ)) |
147 | 146 | ne0d 4336 |
. 2
β’ ((π β§ πΉ(βπ‘βπ½)π₯) β (π½ fLim πΊ) β β
) |
148 | 4, 147 | exlimddv 1939 |
1
β’ (π β (π½ fLim πΊ) β β
) |