minvecolem4

Description: Lemma for minveco . The convergent point of the cauchy sequence F attains the minimum distance, and so is closer to A than any other point in Y . (Contributed by Mario Carneiro, 7-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})$
	minveco.t	$⊢ T = \frac{1}{{(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}}$
Assertion	minvecolem4	$⊢ φ \to \exists x \in Y \forall y \in Y N (A M x) \leq N (A M y)$

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		minveco.t	$⊢ T = \frac{1}{{(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}}$
15		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
16	1 8	imsxmet	$⊢ U \in NrmCVec \to D \in ∞Met (X)$
17	5 15 16	3syl	$⊢ φ \to D \in ∞Met (X)$
18	9	methaus	$⊢ D \in ∞Met (X) \to J \in Haus$
19		lmfun	$⊢ J \in Haus \to Fun \underset{t}{⇝} (J)$
20	17 18 19	3syl	$⊢ φ \to Fun \underset{t}{⇝} (J)$
21	1 2 3 4 5 6 7 8 9 10 11 12 13	minvecolem4a	$⊢ φ \to F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)$
22		eqid	$⊢ J ↾_{𝑡} Y = J ↾_{𝑡} Y$
23		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
24	4	fvexi	$⊢ Y \in V$
25	24	a1i	$⊢ φ \to Y \in V$
26	5 15	syl	$⊢ φ \to U \in NrmCVec$
27	9	mopntop	$⊢ D \in ∞Met (X) \to J \in Top$
28	26 16 27	3syl	$⊢ φ \to J \in Top$
29		elin	$⊢ W \in (SubSp (U) \cap CBan) \leftrightarrow (W \in SubSp (U) \land W \in CBan)$
30	6 29	sylib	$⊢ φ \to (W \in SubSp (U) \land W \in CBan)$
31	30	simpld	$⊢ φ \to W \in SubSp (U)$
32		eqid	$⊢ SubSp (U) = SubSp (U)$
33	1 4 32	sspba	$⊢ (U \in NrmCVec \land W \in SubSp (U)) \to Y \subseteq X$
34	26 31 33	syl2anc	$⊢ φ \to Y \subseteq X$
35		xmetres2	$⊢ (D \in ∞Met (X) \land Y \subseteq X) \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
36	17 34 35	syl2anc	$⊢ φ \to {D ↾}_{(Y \times Y)} \in ∞Met (Y)$
37		eqid	$⊢ MetOpen ({D ↾}_{(Y \times Y)}) = MetOpen ({D ↾}_{(Y \times Y)})$
38	37	mopntopon	$⊢ {D ↾}_{(Y \times Y)} \in ∞Met (Y) \to MetOpen ({D ↾}_{(Y \times Y)}) \in TopOn (Y)$
39	36 38	syl	$⊢ φ \to MetOpen ({D ↾}_{(Y \times Y)}) \in TopOn (Y)$
40		lmcl	$⊢ (MetOpen ({D ↾}_{(Y \times Y)}) \in TopOn (Y) \land F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)) \to \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \in Y$
41	39 21 40	syl2anc	$⊢ φ \to \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \in Y$
42		1zzd	$⊢ φ \to 1 \in ℤ$
43	22 23 25 28 41 42 12	lmss	$⊢ φ \to (F \underset{t}{⇝} (J) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \leftrightarrow F \underset{t}{⇝} (J ↾_{𝑡} Y) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
44		eqid	$⊢ {D ↾}_{(Y \times Y)} = {D ↾}_{(Y \times Y)}$
45	44 9 37	metrest	$⊢ (D \in ∞Met (X) \land Y \subseteq X) \to J ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
46	17 34 45	syl2anc	$⊢ φ \to J ↾_{𝑡} Y = MetOpen ({D ↾}_{(Y \times Y)})$
47	46	fveq2d	$⊢ φ \to \underset{t}{⇝} (J ↾_{𝑡} Y) = \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)}))$
48	47	breqd	$⊢ φ \to (F \underset{t}{⇝} (J ↾_{𝑡} Y) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \leftrightarrow F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
49	43 48	bitrd	$⊢ φ \to (F \underset{t}{⇝} (J) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \leftrightarrow F \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
50	21 49	mpbird	$⊢ φ \to F \underset{t}{⇝} (J) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)$
51		funbrfv	$⊢ Fun \underset{t}{⇝} (J) \to (F \underset{t}{⇝} (J) \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F) \to \underset{t}{⇝} (J) (F) = \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F))$
52	20 50 51	sylc	$⊢ φ \to \underset{t}{⇝} (J) (F) = \underset{t}{⇝} (MetOpen ({D ↾}_{(Y \times Y)})) (F)$
53	52 41	eqeltrd	$⊢ φ \to \underset{t}{⇝} (J) (F) \in Y$
54	1 2 3 4 5 6 7 8 9 10 11 12 13	minvecolem4b	$⊢ φ \to \underset{t}{⇝} (J) (F) \in X$
55	1 2 3 8	imsdval	$⊢ (U \in NrmCVec \land A \in X \land \underset{t}{⇝} (J) (F) \in X) \to A D \underset{t}{⇝} (J) (F) = N (A M \underset{t}{⇝} (J) (F))$
56	26 7 54 55	syl3anc	$⊢ φ \to A D \underset{t}{⇝} (J) (F) = N (A M \underset{t}{⇝} (J) (F))$
57	56	adantr	$⊢ (φ \land y \in Y) \to A D \underset{t}{⇝} (J) (F) = N (A M \underset{t}{⇝} (J) (F))$
58	1 8	imsmet	$⊢ U \in NrmCVec \to D \in Met (X)$
59	5 15 58	3syl	$⊢ φ \to D \in Met (X)$
60		metcl	$⊢ (D \in Met (X) \land A \in X \land \underset{t}{⇝} (J) (F) \in X) \to A D \underset{t}{⇝} (J) (F) \in ℝ$
61	59 7 54 60	syl3anc	$⊢ φ \to A D \underset{t}{⇝} (J) (F) \in ℝ$
62	61	adantr	$⊢ (φ \land y \in Y) \to A D \underset{t}{⇝} (J) (F) \in ℝ$
63	1 2 3 4 5 6 7 8 9 10 11 12 13	minvecolem4c	$⊢ φ \to S \in ℝ$
64	63	adantr	$⊢ (φ \land y \in Y) \to S \in ℝ$
65	26	adantr	$⊢ (φ \land y \in Y) \to U \in NrmCVec$
66	7	adantr	$⊢ (φ \land y \in Y) \to A \in X$
67	34	sselda	$⊢ (φ \land y \in Y) \to y \in X$
68	1 2	nvmcl	$⊢ (U \in NrmCVec \land A \in X \land y \in X) \to A M y \in X$
69	65 66 67 68	syl3anc	$⊢ (φ \land y \in Y) \to A M y \in X$
70	1 3	nvcl	$⊢ (U \in NrmCVec \land A M y \in X) \to N (A M y) \in ℝ$
71	65 69 70	syl2anc	$⊢ (φ \land y \in Y) \to N (A M y) \in ℝ$
72	63 61	ltnled	$⊢ φ \to (S < A D \underset{t}{⇝} (J) (F) \leftrightarrow \neg A D \underset{t}{⇝} (J) (F) \leq S)$
73		eqid	$⊢ ℤ_{\geq (⌊T⌋ + 1)} = ℤ_{\geq (⌊T⌋ + 1)}$
74	17	adantr	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to D \in ∞Met (X)$
75	61 63	readdcld	$⊢ φ \to (A D \underset{t}{⇝} (J) (F)) + S \in ℝ$
76	75	rehalfcld	$⊢ φ \to \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2} \in ℝ$
77	76	resqcld	$⊢ φ \to {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} \in ℝ$
78	63	resqcld	$⊢ φ \to S^{2} \in ℝ$
79	77 78	resubcld	$⊢ φ \to {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2} \in ℝ$
80	79	adantr	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2} \in ℝ$
81	63 61 63	ltadd1d	$⊢ φ \to (S < A D \underset{t}{⇝} (J) (F) \leftrightarrow S + S < (A D \underset{t}{⇝} (J) (F)) + S)$
82	63	recnd	$⊢ φ \to S \in ℂ$
83	82	2timesd	$⊢ φ \to 2 S = S + S$
84	83	breq1d	$⊢ φ \to (2 S < (A D \underset{t}{⇝} (J) (F)) + S \leftrightarrow S + S < (A D \underset{t}{⇝} (J) (F)) + S)$
85		2re	$⊢ 2 \in ℝ$
86		2pos	$⊢ 0 < 2$
87	85 86	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
88	87	a1i	$⊢ φ \to (2 \in ℝ \land 0 < 2)$
89		ltmuldiv2	$⊢ (S \in ℝ \land (A D \underset{t}{⇝} (J) (F)) + S \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 S < (A D \underset{t}{⇝} (J) (F)) + S \leftrightarrow S < \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})$
90	63 75 88 89	syl3anc	$⊢ φ \to (2 S < (A D \underset{t}{⇝} (J) (F)) + S \leftrightarrow S < \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})$
91	81 84 90	3bitr2d	$⊢ φ \to (S < A D \underset{t}{⇝} (J) (F) \leftrightarrow S < \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})$
92	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)$
93	92	simp3d	$⊢ φ \to \forall w \in R 0 \leq w$
94	92	simp1d	$⊢ φ \to R \subseteq ℝ$
95	92	simp2d	$⊢ φ \to R \neq \emptyset$
96		0re	$⊢ 0 \in ℝ$
97		breq1	$⊢ x = 0 \to (x \leq w \leftrightarrow 0 \leq w)$
98	97	ralbidv	$⊢ x = 0 \to (\forall w \in R x \leq w \leftrightarrow \forall w \in R 0 \leq w)$
99	98	rspcev	$⊢ (0 \in ℝ \land \forall w \in R 0 \leq w) \to \exists x \in ℝ \forall w \in R x \leq w$
100	96 93 99	sylancr	$⊢ φ \to \exists x \in ℝ \forall w \in R x \leq w$
101	96	a1i	$⊢ φ \to 0 \in ℝ$
102		infregelb	$⊢ ((R \subseteq ℝ \land R \neq \emptyset \land \exists x \in ℝ \forall w \in R x \leq w) \land 0 \in ℝ) \to (0 \leq sup (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
103	94 95 100 101 102	syl31anc	$⊢ φ \to (0 \leq sup (R ℝ <) \leftrightarrow \forall w \in R 0 \leq w)$
104	93 103	mpbird	$⊢ φ \to 0 \leq sup (R ℝ <)$
105	104 11	breqtrrdi	$⊢ φ \to 0 \leq S$
106		metge0	$⊢ (D \in Met (X) \land A \in X \land \underset{t}{⇝} (J) (F) \in X) \to 0 \leq A D \underset{t}{⇝} (J) (F)$
107	59 7 54 106	syl3anc	$⊢ φ \to 0 \leq A D \underset{t}{⇝} (J) (F)$
108	61 63 107 105	addge0d	$⊢ φ \to 0 \leq (A D \underset{t}{⇝} (J) (F)) + S$
109		divge0	$⊢ (((A D \underset{t}{⇝} (J) (F)) + S \in ℝ \land 0 \leq (A D \underset{t}{⇝} (J) (F)) + S) \land (2 \in ℝ \land 0 < 2)) \to 0 \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2}$
110	75 108 88 109	syl21anc	$⊢ φ \to 0 \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2}$
111	63 76 105 110	lt2sqd	$⊢ φ \to (S < \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2} \leftrightarrow S^{2} < {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2})$
112	78 77	posdifd	$⊢ φ \to (S^{2} < {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} \leftrightarrow 0 < {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2})$
113	91 111 112	3bitrd	$⊢ φ \to (S < A D \underset{t}{⇝} (J) (F) \leftrightarrow 0 < {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2})$
114	113	biimpa	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to 0 < {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}$
115	80 114	elrpd	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2} \in ℝ^{+}$
116	115	rpreccld	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to \frac{1}{{(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}} \in ℝ^{+}$
117	14 116	eqeltrid	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to T \in ℝ^{+}$
118	117	rprege0d	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to (T \in ℝ \land 0 \leq T)$
119		flge0nn0	$⊢ (T \in ℝ \land 0 \leq T) \to ⌊T⌋ \in ℕ_{0}$
120		nn0p1nn	$⊢ ⌊T⌋ \in ℕ_{0} \to ⌊T⌋ + 1 \in ℕ$
121	118 119 120	3syl	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to ⌊T⌋ + 1 \in ℕ$
122	121	nnzd	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to ⌊T⌋ + 1 \in ℤ$
123	50 52	breqtrrd	$⊢ φ \to F \underset{t}{⇝} (J) \underset{t}{⇝} (J) (F)$
124	123	adantr	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to F \underset{t}{⇝} (J) \underset{t}{⇝} (J) (F)$
125	7	adantr	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to A \in X$
126	76	adantr	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2} \in ℝ$
127	126	rexrd	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2} \in ℝ^{*}$
128		simpll	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to φ$
129		eluznn	$⊢ (⌊T⌋ + 1 \in ℕ \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to n \in ℕ$
130	121 129	sylan	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to n \in ℕ$
131	59	adantr	$⊢ (φ \land n \in ℕ) \to D \in Met (X)$
132	7	adantr	$⊢ (φ \land n \in ℕ) \to A \in X$
133	12 34	fssd	$⊢ φ \to F : ℕ ⟶ X$
134	133	ffvelrnda	$⊢ (φ \land n \in ℕ) \to F (n) \in X$
135		metcl	$⊢ (D \in Met (X) \land A \in X \land F (n) \in X) \to A D F (n) \in ℝ$
136	131 132 134 135	syl3anc	$⊢ (φ \land n \in ℕ) \to A D F (n) \in ℝ$
137	128 130 136	syl2anc	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to A D F (n) \in ℝ$
138	137	resqcld	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to {(A D F (n))}^{2} \in ℝ$
139	63	ad2antrr	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to S \in ℝ$
140	139	resqcld	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to S^{2} \in ℝ$
141	130	nnrecred	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to \frac{1}{n} \in ℝ$
142	140 141	readdcld	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to S^{2} + (\frac{1}{n}) \in ℝ$
143	77	ad2antrr	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} \in ℝ$
144	128 130 13	syl2anc	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to {(A D F (n))}^{2} \leq S^{2} + (\frac{1}{n})$
145	117	adantr	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to T \in ℝ^{+}$
146	145	rpred	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to T \in ℝ$
147		reflcl	$⊢ T \in ℝ \to ⌊T⌋ \in ℝ$
148		peano2re	$⊢ ⌊T⌋ \in ℝ \to ⌊T⌋ + 1 \in ℝ$
149	146 147 148	3syl	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to ⌊T⌋ + 1 \in ℝ$
150	130	nnred	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to n \in ℝ$
151		fllep1	$⊢ T \in ℝ \to T \leq ⌊T⌋ + 1$
152	146 151	syl	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to T \leq ⌊T⌋ + 1$
153		eluzle	$⊢ n \in ℤ_{\geq (⌊T⌋ + 1)} \to ⌊T⌋ + 1 \leq n$
154	153	adantl	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to ⌊T⌋ + 1 \leq n$
155	146 149 150 152 154	letrd	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to T \leq n$
156	14 155	eqbrtrrid	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to \frac{1}{{(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}} \leq n$
157		1red	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to 1 \in ℝ$
158	79	ad2antrr	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2} \in ℝ$
159	114	adantr	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to 0 < {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}$
160	130	nngt0d	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to 0 < n$
161		lediv23	$⊢ (1 \in ℝ \land ({(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2} \in ℝ \land 0 < {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}) \land (n \in ℝ \land 0 < n)) \to (\frac{1}{{(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}} \leq n \leftrightarrow \frac{1}{n} \leq {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2})$
162	157 158 159 150 160 161	syl122anc	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to (\frac{1}{{(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}} \leq n \leftrightarrow \frac{1}{n} \leq {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2})$
163	156 162	mpbid	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to \frac{1}{n} \leq {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2}$
164	140 141 143	leaddsub2d	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to (S^{2} + (\frac{1}{n}) \leq {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} \leftrightarrow \frac{1}{n} \leq {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2} - S^{2})$
165	163 164	mpbird	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to S^{2} + (\frac{1}{n}) \leq {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2}$
166	138 142 143 144 165	letrd	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to {(A D F (n))}^{2} \leq {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2}$
167	76	ad2antrr	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2} \in ℝ$
168		metge0	$⊢ (D \in Met (X) \land A \in X \land F (n) \in X) \to 0 \leq A D F (n)$
169	131 132 134 168	syl3anc	$⊢ (φ \land n \in ℕ) \to 0 \leq A D F (n)$
170	128 130 169	syl2anc	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to 0 \leq A D F (n)$
171	110	ad2antrr	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to 0 \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2}$
172	137 167 170 171	le2sqd	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to (A D F (n) \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2} \leftrightarrow {(A D F (n))}^{2} \leq {(\frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})}^{2})$
173	166 172	mpbird	$⊢ ((φ \land S < A D \underset{t}{⇝} (J) (F)) \land n \in ℤ_{\geq (⌊T⌋ + 1)}) \to A D F (n) \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2}$
174	73 9 74 122 124 125 127 173	lmle	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to A D \underset{t}{⇝} (J) (F) \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2}$
175	61 63 61	leadd2d	$⊢ φ \to (A D \underset{t}{⇝} (J) (F) \leq S \leftrightarrow (A D \underset{t}{⇝} (J) (F)) + (A D \underset{t}{⇝} (J) (F)) \leq (A D \underset{t}{⇝} (J) (F)) + S)$
176	61	recnd	$⊢ φ \to A D \underset{t}{⇝} (J) (F) \in ℂ$
177	176	2timesd	$⊢ φ \to 2 (A D \underset{t}{⇝} (J) (F)) = (A D \underset{t}{⇝} (J) (F)) + (A D \underset{t}{⇝} (J) (F))$
178	177	breq1d	$⊢ φ \to (2 (A D \underset{t}{⇝} (J) (F)) \leq (A D \underset{t}{⇝} (J) (F)) + S \leftrightarrow (A D \underset{t}{⇝} (J) (F)) + (A D \underset{t}{⇝} (J) (F)) \leq (A D \underset{t}{⇝} (J) (F)) + S)$
179		lemuldiv2	$⊢ (A D \underset{t}{⇝} (J) (F) \in ℝ \land (A D \underset{t}{⇝} (J) (F)) + S \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (2 (A D \underset{t}{⇝} (J) (F)) \leq (A D \underset{t}{⇝} (J) (F)) + S \leftrightarrow A D \underset{t}{⇝} (J) (F) \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})$
180	87 179	mp3an3	$⊢ (A D \underset{t}{⇝} (J) (F) \in ℝ \land (A D \underset{t}{⇝} (J) (F)) + S \in ℝ) \to (2 (A D \underset{t}{⇝} (J) (F)) \leq (A D \underset{t}{⇝} (J) (F)) + S \leftrightarrow A D \underset{t}{⇝} (J) (F) \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})$
181	61 75 180	syl2anc	$⊢ φ \to (2 (A D \underset{t}{⇝} (J) (F)) \leq (A D \underset{t}{⇝} (J) (F)) + S \leftrightarrow A D \underset{t}{⇝} (J) (F) \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})$
182	175 178 181	3bitr2d	$⊢ φ \to (A D \underset{t}{⇝} (J) (F) \leq S \leftrightarrow A D \underset{t}{⇝} (J) (F) \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2})$
183	182	biimpar	$⊢ (φ \land A D \underset{t}{⇝} (J) (F) \leq \frac{(A D \underset{t}{⇝} (J) (F)) + S}{2}) \to A D \underset{t}{⇝} (J) (F) \leq S$
184	174 183	syldan	$⊢ (φ \land S < A D \underset{t}{⇝} (J) (F)) \to A D \underset{t}{⇝} (J) (F) \leq S$
185	184	ex	$⊢ φ \to (S < A D \underset{t}{⇝} (J) (F) \to A D \underset{t}{⇝} (J) (F) \leq S)$
186	72 185	sylbird	$⊢ φ \to (\neg A D \underset{t}{⇝} (J) (F) \leq S \to A D \underset{t}{⇝} (J) (F) \leq S)$
187	186	pm2.18d	$⊢ φ \to A D \underset{t}{⇝} (J) (F) \leq S$
188	187	adantr	$⊢ (φ \land y \in Y) \to A D \underset{t}{⇝} (J) (F) \leq S$
189	94	adantr	$⊢ (φ \land y \in Y) \to R \subseteq ℝ$
190	100	adantr	$⊢ (φ \land y \in Y) \to \exists x \in ℝ \forall w \in R x \leq w$
191		simpr	$⊢ (φ \land y \in Y) \to y \in Y$
192		fvex	$⊢ N (A M y) \in V$
193		eqid	$⊢ (y \in Y ⟼ N (A M y)) = (y \in Y ⟼ N (A M y))$
194	193	elrnmpt1	$⊢ (y \in Y \land N (A M y) \in V) \to N (A M y) \in ran (y \in Y ⟼ N (A M y))$
195	191 192 194	sylancl	$⊢ (φ \land y \in Y) \to N (A M y) \in ran (y \in Y ⟼ N (A M y))$
196	195 10	eleqtrrdi	$⊢ (φ \land y \in Y) \to N (A M y) \in R$
197		infrelb	$⊢ (R \subseteq ℝ \land \exists x \in ℝ \forall w \in R x \leq w \land N (A M y) \in R) \to sup (R ℝ <) \leq N (A M y)$
198	189 190 196 197	syl3anc	$⊢ (φ \land y \in Y) \to sup (R ℝ <) \leq N (A M y)$
199	11 198	eqbrtrid	$⊢ (φ \land y \in Y) \to S \leq N (A M y)$
200	62 64 71 188 199	letrd	$⊢ (φ \land y \in Y) \to A D \underset{t}{⇝} (J) (F) \leq N (A M y)$
201	57 200	eqbrtrrd	$⊢ (φ \land y \in Y) \to N (A M \underset{t}{⇝} (J) (F)) \leq N (A M y)$
202	201	ralrimiva	$⊢ φ \to \forall y \in Y N (A M \underset{t}{⇝} (J) (F)) \leq N (A M y)$
203		oveq2	$⊢ x = \underset{t}{⇝} (J) (F) \to A M x = A M \underset{t}{⇝} (J) (F)$
204	203	fveq2d	$⊢ x = \underset{t}{⇝} (J) (F) \to N (A M x) = N (A M \underset{t}{⇝} (J) (F))$
205	204	breq1d	$⊢ x = \underset{t}{⇝} (J) (F) \to (N (A M x) \leq N (A M y) \leftrightarrow N (A M \underset{t}{⇝} (J) (F)) \leq N (A M y))$
206	205	ralbidv	$⊢ x = \underset{t}{⇝} (J) (F) \to (\forall y \in Y N (A M x) \leq N (A M y) \leftrightarrow \forall y \in Y N (A M \underset{t}{⇝} (J) (F)) \leq N (A M y))$
207	206	rspcev	$⊢ (\underset{t}{⇝} (J) (F) \in Y \land \forall y \in Y N (A M \underset{t}{⇝} (J) (F)) \leq N (A M y)) \to \exists x \in Y \forall y \in Y N (A M x) \leq N (A M y)$
208	53 202 207	syl2anc	$⊢ φ \to \exists x \in Y \forall y \in Y N (A M x) \leq N (A M y)$

Metamath Proof Explorer

Theorem minvecolem4

Proof