cvgcaule

Description: A convergent function is Cauchy. (Contributed by Glauco Siliprandi, 15-Feb-2025)

	Ref	Expression
Hypotheses	cvgcaule.1	$⊢ \underline{Ⅎ} j F$
	cvgcaule.2	$⊢ \underline{Ⅎ} k F$
	cvgcaule.3	$⊢ φ \to M \in Z$
	cvgcaule.4	$⊢ φ \to F \in V$
	cvgcaule.5	$⊢ Z = ℤ_{\geq M}$
	cvgcaule.6	$⊢ φ \to F \in dom ⇝$
	cvgcaule.7	$⊢ φ \to X \in ℝ^{+}$
Assertion	cvgcaule	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| \leq X)$

Proof

Step	Hyp	Ref	Expression
1		cvgcaule.1	$⊢ \underline{Ⅎ} j F$
2		cvgcaule.2	$⊢ \underline{Ⅎ} k F$
3		cvgcaule.3	$⊢ φ \to M \in Z$
4		cvgcaule.4	$⊢ φ \to F \in V$
5		cvgcaule.5	$⊢ Z = ℤ_{\geq M}$
6		cvgcaule.6	$⊢ φ \to F \in dom ⇝$
7		cvgcaule.7	$⊢ φ \to X \in ℝ^{+}$
8	1 2 3 4 5 6 7	cvgcau	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)$
9		nfv	$⊢ Ⅎ k (X \in ℝ^{+} \land j \in Z)$
10		nfra1	$⊢ Ⅎ k \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)$
11	9 10	nfan	$⊢ Ⅎ k ((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X))$
12		rspa	$⊢ (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X) \land k \in ℤ_{\geq j}) \to (F (k) \in ℂ \land \|F (k) - F (j)\| < X)$
13	12	simpld	$⊢ (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X) \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
14	13	adantll	$⊢ (((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
15	13	adantll	$⊢ ((j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
16	5	uzid3	$⊢ j \in Z \to j \in ℤ_{\geq j}$
17		nfcv	$⊢ \underline{Ⅎ} k j$
18	2 17	nffv	$⊢ \underline{Ⅎ} k F (j)$
19	18	nfel1	$⊢ Ⅎ k F (j) \in ℂ$
20		nfcv	$⊢ \underline{Ⅎ} k abs$
21		nfcv	$⊢ \underline{Ⅎ} k -$
22	18 21 18	nfov	$⊢ \underline{Ⅎ} k (F (j) - F (j))$
23	20 22	nffv	$⊢ \underline{Ⅎ} k \|F (j) - F (j)\|$
24		nfcv	$⊢ \underline{Ⅎ} k <$
25		nfcv	$⊢ \underline{Ⅎ} k X$
26	23 24 25	nfbr	$⊢ Ⅎ k \|F (j) - F (j)\| < X$
27	19 26	nfan	$⊢ Ⅎ k (F (j) \in ℂ \land \|F (j) - F (j)\| < X)$
28		fveq2	$⊢ k = j \to F (k) = F (j)$
29	28	eleq1d	$⊢ k = j \to (F (k) \in ℂ \leftrightarrow F (j) \in ℂ)$
30	28	fvoveq1d	$⊢ k = j \to \|F (k) - F (j)\| = \|F (j) - F (j)\|$
31	30	breq1d	$⊢ k = j \to (\|F (k) - F (j)\| < X \leftrightarrow \|F (j) - F (j)\| < X)$
32	29 31	anbi12d	$⊢ k = j \to ((F (k) \in ℂ \land \|F (k) - F (j)\| < X) \leftrightarrow (F (j) \in ℂ \land \|F (j) - F (j)\| < X))$
33	27 32	rspc	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X) \to (F (j) \in ℂ \land \|F (j) - F (j)\| < X))$
34	16 33	syl	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X) \to (F (j) \in ℂ \land \|F (j) - F (j)\| < X))$
35	34	imp	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \to (F (j) \in ℂ \land \|F (j) - F (j)\| < X)$
36	35	simpld	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \to F (j) \in ℂ$
37	36	adantr	$⊢ ((j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to F (j) \in ℂ$
38	15 37	subcld	$⊢ ((j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to F (k) - F (j) \in ℂ$
39	38	abscld	$⊢ ((j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to \|F (k) - F (j)\| \in ℝ$
40	39	adantlll	$⊢ (((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to \|F (k) - F (j)\| \in ℝ$
41		simplll	$⊢ (((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to X \in ℝ^{+}$
42	41	rpred	$⊢ (((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to X \in ℝ$
43	12	adantll	$⊢ (((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to (F (k) \in ℂ \land \|F (k) - F (j)\| < X)$
44	43	simprd	$⊢ (((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to \|F (k) - F (j)\| < X$
45	40 42 44	ltled	$⊢ (((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to \|F (k) - F (j)\| \leq X$
46	14 45	jca	$⊢ (((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \land k \in ℤ_{\geq j}) \to (F (k) \in ℂ \land \|F (k) - F (j)\| \leq X)$
47	11 46	ralrimia	$⊢ ((X \in ℝ^{+} \land j \in Z) \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X)) \to \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| \leq X)$
48	47	ex	$⊢ (X \in ℝ^{+} \land j \in Z) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X) \to \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| \leq X))$
49	48	reximdva	$⊢ X \in ℝ^{+} \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < X) \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| \leq X))$
50	7 8 49	sylc	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| \leq X)$

Metamath Proof Explorer

Theorem cvgcaule

Proof