Metamath Proof Explorer


Theorem caun0

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 D∞MetXFCauDX

Proof

Step Hyp Ref Expression
1 1rp 1+
2 1 ne0ii +
3 iscau2 D∞MetXFCauDFX𝑝𝑚x+jkjkdomFFkXFkDFj<x
4 3 simplbda D∞MetXFCauDx+jkjkdomFFkXFkDFj<x
5 r19.2z +x+jkjkdomFFkXFkDFj<xx+jkjkdomFFkXFkDFj<x
6 2 4 5 sylancr D∞MetXFCauDx+jkjkdomFFkXFkDFj<x
7 uzid jjj
8 ne0i jjj
9 r19.2z jkjkdomFFkXFkDFj<xkjkdomFFkXFkDFj<x
10 9 ex jkjkdomFFkXFkDFj<xkjkdomFFkXFkDFj<x
11 7 8 10 3syl jkjkdomFFkXFkDFj<xkjkdomFFkXFkDFj<x
12 ne0i FkXX
13 12 3ad2ant2 kdomFFkXFkDFj<xX
14 13 rexlimivw kjkdomFFkXFkDFj<xX
15 11 14 syl6 jkjkdomFFkXFkDFj<xX
16 15 rexlimiv jkjkdomFFkXFkDFj<xX
17 16 rexlimivw x+jkjkdomFFkXFkDFj<xX
18 6 17 syl D∞MetXFCauDX