Description: The standard bounded metric is a proper metric given an extended metric and a positive real cutoff. (Contributed by Mario Carneiro, 26-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | stdbdmet.1 | |
|
Assertion | stdbdmet | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | stdbdmet.1 | |
|
2 | rpxr | |
|
3 | rpgt0 | |
|
4 | 2 3 | jca | |
5 | 1 | stdbdxmet | |
6 | 5 | 3expb | |
7 | 4 6 | sylan2 | |
8 | xmetcl | |
|
9 | 8 | 3expb | |
10 | 9 | adantlr | |
11 | 2 | ad2antlr | |
12 | 10 11 | ifcld | |
13 | rpre | |
|
14 | 13 | ad2antlr | |
15 | xmetge0 | |
|
16 | 15 | 3expb | |
17 | 16 | adantlr | |
18 | rpge0 | |
|
19 | 18 | ad2antlr | |
20 | breq2 | |
|
21 | breq2 | |
|
22 | 20 21 | ifboth | |
23 | 17 19 22 | syl2anc | |
24 | xrmin2 | |
|
25 | 10 11 24 | syl2anc | |
26 | xrrege0 | |
|
27 | 12 14 23 25 26 | syl22anc | |
28 | 27 | ralrimivva | |
29 | 1 | fmpo | |
30 | 28 29 | sylib | |
31 | ismet2 | |
|
32 | 7 30 31 | sylanbrc | |