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 30819

Description: Lemma for minveco 30828. 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 12212	. . . . . 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 30818	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
14	13	simp1d 1142	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
15	13	simp2d 1143	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ≠ ∅)
16		0re 11117	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
17	13	simp3d 1144	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
18		breq1 5095	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
19	18	ralbidv 3152	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
20	19	rspcev 3577	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
21	16, 17, 20	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
22		infrecl 12107	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈ ℝ)
23	14, 15, 21, 22	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ∈ ℝ)
24	2, 23	eqeltrid 2832	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
25	24	resqcld 14032	. . . . . 6 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
26		remulcl 11094	. . . . . 6 ⊢ ((4 ∈ ℝ ∧ (𝑆↑2) ∈ ℝ) → (4 · (𝑆↑2)) ∈ ℝ)
27	1, 25, 26	sylancr 587	. . . . 5 ⊢ (𝜑 → (4 · (𝑆↑2)) ∈ ℝ)
28		phnv 30758	. . . . . . . . 9 ⊢ (𝑈 ∈ CPreHil_OLD → 𝑈 ∈ NrmCVec)
29	7, 28	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ NrmCVec)
30	3, 10	imsmet 30635	. . . . . . . 8 ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
31	29, 30	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
32		inss1 4188	. . . . . . . . . 10 ⊢ ((SubSp‘𝑈) ∩ CBan) ⊆ (SubSp‘𝑈)
33	32, 8	sselid 3933	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈))
34		eqid 2729	. . . . . . . . . 10 ⊢ (SubSp‘𝑈) = (SubSp‘𝑈)
35	3, 6, 34	sspba 30671	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋)
36	29, 33, 35	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
37		minvecolem2.3	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ 𝑌)
38	36, 37	sseldd 3936	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
39		minvecolem2.4	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ 𝑌)
40	36, 39	sseldd 3936	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑋)
41		metcl 24218	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) ∈ ℝ)
42	31, 38, 40, 41	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (𝐾𝐷𝐿) ∈ ℝ)
43	42	resqcld 14032	. . . . 5 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ∈ ℝ)
44	27, 43	readdcld 11144	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
45		ax-1cn 11067	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
46		halfcl 12350	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℂ → (1 / 2) ∈ ℂ)
47	45, 46	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
48		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
49		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑊) = ( +_𝑣 ‘𝑊)
50	6, 48, 49, 34	sspgval 30673	. . . . . . . . . . . . . 14 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ (𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌)) → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
51	29, 33, 37, 39, 50	syl22anc 838	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
52	34	sspnv 30670	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑊 ∈ NrmCVec)
53	29, 33, 52	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊 ∈ NrmCVec)
54	6, 49	nvgcl 30564	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌) → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
55	53, 37, 39, 54	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
56	51, 55	eqeltrrd 2829	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌)
57		eqid 2729	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑈) = ( ·_𝑠OLD ‘𝑈)
58		eqid 2729	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑊) = ( ·_𝑠OLD ‘𝑊)
59	6, 57, 58, 34	sspsval 30675	. . . . . . . . . . . 12 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ ((1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌)) → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))
60	29, 33, 47, 56, 59	syl22anc 838	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))
61	6, 58	nvscl 30570	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌) → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
62	53, 47, 56, 61	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
63	60, 62	eqeltrrd 2829	. . . . . . . . . 10 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
64	36, 63	sseldd 3936	. . . . . . . . 9 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋)
65	3, 4	nvmcl 30590	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋) → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
66	29, 9, 64, 65	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
67	3, 5	nvcl 30605	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ)
68	29, 66, 67	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ)
69	68	resqcld 14032	. . . . . 6 ⊢ (𝜑 → ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ)
70		remulcl 11094	. . . . . 6 ⊢ ((4 ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ) → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) ∈ ℝ)
71	1, 69, 70	sylancr 587	. . . . 5 ⊢ (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) ∈ ℝ)
72	71, 43	readdcld 11144	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
73		minvecolem2.1	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	25, 73	readdcld 11144	. . . . 5 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℝ)
75		remulcl 11094	. . . . 5 ⊢ ((4 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
76	1, 74, 75	sylancr 587	. . . 4 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
77	16	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
78		infregelb 12109	. . . . . . . . . 10 ⊢ (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
79	14, 15, 21, 77, 78	syl31anc 1375	. . . . . . . . 9 ⊢ (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
80	17, 79	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
81	80, 2	breqtrrdi 5134	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝑆)
82		eqid 2729	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
83		oveq2 7357	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝐴𝑀𝑦) = (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
84	83	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝑁‘(𝐴𝑀𝑦)) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
85	84	rspceeqv 3600	. . . . . . . . . . . 12 ⊢ ((((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) → ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
86	63, 82, 85	sylancl 586	. . . . . . . . . . 11 ⊢ (𝜑 → ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
87		eqid 2729	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
88		fvex 6835	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V
89	87, 88	elrnmpti 5904	. . . . . . . . . . 11 ⊢ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) ↔ ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
90	86, 89	sylibr 234	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
91	90, 12	eleqtrrdi 2839	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅)
92		infrelb 12110	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
93	14, 21, 91, 92	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
94	2, 93	eqbrtrid 5127	. . . . . . 7 ⊢ (𝜑 → 𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
95		le2sq2 14042	. . . . . . 7 ⊢ (((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℝ ∧ 𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))) → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
96	24, 81, 68, 94, 95	syl22anc 838	. . . . . 6 ⊢ (𝜑 → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
97		4pos 12235	. . . . . . . . 9 ⊢ 0 < 4
98	1, 97	pm3.2i 470	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 0 < 4)
99		lemul2 11977	. . . . . . . 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 1452	. . . . . . 7 ⊢ (((𝑆↑2) ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ∈ ℝ) → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))))
101	25, 69, 100	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))))
102	96, 101	mpbid 232	. . . . 5 ⊢ (𝜑 → (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
103	27, 71, 43, 102	leadd1dd 11734	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)))
104		metcl 24218	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) ∈ ℝ)
105	31, 9, 38, 104	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) ∈ ℝ)
106	105	resqcld 14032	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ∈ ℝ)
107		metcl 24218	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝐷𝐿) ∈ ℝ)
108	31, 9, 40, 107	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐿) ∈ ℝ)
109	108	resqcld 14032	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ∈ ℝ)
110		minvecolem2.5	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))
111		minvecolem2.6	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))
112	106, 109, 74, 74, 110, 111	le2addd 11739	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
113	74	recnd 11143	. . . . . . . 8 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℂ)
114	113	2timesd 12367	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) = (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
115	112, 114	breqtrrd 5120	. . . . . 6 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)))
116	106, 109	readdcld 11144	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ)
117		2re 12202	. . . . . . . 8 ⊢ 2 ∈ ℝ
118		remulcl 11094	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
119	117, 74, 118	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
120		2pos 12231	. . . . . . . . 9 ⊢ 0 < 2
121	117, 120	pm3.2i 470	. . . . . . . 8 ⊢ (2 ∈ ℝ ∧ 0 < 2)
122		lemul2 11977	. . . . . . . 8 ⊢ (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
123	121, 122	mp3an3 1452	. . . . . . 7 ⊢ (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
124	116, 119, 123	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
125	115, 124	mpbid 232	. . . . 5 ⊢ (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵))))
126	3, 4	nvmcl 30590	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝑀𝐾) ∈ 𝑋)
127	29, 9, 38, 126	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐾) ∈ 𝑋)
128	3, 4	nvmcl 30590	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝑀𝐿) ∈ 𝑋)
129	29, 9, 40, 128	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐿) ∈ 𝑋)
130	3, 48, 4, 5	phpar2 30767	. . . . . . 7 ⊢ ((𝑈 ∈ CPreHil_OLD ∧ (𝐴𝑀𝐾) ∈ 𝑋 ∧ (𝐴𝑀𝐿) ∈ 𝑋) → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
131	7, 127, 129, 130	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
132		2cn 12203	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
133	68	recnd 11143	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℂ)
134		sqmul 14026	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ℂ) → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
135	132, 133, 134	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
136		sq2 14104	. . . . . . . . . 10 ⊢ (2↑2) = 4
137	136	oveq1i 7359	. . . . . . . . 9 ⊢ ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
138	135, 137	eqtrdi 2780	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
139	132	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
140	3, 57, 5	nvs 30607	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
141	29, 139, 66, 140	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
142		0le2 12230	. . . . . . . . . . . . 13 ⊢ 0 ≤ 2
143		absid 15203	. . . . . . . . . . . . 13 ⊢ ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
144	117, 142, 143	mp2an 692	. . . . . . . . . . . 12 ⊢ (abs‘2) = 2
145	144	oveq1i 7359	. . . . . . . . . . 11 ⊢ ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
146	141, 145	eqtrdi 2780	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
147	3, 4, 57	nvmdi 30592	. . . . . . . . . . . . 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 1374	. . . . . . . . . . . 12 ⊢ (𝜑 → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
149	3, 48, 57	nv2 30576	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
150	29, 9, 149	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
151		2ne0 12232	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
152	132, 151	recidi 11855	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 2)) = 1
153	152	oveq1i 7359	. . . . . . . . . . . . . . 15 ⊢ ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))
154	3, 48	nvgcl 30564	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
155	29, 38, 40, 154	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
156	3, 57	nvsid 30571	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋) → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
157	29, 155, 156	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
158	153, 157	eqtrid 2776	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
159	3, 57	nvsass 30572	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)) → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
160	29, 139, 47, 155, 159	syl13anc 1374	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
161	158, 160	eqtr3d 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
162	150, 161	oveq12d 7367	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
163	3, 48, 4	nvaddsub4 30601	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
164	29, 9, 9, 38, 40, 163	syl122anc 1381	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
165	148, 162, 164	3eqtr2d 2770	. . . . . . . . . . 11 ⊢ (𝜑 → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
166	165	fveq2d 6826	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
167	146, 166	eqtr3d 2766	. . . . . . . . 9 ⊢ (𝜑 → (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
168	167	oveq1d 7364	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
169	138, 168	eqtr3d 2766	. . . . . . 7 ⊢ (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
170	3, 4, 5, 10	imsdval 30630	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐿 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
171	29, 40, 38, 170	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
172		metsym 24236	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
173	31, 38, 40, 172	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
174	3, 4	nvnnncan1 30591	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
175	29, 9, 38, 40, 174	syl13anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
176	175	fveq2d 6826	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))) = (𝑁‘(𝐿𝑀𝐾)))
177	171, 173, 176	3eqtr4d 2774	. . . . . . . 8 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))))
178	177	oveq1d 7364	. . . . . . 7 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) = ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2))
179	169, 178	oveq12d 7367	. . . . . 6 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)))
180	3, 4, 5, 10	imsdval 30630	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
181	29, 9, 38, 180	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
182	181	oveq1d 7364	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) = ((𝑁‘(𝐴𝑀𝐾))↑2))
183	3, 4, 5, 10	imsdval 30630	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
184	29, 9, 40, 183	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
185	184	oveq1d 7364	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) = ((𝑁‘(𝐴𝑀𝐿))↑2))
186	182, 185	oveq12d 7367	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) = (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2)))
187	186	oveq2d 7365	. . . . . 6 ⊢ (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
188	131, 179, 187	3eqtr4d 2774	. . . . 5 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))))
189		2t2e4 12287	. . . . . . 7 ⊢ (2 · 2) = 4
190	189	oveq1i 7359	. . . . . 6 ⊢ ((2 · 2) · ((𝑆↑2) + 𝐵)) = (4 · ((𝑆↑2) + 𝐵))
191	139, 139, 113	mulassd 11138	. . . . . 6 ⊢ (𝜑 → ((2 · 2) · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
192	190, 191	eqtr3id 2778	. . . . 5 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
193	125, 188, 192	3brtr4d 5124	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
194	44, 72, 76, 103, 193	letrd 11273	. . 3 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
195		4cn 12213	. . . . 5 ⊢ 4 ∈ ℂ
196	195	a1i 11	. . . 4 ⊢ (𝜑 → 4 ∈ ℂ)
197	25	recnd 11143	. . . 4 ⊢ (𝜑 → (𝑆↑2) ∈ ℂ)
198	73	recnd 11143	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℂ)
199	196, 197, 198	adddid 11139	. . 3 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = ((4 · (𝑆↑2)) + (4 · 𝐵)))
200	194, 199	breqtrd 5118	. 2 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵)))
201		remulcl 11094	. . . 4 ⊢ ((4 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (4 · 𝐵) ∈ ℝ)
202	1, 73, 201	sylancr 587	. . 3 ⊢ (𝜑 → (4 · 𝐵) ∈ ℝ)
203	43, 202, 27	leadd2d 11715	. 2 ⊢ (𝜑 → (((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵) ↔ ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵))))
204	200, 203	mpbird 257	1 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 ∩ cin 3902 ⊆ wss 3903 ∅c0 4284 class class class wbr 5092 ↦ cmpt 5173 ran crn 5620 ‘cfv 6482 (class class class)co 7349 infcinf 9331 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 < clt 11149 ≤ cle 11150 / cdiv 11777 2c2 12183 4c4 12185 ↑cexp 13968 abscabs 15141 Metcmet 21247 MetOpencmopn 21251 NrmCVeccnv 30528 +_𝑣 cpv 30529 BaseSetcba 30530 ·_𝑠OLD cns 30531 −_𝑣 cnsb 30533 norm_CVcnmcv 30534 IndMetcims 30535 SubSpcss 30665 CPreHil_OLDccphlo 30756 CBanccbn 30806

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087 ax-addf 11088 ax-mulf 11089

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-er 8625 df-map 8755 df-en 8873 df-dom 8874 df-sdom 8875 df-sup 9332 df-inf 9333 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-4 12193 df-n0 12385 df-z 12472 df-uz 12736 df-rp 12894 df-xadd 13015 df-seq 13909 df-exp 13969 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-xmet 21254 df-met 21255 df-grpo 30437 df-gid 30438 df-ginv 30439 df-gdiv 30440 df-ablo 30489 df-vc 30503 df-nv 30536 df-va 30539 df-ba 30540 df-sm 30541 df-0v 30542 df-vs 30543 df-nmcv 30544 df-ims 30545 df-ssp 30666 df-ph 30757 df-cbn 30807

This theorem is referenced by: minvecolem3 30820 minvecolem7 30827

W3C validator