Step | Hyp | Ref
| Expression |
1 | | lmcau.1 |
. . . . 5
β’ π½ = (MetOpenβπ·) |
2 | 1 | methaus 23899 |
. . . 4
β’ (π· β (βMetβπ) β π½ β Haus) |
3 | | lmfun 22755 |
. . . 4
β’ (π½ β Haus β Fun
(βπ‘βπ½)) |
4 | | funfvbrb 7005 |
. . . 4
β’ (Fun
(βπ‘βπ½) β (π β dom
(βπ‘βπ½) β π(βπ‘βπ½)((βπ‘βπ½)βπ))) |
5 | 2, 3, 4 | 3syl 18 |
. . 3
β’ (π· β (βMetβπ) β (π β dom
(βπ‘βπ½) β π(βπ‘βπ½)((βπ‘βπ½)βπ))) |
6 | | id 22 |
. . . . . . . 8
β’ (π· β (βMetβπ) β π· β (βMetβπ)) |
7 | 1, 6 | lmmbr 24645 |
. . . . . . 7
β’ (π· β (βMetβπ) β (π(βπ‘βπ½)((βπ‘βπ½)βπ) β (π β (π βpm β) β§
((βπ‘βπ½)βπ) β π β§ βπ¦ β β+ βπ’ β ran
β€β₯(π
βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)π¦)))) |
8 | 7 | biimpa 478 |
. . . . . 6
β’ ((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β (π β (π βpm β) β§
((βπ‘βπ½)βπ) β π β§ βπ¦ β β+ βπ’ β ran
β€β₯(π
βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)π¦))) |
9 | 8 | simp1d 1143 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β π β (π βpm
β)) |
10 | | simprr 772 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2))) |
11 | | simplll 774 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β π· β (βMetβπ)) |
12 | 8 | simp2d 1144 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β
((βπ‘βπ½)βπ) β π) |
13 | 12 | ad2antrr 725 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β
((βπ‘βπ½)βπ) β π) |
14 | | rpre 12931 |
. . . . . . . . . 10
β’ (π₯ β β+
β π₯ β
β) |
15 | 14 | ad2antlr 726 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β π₯ β β) |
16 | | uzid 12786 |
. . . . . . . . . . . 12
β’ (π β β€ β π β
(β€β₯βπ)) |
17 | 16 | ad2antrl 727 |
. . . . . . . . . . 11
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β π β (β€β₯βπ)) |
18 | 17 | fvresd 6866 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β ((π βΎ (β€β₯βπ))βπ) = (πβπ)) |
19 | 10, 17 | ffvelcdmd 7040 |
. . . . . . . . . 10
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β ((π βΎ (β€β₯βπ))βπ) β (((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2))) |
20 | 18, 19 | eqeltrrd 2835 |
. . . . . . . . 9
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β (πβπ) β (((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2))) |
21 | | blhalf 23781 |
. . . . . . . . 9
β’ (((π· β (βMetβπ) β§
((βπ‘βπ½)βπ) β π) β§ (π₯ β β β§ (πβπ) β
(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β
(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)) β ((πβπ)(ballβπ·)π₯)) |
22 | 11, 13, 15, 20, 21 | syl22anc 838 |
. . . . . . . 8
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β
(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)) β ((πβπ)(ballβπ·)π₯)) |
23 | 10, 22 | fssd 6690 |
. . . . . . 7
β’ ((((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β§ (π β β€ β§ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) β (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)) |
24 | | rphalfcl 12950 |
. . . . . . . . . 10
β’ (π₯ β β+
β (π₯ / 2) β
β+) |
25 | 8 | simp3d 1145 |
. . . . . . . . . 10
β’ ((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β βπ¦ β β+ βπ’ β ran
β€β₯(π
βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)π¦)) |
26 | | oveq2 7369 |
. . . . . . . . . . . . 13
β’ (π¦ = (π₯ / 2) β
(((βπ‘βπ½)βπ)(ballβπ·)π¦) =
(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2))) |
27 | 26 | feq3d 6659 |
. . . . . . . . . . . 12
β’ (π¦ = (π₯ / 2) β ((π βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)π¦) β (π βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) |
28 | 27 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π¦ = (π₯ / 2) β (βπ’ β ran β€β₯(π βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)π¦) β βπ’ β ran β€β₯(π βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) |
29 | 28 | rspcv 3579 |
. . . . . . . . . 10
β’ ((π₯ / 2) β β+
β (βπ¦ β
β+ βπ’ β ran β€β₯(π βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)π¦) β βπ’ β ran β€β₯(π βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) |
30 | 24, 25, 29 | syl2im 40 |
. . . . . . . . 9
β’ (π₯ β β+
β ((π· β
(βMetβπ) β§
π(βπ‘βπ½)((βπ‘βπ½)βπ)) β βπ’ β ran β€β₯(π βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) |
31 | 30 | impcom 409 |
. . . . . . . 8
β’ (((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β
βπ’ β ran
β€β₯(π
βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2))) |
32 | | uzf 12774 |
. . . . . . . . 9
β’
β€β₯:β€βΆπ« β€ |
33 | | ffn 6672 |
. . . . . . . . 9
β’
(β€β₯:β€βΆπ« β€ β
β€β₯ Fn β€) |
34 | | reseq2 5936 |
. . . . . . . . . . 11
β’ (π’ =
(β€β₯βπ) β (π βΎ π’) = (π βΎ (β€β₯βπ))) |
35 | | id 22 |
. . . . . . . . . . 11
β’ (π’ =
(β€β₯βπ) β π’ = (β€β₯βπ)) |
36 | 34, 35 | feq12d 6660 |
. . . . . . . . . 10
β’ (π’ =
(β€β₯βπ) β ((π βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)) β (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) |
37 | 36 | rexrn 7041 |
. . . . . . . . 9
β’
(β€β₯ Fn β€ β (βπ’ β ran β€β₯(π βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)) β βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)))) |
38 | 32, 33, 37 | mp2b 10 |
. . . . . . . 8
β’
(βπ’ β ran
β€β₯(π
βΎ π’):π’βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2)) β βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2))) |
39 | 31, 38 | sylib 217 |
. . . . . . 7
β’ (((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β
βπ β β€
(π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ(((βπ‘βπ½)βπ)(ballβπ·)(π₯ / 2))) |
40 | 23, 39 | reximddv 3165 |
. . . . . 6
β’ (((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β§ π₯ β β+) β
βπ β β€
(π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)) |
41 | 40 | ralrimiva 3140 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β βπ₯ β β+ βπ β β€ (π βΎ
(β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)) |
42 | | iscau 24663 |
. . . . . 6
β’ (π· β (βMetβπ) β (π β (Cauβπ·) β (π β (π βpm β) β§
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)))) |
43 | 42 | adantr 482 |
. . . . 5
β’ ((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β (π β (Cauβπ·) β (π β (π βpm β) β§
βπ₯ β
β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)))) |
44 | 9, 41, 43 | mpbir2and 712 |
. . . 4
β’ ((π· β (βMetβπ) β§ π(βπ‘βπ½)((βπ‘βπ½)βπ)) β π β (Cauβπ·)) |
45 | 44 | ex 414 |
. . 3
β’ (π· β (βMetβπ) β (π(βπ‘βπ½)((βπ‘βπ½)βπ) β π β (Cauβπ·))) |
46 | 5, 45 | sylbid 239 |
. 2
β’ (π· β (βMetβπ) β (π β dom
(βπ‘βπ½) β π β (Cauβπ·))) |
47 | 46 | ssrdv 3954 |
1
β’ (π· β (βMetβπ) β dom
(βπ‘βπ½) β (Cauβπ·)) |