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 31534

Description: Lemma for minveco 31543. 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 12467	. . . . . 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 31533	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
14	13	simp1d 1160	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
15	13	simp2d 1161	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ≠ ∅)
16		0re 11349	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
17	13	simp3d 1162	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
18		breq1 5111	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
19	18	ralbidv 3189	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
20	19	rspcev 3580	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
21	16, 17, 20	sylancr 599	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
22		infrecl 12339	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈ ℝ)
23	14, 15, 21, 22	syl3anc 1399	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ∈ ℝ)
24	2, 23	eqeltrid 2868	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
25	24	resqcld 14308	. . . . . 6 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
26		remulcl 11324	. . . . . 6 ⊢ ((4 ∈ ℝ ∧ (𝑆↑2) ∈ ℝ) → (4 · (𝑆↑2)) ∈ ℝ)
27	1, 25, 26	sylancr 599	. . . . 5 ⊢ (𝜑 → (4 · (𝑆↑2)) ∈ ℝ)
28		phnv 31473	. . . . . . . . 9 ⊢ (𝑈 ∈ CPreHil_OLD → 𝑈 ∈ NrmCVec)
29	7, 28	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ NrmCVec)
30	3, 10	imsmet 31350	. . . . . . . 8 ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
31	29, 30	syl 18	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
32		inss1 4136	. . . . . . . . . 10 ⊢ ((SubSp‘𝑈) ∩ CBan) ⊆ (SubSp‘𝑈)
33	32, 8	sselid 3911	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈))
34		eqid 2763	. . . . . . . . . 10 ⊢ (SubSp‘𝑈) = (SubSp‘𝑈)
35	3, 6, 34	sspba 31386	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋)
36	29, 33, 35	syl2anc 596	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
37		minvecolem2.3	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ 𝑌)
38	36, 37	sseldd 3914	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
39		minvecolem2.4	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ 𝑌)
40	36, 39	sseldd 3914	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑋)
41		metcl 24706	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) ∈ ℝ)
42	31, 38, 40, 41	syl3anc 1399	. . . . . 6 ⊢ (𝜑 → (𝐾𝐷𝐿) ∈ ℝ)
43	42	resqcld 14308	. . . . 5 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ∈ ℝ)
44	27, 43	readdcld 11377	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
45		ax-1cn 11297	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
46		halfcl 12612	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℂ → (1 / 2) ∈ ℂ)
47	45, 46	mp1i 14	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
48		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
49		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑊) = ( +_𝑣 ‘𝑊)
50	6, 48, 49, 34	sspgval 31388	. . . . . . . . . . . . . 14 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ (𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌)) → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
51	29, 33, 37, 39, 50	syl22anc 852	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
52	34	sspnv 31385	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑊 ∈ NrmCVec)
53	29, 33, 52	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊 ∈ NrmCVec)
54	6, 49	nvgcl 31279	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌) → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
55	53, 37, 39, 54	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
56	51, 55	eqeltrrd 2865	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌)
57		eqid 2763	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑈) = ( ·_𝑠OLD ‘𝑈)
58		eqid 2763	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑊) = ( ·_𝑠OLD ‘𝑊)
59	6, 57, 58, 34	sspsval 31390	. . . . . . . . . . . 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 31285	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌) → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
62	53, 47, 56, 61	syl3anc 1399	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
63	60, 62	eqeltrrd 2865	. . . . . . . . . 10 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
64	36, 63	sseldd 3914	. . . . . . . . 9 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋)
65	3, 4	nvmcl 31305	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋) → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
66	29, 9, 64, 65	syl3anc 1399	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
67	3, 5	nvcl 31320	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ)
68	29, 66, 67	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ)
69	68	resqcld 14308	. . . . . 6 ⊢ (𝜑 → ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ)
70		remulcl 11324	. . . . . 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 11377	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
73		minvecolem2.1	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	25, 73	readdcld 11377	. . . . 5 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℝ)
75		remulcl 11324	. . . . 5 ⊢ ((4 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
76	1, 74, 75	sylancr 599	. . . 4 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
77	16	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
78		infregelb 12341	. . . . . . . . . 10 ⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
79	14, 15, 21, 77, 78	syl31anc 1401	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
80	17, 79	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
81	80, 2	breqtrrdi 5153	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝑆)
82		eqid 2763	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
83		oveq2 7459	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝐴𝑀𝑦) = (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
84	83	fveq2d 6920	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝑁‘(𝐴𝑀𝑦)) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
85	84	rspceeqv 3602	. . . . . . . . . . . 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 2763	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
88		fvex 6929	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V
89	87, 88	elrnmpti 5956	. . . . . . . . . . 11 ⊢ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) ↔ ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
90	86, 89	sylibr 237	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
91	90, 12	eleqtrrdi 2875	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅)
92		infrelb 12342	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
93	14, 21, 91, 92	syl3anc 1399	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
94	2, 93	eqbrtrid 5146	. . . . . . 7 ⊢ (𝜑 → 𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
95		le2sq2 14318	. . . . . . 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 12493	. . . . . . . . 9 ⊢ 0 < 4
98	1, 97	pm3.2i 476	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 0 < 4)
99		lemul2 12210	. . . . . . . 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 1480	. . . . . . 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 11970	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)))
104		metcl 24706	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) ∈ ℝ)
105	31, 9, 38, 104	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) ∈ ℝ)
106	105	resqcld 14308	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ∈ ℝ)
107		metcl 24706	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝐷𝐿) ∈ ℝ)
108	31, 9, 40, 107	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐿) ∈ ℝ)
109	108	resqcld 14308	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ∈ ℝ)
110		minvecolem2.5	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))
111		minvecolem2.6	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))
112	106, 109, 74, 74, 110, 111	le2addd 11975	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
113	74	recnd 11376	. . . . . . . 8 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℂ)
114	113	2timesd 12629	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) = (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
115	112, 114	breqtrrd 5139	. . . . . 6 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)))
116	106, 109	readdcld 11377	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ)
117		2re 12457	. . . . . . . 8 ⊢ 2 ∈ ℝ
118		remulcl 11324	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
119	117, 74, 118	sylancr 599	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
120		2pos 12487	. . . . . . . . 9 ⊢ 0 < 2
121	117, 120	pm3.2i 476	. . . . . . . 8 ⊢ (2 ∈ ℝ ∧ 0 < 2)
122		lemul2 12210	. . . . . . . 8 ⊢ (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
123	121, 122	mp3an3 1480	. . . . . . 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 31305	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝑀𝐾) ∈ 𝑋)
127	29, 9, 38, 126	syl3anc 1399	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐾) ∈ 𝑋)
128	3, 4	nvmcl 31305	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝑀𝐿) ∈ 𝑋)
129	29, 9, 40, 128	syl3anc 1399	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐿) ∈ 𝑋)
130	3, 48, 4, 5	phpar2 31482	. . . . . . 7 ⊢ ((𝑈 ∈ CPreHil_OLD ∧ (𝐴𝑀𝐾) ∈ 𝑋 ∧ (𝐴𝑀𝐿) ∈ 𝑋) → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
131	7, 127, 129, 130	syl3anc 1399	. . . . . 6 ⊢ (𝜑 → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
132		2cn 12458	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
133	68	recnd 11376	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℂ)
134		sqmul 14302	. . . . . . . . . 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 14380	. . . . . . . . . 10 ⊢ (2↑2) = 4
137	136	oveq1i 7461	. . . . . . . . 9 ⊢ ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
138	135, 137	eqtrdi 2814	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
139	132	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
140	3, 57, 5	nvs 31322	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
141	29, 139, 66, 140	syl3anc 1399	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
142		0le2 12485	. . . . . . . . . . . . 13 ⊢ 0 ≤ 2
143		absid 15506	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
144	117, 142, 143	mp2an 705	. . . . . . . . . . . 12 ⊢ (abs‘2) = 2
145	144	oveq1i 7461	. . . . . . . . . . 11 ⊢ ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
146	141, 145	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
147	3, 4, 57	nvmdi 31307	. . . . . . . . . . . . 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 1400	. . . . . . . . . . . 12 ⊢ (𝜑 → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
149	3, 48, 57	nv2 31291	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
150	29, 9, 149	syl2anc 596	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
151		2thalfe1 12490	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 2)) = 1
152	151	oveq1i 7461	. . . . . . . . . . . . . . 15 ⊢ ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))
153	3, 48	nvgcl 31279	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
154	29, 38, 40, 153	syl3anc 1399	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
155	3, 57	nvsid 31286	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋) → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
156	29, 154, 155	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
157	152, 156	eqtrid 2810	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
158	3, 57	nvsass 31287	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)) → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
159	29, 139, 47, 154, 158	syl13anc 1400	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
160	157, 159	eqtr3d 2800	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
161	150, 160	oveq12d 7469	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
162	3, 48, 4	nvaddsub4 31316	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
163	29, 9, 9, 38, 40, 162	syl122anc 1407	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
164	148, 161, 163	3eqtr2d 2804	. . . . . . . . . . 11 ⊢ (𝜑 → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
165	164	fveq2d 6920	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
166	146, 165	eqtr3d 2800	. . . . . . . . 9 ⊢ (𝜑 → (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
167	166	oveq1d 7466	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
168	138, 167	eqtr3d 2800	. . . . . . 7 ⊢ (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
169	3, 4, 5, 10	imsdval 31345	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐿 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
170	29, 40, 38, 169	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
171		metsym 24724	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
172	31, 38, 40, 171	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
173	3, 4	nvnnncan1 31306	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
174	29, 9, 38, 40, 173	syl13anc 1400	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
175	174	fveq2d 6920	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))) = (𝑁‘(𝐿𝑀𝐾)))
176	170, 172, 175	3eqtr4d 2808	. . . . . . . 8 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))))
177	176	oveq1d 7466	. . . . . . 7 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) = ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2))
178	168, 177	oveq12d 7469	. . . . . 6 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)))
179	3, 4, 5, 10	imsdval 31345	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
180	29, 9, 38, 179	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
181	180	oveq1d 7466	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) = ((𝑁‘(𝐴𝑀𝐾))↑2))
182	3, 4, 5, 10	imsdval 31345	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
183	29, 9, 40, 182	syl3anc 1399	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
184	183	oveq1d 7466	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) = ((𝑁‘(𝐴𝑀𝐿))↑2))
185	181, 184	oveq12d 7469	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) = (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2)))
186	185	oveq2d 7467	. . . . . 6 ⊢ (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
187	131, 178, 186	3eqtr4d 2808	. . . . 5 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))))
188		2t2e4 12546	. . . . . . 7 ⊢ (2 · 2) = 4
189	188	oveq1i 7461	. . . . . 6 ⊢ ((2 · 2) · ((𝑆↑2) + 𝐵)) = (4 · ((𝑆↑2) + 𝐵))
190	139, 139, 113	mulassd 11371	. . . . . 6 ⊢ (𝜑 → ((2 · 2) · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
191	189, 190	eqtr3id 2812	. . . . 5 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
192	125, 187, 191	3brtr4d 5143	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
193	44, 72, 76, 103, 192	letrd 11506	. . 3 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
194		4cn 12468	. . . . 5 ⊢ 4 ∈ ℂ
195	194	a1i 11	. . . 4 ⊢ (𝜑 → 4 ∈ ℂ)
196	25	recnd 11376	. . . 4 ⊢ (𝜑 → (𝑆↑2) ∈ ℂ)
197	73	recnd 11376	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℂ)
198	195, 196, 197	adddid 11372	. . 3 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = ((4 · (𝑆↑2)) + (4 · 𝐵)))
199	193, 198	breqtrd 5137	. 2 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵)))
200		remulcl 11324	. . . 4 ⊢ ((4 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (4 · 𝐵) ∈ ℝ)
201	1, 73, 200	sylancr 599	. . 3 ⊢ (𝜑 → (4 · 𝐵) ∈ ℝ)
202	43, 201, 27	leadd2d 11951	. 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 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 ⊆ wss 3900 ∩ cin 4092 ∅c0 4281 class class class wbr 5108 ↦ cmpt 5192 ran crn 5659 ‘cfv 6566 (class class class)co 7451 infcinf 9470 ℂcc 11237 ℝcr 11238 0cc0 11239 1c1 11240 + caddc 11242 · cmul 11244 < clt 11382 ≤ cle 11383 / cdiv 12013 2c2 12437 4c4 12439 ↑cexp 14244 abscabs 15444 Metcmet 21715 MetOpencmopn 21719 NrmCVeccnv 31243 +_𝑣 cpv 31244 BaseSetcba 31245 ·_𝑠OLD cns 31246 −_𝑣 cnsb 31248 norm_CVcnmcv 31249 IndMetcims 31250 SubSpcss 31380 CPreHil_OLDccphlo 31471 CBanccbn 31521

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 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317 ax-addf 11318 ax-mulf 11319

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 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-er 8755 df-map 8887 df-en 9012 df-dom 9013 df-sdom 9014 df-sup 9471 df-inf 9472 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-n0 12647 df-z 12734 df-uz 13006 df-rp 13161 df-xadd 13282 df-seq 14185 df-exp 14245 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-xmet 21722 df-met 21723 df-grpo 31152 df-gid 31153 df-ginv 31154 df-gdiv 31155 df-ablo 31204 df-vc 31218 df-nv 31251 df-va 31254 df-ba 31255 df-sm 31256 df-0v 31257 df-vs 31258 df-nmcv 31259 df-ims 31260 df-ssp 31381 df-ph 31472 df-cbn 31522

This theorem is used by: minvecolem3 31535 minvecolem7 31542

W3C validator