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 30855

Description: Lemma for minveco 30864. 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 12209	. . . . . 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 30854	. . . . . . . . . 10 ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
14	13	simp1d 1142	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ⊆ ℝ)
15	13	simp2d 1143	. . . . . . . . 9 ⊢ (𝜑 → 𝑅 ≠ ∅)
16		0re 11114	. . . . . . . . . 10 ⊢ 0 ∈ ℝ
17	13	simp3d 1144	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)
18		breq1 5092	. . . . . . . . . . . 12 ⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤))
19	18	ralbidv 3155	. . . . . . . . . . 11 ⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
20	19	rspcev 3572	. . . . . . . . . 10 ⊢ ((0 ∈ ℝ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
21	16, 17, 20	sylancr 587	. . . . . . . . 9 ⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤)
22		infrecl 12104	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤) → inf(𝑅, ℝ, < ) ∈ ℝ)
23	14, 15, 21, 22	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ∈ ℝ)
24	2, 23	eqeltrid 2835	. . . . . . 7 ⊢ (𝜑 → 𝑆 ∈ ℝ)
25	24	resqcld 14032	. . . . . 6 ⊢ (𝜑 → (𝑆↑2) ∈ ℝ)
26		remulcl 11091	. . . . . 6 ⊢ ((4 ∈ ℝ ∧ (𝑆↑2) ∈ ℝ) → (4 · (𝑆↑2)) ∈ ℝ)
27	1, 25, 26	sylancr 587	. . . . 5 ⊢ (𝜑 → (4 · (𝑆↑2)) ∈ ℝ)
28		phnv 30794	. . . . . . . . 9 ⊢ (𝑈 ∈ CPreHil_OLD → 𝑈 ∈ NrmCVec)
29	7, 28	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ NrmCVec)
30	3, 10	imsmet 30671	. . . . . . . 8 ⊢ (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
31	29, 30	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))
32		inss1 4184	. . . . . . . . . 10 ⊢ ((SubSp‘𝑈) ∩ CBan) ⊆ (SubSp‘𝑈)
33	32, 8	sselid 3927	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (SubSp‘𝑈))
34		eqid 2731	. . . . . . . . . 10 ⊢ (SubSp‘𝑈) = (SubSp‘𝑈)
35	3, 6, 34	sspba 30707	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌 ⊆ 𝑋)
36	29, 33, 35	syl2anc 584	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ⊆ 𝑋)
37		minvecolem2.3	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ 𝑌)
38	36, 37	sseldd 3930	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ 𝑋)
39		minvecolem2.4	. . . . . . . 8 ⊢ (𝜑 → 𝐿 ∈ 𝑌)
40	36, 39	sseldd 3930	. . . . . . 7 ⊢ (𝜑 → 𝐿 ∈ 𝑋)
41		metcl 24247	. . . . . . 7 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) ∈ ℝ)
42	31, 38, 40, 41	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (𝐾𝐷𝐿) ∈ ℝ)
43	42	resqcld 14032	. . . . 5 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ∈ ℝ)
44	27, 43	readdcld 11141	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
45		ax-1cn 11064	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
46		halfcl 12347	. . . . . . . . . . . . 13 ⊢ (1 ∈ ℂ → (1 / 2) ∈ ℂ)
47	45, 46	mp1i 13	. . . . . . . . . . . 12 ⊢ (𝜑 → (1 / 2) ∈ ℂ)
48		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑈) = ( +_𝑣 ‘𝑈)
49		eqid 2731	. . . . . . . . . . . . . . 15 ⊢ ( +_𝑣 ‘𝑊) = ( +_𝑣 ‘𝑊)
50	6, 48, 49, 34	sspgval 30709	. . . . . . . . . . . . . 14 ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ (𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌)) → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
51	29, 33, 37, 39, 50	syl22anc 838	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) = (𝐾( +_𝑣 ‘𝑈)𝐿))
52	34	sspnv 30706	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑊 ∈ NrmCVec)
53	29, 33, 52	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑊 ∈ NrmCVec)
54	6, 49	nvgcl 30600	. . . . . . . . . . . . . 14 ⊢ ((𝑊 ∈ NrmCVec ∧ 𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌) → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
55	53, 37, 39, 54	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑊)𝐿) ∈ 𝑌)
56	51, 55	eqeltrrd 2832	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌)
57		eqid 2731	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑈) = ( ·_𝑠OLD ‘𝑈)
58		eqid 2731	. . . . . . . . . . . . 13 ⊢ ( ·_𝑠OLD ‘𝑊) = ( ·_𝑠OLD ‘𝑊)
59	6, 57, 58, 34	sspsval 30711	. . . . . . . . . . . 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 30606	. . . . . . . . . . . 12 ⊢ ((𝑊 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑌) → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
62	53, 47, 56, 61	syl3anc 1373	. . . . . . . . . . 11 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑊)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
63	60, 62	eqeltrrd 2832	. . . . . . . . . 10 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑌)
64	36, 63	sseldd 3930	. . . . . . . . 9 ⊢ (𝜑 → ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋)
65	3, 4	nvmcl 30626	. . . . . . . . 9 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) ∈ 𝑋) → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
66	29, 9, 64, 65	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))) ∈ 𝑋)
67	3, 5	nvcl 30641	. . . . . . . 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 11091	. . . . . 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 11141	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
73		minvecolem2.1	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ ℝ)
74	25, 73	readdcld 11141	. . . . 5 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℝ)
75		remulcl 11091	. . . . 5 ⊢ ((4 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
76	1, 74, 75	sylancr 587	. . . 4 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
77	16	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → 0 ∈ ℝ)
78		infregelb 12106	. . . . . . . . . 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 5131	. . . . . . 7 ⊢ (𝜑 → 0 ≤ 𝑆)
82		eqid 2731	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
83		oveq2 7354	. . . . . . . . . . . . . 14 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝐴𝑀𝑦) = (𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
84	83	fveq2d 6826	. . . . . . . . . . . . 13 ⊢ (𝑦 = ((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) → (𝑁‘(𝐴𝑀𝑦)) = (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
85	84	rspceeqv 3595	. . . . . . . . . . . 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 2731	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
88		fvex 6835	. . . . . . . . . . . 12 ⊢ (𝑁‘(𝐴𝑀𝑦)) ∈ V
89	87, 88	elrnmpti 5901	. . . . . . . . . . 11 ⊢ ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) ↔ ∃𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
90	86, 89	sylibr 234	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
91	90, 12	eleqtrrdi 2842	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅)
92		infrelb 12107	. . . . . . . . 9 ⊢ ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
93	14, 21, 91, 92	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
94	2, 93	eqbrtrid 5124	. . . . . . 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 12232	. . . . . . . . 9 ⊢ 0 < 4
98	1, 97	pm3.2i 470	. . . . . . . 8 ⊢ (4 ∈ ℝ ∧ 0 < 4)
99		lemul2 11974	. . . . . . . 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 11731	. . . 4 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)))
104		metcl 24247	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) ∈ ℝ)
105	31, 9, 38, 104	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) ∈ ℝ)
106	105	resqcld 14032	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ∈ ℝ)
107		metcl 24247	. . . . . . . . . 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 11736	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
113	74	recnd 11140	. . . . . . . 8 ⊢ (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℂ)
114	113	2timesd 12364	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) = (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
115	112, 114	breqtrrd 5117	. . . . . 6 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)))
116	106, 109	readdcld 11141	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ)
117		2re 12199	. . . . . . . 8 ⊢ 2 ∈ ℝ
118		remulcl 11091	. . . . . . . 8 ⊢ ((2 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
119	117, 74, 118	sylancr 587	. . . . . . 7 ⊢ (𝜑 → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
120		2pos 12228	. . . . . . . . 9 ⊢ 0 < 2
121	117, 120	pm3.2i 470	. . . . . . . 8 ⊢ (2 ∈ ℝ ∧ 0 < 2)
122		lemul2 11974	. . . . . . . 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 30626	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝑀𝐾) ∈ 𝑋)
127	29, 9, 38, 126	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐾) ∈ 𝑋)
128	3, 4	nvmcl 30626	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝑀𝐿) ∈ 𝑋)
129	29, 9, 40, 128	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → (𝐴𝑀𝐿) ∈ 𝑋)
130	3, 48, 4, 5	phpar2 30803	. . . . . . 7 ⊢ ((𝑈 ∈ CPreHil_OLD ∧ (𝐴𝑀𝐾) ∈ 𝑋 ∧ (𝐴𝑀𝐿) ∈ 𝑋) → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
131	7, 127, 129, 130	syl3anc 1373	. . . . . 6 ⊢ (𝜑 → (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
132		2cn 12200	. . . . . . . . . 10 ⊢ 2 ∈ ℂ
133	68	recnd 11140	. . . . . . . . . 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 7356	. . . . . . . . 9 ⊢ ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2))
138	135, 137	eqtrdi 2782	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)))
139	132	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → 2 ∈ ℂ)
140	3, 57, 5	nvs 30643	. . . . . . . . . . . 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 12227	. . . . . . . . . . . . 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 7356	. . . . . . . . . . 11 ⊢ ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
146	141, 145	eqtrdi 2782	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))))
147	3, 4, 57	nvmdi 30628	. . . . . . . . . . . . 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 30612	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
150	29, 9, 149	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴( +_𝑣 ‘𝑈)𝐴) = (2( ·_𝑠OLD ‘𝑈)𝐴))
151		2ne0 12229	. . . . . . . . . . . . . . . . 17 ⊢ 2 ≠ 0
152	132, 151	recidi 11852	. . . . . . . . . . . . . . . 16 ⊢ (2 · (1 / 2)) = 1
153	152	oveq1i 7356	. . . . . . . . . . . . . . 15 ⊢ ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))
154	3, 48	nvgcl 30600	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
155	29, 38, 40, 154	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋)
156	3, 57	nvsid 30607	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐾( +_𝑣 ‘𝑈)𝐿) ∈ 𝑋) → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
157	29, 155, 156	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
158	153, 157	eqtrid 2778	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((2 · (1 / 2))( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)) = (𝐾( +_𝑣 ‘𝑈)𝐿))
159	3, 57	nvsass 30608	. . . . . . . . . . . . . . 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 2768	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾( +_𝑣 ‘𝑈)𝐿) = (2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))
162	150, 161	oveq12d 7364	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((2( ·_𝑠OLD ‘𝑈)𝐴)𝑀(2( ·_𝑠OLD ‘𝑈)((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))
163	3, 48, 4	nvaddsub4 30637	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋) ∧ (𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
164	29, 9, 9, 38, 40, 163	syl122anc 1381	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐴( +_𝑣 ‘𝑈)𝐴)𝑀(𝐾( +_𝑣 ‘𝑈)𝐿)) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
165	148, 162, 164	3eqtr2d 2772	. . . . . . . . . . 11 ⊢ (𝜑 → (2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))) = ((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))
166	165	fveq2d 6826	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘(2( ·_𝑠OLD ‘𝑈)(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
167	146, 166	eqtr3d 2768	. . . . . . . . 9 ⊢ (𝜑 → (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿))))
168	167	oveq1d 7361	. . . . . . . 8 ⊢ (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿)))))↑2) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
169	138, 168	eqtr3d 2768	. . . . . . 7 ⊢ (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) = ((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2))
170	3, 4, 5, 10	imsdval 30666	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐿 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
171	29, 40, 38, 170	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
172		metsym 24265	. . . . . . . . . 10 ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
173	31, 38, 40, 172	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
174	3, 4	nvnnncan1 30627	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋)) → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
175	29, 9, 38, 40, 174	syl13anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
176	175	fveq2d 6826	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))) = (𝑁‘(𝐿𝑀𝐾)))
177	171, 173, 176	3eqtr4d 2776	. . . . . . . 8 ⊢ (𝜑 → (𝐾𝐷𝐿) = (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))))
178	177	oveq1d 7361	. . . . . . 7 ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) = ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2))
179	169, 178	oveq12d 7364	. . . . . 6 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (((𝑁‘((𝐴𝑀𝐾)( +_𝑣 ‘𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)))
180	3, 4, 5, 10	imsdval 30666	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋) → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
181	29, 9, 38, 180	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
182	181	oveq1d 7361	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) = ((𝑁‘(𝐴𝑀𝐾))↑2))
183	3, 4, 5, 10	imsdval 30666	. . . . . . . . . 10 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋) → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
184	29, 9, 40, 183	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
185	184	oveq1d 7361	. . . . . . . 8 ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) = ((𝑁‘(𝐴𝑀𝐿))↑2))
186	182, 185	oveq12d 7364	. . . . . . 7 ⊢ (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) = (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2)))
187	186	oveq2d 7362	. . . . . 6 ⊢ (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
188	131, 179, 187	3eqtr4d 2776	. . . . 5 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))))
189		2t2e4 12284	. . . . . . 7 ⊢ (2 · 2) = 4
190	189	oveq1i 7356	. . . . . 6 ⊢ ((2 · 2) · ((𝑆↑2) + 𝐵)) = (4 · ((𝑆↑2) + 𝐵))
191	139, 139, 113	mulassd 11135	. . . . . 6 ⊢ (𝜑 → ((2 · 2) · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
192	190, 191	eqtr3id 2780	. . . . 5 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
193	125, 188, 192	3brtr4d 5121	. . . 4 ⊢ (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·_𝑠OLD ‘𝑈)(𝐾( +_𝑣 ‘𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
194	44, 72, 76, 103, 193	letrd 11270	. . 3 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
195		4cn 12210	. . . . 5 ⊢ 4 ∈ ℂ
196	195	a1i 11	. . . 4 ⊢ (𝜑 → 4 ∈ ℂ)
197	25	recnd 11140	. . . 4 ⊢ (𝜑 → (𝑆↑2) ∈ ℂ)
198	73	recnd 11140	. . . 4 ⊢ (𝜑 → 𝐵 ∈ ℂ)
199	196, 197, 198	adddid 11136	. . 3 ⊢ (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = ((4 · (𝑆↑2)) + (4 · 𝐵)))
200	194, 199	breqtrd 5115	. 2 ⊢ (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵)))
201		remulcl 11091	. . . 4 ⊢ ((4 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (4 · 𝐵) ∈ ℝ)
202	1, 73, 201	sylancr 587	. . 3 ⊢ (𝜑 → (4 · 𝐵) ∈ ℝ)
203	43, 202, 27	leadd2d 11712	. 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 1541 ∈ wcel 2111 ≠ wne 2928 ∀wral 3047 ∃wrex 3056 ∩ cin 3896 ⊆ wss 3897 ∅c0 4280 class class class wbr 5089 ↦ cmpt 5170 ran crn 5615 ‘cfv 6481 (class class class)co 7346 infcinf 9325 ℂcc 11004 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 < clt 11146 ≤ cle 11147 / cdiv 11774 2c2 12180 4c4 12182 ↑cexp 13968 abscabs 15141 Metcmet 21277 MetOpencmopn 21281 NrmCVeccnv 30564 +_𝑣 cpv 30565 BaseSetcba 30566 ·_𝑠OLD cns 30567 −_𝑣 cnsb 30569 norm_CVcnmcv 30570 IndMetcims 30571 SubSpcss 30701 CPreHil_OLDccphlo 30792 CBanccbn 30842

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084 ax-addf 11085 ax-mulf 11086

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-er 8622 df-map 8752 df-en 8870 df-dom 8871 df-sdom 8872 df-sup 9326 df-inf 9327 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-4 12190 df-n0 12382 df-z 12469 df-uz 12733 df-rp 12891 df-xadd 13012 df-seq 13909 df-exp 13969 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-xmet 21284 df-met 21285 df-grpo 30473 df-gid 30474 df-ginv 30475 df-gdiv 30476 df-ablo 30525 df-vc 30539 df-nv 30572 df-va 30575 df-ba 30576 df-sm 30577 df-0v 30578 df-vs 30579 df-nmcv 30580 df-ims 30581 df-ssp 30702 df-ph 30793 df-cbn 30843

This theorem is referenced by: minvecolem3 30856 minvecolem7 30863

W3C validator