Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 4-Sep-2015)
Ref | Expression | ||
---|---|---|---|
Hypotheses | metdscn.f | |
|
metdscn.j | |
||
metnrmlem.1 | |
||
metnrmlem.2 | |
||
metnrmlem.3 | |
||
metnrmlem.4 | |
||
Assertion | metnrmlem1a | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | metdscn.f | |
|
2 | metdscn.j | |
|
3 | metnrmlem.1 | |
|
4 | metnrmlem.2 | |
|
5 | metnrmlem.3 | |
|
6 | metnrmlem.4 | |
|
7 | 6 | adantr | |
8 | inelcm | |
|
9 | 8 | expcom | |
10 | 9 | adantl | |
11 | 10 | necon2bd | |
12 | 7 11 | mpd | |
13 | eqcom | |
|
14 | 3 | adantr | |
15 | 4 | adantr | |
16 | eqid | |
|
17 | 16 | cldss | |
18 | 15 17 | syl | |
19 | 2 | mopnuni | |
20 | 14 19 | syl | |
21 | 18 20 | sseqtrrd | |
22 | 5 | adantr | |
23 | 16 | cldss | |
24 | 22 23 | syl | |
25 | 24 20 | sseqtrrd | |
26 | simpr | |
|
27 | 25 26 | sseldd | |
28 | 1 2 | metdseq0 | |
29 | 14 21 27 28 | syl3anc | |
30 | 13 29 | syl5bb | |
31 | cldcls | |
|
32 | 15 31 | syl | |
33 | 32 | eleq2d | |
34 | 30 33 | bitrd | |
35 | 12 34 | mtbird | |
36 | 1 | metdsf | |
37 | 14 21 36 | syl2anc | |
38 | 37 27 | ffvelrnd | |
39 | elxrge0 | |
|
40 | 39 | simprbi | |
41 | 38 40 | syl | |
42 | 0xr | |
|
43 | eliccxr | |
|
44 | 38 43 | syl | |
45 | xrleloe | |
|
46 | 42 44 45 | sylancr | |
47 | 41 46 | mpbid | |
48 | 47 | ord | |
49 | 35 48 | mt3d | |
50 | 1xr | |
|
51 | ifcl | |
|
52 | 50 44 51 | sylancr | |
53 | 1red | |
|
54 | 0lt1 | |
|
55 | breq2 | |
|
56 | breq2 | |
|
57 | 55 56 | ifboth | |
58 | 54 49 57 | sylancr | |
59 | xrltle | |
|
60 | 42 52 59 | sylancr | |
61 | 58 60 | mpd | |
62 | xrmin1 | |
|
63 | 50 44 62 | sylancr | |
64 | xrrege0 | |
|
65 | 52 53 61 63 64 | syl22anc | |
66 | 65 58 | elrpd | |
67 | 49 66 | jca | |