ulmcaulem

Description: Lemma for ulmcau and ulmcau2 : show the equivalence of the four- and five-quantifier forms of the Cauchy convergence condition. Compare cau3 . (Contributed by Mario Carneiro, 1-Mar-2015)

	Ref	Expression
Hypotheses	ulmcau.z	$⊢ Z = ℤ_{\geq M}$
	ulmcau.m	$⊢ φ \to M \in ℤ$
	ulmcau.s	$⊢ φ \to S \in V$
	ulmcau.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
Assertion	ulmcaulem	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$

Proof

Step	Hyp	Ref	Expression
1		ulmcau.z	$⊢ Z = ℤ_{\geq M}$
2		ulmcau.m	$⊢ φ \to M \in ℤ$
3		ulmcau.s	$⊢ φ \to S \in V$
4		ulmcau.f	$⊢ φ \to F : Z ⟶ ℂ^{S}$
5		breq2	$⊢ x = w \to (\|F (k) (z) - F (j) (z)\| < x \leftrightarrow \|F (k) (z) - F (j) (z)\| < w)$
6	5	ralbidv	$⊢ x = w \to (\forall z \in S \|F (k) (z) - F (j) (z)\| < x \leftrightarrow \forall z \in S \|F (k) (z) - F (j) (z)\| < w)$
7	6	rexralbidv	$⊢ x = w \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < w)$
8	7	cbvralvw	$⊢ \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \leftrightarrow \forall w \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < w$
9		rphalfcl	$⊢ x \in ℝ^{+} \to \frac{x}{2} \in ℝ^{+}$
10		breq2	$⊢ w = \frac{x}{2} \to (\|F (k) (z) - F (j) (z)\| < w \leftrightarrow \|F (k) (z) - F (j) (z)\| < \frac{x}{2})$
11	10	ralbidv	$⊢ w = \frac{x}{2} \to (\forall z \in S \|F (k) (z) - F (j) (z)\| < w \leftrightarrow \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2})$
12	11	rexralbidv	$⊢ w = \frac{x}{2} \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < w \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2})$
13	12	rspcv	$⊢ \frac{x}{2} \in ℝ^{+} \to (\forall w \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < w \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2})$
14	9 13	syl	$⊢ x \in ℝ^{+} \to (\forall w \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < w \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2})$
15	14	adantl	$⊢ (φ \land x \in ℝ^{+}) \to (\forall w \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < w \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2})$
16		fveq2	$⊢ k = m \to F (k) = F (m)$
17	16	fveq1d	$⊢ k = m \to F (k) (z) = F (m) (z)$
18	17	fvoveq1d	$⊢ k = m \to \|F (k) (z) - F (j) (z)\| = \|F (m) (z) - F (j) (z)\|$
19	18	breq1d	$⊢ k = m \to (\|F (k) (z) - F (j) (z)\| < \frac{x}{2} \leftrightarrow \|F (m) (z) - F (j) (z)\| < \frac{x}{2})$
20	19	ralbidv	$⊢ k = m \to (\forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \leftrightarrow \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2})$
21	20	cbvralvw	$⊢ \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \leftrightarrow \forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2}$
22	21	biimpi	$⊢ \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \to \forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2}$
23		uzss	$⊢ k \in ℤ_{\geq j} \to ℤ_{\geq k} \subseteq ℤ_{\geq j}$
24	23	ad2antlr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2}) \to ℤ_{\geq k} \subseteq ℤ_{\geq j}$
25		ssralv	$⊢ ℤ_{\geq k} \subseteq ℤ_{\geq j} \to (\forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2} \to \forall m \in ℤ_{\geq k} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2})$
26	24 25	syl	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2}) \to (\forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2} \to \forall m \in ℤ_{\geq k} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2})$
27		r19.26	$⊢ \forall z \in S (\|F (k) (z) - F (j) (z)\| < \frac{x}{2} \land \|F (m) (z) - F (j) (z)\| < \frac{x}{2}) \leftrightarrow (\forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \land \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2})$
28	4	adantr	$⊢ (φ \land x \in ℝ^{+}) \to F : Z ⟶ ℂ^{S}$
29	28	ad3antrrr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to F : Z ⟶ ℂ^{S}$
30	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
31	30	adantll	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
32	1	uztrn2	$⊢ (k \in Z \land m \in ℤ_{\geq k}) \to m \in Z$
33	31 32	sylan	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to m \in Z$
34	29 33	ffvelcdmd	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to F (m) \in (ℂ^{S})$
35		elmapi	$⊢ F (m) \in (ℂ^{S}) \to F (m) : S ⟶ ℂ$
36	34 35	syl	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to F (m) : S ⟶ ℂ$
37	36	ffvelcdmda	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land z \in S) \to F (m) (z) \in ℂ$
38	28	ffvelcdmda	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to F (j) \in (ℂ^{S})$
39	38	ad2antrr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to F (j) \in (ℂ^{S})$
40		elmapi	$⊢ F (j) \in (ℂ^{S}) \to F (j) : S ⟶ ℂ$
41	39 40	syl	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to F (j) : S ⟶ ℂ$
42	41	ffvelcdmda	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land z \in S) \to F (j) (z) \in ℂ$
43	37 42	abssubd	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land z \in S) \to \|F (m) (z) - F (j) (z)\| = \|F (j) (z) - F (m) (z)\|$
44	43	breq1d	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land z \in S) \to (\|F (m) (z) - F (j) (z)\| < \frac{x}{2} \leftrightarrow \|F (j) (z) - F (m) (z)\| < \frac{x}{2})$
45	44	biimpd	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land z \in S) \to (\|F (m) (z) - F (j) (z)\| < \frac{x}{2} \to \|F (j) (z) - F (m) (z)\| < \frac{x}{2})$
46		ffvelcdm	$⊢ (F : Z ⟶ ℂ^{S} \land k \in Z) \to F (k) \in (ℂ^{S})$
47	28 30 46	syl2an	$⊢ ((φ \land x \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \in (ℂ^{S})$
48	47	anassrs	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in (ℂ^{S})$
49	48	adantr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to F (k) \in (ℂ^{S})$
50		elmapi	$⊢ F (k) \in (ℂ^{S}) \to F (k) : S ⟶ ℂ$
51	49 50	syl	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to F (k) : S ⟶ ℂ$
52	51	ffvelcdmda	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land z \in S) \to F (k) (z) \in ℂ$
53		rpre	$⊢ x \in ℝ^{+} \to x \in ℝ$
54	53	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to x \in ℝ$
55	54	ad3antrrr	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land z \in S) \to x \in ℝ$
56		abs3lem	$⊢ ((F (k) (z) \in ℂ \land F (m) (z) \in ℂ) \land (F (j) (z) \in ℂ \land x \in ℝ)) \to ((\|F (k) (z) - F (j) (z)\| < \frac{x}{2} \land \|F (j) (z) - F (m) (z)\| < \frac{x}{2}) \to \|F (k) (z) - F (m) (z)\| < x)$
57	52 37 42 55 56	syl22anc	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land z \in S) \to ((\|F (k) (z) - F (j) (z)\| < \frac{x}{2} \land \|F (j) (z) - F (m) (z)\| < \frac{x}{2}) \to \|F (k) (z) - F (m) (z)\| < x)$
58	45 57	sylan2d	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land z \in S) \to ((\|F (k) (z) - F (j) (z)\| < \frac{x}{2} \land \|F (m) (z) - F (j) (z)\| < \frac{x}{2}) \to \|F (k) (z) - F (m) (z)\| < x)$
59	58	ralimdva	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to (\forall z \in S (\|F (k) (z) - F (j) (z)\| < \frac{x}{2} \land \|F (m) (z) - F (j) (z)\| < \frac{x}{2}) \to \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
60	27 59	biimtrrid	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \to ((\forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \land \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2}) \to \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
61	60	expdimp	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land m \in ℤ_{\geq k}) \land \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2}) \to (\forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2} \to \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
62	61	an32s	$⊢ (((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2}) \land m \in ℤ_{\geq k}) \to (\forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2} \to \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
63	62	ralimdva	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2}) \to (\forall m \in ℤ_{\geq k} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2} \to \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
64	26 63	syld	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2}) \to (\forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2} \to \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
65	64	impancom	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \land \forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2}) \to (\forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \to \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
66	65	an32s	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2}) \land k \in ℤ_{\geq j}) \to (\forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \to \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
67	66	ralimdva	$⊢ (((φ \land x \in ℝ^{+}) \land j \in Z) \land \forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2}) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
68	67	ex	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2} \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x))$
69	68	com23	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \to (\forall m \in ℤ_{\geq j} \forall z \in S \|F (m) (z) - F (j) (z)\| < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x))$
70	22 69	mpdi	$⊢ ((φ \land x \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \to \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
71	70	reximdva	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < \frac{x}{2} \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
72	15 71	syld	$⊢ (φ \land x \in ℝ^{+}) \to (\forall w \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < w \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
73	72	ralrimdva	$⊢ φ \to (\forall w \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < w \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
74	8 73	biimtrid	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$
75		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
76	75 1	eleq2s	$⊢ j \in Z \to j \in ℤ$
77		uzid	$⊢ j \in ℤ \to j \in ℤ_{\geq j}$
78	76 77	syl	$⊢ j \in Z \to j \in ℤ_{\geq j}$
79	78	adantl	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq j}$
80		fveq2	$⊢ k = j \to ℤ_{\geq k} = ℤ_{\geq j}$
81		fveq2	$⊢ k = j \to F (k) = F (j)$
82	81	fveq1d	$⊢ k = j \to F (k) (z) = F (j) (z)$
83	82	fvoveq1d	$⊢ k = j \to \|F (k) (z) - F (m) (z)\| = \|F (j) (z) - F (m) (z)\|$
84	83	breq1d	$⊢ k = j \to (\|F (k) (z) - F (m) (z)\| < x \leftrightarrow \|F (j) (z) - F (m) (z)\| < x)$
85	84	ralbidv	$⊢ k = j \to (\forall z \in S \|F (k) (z) - F (m) (z)\| < x \leftrightarrow \forall z \in S \|F (j) (z) - F (m) (z)\| < x)$
86	80 85	raleqbidv	$⊢ k = j \to (\forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \leftrightarrow \forall m \in ℤ_{\geq j} \forall z \in S \|F (j) (z) - F (m) (z)\| < x)$
87	86	rspcv	$⊢ j \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \to \forall m \in ℤ_{\geq j} \forall z \in S \|F (j) (z) - F (m) (z)\| < x)$
88	79 87	syl	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \to \forall m \in ℤ_{\geq j} \forall z \in S \|F (j) (z) - F (m) (z)\| < x)$
89		fveq2	$⊢ m = k \to F (m) = F (k)$
90	89	fveq1d	$⊢ m = k \to F (m) (z) = F (k) (z)$
91	90	oveq2d	$⊢ m = k \to F (j) (z) - F (m) (z) = F (j) (z) - F (k) (z)$
92	91	fveq2d	$⊢ m = k \to \|F (j) (z) - F (m) (z)\| = \|F (j) (z) - F (k) (z)\|$
93	92	breq1d	$⊢ m = k \to (\|F (j) (z) - F (m) (z)\| < x \leftrightarrow \|F (j) (z) - F (k) (z)\| < x)$
94	93	ralbidv	$⊢ m = k \to (\forall z \in S \|F (j) (z) - F (m) (z)\| < x \leftrightarrow \forall z \in S \|F (j) (z) - F (k) (z)\| < x)$
95	94	cbvralvw	$⊢ \forall m \in ℤ_{\geq j} \forall z \in S \|F (j) (z) - F (m) (z)\| < x \leftrightarrow \forall k \in ℤ_{\geq j} \forall z \in S \|F (j) (z) - F (k) (z)\| < x$
96	4	ffvelcdmda	$⊢ (φ \land j \in Z) \to F (j) \in (ℂ^{S})$
97	96	adantr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (j) \in (ℂ^{S})$
98	97 40	syl	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (j) : S ⟶ ℂ$
99	98	ffvelcdmda	$⊢ (((φ \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to F (j) (z) \in ℂ$
100	4 30 46	syl2an	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to F (k) \in (ℂ^{S})$
101	100	anassrs	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in (ℂ^{S})$
102	101 50	syl	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) : S ⟶ ℂ$
103	102	ffvelcdmda	$⊢ (((φ \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to F (k) (z) \in ℂ$
104	99 103	abssubd	$⊢ (((φ \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to \|F (j) (z) - F (k) (z)\| = \|F (k) (z) - F (j) (z)\|$
105	104	breq1d	$⊢ (((φ \land j \in Z) \land k \in ℤ_{\geq j}) \land z \in S) \to (\|F (j) (z) - F (k) (z)\| < x \leftrightarrow \|F (k) (z) - F (j) (z)\| < x)$
106	105	ralbidva	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (\forall z \in S \|F (j) (z) - F (k) (z)\| < x \leftrightarrow \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
107	106	ralbidva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall z \in S \|F (j) (z) - F (k) (z)\| < x \leftrightarrow \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
108	95 107	bitrid	$⊢ (φ \land j \in Z) \to (\forall m \in ℤ_{\geq j} \forall z \in S \|F (j) (z) - F (m) (z)\| < x \leftrightarrow \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
109	88 108	sylibd	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \to \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
110	109	reximdva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \to \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
111	110	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x)$
112	74 111	impbid	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall z \in S \|F (k) (z) - F (j) (z)\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \forall m \in ℤ_{\geq k} \forall z \in S \|F (k) (z) - F (m) (z)\| < x)$

Metamath Proof Explorer

Theorem ulmcaulem

Proof