caubnd2

Description: A Cauchy sequence of complex numbers is eventually bounded. (Contributed by Mario Carneiro, 14-Feb-2014)

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

Proof

Step	Hyp	Ref	Expression
1		cau3.1	$⊢ Z = ℤ_{\geq M}$
2		1rp	$⊢ 1 \in ℝ^{+}$
3		breq2	$⊢ x = 1 \to (\|F (k) - F (j)\| < x \leftrightarrow \|F (k) - F (j)\| < 1)$
4	3	anbi2d	$⊢ x = 1 \to ((F (k) \in ℂ \land \|F (k) - F (j)\| < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - F (j)\| < 1))$
5	4	rexralbidv	$⊢ x = 1 \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1))$
6	5	rspcv	$⊢ 1 \in ℝ^{+} \to (\forall x \in ℝ^{+} \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)\| < 1))$
7	2 6	ax-mp	$⊢ \forall x \in ℝ^{+} \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)\| < 1)$
8		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
9	8 1	eleq2s	$⊢ j \in Z \to j \in ℤ$
10		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
11	9 10	syl	$⊢ j \in Z \to j \in ℤ_{\geq j}$
12		simpl	$⊢ (F (k) \in ℂ \land \|F (k) - F (j)\| < 1) \to F (k) \in ℂ$
13	12	ralimi	$⊢ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1) \to \forall k \in ℤ_{\geq j} F (k) \in ℂ$
14		fveq2	$⊢ k = j \to F (k) = F (j)$
15	14	eleq1d	$⊢ k = j \to (F (k) \in ℂ \leftrightarrow F (j) \in ℂ)$
16	15	rspcva	$⊢ (j \in ℤ_{\geq j} \land \forall k \in ℤ_{\geq j} F (k) \in ℂ) \to F (j) \in ℂ$
17	11 13 16	syl2an	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1)) \to F (j) \in ℂ$
18		abscl	$⊢ F (j) \in ℂ \to \|F (j)\| \in ℝ$
19	17 18	syl	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1)) \to \|F (j)\| \in ℝ$
20		1re	$⊢ 1 \in ℝ$
21		readdcl	$⊢ (\|F (j)\| \in ℝ \land 1 \in ℝ) \to \|F (j)\| + 1 \in ℝ$
22	19 20 21	sylancl	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1)) \to \|F (j)\| + 1 \in ℝ$
23		simpr	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to F (k) \in ℂ$
24		simplr	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to F (j) \in ℂ$
25		abs2dif	$⊢ (F (k) \in ℂ \land F (j) \in ℂ) \to \|F (k)\| - \|F (j)\| \leq \|F (k) - F (j)\|$
26	23 24 25	syl2anc	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to \|F (k)\| - \|F (j)\| \leq \|F (k) - F (j)\|$
27		abscl	$⊢ F (k) \in ℂ \to \|F (k)\| \in ℝ$
28	23 27	syl	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to \|F (k)\| \in ℝ$
29	24 18	syl	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to \|F (j)\| \in ℝ$
30	28 29	resubcld	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to \|F (k)\| - \|F (j)\| \in ℝ$
31	23 24	subcld	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to F (k) - F (j) \in ℂ$
32		abscl	$⊢ F (k) - F (j) \in ℂ \to \|F (k) - F (j)\| \in ℝ$
33	31 32	syl	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to \|F (k) - F (j)\| \in ℝ$
34		lelttr	$⊢ (\|F (k)\| - \|F (j)\| \in ℝ \land \|F (k) - F (j)\| \in ℝ \land 1 \in ℝ) \to ((\|F (k)\| - \|F (j)\| \leq \|F (k) - F (j)\| \land \|F (k) - F (j)\| < 1) \to \|F (k)\| - \|F (j)\| < 1)$
35	20 34	mp3an3	$⊢ (\|F (k)\| - \|F (j)\| \in ℝ \land \|F (k) - F (j)\| \in ℝ) \to ((\|F (k)\| - \|F (j)\| \leq \|F (k) - F (j)\| \land \|F (k) - F (j)\| < 1) \to \|F (k)\| - \|F (j)\| < 1)$
36	30 33 35	syl2anc	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to ((\|F (k)\| - \|F (j)\| \leq \|F (k) - F (j)\| \land \|F (k) - F (j)\| < 1) \to \|F (k)\| - \|F (j)\| < 1)$
37	26 36	mpand	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to (\|F (k) - F (j)\| < 1 \to \|F (k)\| - \|F (j)\| < 1)$
38		ltsubadd2	$⊢ (\|F (k)\| \in ℝ \land \|F (j)\| \in ℝ \land 1 \in ℝ) \to (\|F (k)\| - \|F (j)\| < 1 \leftrightarrow \|F (k)\| < \|F (j)\| + 1)$
39	20 38	mp3an3	$⊢ (\|F (k)\| \in ℝ \land \|F (j)\| \in ℝ) \to (\|F (k)\| - \|F (j)\| < 1 \leftrightarrow \|F (k)\| < \|F (j)\| + 1)$
40	28 29 39	syl2anc	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to (\|F (k)\| - \|F (j)\| < 1 \leftrightarrow \|F (k)\| < \|F (j)\| + 1)$
41	37 40	sylibd	$⊢ ((j \in Z \land F (j) \in ℂ) \land F (k) \in ℂ) \to (\|F (k) - F (j)\| < 1 \to \|F (k)\| < \|F (j)\| + 1)$
42	41	expimpd	$⊢ (j \in Z \land F (j) \in ℂ) \to ((F (k) \in ℂ \land \|F (k) - F (j)\| < 1) \to \|F (k)\| < \|F (j)\| + 1)$
43	42	ralimdv	$⊢ (j \in Z \land F (j) \in ℂ) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1) \to \forall k \in ℤ_{\geq j} \|F (k)\| < \|F (j)\| + 1)$
44	43	impancom	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1)) \to (F (j) \in ℂ \to \forall k \in ℤ_{\geq j} \|F (k)\| < \|F (j)\| + 1)$
45	17 44	mpd	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1)) \to \forall k \in ℤ_{\geq j} \|F (k)\| < \|F (j)\| + 1$
46		brralrspcev	$⊢ (\|F (j)\| + 1 \in ℝ \land \forall k \in ℤ_{\geq j} \|F (k)\| < \|F (j)\| + 1) \to \exists y \in ℝ \forall k \in ℤ_{\geq j} \|F (k)\| < y$
47	22 45 46	syl2anc	$⊢ (j \in Z \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1)) \to \exists y \in ℝ \forall k \in ℤ_{\geq j} \|F (k)\| < y$
48	47	ex	$⊢ j \in Z \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1) \to \exists y \in ℝ \forall k \in ℤ_{\geq j} \|F (k)\| < y)$
49	48	reximia	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1) \to \exists j \in Z \exists y \in ℝ \forall k \in ℤ_{\geq j} \|F (k)\| < y$
50		rexcom	$⊢ \exists j \in Z \exists y \in ℝ \forall k \in ℤ_{\geq j} \|F (k)\| < y \leftrightarrow \exists y \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k)\| < y$
51	49 50	sylib	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < 1) \to \exists y \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k)\| < y$
52	7 51	syl	$⊢ \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - F (j)\| < x) \to \exists y \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k)\| < y$

Metamath Proof Explorer

Theorem caubnd2

Proof