iscauf

Description: Express the property " F is a Cauchy sequence of metric D " presupposing F is a function. (Contributed by NM, 24-Jul-2007) (Revised by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Hypotheses	iscau3.2	$⊢ Z = ℤ_{\geq M}$
	iscau3.3	$⊢ φ \to D \in ∞Met (X)$
	iscau3.4	$⊢ φ \to M \in ℤ$
	iscau4.5	$⊢ (φ \land k \in Z) \to F (k) = A$
	iscau4.6	$⊢ (φ \land j \in Z) \to F (j) = B$
	iscauf.7	$⊢ φ \to F : Z ⟶ X$
Assertion	iscauf	$⊢ φ \to (F \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} B D A < x)$

Proof

Step	Hyp	Ref	Expression
1		iscau3.2	$⊢ Z = ℤ_{\geq M}$
2		iscau3.3	$⊢ φ \to D \in ∞Met (X)$
3		iscau3.4	$⊢ φ \to M \in ℤ$
4		iscau4.5	$⊢ (φ \land k \in Z) \to F (k) = A$
5		iscau4.6	$⊢ (φ \land j \in Z) \to F (j) = B$
6		iscauf.7	$⊢ φ \to F : Z ⟶ X$
7		elfvdm	$⊢ D \in ∞Met (X) \to X \in dom ∞Met$
8	2 7	syl	$⊢ φ \to X \in dom ∞Met$
9		cnex	$⊢ ℂ \in V$
10	8 9	jctir	$⊢ φ \to (X \in dom ∞Met \land ℂ \in V)$
11		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
12		zsscn	$⊢ ℤ \subseteq ℂ$
13	11 12	sstri	$⊢ ℤ_{\geq M} \subseteq ℂ$
14	1 13	eqsstri	$⊢ Z \subseteq ℂ$
15	6 14	jctir	$⊢ φ \to (F : Z ⟶ X \land Z \subseteq ℂ)$
16		elpm2r	$⊢ ((X \in dom ∞Met \land ℂ \in V) \land (F : Z ⟶ X \land Z \subseteq ℂ)) \to F \in (X ↑_{𝑝𝑚} ℂ)$
17	10 15 16	syl2anc	$⊢ φ \to F \in (X ↑_{𝑝𝑚} ℂ)$
18	17	biantrurd	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x)))$
19	2	adantr	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to D \in ∞Met (X)$
20	5	adantrr	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to F (j) = B$
21	6	adantr	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to F : Z ⟶ X$
22		simprl	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to j \in Z$
23	21 22	ffvelcdmd	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to F (j) \in X$
24	20 23	eqeltrrd	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to B \in X$
25	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
26	25 4	sylan2	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) = A$
27		ffvelcdm	$⊢ (F : Z ⟶ X \land k \in Z) \to F (k) \in X$
28	6 25 27	syl2an	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \in X$
29	26 28	eqeltrrd	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to A \in X$
30		xmetsym	$⊢ (D \in ∞Met (X) \land B \in X \land A \in X) \to B D A = A D B$
31	19 24 29 30	syl3anc	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to B D A = A D B$
32	31	breq1d	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to (B D A < x \leftrightarrow A D B < x)$
33		fdm	$⊢ F : Z ⟶ X \to dom F = Z$
34	33	eleq2d	$⊢ F : Z ⟶ X \to (k \in dom F \leftrightarrow k \in Z)$
35	34	biimpar	$⊢ (F : Z ⟶ X \land k \in Z) \to k \in dom F$
36	6 25 35	syl2an	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to k \in dom F$
37	36 29	jca	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to (k \in dom F \land A \in X)$
38	37	biantrurd	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to (A D B < x \leftrightarrow ((k \in dom F \land A \in X) \land A D B < x))$
39		df-3an	$⊢ (k \in dom F \land A \in X \land A D B < x) \leftrightarrow ((k \in dom F \land A \in X) \land A D B < x)$
40	38 39	bitr4di	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to (A D B < x \leftrightarrow (k \in dom F \land A \in X \land A D B < x))$
41	32 40	bitrd	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to (B D A < x \leftrightarrow (k \in dom F \land A \in X \land A D B < x))$
42	41	anassrs	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (B D A < x \leftrightarrow (k \in dom F \land A \in X \land A D B < x))$
43	42	ralbidva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} B D A < x \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x))$
44	43	rexbidva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} B D A < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x))$
45	44	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} B D A < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x))$
46	1 2 3 4 5	iscau4	$⊢ φ \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x)))$
47	18 45 46	3bitr4rd	$⊢ φ \to (F \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} B D A < x)$

Metamath Proof Explorer

Theorem iscauf

Proof