# 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 ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \mathrm{Cau}\left({D}\right)\right)\to {X}\ne \varnothing$

### Proof

Step Hyp Ref Expression
1 1rp ${⊢}1\in {ℝ}^{+}$
2 1 ne0ii ${⊢}{ℝ}^{+}\ne \varnothing$
3 iscau2 ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({F}\in \mathrm{Cau}\left({D}\right)↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)\right)$
4 3 simplbda ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \mathrm{Cau}\left({D}\right)\right)\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)$
5 r19.2z ${⊢}\left({ℝ}^{+}\ne \varnothing \wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)$
6 2 4 5 sylancr ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \mathrm{Cau}\left({D}\right)\right)\to \exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)$
7 uzid ${⊢}{j}\in ℤ\to {j}\in {ℤ}_{\ge {j}}$
8 ne0i ${⊢}{j}\in {ℤ}_{\ge {j}}\to {ℤ}_{\ge {j}}\ne \varnothing$
9 r19.2z ${⊢}\left({ℤ}_{\ge {j}}\ne \varnothing \wedge \forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)\to \exists {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)$
10 9 ex ${⊢}{ℤ}_{\ge {j}}\ne \varnothing \to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to \exists {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
11 7 8 10 3syl ${⊢}{j}\in ℤ\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to \exists {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\right)$
12 ne0i ${⊢}{F}\left({k}\right)\in {X}\to {X}\ne \varnothing$
13 12 3ad2ant2 ${⊢}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to {X}\ne \varnothing$
14 13 rexlimivw ${⊢}\exists {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to {X}\ne \varnothing$
15 11 14 syl6 ${⊢}{j}\in ℤ\to \left(\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to {X}\ne \varnothing \right)$
16 15 rexlimiv ${⊢}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to {X}\ne \varnothing$
17 16 rexlimivw ${⊢}\exists {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {j}\in ℤ\phantom{\rule{.4em}{0ex}}\forall {k}\in {ℤ}_{\ge {j}}\phantom{\rule{.4em}{0ex}}\left({k}\in \mathrm{dom}{F}\wedge {F}\left({k}\right)\in {X}\wedge {F}\left({k}\right){D}{F}\left({j}\right)<{x}\right)\to {X}\ne \varnothing$
18 6 17 syl ${⊢}\left({D}\in \mathrm{\infty Met}\left({X}\right)\wedge {F}\in \mathrm{Cau}\left({D}\right)\right)\to {X}\ne \varnothing$