climcau

Description: A converging sequence of complex numbers is a Cauchy sequence. Theorem 12-5.3 of Gleason p. 180 (necessity part). (Contributed by NM, 16-Apr-2005) (Revised by Mario Carneiro, 26-Apr-2014)

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

Proof

Step	Hyp	Ref	Expression
1		climcau.1	$⊢ Z = ℤ_{\geq M}$
2		df-br	$⊢ F ⇝ y \leftrightarrow ⟨F, y⟩ \in ⇝$
3		simpll	$⊢ ((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \to M \in ℤ$
4		rphalfcl	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{+}$
5	4	adantl	$⊢ ((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \to \frac{x}{2} \in ℝ^{+}$
6		eqidd	$⊢ (((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \land k \in Z) \to F (k) = F (k)$
7		simplr	$⊢ ((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \to F ⇝ y$
8	1 3 5 6 7	climi	$⊢ ((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})$
9		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
10		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
11	9 10	syl	$⊢ j \in ℤ_{\geq M} \to j \in ℤ_{\geq j}$
12	11 1	eleq2s	$⊢ j \in Z \to j \in ℤ_{\geq j}$
13	12	adantl	$⊢ (((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \land j \in Z) \to j \in ℤ_{\geq j}$
14		fveq2	$⊢ k = j \to F (k) = F (j)$
15	14	eleq1d	$⊢ k = j \to (F (k) \in ℂ \leftrightarrow F (j) \in ℂ)$
16	14	fvoveq1d	$⊢ k = j \to \|F (k) - y\| = \|F (j) - y\|$
17	16	breq1d	$⊢ k = j \to (\|F (k) - y\| < \frac{x}{2} \leftrightarrow \|F (j) - y\| < \frac{x}{2})$
18	15 17	anbi12d	$⊢ k = j \to ((F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \leftrightarrow (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2}))$
19	18	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \to (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2}))$
20	13 19	syl	$⊢ (((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \to (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2}))$
21		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
22	21	ad2antlr	$⊢ (((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \land j \in Z) \to x \in ℝ$
23		simpllr	$⊢ (((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \land j \in Z) \to F ⇝ y$
24		climcl	$⊢ F ⇝ y \to y \in ℂ$
25	23 24	syl	$⊢ (((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \land j \in Z) \to y \in ℂ$
26		simprl	$⊢ (((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \land (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})) \to F (k) \in ℂ$
27		simplrl	$⊢ (((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \land (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})) \to F (j) \in ℂ$
28		simpllr	$⊢ (((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \land (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})) \to y \in ℂ$
29		simplll	$⊢ (((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \land (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})) \to x \in ℝ$
30		simprr	$⊢ (((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \land (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})) \to \|F (k) - y\| < \frac{x}{2}$
31	28 27	abssubd	$⊢ (((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \land (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})) \to \|y - F (j)\| = \|F (j) - y\|$
32		simplrr	$⊢ (((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \land (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})) \to \|F (j) - y\| < \frac{x}{2}$
33	31 32	eqbrtrd	$⊢ (((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \land (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})) \to \|y - F (j)\| < \frac{x}{2}$
34	26 27 28 29 30 33	abs3lemd	$⊢ (((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \land (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2})) \to \|F (k) - F (j)\| < x$
35	34	ex	$⊢ ((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \to ((F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \to \|F (k) - F (j)\| < x)$
36	35	ralimdv	$⊢ ((x \in ℝ \land y \in ℂ) \land (F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2})) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \to \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x)$
37	36	ex	$⊢ (x \in ℝ \land y \in ℂ) \to ((F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2}) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \to \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x))$
38	37	com23	$⊢ (x \in ℝ \land y \in ℂ) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \to ((F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2}) \to \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x))$
39	22 25 38	syl2anc	$⊢ (((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \to ((F (j) \in ℂ \land \|F (j) - y\| < \frac{x}{2}) \to \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x))$
40	20 39	mpdd	$⊢ (((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \to \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x)$
41	40	reximdva	$⊢ ((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - y\| < \frac{x}{2}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x)$
42	8 41	mpd	$⊢ ((M \in ℤ \land F ⇝ y) \land x \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$
43	42	ralrimiva	$⊢ (M \in ℤ \land F ⇝ y) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$
44	43	ex	$⊢ M \in ℤ \to (F ⇝ y \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x)$
45	2 44	biimtrrid	$⊢ M \in ℤ \to (⟨F, y⟩ \in ⇝ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x)$
46	45	exlimdv	$⊢ M \in ℤ \to (\exists y ⟨F, y⟩ \in ⇝ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x)$
47		eldm2g	$⊢ F \in dom ⇝ \to (F \in dom ⇝ \leftrightarrow \exists y ⟨F, y⟩ \in ⇝)$
48	47	ibi	$⊢ F \in dom ⇝ \to \exists y ⟨F, y⟩ \in ⇝$
49	46 48	impel	$⊢ (M \in ℤ \land F \in dom ⇝) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - F (j)\| < x$

Metamath Proof Explorer

Theorem climcau

Proof