minvecolem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > minvecolem2		Structured version Visualization version GIF version

Theorem minvecolem2 31477

Description: Lemma for minveco 31486. Any two points 𝐾 and 𝐿 in 𝑌 are close to each other if they are close to the infimum of distance to 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
minveco.x	⊢ 𝑋 = (BaseSet‘𝑈)
minveco.m	⊢ 𝑀 = ( −_𝑣 ‘𝑈)
minveco.n	⊢ 𝑁 = (norm_CV‘𝑈)
minveco.y	⊢ 𝑌 = (BaseSet‘𝑊)
minveco.u	⊢ (𝜑 → 𝑈 ∈ CPreHil_OLD)
minveco.w	⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))
minveco.a	⊢ (𝜑 → 𝐴 ∈ 𝑋)
minveco.d	⊢ 𝐷 = (IndMet‘𝑈)
minveco.j	⊢ 𝐽 = (MetOpen‘𝐷)
minveco.r	⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
minveco.s	⊢ 𝑆 = inf(𝑅, ℝ, < )
minvecolem2.1	⊢ (𝜑 → 𝐵 ∈ ℝ)
minvecolem2.2	⊢ (𝜑 → 0 ≤ 𝐵)
minvecolem2.3	⊢ (𝜑 → 𝐾 ∈ 𝑌)
minvecolem2.4	⊢ (𝜑 → 𝐿 ∈ 𝑌)
minvecolem2.5	⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))
minvecolem2.6	⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))

**Assertion**
Ref	Expression
minvecolem2	⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵))

Distinct variable groups: 𝑦,𝐽 𝑦,𝐾 𝑦,𝐿 𝑦,𝑀 𝑦,𝑁 𝜑,𝑦 𝑦,𝑆 𝑦,𝐴 𝑦,𝐷 𝑦,𝑈 𝑦,𝑊 𝑦,𝑌 Allowed substitution hints: 𝐵(𝑦) 𝑅(𝑦) 𝑋(𝑦)

Proof of Theorem minvecolem2 Dummy variables 𝑥 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		4re 12427	. . . . . 6 ⊢ 4 ∈ ℝ
2		minveco.s	. . . . . . . 8 ⊢ 𝑆 = inf(𝑅, ℝ, < )
3		minveco.x	. . . . . . . . . . 11 ⊢ 𝑋 = (BaseSet‘𝑈)
4		minveco.m	. . . . . . . . . . 11 ⊢ 𝑀 = ( −_𝑣 ‘𝑈)
5		minveco.n	. . . . . . . . . . 11 ⊢ 𝑁 = (norm_CV‘𝑈)
6		minveco.y	. . . . . . . . . . 11 ⊢ 𝑌 = (BaseSet‘𝑊)
7		minveco.u	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ CPreHil_OLD)
8		minveco.w	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan))
9		minveco.a	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ 𝑋)
10		minveco.d	. . . . . . . . . . 11 ⊢ 𝐷 = (IndMet‘𝑈)
11		minveco.j	. . . . . . . . . . 11 ⊢ 𝐽 = (MetOpen‘𝐷)
12		minveco.r	. . . . . . . . . . 11 ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
13	3, 4, 5, 6, 7, 8, 9, 10, 11, 12	minvecolem1 31476	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
14	13	simp1d 1160	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
15	13	simp2d 1161	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ≠ ∅)
16		0re 11310	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
17	13	simp3d 1162	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
18		breq1 5106	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
19	18	ralbidv 3186	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
20	19	rspcev 3577	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
21	16, 17, 20	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
22		infrecl 12299	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈ ℝ)
23	14, 15, 21, 22	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ∈ ℝ)
24	2, 23	eqeltrid 2865	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
25	24	resqcld 14268	. . . . . 6 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
26		remulcl 11285	. . . . . 6 ⊢ ((4 ∈ ℝ ∧ (𝑆↑2) ∈ ℝ) → (4 · (𝑆↑2)) ∈ ℝ)
27	1, 25, 26	sylancr 599	. . . . 5 ⊢ (𝜑 → (4 · (𝑆↑2)) ∈ ℝ)
28		phnv 31416	. . . . . . . . 9 ⊢ (𝑈 ∈ CPreHil_OLD → 𝑈 ∈ NrmCVec)
29	7, 28	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ NrmCVec)
30	3, 10	imsmet 31293	. . . . . . . 8 ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
31	29, 30	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
32		inss1 4182	. . . . . . . . . 10 ⊢ ((SubSp‘𝑈) ∩ CBan) ⊆ (SubSp‘𝑈)
33	32, 8	sselid 3929	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈))
34		eqid 2761	. . . . . . . . . 10 ⊢ (SubSp‘𝑈) = (SubSp‘𝑈)
35	3, 6, 34	sspba 31329	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋)
36	29, 33, 35	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
37		minvecolem2.3	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ 𝑌)
38	36, 37	sseldd 3932	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
39		minvecolem2.4	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ 𝑌)
40	36, 39	sseldd 3932	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑋)
41		metcl 24651	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) ∈ ℝ)
42	31, 38, 40, 41	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → (𝐾𝐷𝐿) ∈ ℝ)
43	42	resqcld 14268	. . . . 5 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ∈ ℝ)
44	27, 43	readdcld 11338	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
45		ax-1cn 11258	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
46		halfcl 12572	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℂ → (1 / 2) ∈ ℂ)
47	45, 46	mp1i 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
48		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
49		eqid 2761	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑊) = ( +_𝑣 ‘𝑊)
50	6, 48, 49, 34	sspgval 31331	. . . . . . . . . . . . . 14 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ (𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌)) → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
51	29, 33, 37, 39, 50	syl22anc 852	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
52	34	sspnv 31328	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑊 ∈ NrmCVec)
53	29, 33, 52	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊 ∈ NrmCVec)
54	6, 49	nvgcl 31222	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌) → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
55	53, 37, 39, 54	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
56	51, 55	eqeltrrd 2862	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌)
57		eqid 2761	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑈) = ( ·_𝑠OLD ‘𝑈)
58		eqid 2761	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑊) = ( ·_𝑠OLD ‘𝑊)
59	6, 57, 58, 34	sspsval 31333	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ ((1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌)) → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))
60	29, 33, 47, 56, 59	syl22anc 852	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))
61	6, 58	nvscl 31228	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌) → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
62	53, 47, 56, 61	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
63	60, 62	eqeltrrd 2862	. . . . . . . . . 10 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
64	36, 63	sseldd 3932	. . . . . . . . 9 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋)
65	3, 4	nvmcl 31248	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋) → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
66	29, 9, 64, 65	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
67	3, 5	nvcl 31263	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ)
68	29, 66, 67	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ)
69	68	resqcld 14268	. . . . . 6 ⊢ (𝜑 → ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ)
70		remulcl 11285	. . . . . 6 ⊢ ((4 ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ) → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) ∈ ℝ)
71	1, 69, 70	sylancr 599	. . . . 5 ⊢ (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) ∈ ℝ)
72	71, 43	readdcld 11338	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
73		minvecolem2.1	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	25, 73	readdcld 11338	. . . . 5 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℝ)
75		remulcl 11285	. . . . 5 ⊢ ((4 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
76	1, 74, 75	sylancr 599	. . . 4 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
77	16	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
78		infregelb 12301	. . . . . . . . . 10 ⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
79	14, 15, 21, 77, 78	syl31anc 1400	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
80	17, 79	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
81	80, 2	breqtrrdi 5147	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝑆)
82		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
83		oveq2 7428	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝐴𝑀𝑦) = (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
84	83	fveq2d 6889	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝑁‘(𝐴𝑀𝑦)) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
85	84	rspceeqv 3599	. . . . . . . . . . . 12 ⊢ ((((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) → ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
86	63, 82, 85	sylancl 598	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
87		eqid 2761	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
88		fvex 6898	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V
89	87, 88	elrnmpti 5944	. . . . . . . . . . 11 ⊢ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) ↔ ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
90	86, 89	sylibr 237	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
91	90, 12	eleqtrrdi 2872	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅)
92		infrelb 12302	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
93	14, 21, 91, 92	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
94	2, 93	eqbrtrid 5140	. . . . . . 7 ⊢ (𝜑 → 𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
95		le2sq2 14278	. . . . . . 7 ⊢ (((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ ∧ 𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))) → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
96	24, 81, 68, 94, 95	syl22anc 852	. . . . . 6 ⊢ (𝜑 → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
97		4pos 12453	. . . . . . . . 9 ⊢ 0 < 4
98	1, 97	pm3.2i 476	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 0 < 4)
99		lemul2 12170	. . . . . . . 8 ⊢ (((𝑆↑2) ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))))
100	98, 99	mp3an3 1479	. . . . . . 7 ⊢ (((𝑆↑2) ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ) → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))))
101	25, 69, 100	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))))
102	96, 101	mpbid 235	. . . . 5 ⊢ (𝜑 → (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
103	27, 71, 43, 102	leadd1dd 11930	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)))
104		metcl 24651	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) ∈ ℝ)
105	31, 9, 38, 104	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) ∈ ℝ)
106	105	resqcld 14268	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ∈ ℝ)
107		metcl 24651	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝐷𝐿) ∈ ℝ)
108	31, 9, 40, 107	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐿) ∈ ℝ)
109	108	resqcld 14268	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ∈ ℝ)
110		minvecolem2.5	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))
111		minvecolem2.6	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))
112	106, 109, 74, 74, 110, 111	le2addd 11935	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
113	74	recnd 11337	. . . . . . . 8 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℂ)
114	113	2timesd 12589	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) = (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
115	112, 114	breqtrrd 5133	. . . . . 6 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)))
116	106, 109	readdcld 11338	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ)
117		2re 12417	. . . . . . . 8 ⊢ 2 ∈ ℝ
118		remulcl 11285	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
119	117, 74, 118	sylancr 599	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
120		2pos 12447	. . . . . . . . 9 ⊢ 0 < 2
121	117, 120	pm3.2i 476	. . . . . . . 8 ⊢ (2 ∈ ℝ ∧ 0 < 2)
122		lemul2 12170	. . . . . . . 8 ⊢ (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
123	121, 122	mp3an3 1479	. . . . . . 7 ⊢ (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
124	116, 119, 123	syl2anc 596	. . . . . 6 ⊢ (𝜑 → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
125	115, 124	mpbid 235	. . . . 5 ⊢ (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵))))
126	3, 4	nvmcl 31248	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝑀𝐾) ∈ 𝑋)
127	29, 9, 38, 126	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐾) ∈ 𝑋)
128	3, 4	nvmcl 31248	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝑀𝐿) ∈ 𝑋)
129	29, 9, 40, 128	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐿) ∈ 𝑋)
130	3, 48, 4, 5	phpar2 31425	. . . . . . 7 ⊢ ((𝑈 ∈ CPreHil_OLD ∧ (𝐴𝑀𝐾) ∈ 𝑋 ∧ (𝐴𝑀𝐿) ∈ 𝑋) → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
131	7, 127, 129, 130	syl3anc 1398	. . . . . 6 ⊢ (𝜑 → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
132		2cn 12418	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
133	68	recnd 11337	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℂ)
134		sqmul 14262	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℂ) → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
135	132, 133, 134	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
136		sq2 14340	. . . . . . . . . 10 ⊢ (2↑2) = 4
137	136	oveq1i 7430	. . . . . . . . 9 ⊢ ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
138	135, 137	eqtrdi 2812	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
139	132	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
140	3, 57, 5	nvs 31265	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
141	29, 139, 66, 140	syl3anc 1398	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
142		0le2 12445	. . . . . . . . . . . . 13 ⊢ 0 ≤ 2
143		absid 15463	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
144	117, 142, 143	mp2an 705	. . . . . . . . . . . 12 ⊢ (abs‘2) = 2
145	144	oveq1i 7430	. . . . . . . . . . 11 ⊢ ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
146	141, 145	eqtrdi 2812	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
147	3, 4, 57	nvmdi 31250	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋)) → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
148	29, 139, 9, 64, 147	syl13anc 1399	. . . . . . . . . . . 12 ⊢ (𝜑 → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
149	3, 48, 57	nv2 31234	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
150	29, 9, 149	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
151		2thalfe1 12450	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 2)) = 1
152	151	oveq1i 7430	. . . . . . . . . . . . . . 15 ⊢ ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))
153	3, 48	nvgcl 31222	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
154	29, 38, 40, 153	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
155	3, 57	nvsid 31229	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋) → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
156	29, 154, 155	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
157	152, 156	eqtrid 2808	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
158	3, 57	nvsass 31230	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)) → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
159	29, 139, 47, 154, 158	syl13anc 1399	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
160	157, 159	eqtr3d 2798	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
161	150, 160	oveq12d 7438	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
162	3, 48, 4	nvaddsub4 31259	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
163	29, 9, 9, 38, 40, 162	syl122anc 1406	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
164	148, 161, 163	3eqtr2d 2802	. . . . . . . . . . 11 ⊢ (𝜑 → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
165	164	fveq2d 6889	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
166	146, 165	eqtr3d 2798	. . . . . . . . 9 ⊢ (𝜑 → (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
167	166	oveq1d 7435	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
168	138, 167	eqtr3d 2798	. . . . . . 7 ⊢ (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
169	3, 4, 5, 10	imsdval 31288	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐿 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
170	29, 40, 38, 169	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
171		metsym 24669	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
172	31, 38, 40, 171	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
173	3, 4	nvnnncan1 31249	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
174	29, 9, 38, 40, 173	syl13anc 1399	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
175	174	fveq2d 6889	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))) = (𝑁‘(𝐿𝑀𝐾)))
176	170, 172, 175	3eqtr4d 2806	. . . . . . . 8 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))))
177	176	oveq1d 7435	. . . . . . 7 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) = ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2))
178	168, 177	oveq12d 7438	. . . . . 6 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)))
179	3, 4, 5, 10	imsdval 31288	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
180	29, 9, 38, 179	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
181	180	oveq1d 7435	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) = ((𝑁‘(𝐴𝑀𝐾))↑2))
182	3, 4, 5, 10	imsdval 31288	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
183	29, 9, 40, 182	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
184	183	oveq1d 7435	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) = ((𝑁‘(𝐴𝑀𝐿))↑2))
185	181, 184	oveq12d 7438	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) = (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2)))
186	185	oveq2d 7436	. . . . . 6 ⊢ (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
187	131, 178, 186	3eqtr4d 2806	. . . . 5 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))))
188		2t2e4 12506	. . . . . . 7 ⊢ (2 · 2) = 4
189	188	oveq1i 7430	. . . . . 6 ⊢ ((2 · 2) · ((𝑆↑2) + 𝐵)) = (4 · ((𝑆↑2) + 𝐵))
190	139, 139, 113	mulassd 11332	. . . . . 6 ⊢ (𝜑 → ((2 · 2) · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
191	189, 190	eqtr3id 2810	. . . . 5 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
192	125, 187, 191	3brtr4d 5137	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
193	44, 72, 76, 103, 192	letrd 11467	. . 3 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
194		4cn 12428	. . . . 5 ⊢ 4 ∈ ℂ
195	194	a1i 11	. . . 4 ⊢ (𝜑 → 4 ∈ ℂ)
196	25	recnd 11337	. . . 4 ⊢ (𝜑 → (𝑆↑2) ∈ ℂ)
197	73	recnd 11337	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℂ)
198	195, 196, 197	adddid 11333	. . 3 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = ((4 · (𝑆↑2)) + (4 · 𝐵)))
199	193, 198	breqtrd 5131	. 2 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵)))
200		remulcl 11285	. . . 4 ⊢ ((4 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (4 · 𝐵) ∈ ℝ)
201	1, 73, 200	sylancr 599	. . 3 ⊢ (𝜑 → (4 · 𝐵) ∈ ℝ)
202	43, 201, 27	leadd2d 11911	. 2 ⊢ (𝜑 → (((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵) ↔ ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵))))
203	199, 202	mpbird 260	1 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∀wral 3077 ∃wrex 3087 ∩ cin 3898 ⊆ wss 3899 ∅c0 4279 class class class wbr 5103 ↦ cmpt 5186 ran crn 5652 ‘cfv 6538 (class class class)co 7420 infcinf 9433 ℂcc 11198 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 < clt 11343 ≤ cle 11344 / cdiv 11973 2c2 12397 4c4 12399 ↑cexp 14204 abscabs 15401 Metcmet 21664 MetOpencmopn 21668 NrmCVeccnv 31186 +_𝑣 cpv 31187 BaseSetcba 31188 ·_𝑠OLD cns 31189 −_𝑣 cnsb 31191 norm_CVcnmcv 31192 IndMetcims 31193 SubSpcss 31323 CPreHil_OLDccphlo 31414 CBanccbn 31464

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-rep 5232 ax-sep 5249 ax-nul 5260 ax-pow 5327 ax-pr 5391 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278 ax-addf 11279 ax-mulf 11280

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3063 df-ral 3078 df-rex 3088 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-1st 8001 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-er 8717 df-map 8849 df-en 8974 df-dom 8975 df-sdom 8976 df-sup 9434 df-inf 9435 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-4 12407 df-n0 12607 df-z 12694 df-uz 12966 df-rp 13121 df-xadd 13242 df-seq 14145 df-exp 14205 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403 df-xmet 21671 df-met 21672 df-grpo 31095 df-gid 31096 df-ginv 31097 df-gdiv 31098 df-ablo 31147 df-vc 31161 df-nv 31194 df-va 31197 df-ba 31198 df-sm 31199 df-0v 31200 df-vs 31201 df-nmcv 31202 df-ims 31203 df-ssp 31324 df-ph 31415 df-cbn 31465

This theorem is used by: minvecolem3 31478 minvecolem7 31485

W3C validator