caurcvg2

Description: A Cauchy sequence of real numbers converges, existence version. (Contributed by NM, 4-Apr-2005) (Revised by Mario Carneiro, 7-Sep-2014)

	Ref	Expression
Hypotheses	caucvg.1	$⊢ Z = ℤ_{\geq M}$
	caurcvg2.2	$⊢ φ \to F \in V$
	caurcvg2.3	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x)$
Assertion	caurcvg2	$⊢ φ \to F \in dom ⇝$

Proof

Step	Hyp	Ref	Expression
1		caucvg.1	$⊢ Z = ℤ_{\geq M}$
2		caurcvg2.2	$⊢ φ \to F \in V$
3		caurcvg2.3	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x)$
4		1rp	$⊢ 1 \in ℝ^{+}$
5	4	ne0ii	$⊢ ℝ^{+} \neq \emptyset$
6		r19.2z	$⊢ (ℝ^{+} \neq \emptyset \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x)) \to \exists x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x)$
7	5 3 6	sylancr	$⊢ φ \to \exists x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x)$
8		simpl	$⊢ (F (k) \in ℝ \land \|F (k) - F (j)\| < x) \to F (k) \in ℝ$
9	8	ralimi	$⊢ \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x) \to \forall k \in ℤ_{\geq j} F (k) \in ℝ$
10		eqid	$⊢ ℤ_{\geq j} = ℤ_{\geq j}$
11		simprr	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to \forall k \in ℤ_{\geq j} F (k) \in ℝ$
12		fveq2	$⊢ k = n \to F (k) = F (n)$
13	12	eleq1d	$⊢ k = n \to (F (k) \in ℝ \leftrightarrow F (n) \in ℝ)$
14	13	rspccva	$⊢ (\forall k \in ℤ_{\geq j} F (k) \in ℝ \land n \in ℤ_{\geq j}) \to F (n) \in ℝ$
15	11 14	sylan	$⊢ ((φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \land n \in ℤ_{\geq j}) \to F (n) \in ℝ$
16	15	fmpttd	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to (n \in ℤ_{\geq j} ⟼ F (n)) : ℤ_{\geq j} ⟶ ℝ$
17		fveq2	$⊢ j = m \to ℤ_{\geq j} = ℤ_{\geq m}$
18		fveq2	$⊢ j = m \to F (j) = F (m)$
19	18	oveq2d	$⊢ j = m \to F (k) - F (j) = F (k) - F (m)$
20	19	fveq2d	$⊢ j = m \to \|F (k) - F (j)\| = \|F (k) - F (m)\|$
21	20	breq1d	$⊢ j = m \to (\|F (k) - F (j)\| < x \leftrightarrow \|F (k) - F (m)\| < x)$
22	21	anbi2d	$⊢ j = m \to ((F (k) \in ℝ \land \|F (k) - F (j)\| < x) \leftrightarrow (F (k) \in ℝ \land \|F (k) - F (m)\| < x))$
23	17 22	raleqbidv	$⊢ j = m \to (\forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x) \leftrightarrow \forall k \in ℤ_{\geq m} (F (k) \in ℝ \land \|F (k) - F (m)\| < x))$
24	23	cbvrexvw	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x) \leftrightarrow \exists m \in Z \forall k \in ℤ_{\geq m} (F (k) \in ℝ \land \|F (k) - F (m)\| < x)$
25		fveq2	$⊢ k = i \to F (k) = F (i)$
26	25	eleq1d	$⊢ k = i \to (F (k) \in ℝ \leftrightarrow F (i) \in ℝ)$
27	25	fvoveq1d	$⊢ k = i \to \|F (k) - F (m)\| = \|F (i) - F (m)\|$
28	27	breq1d	$⊢ k = i \to (\|F (k) - F (m)\| < x \leftrightarrow \|F (i) - F (m)\| < x)$
29	26 28	anbi12d	$⊢ k = i \to ((F (k) \in ℝ \land \|F (k) - F (m)\| < x) \leftrightarrow (F (i) \in ℝ \land \|F (i) - F (m)\| < x))$
30	29	cbvralvw	$⊢ \forall k \in ℤ_{\geq m} (F (k) \in ℝ \land \|F (k) - F (m)\| < x) \leftrightarrow \forall i \in ℤ_{\geq m} (F (i) \in ℝ \land \|F (i) - F (m)\| < x)$
31		recn	$⊢ F (i) \in ℝ \to F (i) \in ℂ$
32	31	anim1i	$⊢ (F (i) \in ℝ \land \|F (i) - F (m)\| < x) \to (F (i) \in ℂ \land \|F (i) - F (m)\| < x)$
33	32	ralimi	$⊢ \forall i \in ℤ_{\geq m} (F (i) \in ℝ \land \|F (i) - F (m)\| < x) \to \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x)$
34	30 33	sylbi	$⊢ \forall k \in ℤ_{\geq m} (F (k) \in ℝ \land \|F (k) - F (m)\| < x) \to \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x)$
35	34	reximi	$⊢ \exists m \in Z \forall k \in ℤ_{\geq m} (F (k) \in ℝ \land \|F (k) - F (m)\| < x) \to \exists m \in Z \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x)$
36	24 35	sylbi	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x) \to \exists m \in Z \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x)$
37	36	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 m \in Z \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x)$
38	3 37	syl	$⊢ φ \to \forall x \in ℝ^{+} \exists m \in Z \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x)$
39	38	adantr	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to \forall x \in ℝ^{+} \exists m \in Z \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x)$
40	1 10	cau4	$⊢ j \in Z \to (\forall x \in ℝ^{+} \exists m \in Z \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x))$
41	40	ad2antrl	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to (\forall x \in ℝ^{+} \exists m \in Z \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x))$
42	39 41	mpbid	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to \forall x \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x)$
43		simpr	$⊢ (F (i) \in ℂ \land \|F (i) - F (m)\| < x) \to \|F (i) - F (m)\| < x$
44	10	uztrn2	$⊢ (m \in ℤ_{\geq j} \land i \in ℤ_{\geq m}) \to i \in ℤ_{\geq j}$
45		fveq2	$⊢ n = i \to F (n) = F (i)$
46		eqid	$⊢ (n \in ℤ_{\geq j} ⟼ F (n)) = (n \in ℤ_{\geq j} ⟼ F (n))$
47		fvex	$⊢ F (i) \in V$
48	45 46 47	fvmpt	$⊢ i \in ℤ_{\geq j} \to (n \in ℤ_{\geq j} ⟼ F (n)) (i) = F (i)$
49	44 48	syl	$⊢ (m \in ℤ_{\geq j} \land i \in ℤ_{\geq m}) \to (n \in ℤ_{\geq j} ⟼ F (n)) (i) = F (i)$
50		fveq2	$⊢ n = m \to F (n) = F (m)$
51		fvex	$⊢ F (m) \in V$
52	50 46 51	fvmpt	$⊢ m \in ℤ_{\geq j} \to (n \in ℤ_{\geq j} ⟼ F (n)) (m) = F (m)$
53	52	adantr	$⊢ (m \in ℤ_{\geq j} \land i \in ℤ_{\geq m}) \to (n \in ℤ_{\geq j} ⟼ F (n)) (m) = F (m)$
54	49 53	oveq12d	$⊢ (m \in ℤ_{\geq j} \land i \in ℤ_{\geq m}) \to (n \in ℤ_{\geq j} ⟼ F (n)) (i) - (n \in ℤ_{\geq j} ⟼ F (n)) (m) = F (i) - F (m)$
55	54	fveq2d	$⊢ (m \in ℤ_{\geq j} \land i \in ℤ_{\geq m}) \to \|(n \in ℤ_{\geq j} ⟼ F (n)) (i) - (n \in ℤ_{\geq j} ⟼ F (n)) (m)\| = \|F (i) - F (m)\|$
56	55	breq1d	$⊢ (m \in ℤ_{\geq j} \land i \in ℤ_{\geq m}) \to (\|(n \in ℤ_{\geq j} ⟼ F (n)) (i) - (n \in ℤ_{\geq j} ⟼ F (n)) (m)\| < x \leftrightarrow \|F (i) - F (m)\| < x)$
57	43 56	syl5ibr	$⊢ (m \in ℤ_{\geq j} \land i \in ℤ_{\geq m}) \to ((F (i) \in ℂ \land \|F (i) - F (m)\| < x) \to \|(n \in ℤ_{\geq j} ⟼ F (n)) (i) - (n \in ℤ_{\geq j} ⟼ F (n)) (m)\| < x)$
58	57	ralimdva	$⊢ m \in ℤ_{\geq j} \to (\forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x) \to \forall i \in ℤ_{\geq m} \|(n \in ℤ_{\geq j} ⟼ F (n)) (i) - (n \in ℤ_{\geq j} ⟼ F (n)) (m)\| < x)$
59	58	reximia	$⊢ \exists m \in ℤ_{\geq j} \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x) \to \exists m \in ℤ_{\geq j} \forall i \in ℤ_{\geq m} \|(n \in ℤ_{\geq j} ⟼ F (n)) (i) - (n \in ℤ_{\geq j} ⟼ F (n)) (m)\| < x$
60	59	ralimi	$⊢ \forall x \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall i \in ℤ_{\geq m} (F (i) \in ℂ \land \|F (i) - F (m)\| < x) \to \forall x \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall i \in ℤ_{\geq m} \|(n \in ℤ_{\geq j} ⟼ F (n)) (i) - (n \in ℤ_{\geq j} ⟼ F (n)) (m)\| < x$
61	42 60	syl	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to \forall x \in ℝ^{+} \exists m \in ℤ_{\geq j} \forall i \in ℤ_{\geq m} \|(n \in ℤ_{\geq j} ⟼ F (n)) (i) - (n \in ℤ_{\geq j} ⟼ F (n)) (m)\| < x$
62	10 16 61	caurcvg	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to (n \in ℤ_{\geq j} ⟼ F (n)) ⇝ lim sup ((n \in ℤ_{\geq j} ⟼ F (n)))$
63		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
64	63 1	eleq2s	$⊢ j \in Z \to j \in ℤ$
65	64	ad2antrl	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to j \in ℤ$
66	2	adantr	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to F \in V$
67		fveq2	$⊢ n = k \to F (n) = F (k)$
68	67	cbvmptv	$⊢ (n \in ℤ_{\geq j} ⟼ F (n)) = (k \in ℤ_{\geq j} ⟼ F (k))$
69	10 68	climmpt	$⊢ (j \in ℤ \land F \in V) \to (F ⇝ lim sup ((n \in ℤ_{\geq j} ⟼ F (n))) \leftrightarrow (n \in ℤ_{\geq j} ⟼ F (n)) ⇝ lim sup ((n \in ℤ_{\geq j} ⟼ F (n))))$
70	65 66 69	syl2anc	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to (F ⇝ lim sup ((n \in ℤ_{\geq j} ⟼ F (n))) \leftrightarrow (n \in ℤ_{\geq j} ⟼ F (n)) ⇝ lim sup ((n \in ℤ_{\geq j} ⟼ F (n))))$
71	62 70	mpbird	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to F ⇝ lim sup ((n \in ℤ_{\geq j} ⟼ F (n)))$
72		climrel	$⊢ Rel ⇝$
73	72	releldmi	$⊢ F ⇝ lim sup ((n \in ℤ_{\geq j} ⟼ F (n))) \to F \in dom ⇝$
74	71 73	syl	$⊢ (φ \land (j \in Z \land \forall k \in ℤ_{\geq j} F (k) \in ℝ)) \to F \in dom ⇝$
75	74	expr	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} F (k) \in ℝ \to F \in dom ⇝)$
76	9 75	syl5	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x) \to F \in dom ⇝)$
77	76	rexlimdva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x) \to F \in dom ⇝)$
78	77	rexlimdvw	$⊢ φ \to (\exists x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℝ \land \|F (k) - F (j)\| < x) \to F \in dom ⇝)$
79	7 78	mpd	$⊢ φ \to F \in dom ⇝$

Metamath Proof Explorer

Theorem caurcvg2

Proof