iscau3

Description: Express the Cauchy sequence property in the more conventional three-quantifier form. (Contributed by NM, 19-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Hypotheses	iscau3.2	$⊢ Z = ℤ_{\geq M}$
	iscau3.3	$⊢ φ \to D \in ∞Met (X)$
	iscau3.4	$⊢ φ \to M \in ℤ$
Assertion	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)))$

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		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)))$
5	2 4	syl	$⊢ φ \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)))$
6	2	adantr	$⊢ (φ \land F \in (X ↑_{𝑝𝑚} ℂ)) \to D \in ∞Met (X)$
7		ssid	$⊢ ℤ \subseteq ℤ$
8		simpr	$⊢ (k \in dom F \land F (k) \in X) \to F (k) \in X$
9		eleq1	$⊢ F (k) = F (j) \to (F (k) \in X \leftrightarrow F (j) \in X)$
10		eleq1	$⊢ F (k) = F (m) \to (F (k) \in X \leftrightarrow F (m) \in X)$
11		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)$
12	11	fveq2d	$⊢ (D \in ∞Met (X) \land F (j) \in X \land F (k) \in X) \to I (F (j) D F (k)) = I (F (k) D F (j))$
13		xmetsym	$⊢ (D \in ∞Met (X) \land F (m) \in X \land F (j) \in X) \to F (m) D F (j) = F (j) D F (m)$
14	13	fveq2d	$⊢ (D \in ∞Met (X) \land F (m) \in X \land F (j) \in X) \to I (F (m) D F (j)) = I (F (j) D F (m))$
15		simp1	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to D \in ∞Met (X)$
16		simp2l	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to F (k) \in X$
17		simp3l	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to F (j) \in X$
18		xmetcl	$⊢ (D \in ∞Met (X) \land F (k) \in X \land F (j) \in X) \to F (k) D F (j) \in ℝ^{*}$
19	15 16 17 18	syl3anc	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to F (k) D F (j) \in ℝ^{*}$
20		simp2r	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to F (m) \in X$
21		xmetcl	$⊢ (D \in ∞Met (X) \land F (j) \in X \land F (m) \in X) \to F (j) D F (m) \in ℝ^{*}$
22	15 17 20 21	syl3anc	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to F (j) D F (m) \in ℝ^{*}$
23		simp3r	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to x \in ℝ$
24	23	rehalfcld	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to \frac{x}{2} \in ℝ$
25	24	rexrd	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to \frac{x}{2} \in ℝ^{*}$
26		xlt2add	$⊢ ((F (k) D F (j) \in ℝ^{} \land F (j) D F (m) \in ℝ^{}) \land (\frac{x}{2} \in ℝ^{} \land \frac{x}{2} \in ℝ^{})) \to ((F (k) D F (j) < \frac{x}{2} \land F (j) D F (m) < \frac{x}{2}) \to (F (k) D F (j)) +_{𝑒} (F (j) D F (m)) < (\frac{x}{2}) +_{𝑒} (\frac{x}{2}))$
27	19 22 25 25 26	syl22anc	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to ((F (k) D F (j) < \frac{x}{2} \land F (j) D F (m) < \frac{x}{2}) \to (F (k) D F (j)) +_{𝑒} (F (j) D F (m)) < (\frac{x}{2}) +_{𝑒} (\frac{x}{2}))$
28	24 24	rexaddd	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to (\frac{x}{2}) +_{𝑒} (\frac{x}{2}) = (\frac{x}{2}) + (\frac{x}{2})$
29	23	recnd	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to x \in ℂ$
30	29	2halvesd	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to (\frac{x}{2}) + (\frac{x}{2}) = x$
31	28 30	eqtrd	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to (\frac{x}{2}) +_{𝑒} (\frac{x}{2}) = x$
32	31	breq2d	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to ((F (k) D F (j)) +_{𝑒} (F (j) D F (m)) < (\frac{x}{2}) +_{𝑒} (\frac{x}{2}) \leftrightarrow (F (k) D F (j)) +_{𝑒} (F (j) D F (m)) < x)$
33		xmettri	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X \land F (j) \in X)) \to F (k) D F (m) \leq (F (k) D F (j)) +_{𝑒} (F (j) D F (m))$
34	15 16 20 17 33	syl13anc	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to F (k) D F (m) \leq (F (k) D F (j)) +_{𝑒} (F (j) D F (m))$
35		xmetcl	$⊢ (D \in ∞Met (X) \land F (k) \in X \land F (m) \in X) \to F (k) D F (m) \in ℝ^{*}$
36	15 16 20 35	syl3anc	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to F (k) D F (m) \in ℝ^{*}$
37	19 22	xaddcld	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to (F (k) D F (j)) +_{𝑒} (F (j) D F (m)) \in ℝ^{*}$
38	23	rexrd	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to x \in ℝ^{*}$
39		xrlelttr	$⊢ (F (k) D F (m) \in ℝ^{} \land (F (k) D F (j)) +_{𝑒} (F (j) D F (m)) \in ℝ^{} \land x \in ℝ^{*}) \to ((F (k) D F (m) \leq (F (k) D F (j)) +_{𝑒} (F (j) D F (m)) \land (F (k) D F (j)) +_{𝑒} (F (j) D F (m)) < x) \to F (k) D F (m) < x)$
40	36 37 38 39	syl3anc	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to ((F (k) D F (m) \leq (F (k) D F (j)) +_{𝑒} (F (j) D F (m)) \land (F (k) D F (j)) +_{𝑒} (F (j) D F (m)) < x) \to F (k) D F (m) < x)$
41	34 40	mpand	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to ((F (k) D F (j)) +_{𝑒} (F (j) D F (m)) < x \to F (k) D F (m) < x)$
42	32 41	sylbid	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to ((F (k) D F (j)) +_{𝑒} (F (j) D F (m)) < (\frac{x}{2}) +_{𝑒} (\frac{x}{2}) \to F (k) D F (m) < x)$
43	27 42	syld	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to ((F (k) D F (j) < \frac{x}{2} \land F (j) D F (m) < \frac{x}{2}) \to F (k) D F (m) < x)$
44		ovex	$⊢ F (k) D F (j) \in V$
45		fvi	$⊢ F (k) D F (j) \in V \to I (F (k) D F (j)) = F (k) D F (j)$
46	44 45	ax-mp	$⊢ I (F (k) D F (j)) = F (k) D F (j)$
47	46	breq1i	$⊢ I (F (k) D F (j)) < \frac{x}{2} \leftrightarrow F (k) D F (j) < \frac{x}{2}$
48		ovex	$⊢ F (j) D F (m) \in V$
49		fvi	$⊢ F (j) D F (m) \in V \to I (F (j) D F (m)) = F (j) D F (m)$
50	48 49	ax-mp	$⊢ I (F (j) D F (m)) = F (j) D F (m)$
51	50	breq1i	$⊢ I (F (j) D F (m)) < \frac{x}{2} \leftrightarrow F (j) D F (m) < \frac{x}{2}$
52	47 51	anbi12i	$⊢ (I (F (k) D F (j)) < \frac{x}{2} \land I (F (j) D F (m)) < \frac{x}{2}) \leftrightarrow (F (k) D F (j) < \frac{x}{2} \land F (j) D F (m) < \frac{x}{2})$
53		ovex	$⊢ F (k) D F (m) \in V$
54		fvi	$⊢ F (k) D F (m) \in V \to I (F (k) D F (m)) = F (k) D F (m)$
55	53 54	ax-mp	$⊢ I (F (k) D F (m)) = F (k) D F (m)$
56	55	breq1i	$⊢ I (F (k) D F (m)) < x \leftrightarrow F (k) D F (m) < x$
57	43 52 56	3imtr4g	$⊢ (D \in ∞Met (X) \land (F (k) \in X \land F (m) \in X) \land (F (j) \in X \land x \in ℝ)) \to ((I (F (k) D F (j)) < \frac{x}{2} \land I (F (j) D F (m)) < \frac{x}{2}) \to I (F (k) D F (m)) < x)$
58	7 8 9 10 12 14 57	cau3lem	$⊢ D \in ∞Met (X) \to (\forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land I (F (k) D F (j)) < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} I (F (k) D F (m)) < x))$
59	6 58	syl	$⊢ (φ \land F \in (X ↑_{𝑝𝑚} ℂ)) \to (\forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land I (F (k) D F (j)) < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} I (F (k) D F (m)) < x))$
60	46	breq1i	$⊢ I (F (k) D F (j)) < x \leftrightarrow F (k) D F (j) < x$
61	60	anbi2i	$⊢ ((k \in dom F \land F (k) \in X) \land I (F (k) D F (j)) < x) \leftrightarrow ((k \in dom F \land F (k) \in X) \land F (k) D F (j) < x)$
62		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)$
63	61 62	bitr4i	$⊢ ((k \in dom F \land F (k) \in X) \land I (F (k) D F (j)) < x) \leftrightarrow (k \in dom F \land F (k) \in X \land F (k) D F (j) < x)$
64	63	ralbii	$⊢ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land I (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)$
65	64	rexbii	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land I (F (k) D F (j)) < x) \leftrightarrow \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	65	ralbii	$⊢ \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land I (F (k) D F (j)) < x) \leftrightarrow \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)$
67	56	ralbii	$⊢ \forall m \in ℤ_{\geq k} I (F (k) D F (m)) < x \leftrightarrow \forall m \in ℤ_{\geq k} F (k) D F (m) < x$
68	67	anbi2i	$⊢ ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} I (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)$
69		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)$
70	68 69	bitr4i	$⊢ ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} I (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)$
71	70	ralbii	$⊢ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} I (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)$
72	71	rexbii	$⊢ \exists j \in ℤ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} I (F (k) D F (m)) < x) \leftrightarrow \exists j \in ℤ \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)$
73	72	ralbii	$⊢ \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} ((k \in dom F \land F (k) \in X) \land \forall m \in ℤ_{\geq k} I (F (k) D F (m)) < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \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)$
74	59 66 73	3bitr3g	$⊢ (φ \land F \in (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) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \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))$
75	3	adantr	$⊢ (φ \land F \in (X ↑_{𝑝𝑚} ℂ)) \to M \in ℤ$
76	1	rexuz3	$⊢ M \in ℤ \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) \leftrightarrow \exists j \in ℤ \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))$
77	75 76	syl	$⊢ (φ \land F \in (X ↑_{𝑝𝑚} ℂ)) \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) \leftrightarrow \exists j \in ℤ \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))$
78	77	ralbidv	$⊢ (φ \land F \in (X ↑_{𝑝𝑚} ℂ)) \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) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \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))$
79	74 78	bitr4d	$⊢ (φ \land F \in (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) \leftrightarrow \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))$
80	79	pm5.32da	$⊢ φ \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)) \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)))$
81	5 80	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 F (k) \in X \land \forall m \in ℤ_{\geq k} F (k) D F (m) < x)))$

Metamath Proof Explorer

Theorem iscau3

Proof