Description: A metric with a Cauchy sequence cannot be empty. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 24-Dec-2013)
Ref | Expression | ||
---|---|---|---|
Assertion | caun0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1rp | |
|
2 | 1 | ne0ii | |
3 | iscau2 | |
|
4 | 3 | simplbda | |
5 | r19.2z | |
|
6 | 2 4 5 | sylancr | |
7 | uzid | |
|
8 | ne0i | |
|
9 | r19.2z | |
|
10 | 9 | ex | |
11 | 7 8 10 | 3syl | |
12 | ne0i | |
|
13 | 12 | 3ad2ant2 | |
14 | 13 | rexlimivw | |
15 | 11 14 | syl6 | |
16 | 15 | rexlimiv | |
17 | 16 | rexlimivw | |
18 | 6 17 | syl | |