iscau4

Description: Express the property " F is a Cauchy sequence of metric D " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 23-Dec-2013)

	Ref	Expression
Hypotheses	iscau3.2	$⊢ Z = ℤ_{\geq M}$
	iscau3.3	$⊢ φ \to D \in ∞Met (X)$
	iscau3.4	$⊢ φ \to M \in ℤ$
	iscau4.5	$⊢ (φ \land k \in Z) \to F (k) = A$
	iscau4.6	$⊢ (φ \land j \in Z) \to F (j) = B$
Assertion	iscau4	$⊢ φ \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x)))$

Proof

Step	Hyp	Ref	Expression
1		iscau3.2	$⊢ Z = ℤ_{\geq M}$
2		iscau3.3	$⊢ φ \to D \in ∞Met (X)$
3		iscau3.4	$⊢ φ \to M \in ℤ$
4		iscau4.5	$⊢ (φ \land k \in Z) \to F (k) = A$
5		iscau4.6	$⊢ (φ \land j \in Z) \to F (j) = B$
6	1 2 3	iscau3	$⊢ φ \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x)))$
7		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
8	7 1	eleqtrdi	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
9		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
10		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
11	8 9 10	3syl	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq j}$
12		fveq2	$⊢ k = j \to ℤ_{\geq k} = ℤ_{\geq j}$
13		fveq2	$⊢ k = j \to F (k) = F (j)$
14	13	oveq1d	$⊢ k = j \to F (k) D F (m) = F (j) D F (m)$
15	14	breq1d	$⊢ k = j \to (F (k) D F (m) < x \leftrightarrow F (j) D F (m) < x)$
16	12 15	raleqbidv	$⊢ k = j \to (\forall m \in ℤ_{\geq k} F (k) D F (m) < x \leftrightarrow \forall m \in ℤ_{\geq j} F (j) D F (m) < x)$
17	16	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} F (k) D F (m) < x \to \forall m \in ℤ_{\geq j} F (j) D F (m) < x)$
18	11 17	syl	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} F (k) D F (m) < x \to \forall m \in ℤ_{\geq j} F (j) D F (m) < x)$
19	18	adantr	$⊢ ((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X)) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} F (k) D F (m) < x \to \forall m \in ℤ_{\geq j} F (j) D F (m) < x)$
20		fveq2	$⊢ m = k \to F (m) = F (k)$
21	20	oveq2d	$⊢ m = k \to F (j) D F (m) = F (j) D F (k)$
22	21	breq1d	$⊢ m = k \to (F (j) D F (m) < x \leftrightarrow F (j) D F (k) < x)$
23	22	cbvralvw	$⊢ \forall m \in ℤ_{\geq j} F (j) D F (m) < x \leftrightarrow \forall k \in ℤ_{\geq j} F (j) D F (k) < x$
24		simpr	$⊢ (k \in dom F \land F (k) \in X) \to F (k) \in X$
25	24	ralimi	$⊢ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X) \to \forall k \in ℤ_{\geq j} F (k) \in X$
26	13	eleq1d	$⊢ k = j \to (F (k) \in X \leftrightarrow F (j) \in X)$
27	26	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} F (k) \in X \to F (j) \in X)$
28	11 25 27	syl2im	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X) \to F (j) \in X)$
29	28	imp	$⊢ ((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X)) \to F (j) \in X$
30		r19.26	$⊢ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land F (j) D F (k) < x) \leftrightarrow (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X) \land \forall k \in ℤ_{\geq j} F (j) D F (k) < x)$
31	2	ad3antrrr	$⊢ (((φ \land j \in Z) \land F (j) \in X) \land (k \in dom F \land F (k) \in X)) \to D \in ∞Met (X)$
32		simplr	$⊢ (((φ \land j \in Z) \land F (j) \in X) \land (k \in dom F \land F (k) \in X)) \to F (j) \in X$
33		simprr	$⊢ (((φ \land j \in Z) \land F (j) \in X) \land (k \in dom F \land F (k) \in X)) \to F (k) \in X$
34		xmetsym	$⊢ (D \in ∞Met (X) \land F (j) \in X \land F (k) \in X) \to F (j) D F (k) = F (k) D F (j)$
35	31 32 33 34	syl3anc	$⊢ (((φ \land j \in Z) \land F (j) \in X) \land (k \in dom F \land F (k) \in X)) \to F (j) D F (k) = F (k) D F (j)$
36	35	breq1d	$⊢ (((φ \land j \in Z) \land F (j) \in X) \land (k \in dom F \land F (k) \in X)) \to (F (j) D F (k) < x \leftrightarrow F (k) D F (j) < x)$
37	36	biimpd	$⊢ (((φ \land j \in Z) \land F (j) \in X) \land (k \in dom F \land F (k) \in X)) \to (F (j) D F (k) < x \to F (k) D F (j) < x)$
38	37	expimpd	$⊢ ((φ \land j \in Z) \land F (j) \in X) \to (((k \in dom F \land F (k) \in X) \land F (j) D F (k) < x) \to F (k) D F (j) < x)$
39	38	ralimdv	$⊢ ((φ \land j \in Z) \land F (j) \in X) \to (\forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land F (j) D F (k) < x) \to \forall k \in ℤ_{\geq j} F (k) D F (j) < x)$
40	30 39	syl5bir	$⊢ ((φ \land j \in Z) \land F (j) \in X) \to ((\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X) \land \forall k \in ℤ_{\geq j} F (j) D F (k) < x) \to \forall k \in ℤ_{\geq j} F (k) D F (j) < x)$
41	40	expd	$⊢ ((φ \land j \in Z) \land F (j) \in X) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X) \to (\forall k \in ℤ_{\geq j} F (j) D F (k) < x \to \forall k \in ℤ_{\geq j} F (k) D F (j) < x))$
42	41	impancom	$⊢ ((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X)) \to (F (j) \in X \to (\forall k \in ℤ_{\geq j} F (j) D F (k) < x \to \forall k \in ℤ_{\geq j} F (k) D F (j) < x))$
43	29 42	mpd	$⊢ ((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X)) \to (\forall k \in ℤ_{\geq j} F (j) D F (k) < x \to \forall k \in ℤ_{\geq j} F (k) D F (j) < x)$
44	23 43	syl5bi	$⊢ ((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X)) \to (\forall m \in ℤ_{\geq j} F (j) D F (m) < x \to \forall k \in ℤ_{\geq j} F (k) D F (j) < x)$
45	19 44	syld	$⊢ ((φ \land j \in Z) \land \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X)) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} F (k) D F (m) < x \to \forall k \in ℤ_{\geq j} F (k) D F (j) < x)$
46	45	imdistanda	$⊢ (φ \land j \in Z) \to ((\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X) \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X) \land \forall k \in ℤ_{\geq j} F (k) D F (j) < x))$
47		r19.26	$⊢ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X) \land \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} F (k) D F (m) < x)$
48		r19.26	$⊢ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land F (k) D F (j) < x) \leftrightarrow (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X) \land \forall k \in ℤ_{\geq j} F (k) D F (j) < x)$
49	46 47 48	3imtr4g	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \to \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land F (k) D F (j) < x))$
50		df-3an	$⊢ (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x)$
51	50	ralbii	$⊢ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \leftrightarrow \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x)$
52		df-3an	$⊢ (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow ((k \in dom F \land F (k) \in X) \land F (k) D F (j) < x)$
53	52	ralbii	$⊢ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land F (k) D F (j) < x)$
54	49 51 53	3imtr4g	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \to \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
55	54	reximdva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
56	55	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
57	56	anim2d	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x)) \to (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)))$
58	6 57	sylbid	$⊢ φ \to (F \in Cau (D) \to (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)))$
59		uzssz	$⊢ ℤ_{\geq M} \subseteq ℤ$
60	1 59	eqsstri	$⊢ Z \subseteq ℤ$
61		ssrexv	$⊢ Z \subseteq ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
62	60 61	ax-mp	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)$
63	62	ralimi	$⊢ \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)$
64	63	anim2i	$⊢ (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)) \to (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x))$
65		iscau2	$⊢ D \in ∞Met (X) \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)))$
66	64 65	syl5ibr	$⊢ D \in ∞Met (X) \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)) \to F \in Cau (D))$
67	2 66	syl	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)) \to F \in Cau (D))$
68	58 67	impbid	$⊢ φ \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)))$
69		simpl	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to j \in Z$
70	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
71	69 70	jca	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to (j \in Z \land k \in Z)$
72	4	adantrl	$⊢ (φ \land (j \in Z \land k \in Z)) \to F (k) = A$
73	72	eleq1d	$⊢ (φ \land (j \in Z \land k \in Z)) \to (F (k) \in X \leftrightarrow A \in X)$
74	5	adantrr	$⊢ (φ \land (j \in Z \land k \in Z)) \to F (j) = B$
75	72 74	oveq12d	$⊢ (φ \land (j \in Z \land k \in Z)) \to F (k) D F (j) = A D B$
76	75	breq1d	$⊢ (φ \land (j \in Z \land k \in Z)) \to (F (k) D F (j) < x \leftrightarrow A D B < x)$
77	73 76	3anbi23d	$⊢ (φ \land (j \in Z \land k \in Z)) \to ((k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow (k \in dom F \land A \in X \land A D B < x))$
78	71 77	sylan2	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to ((k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow (k \in dom F \land A \in X \land A D B < x))$
79	78	anassrs	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to ((k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow (k \in dom F \land A \in X \land A D B < x))$
80	79	ralbidva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x))$
81	80	rexbidva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x))$
82	81	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x))$
83	82	anbi2d	$⊢ φ \to ((F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x)))$
84	68 83	bitrd	$⊢ φ \to (F \in Cau (D) \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land A \in X \land A D B < x)))$

Metamath Proof Explorer

Theorem iscau4

Proof