minvecolem3

Description: Lemma for minveco . The sequence formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014) (Revised by AV, 4-Oct-2020) (New usage is discouraged.)

	Ref	Expression
Hypotheses	minveco.x	$⊢ X = BaseSet (U)$
	minveco.m	$⊢ M = -_{v} (U)$
	minveco.n	$⊢ N = {norm}_{CV} (U)$
	minveco.y	$⊢ Y = BaseSet (W)$
	minveco.u	$⊢ φ \to U \in {CPreHil}_{OLD}$
	minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
	minveco.a	$⊢ φ \to A \in X$
	minveco.d	$⊢ D = IndMet (U)$
	minveco.j	$⊢ J = MetOpen (D)$
	minveco.r	$⊢ R = ran (y \in Y ⟼ N (A M y))$
	minveco.s	$⊢ S = sup (R ℝ <)$
	minveco.f	$⊢ φ \to F : ℕ ⟶ Y$
	minveco.1	$⊢ (φ \land n \in ℕ) \to {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n})$
Assertion	minvecolem3	$⊢ φ \to F \in Cau (D)$

Proof

Step	Hyp	Ref	Expression
1		minveco.x	$⊢ X = BaseSet (U)$
2		minveco.m	$⊢ M = -_{v} (U)$
3		minveco.n	$⊢ N = {norm}_{CV} (U)$
4		minveco.y	$⊢ Y = BaseSet (W)$
5		minveco.u	$⊢ φ \to U \in {CPreHil}_{OLD}$
6		minveco.w	$⊢ φ \to W \in (SubSp (U) \cap CBan)$
7		minveco.a	$⊢ φ \to A \in X$
8		minveco.d	$⊢ D = IndMet (U)$
9		minveco.j	$⊢ J = MetOpen (D)$
10		minveco.r	$⊢ R = ran (y \in Y ⟼ N (A M y))$
11		minveco.s	$⊢ S = sup (R ℝ <)$
12		minveco.f	$⊢ φ \to F : ℕ ⟶ Y$
13		minveco.1	$⊢ (φ \land n \in ℕ) \to {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n})$
14		4re	$⊢ 4 \in ℝ$
15		4pos	$⊢ 0 < 4$
16	14 15	elrpii	$⊢ 4 \in ℝ^{+}$
17		simpr	$⊢ (φ \land x \in ℝ^{+}) \to x \in ℝ^{+}$
18		2z	$⊢ 2 \in ℤ$
19		rpexpcl	$⊢ (x \in ℝ^{+} \land 2 \in ℤ) \to x^{2} \in ℝ^{+}$
20	17 18 19	sylancl	$⊢ (φ \land x \in ℝ^{+}) \to x^{2} \in ℝ^{+}$
21		rpdivcl	$⊢ (4 \in ℝ^{+} \land x^{2} \in ℝ^{+}) \to \frac{4}{x^{2}} \in ℝ^{+}$
22	16 20 21	sylancr	$⊢ (φ \land x \in ℝ^{+}) \to \frac{4}{x^{2}} \in ℝ^{+}$
23		rprege0	$⊢ \frac{4}{x^{2}} \in ℝ^{+} \to (\frac{4}{x^{2}} \in ℝ \land 0 \leq \frac{4}{x^{2}})$
24		flge0nn0	$⊢ (\frac{4}{x^{2}} \in ℝ \land 0 \leq \frac{4}{x^{2}}) \to ⌊\frac{4}{x^{2}}⌋ \in ℕ_{0}$
25		nn0p1nn	$⊢ ⌊\frac{4}{x^{2}}⌋ \in ℕ_{0} \to ⌊\frac{4}{x^{2}}⌋ + 1 \in ℕ$
26	22 23 24 25	4syl	$⊢ (φ \land x \in ℝ^{+}) \to ⌊\frac{4}{x^{2}}⌋ + 1 \in ℕ$
27		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
28	1 8	imsmet	$⊢ U \in NrmCVec \to D \in Met (X)$
29	5 27 28	3syl	$⊢ φ \to D \in Met (X)$
30	29	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to D \in Met (X)$
31	5 27	syl	$⊢ φ \to U \in NrmCVec$
32		inss1	$⊢ SubSp (U) \cap CBan \subseteq SubSp (U)$
33	32 6	sseldi	$⊢ φ \to W \in SubSp (U)$
34		eqid	$⊢ SubSp (U) = SubSp (U)$
35	1 4 34	sspba	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to Y \subseteq X$
36	31 33 35	syl2anc	$⊢ φ \to Y \subseteq X$
37	36	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to Y \subseteq X$
38	12	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to F : ℕ ⟶ Y$
39	26	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to ⌊\frac{4}{x^{2}}⌋ + 1 \in ℕ$
40	38 39	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to F (⌊\frac{4}{x^{2}}⌋ + 1) \in Y$
41	37 40	sseldd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to F (⌊\frac{4}{x^{2}}⌋ + 1) \in X$
42		eluznn	$⊢ (⌊\frac{4}{x^{2}}⌋ + 1 \in ℕ \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to n \in ℕ$
43	26 42	sylan	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to n \in ℕ$
44	38 43	ffvelrnd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to F (n) \in Y$
45	37 44	sseldd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to F (n) \in X$
46		metcl	$⊢ (D \in Met (X) \land F (⌊\frac{4}{x^{2}}⌋ + 1) \in X \land F (n) \in X) \to F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) \in ℝ$
47	30 41 45 46	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) \in ℝ$
48	47	resqcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to {(F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n))}^{2} \in ℝ$
49	39	nnrpd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to ⌊\frac{4}{x^{2}}⌋ + 1 \in ℝ^{+}$
50	49	rpreccld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} \in ℝ^{+}$
51		rpmulcl	$⊢ (4 \in ℝ^{+} \land \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} \in ℝ^{+}) \to 4 (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}) \in ℝ^{+}$
52	16 50 51	sylancr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to 4 (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}) \in ℝ^{+}$
53	52	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to 4 (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}) \in ℝ$
54	20	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to x^{2} \in ℝ^{+}$
55	54	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to x^{2} \in ℝ$
56	5	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to U \in {CPreHil}_{OLD}$
57	6	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to W \in (SubSp (U) \cap CBan)$
58	7	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to A \in X$
59	26	nnrpd	$⊢ (φ \land x \in ℝ^{+}) \to ⌊\frac{4}{x^{2}}⌋ + 1 \in ℝ^{+}$
60	59	rpreccld	$⊢ (φ \land x \in ℝ^{+}) \to \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} \in ℝ^{+}$
61	60	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} \in ℝ^{+}$
62	61	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} \in ℝ$
63	61	rpge0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to 0 \leq \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}$
64	12	adantr	$⊢ (φ \land x \in ℝ^{+}) \to F : ℕ ⟶ Y$
65	64	ffvelrnda	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℕ) \to F (n) \in Y$
66	43 65	syldan	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to F (n) \in Y$
67		fveq2	$⊢ n = ⌊\frac{4}{x^{2}}⌋ + 1 \to F (n) = F (⌊\frac{4}{x^{2}}⌋ + 1)$
68	67	oveq2d	$⊢ n = ⌊\frac{4}{x^{2}}⌋ + 1 \to A D F (n) = A D F (⌊\frac{4}{x^{2}}⌋ + 1)$
69	68	oveq1d	$⊢ n = ⌊\frac{4}{x^{2}}⌋ + 1 \to {(A D F (n))}^{2} = {(A D F (⌊\frac{4}{x^{2}}⌋ + 1))}^{2}$
70		oveq2	$⊢ n = ⌊\frac{4}{x^{2}}⌋ + 1 \to \frac{1}{n} = \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}$
71	70	oveq2d	$⊢ n = ⌊\frac{4}{x^{2}}⌋ + 1 \to S^{2} + (\frac{1}{n}) = S^{2} + (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1})$
72	69 71	breq12d	$⊢ n = ⌊\frac{4}{x^{2}}⌋ + 1 \to ({(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n}) \leftrightarrow {(A D F (⌊\frac{4}{x^{2}}⌋ + 1))}^{2} \leq S^{2} + (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}))$
73	13	ralrimiva	$⊢ φ \to \forall n \in ℕ {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n})$
74	73	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \forall n \in ℕ {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n})$
75	72 74 39	rspcdva	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to {(A D F (⌊\frac{4}{x^{2}}⌋ + 1))}^{2} \leq S^{2} + (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1})$
76	37 66	sseldd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to F (n) \in X$
77		metcl	$⊢ (D \in Met (X) \land A \in X \land F (n) \in X) \to A D F (n) \in ℝ$
78	30 58 76 77	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to A D F (n) \in ℝ$
79	78	resqcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to {(A D F (n))}^{2} \in ℝ$
80	1 2 3 4 5 6 7 8 9 10	minvecolem1	$⊢ φ \to (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w)$
81		0re	$⊢ 0 \in ℝ$
82		breq1	$⊢ x = 0 \to (x \leq w \leftrightarrow 0 \leq w)$
83	82	ralbidv	$⊢ x = 0 \to (\forall w \in R x \leq w \leftrightarrow \forall w \in R 0 \leq w)$
84	83	rspcev	$⊢ (0 \in ℝ \land \forall w \in R 0 \leq w) \to \exists x \in ℝ \forall w \in R x \leq w$
85	81 84	mpan	$⊢ \forall w \in R 0 \leq w \to \exists x \in ℝ \forall w \in R x \leq w$
86	85	3anim3i	$⊢ (R \subseteq ℝ \land R \neq \emptyset \land \forall w \in R 0 \leq w) \to (R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w)$
87		infrecl	$⊢ (R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \to sup (R ℝ <) \in ℝ$
88	80 86 87	3syl	$⊢ φ \to sup (R ℝ <) \in ℝ$
89	11 88	eqeltrid	$⊢ φ \to S \in ℝ$
90	89	resqcld	$⊢ φ \to S^{2} \in ℝ$
91	90	ad2antrr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to S^{2} \in ℝ$
92	43	nnrecred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{1}{n} \in ℝ$
93	91 92	readdcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to S^{2} + (\frac{1}{n}) \in ℝ$
94	91 62	readdcld	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to S^{2} + (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}) \in ℝ$
95	13	adantlr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℕ) \to {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n})$
96	43 95	syldan	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n})$
97		eluzle	$⊢ n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)} \to ⌊\frac{4}{x^{2}}⌋ + 1 \leq n$
98	97	adantl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to ⌊\frac{4}{x^{2}}⌋ + 1 \leq n$
99	49	rpregt0d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to (⌊\frac{4}{x^{2}}⌋ + 1 \in ℝ \land 0 < ⌊\frac{4}{x^{2}}⌋ + 1)$
100		nnre	$⊢ n \in ℕ \to n \in ℝ$
101		nngt0	$⊢ n \in ℕ \to 0 < n$
102	100 101	jca	$⊢ n \in ℕ \to (n \in ℝ \land 0 < n)$
103	43 102	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to (n \in ℝ \land 0 < n)$
104		lerec	$⊢ ((⌊\frac{4}{x^{2}}⌋ + 1 \in ℝ \land 0 < ⌊\frac{4}{x^{2}}⌋ + 1) \land (n \in ℝ \land 0 < n)) \to (⌊\frac{4}{x^{2}}⌋ + 1 \leq n \leftrightarrow \frac{1}{n} \leq \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1})$
105	99 103 104	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to (⌊\frac{4}{x^{2}}⌋ + 1 \leq n \leftrightarrow \frac{1}{n} \leq \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1})$
106	98 105	mpbid	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{1}{n} \leq \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}$
107	92 62 91 106	leadd2dd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to S^{2} + (\frac{1}{n}) \leq S^{2} + (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1})$
108	79 93 94 96 107	letrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1})$
109	1 2 3 4 56 57 58 8 9 10 11 62 63 40 66 75 108	minvecolem2	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to {(F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n))}^{2} \leq 4 (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1})$
110		rpdivcl	$⊢ (x^{2} \in ℝ^{+} \land 4 \in ℝ^{+}) \to \frac{x^{2}}{4} \in ℝ^{+}$
111	54 16 110	sylancl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{x^{2}}{4} \in ℝ^{+}$
112		rpcnne0	$⊢ x^{2} \in ℝ^{+} \to (x^{2} \in ℂ \land x^{2} \neq 0)$
113	54 112	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to (x^{2} \in ℂ \land x^{2} \neq 0)$
114		rpcnne0	$⊢ 4 \in ℝ^{+} \to (4 \in ℂ \land 4 \neq 0)$
115	16 114	ax-mp	$⊢ (4 \in ℂ \land 4 \neq 0)$
116		recdiv	$⊢ ((x^{2} \in ℂ \land x^{2} \neq 0) \land (4 \in ℂ \land 4 \neq 0)) \to \frac{1}{\frac{x^{2}}{4}} = \frac{4}{x^{2}}$
117	113 115 116	sylancl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{1}{\frac{x^{2}}{4}} = \frac{4}{x^{2}}$
118	22	adantr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{4}{x^{2}} \in ℝ^{+}$
119	118	rpred	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{4}{x^{2}} \in ℝ$
120		flltp1	$⊢ \frac{4}{x^{2}} \in ℝ \to \frac{4}{x^{2}} < ⌊\frac{4}{x^{2}}⌋ + 1$
121	119 120	syl	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{4}{x^{2}} < ⌊\frac{4}{x^{2}}⌋ + 1$
122	117 121	eqbrtrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{1}{\frac{x^{2}}{4}} < ⌊\frac{4}{x^{2}}⌋ + 1$
123	111 49 122	ltrec1d	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} < \frac{x^{2}}{4}$
124	14 15	pm3.2i	$⊢ (4 \in ℝ \land 0 < 4)$
125		ltmuldiv2	$⊢ (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} \in ℝ \land x^{2} \in ℝ \land (4 \in ℝ \land 0 < 4)) \to (4 (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}) < x^{2} \leftrightarrow \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} < \frac{x^{2}}{4})$
126	124 125	mp3an3	$⊢ (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} \in ℝ \land x^{2} \in ℝ) \to (4 (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}) < x^{2} \leftrightarrow \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} < \frac{x^{2}}{4})$
127	62 55 126	syl2anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to (4 (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}) < x^{2} \leftrightarrow \frac{1}{⌊\frac{4}{x^{2}}⌋ + 1} < \frac{x^{2}}{4})$
128	123 127	mpbird	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to 4 (\frac{1}{⌊\frac{4}{x^{2}}⌋ + 1}) < x^{2}$
129	48 53 55 109 128	lelttrd	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to {(F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n))}^{2} < x^{2}$
130		metge0	$⊢ (D \in Met (X) \land F (⌊\frac{4}{x^{2}}⌋ + 1) \in X \land F (n) \in X) \to 0 \leq F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n)$
131	30 41 45 130	syl3anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to 0 \leq F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n)$
132		rprege0	$⊢ x \in ℝ^{+} \to (x \in ℝ \land 0 \leq x)$
133	132	ad2antlr	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to (x \in ℝ \land 0 \leq x)$
134		lt2sq	$⊢ ((F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) \in ℝ \land 0 \leq F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n)) \land (x \in ℝ \land 0 \leq x)) \to (F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) < x \leftrightarrow {(F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n))}^{2} < x^{2})$
135	47 131 133 134	syl21anc	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to (F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) < x \leftrightarrow {(F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n))}^{2} < x^{2})$
136	129 135	mpbird	$⊢ ((φ \land x \in ℝ^{+}) \land n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}) \to F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) < x$
137	136	ralrimiva	$⊢ (φ \land x \in ℝ^{+}) \to \forall n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)} F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) < x$
138		fveq2	$⊢ j = ⌊\frac{4}{x^{2}}⌋ + 1 \to ℤ_{\geq j} = ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)}$
139		fveq2	$⊢ j = ⌊\frac{4}{x^{2}}⌋ + 1 \to F (j) = F (⌊\frac{4}{x^{2}}⌋ + 1)$
140	139	oveq1d	$⊢ j = ⌊\frac{4}{x^{2}}⌋ + 1 \to F (j) D F (n) = F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n)$
141	140	breq1d	$⊢ j = ⌊\frac{4}{x^{2}}⌋ + 1 \to (F (j) D F (n) < x \leftrightarrow F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) < x)$
142	138 141	raleqbidv	$⊢ j = ⌊\frac{4}{x^{2}}⌋ + 1 \to (\forall n \in ℤ_{\geq j} F (j) D F (n) < x \leftrightarrow \forall n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)} F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) < x)$
143	142	rspcev	$⊢ (⌊\frac{4}{x^{2}}⌋ + 1 \in ℕ \land \forall n \in ℤ_{\geq (⌊\frac{4}{x^{2}}⌋ + 1)} F (⌊\frac{4}{x^{2}}⌋ + 1) D F (n) < x) \to \exists j \in ℕ \forall n \in ℤ_{\geq j} F (j) D F (n) < x$
144	26 137 143	syl2anc	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in ℕ \forall n \in ℤ_{\geq j} F (j) D F (n) < x$
145	144	ralrimiva	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℕ \forall n \in ℤ_{\geq j} F (j) D F (n) < x$
146		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
147	1 8	imsxmet	$⊢ U \in NrmCVec \to D \in ∞Met (X)$
148	5 27 147	3syl	$⊢ φ \to D \in ∞Met (X)$
149		1zzd	$⊢ φ \to 1 \in ℤ$
150		eqidd	$⊢ (φ \land n \in ℕ) \to F (n) = F (n)$
151		eqidd	$⊢ (φ \land j \in ℕ) \to F (j) = F (j)$
152	12 36	fssd	$⊢ φ \to F : ℕ ⟶ X$
153	146 148 149 150 151 152	iscauf	$⊢ φ \to (F \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall n \in ℤ_{\geq j} F (j) D F (n) < x)$
154	145 153	mpbird	$⊢ φ \to F \in Cau (D)$

Metamath Proof Explorer

Theorem minvecolem3

Proof