# 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 e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> X =/= (/) )`

### Proof

Step Hyp Ref Expression
1 1rp
` |-  1 e. RR+`
2 1 ne0ii
` |-  RR+ =/= (/)`
3 iscau2
` |-  ( D e. ( *Met ` X ) -> ( F e. ( Cau ` D ) <-> ( F e. ( X ^pm CC ) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) ) )`
4 3 simplbda
` |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )`
5 r19.2z
` |-  ( ( RR+ =/= (/) /\ A. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) -> E. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )`
6 2 4 5 sylancr
` |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> E. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )`
7 uzid
` |-  ( j e. ZZ -> j e. ( ZZ>= ` j ) )`
8 ne0i
` |-  ( j e. ( ZZ>= ` j ) -> ( ZZ>= ` j ) =/= (/) )`
9 r19.2z
` |-  ( ( ( ZZ>= ` j ) =/= (/) /\ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) -> E. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) )`
10 9 ex
` |-  ( ( ZZ>= ` j ) =/= (/) -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> E. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )`
11 7 8 10 3syl
` |-  ( j e. ZZ -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> E. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) ) )`
12 ne0i
` |-  ( ( F ` k ) e. X -> X =/= (/) )`
` |-  ( ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) )`
` |-  ( E. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) )`
` |-  ( j e. ZZ -> ( A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) ) )`
` |-  ( E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) )`
` |-  ( E. x e. RR+ E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. X /\ ( ( F ` k ) D ( F ` j ) ) < x ) -> X =/= (/) )`
` |-  ( ( D e. ( *Met ` X ) /\ F e. ( Cau ` D ) ) -> X =/= (/) )`