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 28303

Description: Lemma for minveco 28312. 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 11460	. . . . . 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 28302	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
14	13	simp1d 1133	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
15	13	simp2d 1134	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ≠ ∅)
16		0re 10378	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
17	13	simp3d 1135	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
18		breq1 4889	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
19	18	ralbidv 3167	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
20	19	rspcev 3510	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
21	16, 17, 20	sylancr 581	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
22		infrecl 11359	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈ ℝ)
23	14, 15, 21, 22	syl3anc 1439	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ∈ ℝ)
24	2, 23	syl5eqel 2862	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
25	24	resqcld 13356	. . . . . 6 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
26		remulcl 10357	. . . . . 6 ⊢ ((4 ∈ ℝ ∧ (𝑆↑2) ∈ ℝ) → (4 · (𝑆↑2)) ∈ ℝ)
27	1, 25, 26	sylancr 581	. . . . 5 ⊢ (𝜑 → (4 · (𝑆↑2)) ∈ ℝ)
28		phnv 28241	. . . . . . . . 9 ⊢ (𝑈 ∈ CPreHil_OLD → 𝑈 ∈ NrmCVec)
29	7, 28	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ NrmCVec)
30	3, 10	imsmet 28118	. . . . . . . 8 ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
31	29, 30	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
32		inss1 4052	. . . . . . . . . 10 ⊢ ((SubSp‘𝑈) ∩ CBan) ⊆ (SubSp‘𝑈)
33	32, 8	sseldi 3818	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈))
34		eqid 2777	. . . . . . . . . 10 ⊢ (SubSp‘𝑈) = (SubSp‘𝑈)
35	3, 6, 34	sspba 28154	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋)
36	29, 33, 35	syl2anc 579	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
37		minvecolem2.3	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ 𝑌)
38	36, 37	sseldd 3821	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
39		minvecolem2.4	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ 𝑌)
40	36, 39	sseldd 3821	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑋)
41		metcl 22545	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) ∈ ℝ)
42	31, 38, 40, 41	syl3anc 1439	. . . . . 6 ⊢ (𝜑 → (𝐾𝐷𝐿) ∈ ℝ)
43	42	resqcld 13356	. . . . 5 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ∈ ℝ)
44	27, 43	readdcld 10406	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
45		ax-1cn 10330	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
46		halfcl 11607	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℂ → (1 / 2) ∈ ℂ)
47	45, 46	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
48		eqid 2777	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
49		eqid 2777	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑊) = ( +_𝑣 ‘𝑊)
50	6, 48, 49, 34	sspgval 28156	. . . . . . . . . . . . . 14 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ (𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌)) → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
51	29, 33, 37, 39, 50	syl22anc 829	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
52	34	sspnv 28153	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑊 ∈ NrmCVec)
53	29, 33, 52	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊 ∈ NrmCVec)
54	6, 49	nvgcl 28047	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌) → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
55	53, 37, 39, 54	syl3anc 1439	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
56	51, 55	eqeltrrd 2859	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌)
57		eqid 2777	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑈) = ( ·_𝑠OLD ‘𝑈)
58		eqid 2777	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑊) = ( ·_𝑠OLD ‘𝑊)
59	6, 57, 58, 34	sspsval 28158	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ ((1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌)) → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))
60	29, 33, 47, 56, 59	syl22anc 829	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))
61	6, 58	nvscl 28053	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌) → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
62	53, 47, 56, 61	syl3anc 1439	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
63	60, 62	eqeltrrd 2859	. . . . . . . . . 10 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
64	36, 63	sseldd 3821	. . . . . . . . 9 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋)
65	3, 4	nvmcl 28073	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋) → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
66	29, 9, 64, 65	syl3anc 1439	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
67	3, 5	nvcl 28088	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ)
68	29, 66, 67	syl2anc 579	. . . . . . 7 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ)
69	68	resqcld 13356	. . . . . 6 ⊢ (𝜑 → ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ)
70		remulcl 10357	. . . . . 6 ⊢ ((4 ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ) → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) ∈ ℝ)
71	1, 69, 70	sylancr 581	. . . . 5 ⊢ (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) ∈ ℝ)
72	71, 43	readdcld 10406	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
73		minvecolem2.1	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	25, 73	readdcld 10406	. . . . 5 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℝ)
75		remulcl 10357	. . . . 5 ⊢ ((4 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
76	1, 74, 75	sylancr 581	. . . 4 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
77	16	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
78		infregelb 11361	. . . . . . . . . 10 ⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
79	14, 15, 21, 77, 78	syl31anc 1441	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
80	17, 79	mpbird 249	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
81	80, 2	syl6breqr 4928	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝑆)
82		eqid 2777	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
83		oveq2 6930	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝐴𝑀𝑦) = (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
84	83	fveq2d 6450	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝑁‘(𝐴𝑀𝑦)) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
85	84	rspceeqv 3528	. . . . . . . . . . . 12 ⊢ ((((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) → ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
86	63, 82, 85	sylancl 580	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
87		eqid 2777	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
88		fvex 6459	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V
89	87, 88	elrnmpti 5622	. . . . . . . . . . 11 ⊢ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) ↔ ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
90	86, 89	sylibr 226	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
91	90, 12	syl6eleqr 2869	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅)
92		infrelb 11362	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
93	14, 21, 91, 92	syl3anc 1439	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
94	2, 93	syl5eqbr 4921	. . . . . . 7 ⊢ (𝜑 → 𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
95		le2sq2 13258	. . . . . . 7 ⊢ (((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ ∧ 𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))) → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
96	24, 81, 68, 94, 95	syl22anc 829	. . . . . 6 ⊢ (𝜑 → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
97		4pos 11489	. . . . . . . . 9 ⊢ 0 < 4
98	1, 97	pm3.2i 464	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 0 < 4)
99		lemul2 11230	. . . . . . . 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 1523	. . . . . . 7 ⊢ (((𝑆↑2) ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ) → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))))
101	25, 69, 100	syl2anc 579	. . . . . 6 ⊢ (𝜑 → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))))
102	96, 101	mpbid 224	. . . . 5 ⊢ (𝜑 → (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
103	27, 71, 43, 102	leadd1dd 10989	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)))
104		metcl 22545	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) ∈ ℝ)
105	31, 9, 38, 104	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) ∈ ℝ)
106	105	resqcld 13356	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ∈ ℝ)
107		metcl 22545	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝐷𝐿) ∈ ℝ)
108	31, 9, 40, 107	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐿) ∈ ℝ)
109	108	resqcld 13356	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ∈ ℝ)
110		minvecolem2.5	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))
111		minvecolem2.6	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))
112	106, 109, 74, 74, 110, 111	le2addd 10994	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
113	74	recnd 10405	. . . . . . . 8 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℂ)
114	113	2timesd 11625	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) = (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
115	112, 114	breqtrrd 4914	. . . . . 6 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)))
116	106, 109	readdcld 10406	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ)
117		2re 11449	. . . . . . . 8 ⊢ 2 ∈ ℝ
118		remulcl 10357	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
119	117, 74, 118	sylancr 581	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
120		2pos 11485	. . . . . . . . 9 ⊢ 0 < 2
121	117, 120	pm3.2i 464	. . . . . . . 8 ⊢ (2 ∈ ℝ ∧ 0 < 2)
122		lemul2 11230	. . . . . . . 8 ⊢ (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
123	121, 122	mp3an3 1523	. . . . . . 7 ⊢ (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
124	116, 119, 123	syl2anc 579	. . . . . 6 ⊢ (𝜑 → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
125	115, 124	mpbid 224	. . . . 5 ⊢ (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵))))
126	3, 4	nvmcl 28073	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝑀𝐾) ∈ 𝑋)
127	29, 9, 38, 126	syl3anc 1439	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐾) ∈ 𝑋)
128	3, 4	nvmcl 28073	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝑀𝐿) ∈ 𝑋)
129	29, 9, 40, 128	syl3anc 1439	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐿) ∈ 𝑋)
130	3, 48, 4, 5	phpar2 28250	. . . . . . 7 ⊢ ((𝑈 ∈ CPreHil_OLD ∧ (𝐴𝑀𝐾) ∈ 𝑋 ∧ (𝐴𝑀𝐿) ∈ 𝑋) → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
131	7, 127, 129, 130	syl3anc 1439	. . . . . 6 ⊢ (𝜑 → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
132		2cn 11450	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
133	68	recnd 10405	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℂ)
134		sqmul 13244	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℂ) → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
135	132, 133, 134	sylancr 581	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
136		sq2 13279	. . . . . . . . . 10 ⊢ (2↑2) = 4
137	136	oveq1i 6932	. . . . . . . . 9 ⊢ ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
138	135, 137	syl6eq 2829	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
139	132	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
140	3, 57, 5	nvs 28090	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
141	29, 139, 66, 140	syl3anc 1439	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
142		0le2 11484	. . . . . . . . . . . . 13 ⊢ 0 ≤ 2
143		absid 14443	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
144	117, 142, 143	mp2an 682	. . . . . . . . . . . 12 ⊢ (abs‘2) = 2
145	144	oveq1i 6932	. . . . . . . . . . 11 ⊢ ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
146	141, 145	syl6eq 2829	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
147	3, 4, 57	nvmdi 28075	. . . . . . . . . . . . 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 1440	. . . . . . . . . . . 12 ⊢ (𝜑 → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
149	3, 48, 57	nv2 28059	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
150	29, 9, 149	syl2anc 579	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
151		2ne0 11486	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
152	132, 151	recidi 11106	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 2)) = 1
153	152	oveq1i 6932	. . . . . . . . . . . . . . 15 ⊢ ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))
154	3, 48	nvgcl 28047	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
155	29, 38, 40, 154	syl3anc 1439	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
156	3, 57	nvsid 28054	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋) → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
157	29, 155, 156	syl2anc 579	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
158	153, 157	syl5eq 2825	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
159	3, 57	nvsass 28055	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)) → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
160	29, 139, 47, 155, 159	syl13anc 1440	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
161	158, 160	eqtr3d 2815	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
162	150, 161	oveq12d 6940	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
163	3, 48, 4	nvaddsub4 28084	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
164	29, 9, 9, 38, 40, 163	syl122anc 1447	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
165	148, 162, 164	3eqtr2d 2819	. . . . . . . . . . 11 ⊢ (𝜑 → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
166	165	fveq2d 6450	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
167	146, 166	eqtr3d 2815	. . . . . . . . 9 ⊢ (𝜑 → (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
168	167	oveq1d 6937	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
169	138, 168	eqtr3d 2815	. . . . . . 7 ⊢ (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
170	3, 4, 5, 10	imsdval 28113	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐿 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
171	29, 40, 38, 170	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
172		metsym 22563	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
173	31, 38, 40, 172	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
174	3, 4	nvnnncan1 28074	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
175	29, 9, 38, 40, 174	syl13anc 1440	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
176	175	fveq2d 6450	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))) = (𝑁‘(𝐿𝑀𝐾)))
177	171, 173, 176	3eqtr4d 2823	. . . . . . . 8 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))))
178	177	oveq1d 6937	. . . . . . 7 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) = ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2))
179	169, 178	oveq12d 6940	. . . . . 6 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)))
180	3, 4, 5, 10	imsdval 28113	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
181	29, 9, 38, 180	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
182	181	oveq1d 6937	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) = ((𝑁‘(𝐴𝑀𝐾))↑2))
183	3, 4, 5, 10	imsdval 28113	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
184	29, 9, 40, 183	syl3anc 1439	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
185	184	oveq1d 6937	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) = ((𝑁‘(𝐴𝑀𝐿))↑2))
186	182, 185	oveq12d 6940	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) = (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2)))
187	186	oveq2d 6938	. . . . . 6 ⊢ (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
188	131, 179, 187	3eqtr4d 2823	. . . . 5 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))))
189		2t2e4 11546	. . . . . . 7 ⊢ (2 · 2) = 4
190	189	oveq1i 6932	. . . . . 6 ⊢ ((2 · 2) · ((𝑆↑2) + 𝐵)) = (4 · ((𝑆↑2) + 𝐵))
191	139, 139, 113	mulassd 10400	. . . . . 6 ⊢ (𝜑 → ((2 · 2) · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
192	190, 191	syl5eqr 2827	. . . . 5 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
193	125, 188, 192	3brtr4d 4918	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
194	44, 72, 76, 103, 193	letrd 10533	. . 3 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
195		4cn 11461	. . . . 5 ⊢ 4 ∈ ℂ
196	195	a1i 11	. . . 4 ⊢ (𝜑 → 4 ∈ ℂ)
197	25	recnd 10405	. . . 4 ⊢ (𝜑 → (𝑆↑2) ∈ ℂ)
198	73	recnd 10405	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℂ)
199	196, 197, 198	adddid 10401	. . 3 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = ((4 · (𝑆↑2)) + (4 · 𝐵)))
200	194, 199	breqtrd 4912	. 2 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵)))
201		remulcl 10357	. . . 4 ⊢ ((4 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (4 · 𝐵) ∈ ℝ)
202	1, 73, 201	sylancr 581	. . 3 ⊢ (𝜑 → (4 · 𝐵) ∈ ℝ)
203	43, 202, 27	leadd2d 10970	. 2 ⊢ (𝜑 → (((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵) ↔ ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵))))
204	200, 203	mpbird 249	1 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 386 = wceq 1601 ∈ wcel 2106 ≠ wne 2968 ∀wral 3089 ∃wrex 3090 ∩ cin 3790 ⊆ wss 3791 ∅c0 4140 class class class wbr 4886 ↦ cmpt 4965 ran crn 5356 ‘cfv 6135 (class class class)co 6922 infcinf 8635 ℂcc 10270 ℝcr 10271 0cc0 10272 1c1 10273 + caddc 10275 · cmul 10277 < clt 10411 ≤ cle 10412 / cdiv 11032 2c2 11430 4c4 11432 ↑cexp 13178 abscabs 14381 Metcmet 20128 MetOpencmopn 20132 NrmCVeccnv 28011 +_𝑣 cpv 28012 BaseSetcba 28013 ·_𝑠OLD cns 28014 −_𝑣 cnsb 28016 norm_CVcnmcv 28017 IndMetcims 28018 SubSpcss 28148 CPreHil_OLDccphlo 28239 CBanccbn 28290

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-8 2108 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-13 2333 ax-ext 2753 ax-rep 5006 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 ax-cnex 10328 ax-resscn 10329 ax-1cn 10330 ax-icn 10331 ax-addcl 10332 ax-addrcl 10333 ax-mulcl 10334 ax-mulrcl 10335 ax-mulcom 10336 ax-addass 10337 ax-mulass 10338 ax-distr 10339 ax-i2m1 10340 ax-1ne0 10341 ax-1rid 10342 ax-rnegex 10343 ax-rrecex 10344 ax-cnre 10345 ax-pre-lttri 10346 ax-pre-lttrn 10347 ax-pre-ltadd 10348 ax-pre-mulgt0 10349 ax-pre-sup 10350 ax-addf 10351 ax-mulf 10352

This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3or 1072 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2550 df-eu 2586 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-ne 2969 df-nel 3075 df-ral 3094 df-rex 3095 df-reu 3096 df-rmo 3097 df-rab 3098 df-v 3399 df-sbc 3652 df-csb 3751 df-dif 3794 df-un 3796 df-in 3798 df-ss 3805 df-pss 3807 df-nul 4141 df-if 4307 df-pw 4380 df-sn 4398 df-pr 4400 df-tp 4402 df-op 4404 df-uni 4672 df-iun 4755 df-br 4887 df-opab 4949 df-mpt 4966 df-tr 4988 df-id 5261 df-eprel 5266 df-po 5274 df-so 5275 df-fr 5314 df-we 5316 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-rn 5366 df-res 5367 df-ima 5368 df-pred 5933 df-ord 5979 df-on 5980 df-lim 5981 df-suc 5982 df-iota 6099 df-fun 6137 df-fn 6138 df-f 6139 df-f1 6140 df-fo 6141 df-f1o 6142 df-fv 6143 df-riota 6883 df-ov 6925 df-oprab 6926 df-mpt2 6927 df-om 7344 df-1st 7445 df-2nd 7446 df-wrecs 7689 df-recs 7751 df-rdg 7789 df-er 8026 df-map 8142 df-en 8242 df-dom 8243 df-sdom 8244 df-sup 8636 df-inf 8637 df-pnf 10413 df-mnf 10414 df-xr 10415 df-ltxr 10416 df-le 10417 df-sub 10608 df-neg 10609 df-div 11033 df-nn 11375 df-2 11438 df-3 11439 df-4 11440 df-n0 11643 df-z 11729 df-uz 11993 df-rp 12138 df-xadd 12258 df-seq 13120 df-exp 13179 df-cj 14246 df-re 14247 df-im 14248 df-sqrt 14382 df-abs 14383 df-xmet 20135 df-met 20136 df-grpo 27920 df-gid 27921 df-ginv 27922 df-gdiv 27923 df-ablo 27972 df-vc 27986 df-nv 28019 df-va 28022 df-ba 28023 df-sm 28024 df-0v 28025 df-vs 28026 df-nmcv 28027 df-ims 28028 df-ssp 28149 df-ph 28240 df-cbn 28291

This theorem is referenced by: minvecolem3 28304 minvecolem7 28311

W3C validator