iscmet3lem1

	Ref	Expression
Hypotheses	iscmet3.1	$⊢ Z = ℤ_{\geq M}$
	iscmet3.2	$⊢ J = MetOpen (D)$
	iscmet3.3	$⊢ φ \to M \in ℤ$
	iscmet3.4	$⊢ φ \to D \in Met (X)$
	iscmet3.6	$⊢ φ \to F : Z ⟶ X$
	iscmet3.9	$⊢ φ \to \forall k \in ℤ \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}$
	iscmet3.10	$⊢ φ \to \forall k \in Z \forall n \in (M \dots k) F (k) \in S (n)$
Assertion	iscmet3lem1	$⊢ φ \to F \in Cau (D)$

Proof

Step	Hyp	Ref	Expression
1		iscmet3.1	$⊢ Z = ℤ_{\geq M}$
2		iscmet3.2	$⊢ J = MetOpen (D)$
3		iscmet3.3	$⊢ φ \to M \in ℤ$
4		iscmet3.4	$⊢ φ \to D \in Met (X)$
5		iscmet3.6	$⊢ φ \to F : Z ⟶ X$
6		iscmet3.9	$⊢ φ \to \forall k \in ℤ \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}$
7		iscmet3.10	$⊢ φ \to \forall k \in Z \forall n \in (M \dots k) F (k) \in S (n)$
8	1	iscmet3lem3	$⊢ (M \in ℤ \land r \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < r$
9	3 8	sylan	$⊢ (φ \land r \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < r$
10	1	r19.2uz	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} {(\frac{1}{2})}^{k} < r \to \exists k \in Z {(\frac{1}{2})}^{k} < r$
11	9 10	syl	$⊢ (φ \land r \in ℝ^{+}) \to \exists k \in Z {(\frac{1}{2})}^{k} < r$
12		fveq2	$⊢ n = k \to S (n) = S (k)$
13	12	eleq2d	$⊢ n = k \to (F (k) \in S (n) \leftrightarrow F (k) \in S (k))$
14	7	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to \forall k \in Z \forall n \in (M \dots k) F (k) \in S (n)$
15		simpl	$⊢ (k \in Z \land j \in ℤ_{\geq k}) \to k \in Z$
16	15	adantl	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to k \in Z$
17		rsp	$⊢ \forall k \in Z \forall n \in (M \dots k) F (k) \in S (n) \to (k \in Z \to \forall n \in (M \dots k) F (k) \in S (n))$
18	14 16 17	sylc	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to \forall n \in (M \dots k) F (k) \in S (n)$
19	16 1	eleqtrdi	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to k \in ℤ_{\geq M}$
20		eluzfz2	$⊢ k \in ℤ_{\geq M} \to k \in (M \dots k)$
21	19 20	syl	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to k \in (M \dots k)$
22	13 18 21	rspcdva	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to F (k) \in S (k)$
23	12	eleq2d	$⊢ n = k \to (F (j) \in S (n) \leftrightarrow F (j) \in S (k))$
24		oveq2	$⊢ k = j \to (M \dots k) = (M \dots j)$
25		fveq2	$⊢ k = j \to F (k) = F (j)$
26	25	eleq1d	$⊢ k = j \to (F (k) \in S (n) \leftrightarrow F (j) \in S (n))$
27	24 26	raleqbidv	$⊢ k = j \to (\forall n \in (M \dots k) F (k) \in S (n) \leftrightarrow \forall n \in (M \dots j) F (j) \in S (n))$
28	1	uztrn2	$⊢ (k \in Z \land j \in ℤ_{\geq k}) \to j \in Z$
29	28	adantl	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to j \in Z$
30	27 14 29	rspcdva	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to \forall n \in (M \dots j) F (j) \in S (n)$
31		simprr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to j \in ℤ_{\geq k}$
32		elfzuzb	$⊢ k \in (M \dots j) \leftrightarrow (k \in ℤ_{\geq M} \land j \in ℤ_{\geq k})$
33	19 31 32	sylanbrc	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to k \in (M \dots j)$
34	23 30 33	rspcdva	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to F (j) \in S (k)$
35	6	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to \forall k \in ℤ \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}$
36		eluzelz	$⊢ k \in ℤ_{\geq M} \to k \in ℤ$
37	36 1	eleq2s	$⊢ k \in Z \to k \in ℤ$
38	37	ad2antrl	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to k \in ℤ$
39		rsp	$⊢ \forall k \in ℤ \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k} \to (k \in ℤ \to \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k})$
40	35 38 39	sylc	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}$
41		oveq1	$⊢ u = F (k) \to u D v = F (k) D v$
42	41	breq1d	$⊢ u = F (k) \to (u D v < {(\frac{1}{2})}^{k} \leftrightarrow F (k) D v < {(\frac{1}{2})}^{k})$
43		oveq2	$⊢ v = F (j) \to F (k) D v = F (k) D F (j)$
44	43	breq1d	$⊢ v = F (j) \to (F (k) D v < {(\frac{1}{2})}^{k} \leftrightarrow F (k) D F (j) < {(\frac{1}{2})}^{k})$
45	42 44	rspc2va	$⊢ ((F (k) \in S (k) \land F (j) \in S (k)) \land \forall u \in S (k) \forall v \in S (k) u D v < {(\frac{1}{2})}^{k}) \to F (k) D F (j) < {(\frac{1}{2})}^{k}$
46	22 34 40 45	syl21anc	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to F (k) D F (j) < {(\frac{1}{2})}^{k}$
47	4	ad2antrr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to D \in Met (X)$
48	5	adantr	$⊢ (φ \land r \in ℝ^{+}) \to F : Z ⟶ X$
49		ffvelrn	$⊢ (F : Z ⟶ X \land k \in Z) \to F (k) \in X$
50	48 15 49	syl2an	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to F (k) \in X$
51		ffvelrn	$⊢ (F : Z ⟶ X \land j \in Z) \to F (j) \in X$
52	48 28 51	syl2an	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to F (j) \in X$
53		metcl	$⊢ (D \in Met (X) \land F (k) \in X \land F (j) \in X) \to F (k) D F (j) \in ℝ$
54	47 50 52 53	syl3anc	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to F (k) D F (j) \in ℝ$
55		1rp	$⊢ 1 \in ℝ^{+}$
56		rphalfcl	$⊢ 1 \in ℝ^{+} \to \frac{1}{2} \in ℝ^{+}$
57	55 56	ax-mp	$⊢ \frac{1}{2} \in ℝ^{+}$
58		rpexpcl	$⊢ (\frac{1}{2} \in ℝ^{+} \land k \in ℤ) \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
59	57 38 58	sylancr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to {(\frac{1}{2})}^{k} \in ℝ^{+}$
60	59	rpred	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to {(\frac{1}{2})}^{k} \in ℝ$
61		rpre	$⊢ r \in ℝ^{+} \to r \in ℝ$
62	61	ad2antlr	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to r \in ℝ$
63		lttr	$⊢ (F (k) D F (j) \in ℝ \land {(\frac{1}{2})}^{k} \in ℝ \land r \in ℝ) \to ((F (k) D F (j) < {(\frac{1}{2})}^{k} \land {(\frac{1}{2})}^{k} < r) \to F (k) D F (j) < r)$
64	54 60 62 63	syl3anc	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to ((F (k) D F (j) < {(\frac{1}{2})}^{k} \land {(\frac{1}{2})}^{k} < r) \to F (k) D F (j) < r)$
65	46 64	mpand	$⊢ ((φ \land r \in ℝ^{+}) \land (k \in Z \land j \in ℤ_{\geq k})) \to ({(\frac{1}{2})}^{k} < r \to F (k) D F (j) < r)$
66	65	anassrs	$⊢ (((φ \land r \in ℝ^{+}) \land k \in Z) \land j \in ℤ_{\geq k}) \to ({(\frac{1}{2})}^{k} < r \to F (k) D F (j) < r)$
67	66	ralrimdva	$⊢ ((φ \land r \in ℝ^{+}) \land k \in Z) \to ({(\frac{1}{2})}^{k} < r \to \forall j \in ℤ_{\geq k} F (k) D F (j) < r)$
68	67	reximdva	$⊢ (φ \land r \in ℝ^{+}) \to (\exists k \in Z {(\frac{1}{2})}^{k} < r \to \exists k \in Z \forall j \in ℤ_{\geq k} F (k) D F (j) < r)$
69	11 68	mpd	$⊢ (φ \land r \in ℝ^{+}) \to \exists k \in Z \forall j \in ℤ_{\geq k} F (k) D F (j) < r$
70	69	ralrimiva	$⊢ φ \to \forall r \in ℝ^{+} \exists k \in Z \forall j \in ℤ_{\geq k} F (k) D F (j) < r$
71		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
72	4 71	syl	$⊢ φ \to D \in ∞Met (X)$
73		eqidd	$⊢ (φ \land j \in Z) \to F (j) = F (j)$
74		eqidd	$⊢ (φ \land k \in Z) \to F (k) = F (k)$
75	1 72 3 73 74 5	iscauf	$⊢ φ \to (F \in Cau (D) \leftrightarrow \forall r \in ℝ^{+} \exists k \in Z \forall j \in ℤ_{\geq k} F (k) D F (j) < r)$
76	70 75	mpbird	$⊢ φ \to F \in Cau (D)$

Metamath Proof Explorer

Theorem iscmet3lem1

Proof