Description: Lemma for metdscn . (Contributed by Mario Carneiro, 4-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | metdscn.f | |
|
metdscn.j | |
||
metdscn.c | |
||
metdscn.k | |
||
metdscnlem.1 | |
||
metdscnlem.2 | |
||
metdscnlem.3 | |
||
metdscnlem.4 | |
||
metdscnlem.5 | |
||
metdscnlem.6 | |
||
Assertion | metdscnlem | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | metdscn.f | |
|
2 | metdscn.j | |
|
3 | metdscn.c | |
|
4 | metdscn.k | |
|
5 | metdscnlem.1 | |
|
6 | metdscnlem.2 | |
|
7 | metdscnlem.3 | |
|
8 | metdscnlem.4 | |
|
9 | metdscnlem.5 | |
|
10 | metdscnlem.6 | |
|
11 | 1 | metdsf | |
12 | 5 6 11 | syl2anc | |
13 | 12 7 | ffvelrnd | |
14 | eliccxr | |
|
15 | 13 14 | syl | |
16 | 12 8 | ffvelrnd | |
17 | eliccxr | |
|
18 | 16 17 | syl | |
19 | 18 | xnegcld | |
20 | 15 19 | xaddcld | |
21 | xmetcl | |
|
22 | 5 7 8 21 | syl3anc | |
23 | 9 | rpxrd | |
24 | 1 | metdstri | |
25 | 5 6 7 8 24 | syl22anc | |
26 | elxrge0 | |
|
27 | 26 | simprbi | |
28 | 13 27 | syl | |
29 | elxrge0 | |
|
30 | 29 | simprbi | |
31 | 16 30 | syl | |
32 | ge0nemnf | |
|
33 | 18 31 32 | syl2anc | |
34 | xmetge0 | |
|
35 | 5 7 8 34 | syl3anc | |
36 | xlesubadd | |
|
37 | 15 18 22 28 33 35 36 | syl33anc | |
38 | 25 37 | mpbird | |
39 | 20 22 23 38 10 | xrlelttrd | |