caucvgb

Description: A function is convergent if and only if it is Cauchy. Theorem 12-5.3 of Gleason p. 180. (Contributed by Mario Carneiro, 15-Feb-2014)

		Ref	Expression
	Hypothesis	caucvgb.1	$⊢ Z = ℤ_{\geq M}$
	Assertion	caucvgb	$⊢ (M \in ℤ \land F \in V) \to (F \in dom ⇝ \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x))$

Proof

Step	Hyp	Ref	Expression
1		caucvgb.1	$⊢ Z = ℤ_{\geq M}$
2		eldm2g	$⊢ F \in dom ⇝ \to (F \in dom ⇝ \leftrightarrow \exists m ⟨F, m⟩ \in ⇝)$
3	2	ibi	$⊢ F \in dom ⇝ \to \exists m ⟨F, m⟩ \in ⇝$
4		df-br	$⊢ F ⇝ m \leftrightarrow ⟨F, m⟩ \in ⇝$
5		simpll	$⊢ ((M \in ℤ \land F \in V) \land F ⇝ m) \to M \in ℤ$
6		1rp	$⊢ 1 \in ℝ^{+}$
7	6	a1i	$⊢ ((M \in ℤ \land F \in V) \land F ⇝ m) \to 1 \in ℝ^{+}$
8		eqidd	$⊢ (((M \in ℤ \land F \in V) \land F ⇝ m) \land k \in Z) \to F (k) = F (k)$
9		simpr	$⊢ ((M \in ℤ \land F \in V) \land F ⇝ m) \to F ⇝ m$
10	1 5 7 8 9	climi	$⊢ ((M \in ℤ \land F \in V) \land F ⇝ m) \to \exists n \in Z \forall k \in ℤ_{\geq n} (F (k) \in ℂ \land \|F (k) - m\| < 1)$
11		simpl	$⊢ (F (k) \in ℂ \land \|F (k) - m\| < 1) \to F (k) \in ℂ$
12	11	ralimi	$⊢ \forall k \in ℤ_{\geq n} (F (k) \in ℂ \land \|F (k) - m\| < 1) \to \forall k \in ℤ_{\geq n} F (k) \in ℂ$
13	12	reximi	$⊢ \exists n \in Z \forall k \in ℤ_{\geq n} (F (k) \in ℂ \land \|F (k) - m\| < 1) \to \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ$
14	10 13	syl	$⊢ ((M \in ℤ \land F \in V) \land F ⇝ m) \to \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ$
15	14	ex	$⊢ (M \in ℤ \land F \in V) \to (F ⇝ m \to \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ)$
16	4 15	syl5bir	$⊢ (M \in ℤ \land F \in V) \to (⟨F, m⟩ \in ⇝ \to \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ)$
17	16	exlimdv	$⊢ (M \in ℤ \land F \in V) \to (\exists m ⟨F, m⟩ \in ⇝ \to \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ)$
18	3 17	syl5	$⊢ (M \in ℤ \land F \in V) \to (F \in dom ⇝ \to \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ)$
19		fveq2	$⊢ j = n \to ℤ_{\geq j} = ℤ_{\geq n}$
20	19	raleqdv	$⊢ j = n \to (\forall k \in ℤ_{\geq j} F (k) \in ℂ \leftrightarrow \forall k \in ℤ_{\geq n} F (k) \in ℂ)$
21	20	cbvrexvw	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in ℂ \leftrightarrow \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ$
22	21	a1i	$⊢ x = 1 \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in ℂ \leftrightarrow \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ)$
23		simpl	$⊢ (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to F (k) \in ℂ$
24	23	ralimi	$⊢ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \forall k \in ℤ_{\geq j} F (k) \in ℂ$
25	24	reximi	$⊢ \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 ℂ$
26	25	ralimi	$⊢ \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \in ℂ$
27	6	a1i	$⊢ \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to 1 \in ℝ^{+}$
28	22 26 27	rspcdva	$⊢ \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ$
29	28	a1i	$⊢ (M \in ℤ \land F \in V) \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ)$
30		eluzelz	$⊢ n \in ℤ_{\geq M} \to n \in ℤ$
31	30 1	eleq2s	$⊢ n \in Z \to n \in ℤ$
32		eqid	$⊢ ℤ_{\geq n} = ℤ_{\geq n}$
33	32	climcau	$⊢ (n \in ℤ \land F \in dom ⇝) \to \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$
34	31 33	sylan	$⊢ (n \in Z \land F \in dom ⇝) \to \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$
35	32	r19.29uz	$⊢ (\forall k \in ℤ_{\geq n} F (k) \in ℂ \land \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x) \to \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)$
36	35	ex	$⊢ \forall k \in ℤ_{\geq n} F (k) \in ℂ \to (\exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x \to \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x))$
37	36	ralimdv	$⊢ \forall k \in ℤ_{\geq n} F (k) \in ℂ \to (\forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x \to \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x))$
38	34 37	mpan9	$⊢ ((n \in Z \land F \in dom ⇝) \land \forall k \in ℤ_{\geq n} F (k) \in ℂ) \to \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)$
39	38	an32s	$⊢ ((n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ) \land F \in dom ⇝) \to \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)$
40	39	adantll	$⊢ (((M \in ℤ \land F \in V) \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \land F \in dom ⇝) \to \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)$
41		simplrr	$⊢ ((F \in V \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)) \to \forall k \in ℤ_{\geq n} F (k) \in ℂ$
42		fveq2	$⊢ k = m \to F (k) = F (m)$
43	42	eleq1d	$⊢ k = m \to (F (k) \in ℂ \leftrightarrow F (m) \in ℂ)$
44	43	rspccva	$⊢ (\forall k \in ℤ_{\geq n} F (k) \in ℂ \land m \in ℤ_{\geq n}) \to F (m) \in ℂ$
45	41 44	sylan	$⊢ (((F \in V \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)) \land m \in ℤ_{\geq n}) \to F (m) \in ℂ$
46		simpr	$⊢ (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \|F (k) - F (j)\| < x$
47	46	ralimi	$⊢ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$
48	42	fvoveq1d	$⊢ k = m \to \|F (k) - F (j)\| = \|F (m) - F (j)\|$
49	48	breq1d	$⊢ k = m \to (\|F (k) - F (j)\| < x \leftrightarrow \|F (m) - F (j)\| < x)$
50	49	cbvralvw	$⊢ \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x \leftrightarrow \forall m \in ℤ_{\geq j} \|F (m) - F (j)\| < x$
51	47 50	sylib	$⊢ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \forall m \in ℤ_{\geq j} \|F (m) - F (j)\| < x$
52	51	reximi	$⊢ \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \exists j \in ℤ_{\geq n} \forall m \in ℤ_{\geq j} \|F (m) - F (j)\| < x$
53	52	ralimi	$⊢ \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall m \in ℤ_{\geq j} \|F (m) - F (j)\| < x$
54	53	adantl	$⊢ ((F \in V \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)) \to \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall m \in ℤ_{\geq j} \|F (m) - F (j)\| < x$
55		fveq2	$⊢ j = i \to ℤ_{\geq j} = ℤ_{\geq i}$
56		fveq2	$⊢ j = i \to F (j) = F (i)$
57	56	oveq2d	$⊢ j = i \to F (m) - F (j) = F (m) - F (i)$
58	57	fveq2d	$⊢ j = i \to \|F (m) - F (j)\| = \|F (m) - F (i)\|$
59	58	breq1d	$⊢ j = i \to (\|F (m) - F (j)\| < x \leftrightarrow \|F (m) - F (i)\| < x)$
60	55 59	raleqbidv	$⊢ j = i \to (\forall m \in ℤ_{\geq j} \|F (m) - F (j)\| < x \leftrightarrow \forall m \in ℤ_{\geq i} \|F (m) - F (i)\| < x)$
61	60	cbvrexvw	$⊢ \exists j \in ℤ_{\geq n} \forall m \in ℤ_{\geq j} \|F (m) - F (j)\| < x \leftrightarrow \exists i \in ℤ_{\geq n} \forall m \in ℤ_{\geq i} \|F (m) - F (i)\| < x$
62		breq2	$⊢ x = y \to (\|F (m) - F (i)\| < x \leftrightarrow \|F (m) - F (i)\| < y)$
63	62	rexralbidv	$⊢ x = y \to (\exists i \in ℤ_{\geq n} \forall m \in ℤ_{\geq i} \|F (m) - F (i)\| < x \leftrightarrow \exists i \in ℤ_{\geq n} \forall m \in ℤ_{\geq i} \|F (m) - F (i)\| < y)$
64	61 63	syl5bb	$⊢ x = y \to (\exists j \in ℤ_{\geq n} \forall m \in ℤ_{\geq j} \|F (m) - F (j)\| < x \leftrightarrow \exists i \in ℤ_{\geq n} \forall m \in ℤ_{\geq i} \|F (m) - F (i)\| < y)$
65	64	cbvralvw	$⊢ \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall m \in ℤ_{\geq j} \|F (m) - F (j)\| < x \leftrightarrow \forall y \in ℝ^{+} \exists i \in ℤ_{\geq n} \forall m \in ℤ_{\geq i} \|F (m) - F (i)\| < y$
66	54 65	sylib	$⊢ ((F \in V \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)) \to \forall y \in ℝ^{+} \exists i \in ℤ_{\geq n} \forall m \in ℤ_{\geq i} \|F (m) - F (i)\| < y$
67		simpll	$⊢ ((F \in V \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)) \to F \in V$
68	32 45 66 67	caucvg	$⊢ ((F \in V \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)) \to F \in dom ⇝$
69	68	adantlll	$⊢ (((M \in ℤ \land F \in V) \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \land \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)) \to F \in dom ⇝$
70	40 69	impbida	$⊢ ((M \in ℤ \land F \in V) \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \to (F \in dom ⇝ \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x))$
71	1 32	cau4	$⊢ n \in Z \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x))$
72	71	ad2antrl	$⊢ ((M \in ℤ \land F \in V) \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ_{\geq n} \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x))$
73	70 72	bitr4d	$⊢ ((M \in ℤ \land F \in V) \land (n \in Z \land \forall k \in ℤ_{\geq n} F (k) \in ℂ)) \to (F \in dom ⇝ \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x))$
74	73	rexlimdvaa	$⊢ (M \in ℤ \land F \in V) \to (\exists n \in Z \forall k \in ℤ_{\geq n} F (k) \in ℂ \to (F \in dom ⇝ \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x)))$
75	18 29 74	pm5.21ndd	$⊢ (M \in ℤ \land F \in V) \to (F \in dom ⇝ \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x))$

Metamath Proof Explorer

Theorem caucvgb

Proof