Theorem minvecolem2

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

	Ref	Expression
Hypotheses	minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
	minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
	minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
	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	minvecolem2	⊢ ( 𝜑 → ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ≤ ( 4 · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		minveco.x	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		minveco.m	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3		minveco.n	⊢ 𝑁 = ( normCV ‘ 𝑈 )
4		minveco.y	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
5		minveco.u	⊢ ( 𝜑 → 𝑈 ∈ CPreHilOLD )
6		minveco.w	⊢ ( 𝜑 → 𝑊 ∈ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) )
7		minveco.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
8		minveco.d	⊢ 𝐷 = ( IndMet ‘ 𝑈 )
9		minveco.j	⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
10		minveco.r	⊢ 𝑅 = ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
11		minveco.s	⊢ 𝑆 = inf ( 𝑅 , ℝ , < )
12		minvecolem2.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
13		minvecolem2.2	⊢ ( 𝜑 → 0 ≤ 𝐵 )
14		minvecolem2.3	⊢ ( 𝜑 → 𝐾 ∈ 𝑌 )
15		minvecolem2.4	⊢ ( 𝜑 → 𝐿 ∈ 𝑌 )
16		minvecolem2.5	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝐵 ) )
17		minvecolem2.6	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ≤ ( ( 𝑆 ↑ 2 ) + 𝐵 ) )
18		4re	⊢ 4 ∈ ℝ
19	1 2 3 4 5 6 7 8 9 10	minvecolem1	⊢ ( 𝜑 → ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
20	19	simp1d	⊢ ( 𝜑 → 𝑅 ⊆ ℝ )
21	19	simp2d	⊢ ( 𝜑 → 𝑅 ≠ ∅ )
22		0re	⊢ 0 ∈ ℝ
23	19	simp3d	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 )
24		breq1	⊢ ( 𝑥 = 0 → ( 𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤 ) )
25	24	ralbidv	⊢ ( 𝑥 = 0 → ( ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
26	25	rspcev	⊢ ( ( 0 ∈ ℝ ∧ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
27	22 23 26	sylancr	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 )
28		infrecl	⊢ ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
29	20 21 27 28	syl3anc	⊢ ( 𝜑 → inf ( 𝑅 , ℝ , < ) ∈ ℝ )
30	11 29	eqeltrid	⊢ ( 𝜑 → 𝑆 ∈ ℝ )
31	30	resqcld	⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℝ )
32		remulcl	⊢ ( ( 4 ∈ ℝ ∧ ( 𝑆 ↑ 2 ) ∈ ℝ ) → ( 4 · ( 𝑆 ↑ 2 ) ) ∈ ℝ )
33	18 31 32	sylancr	⊢ ( 𝜑 → ( 4 · ( 𝑆 ↑ 2 ) ) ∈ ℝ )
34		phnv	⊢ ( 𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec )
35	5 34	syl	⊢ ( 𝜑 → 𝑈 ∈ NrmCVec )
36	1 8	imsmet	⊢ ( 𝑈 ∈ NrmCVec → 𝐷 ∈ ( Met ‘ 𝑋 ) )
37	35 36	syl	⊢ ( 𝜑 → 𝐷 ∈ ( Met ‘ 𝑋 ) )
38		inss1	⊢ ( ( SubSp ‘ 𝑈 ) ∩ CBan ) ⊆ ( SubSp ‘ 𝑈 )
39	38 6	sselid	⊢ ( 𝜑 → 𝑊 ∈ ( SubSp ‘ 𝑈 ) )
40		eqid	⊢ ( SubSp ‘ 𝑈 ) = ( SubSp ‘ 𝑈 )
41	1 4 40	sspba	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑌 ⊆ 𝑋 )
42	35 39 41	syl2anc	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
43	42 14	sseldd	⊢ ( 𝜑 → 𝐾 ∈ 𝑋 )
44	42 15	sseldd	⊢ ( 𝜑 → 𝐿 ∈ 𝑋 )
45		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐾 𝐷 𝐿 ) ∈ ℝ )
46	37 43 44 45	syl3anc	⊢ ( 𝜑 → ( 𝐾 𝐷 𝐿 ) ∈ ℝ )
47	46	resqcld	⊢ ( 𝜑 → ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ∈ ℝ )
48	33 47	readdcld	⊢ ( 𝜑 → ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ )
49		ax-1cn	⊢ 1 ∈ ℂ
50		halfcl	⊢ ( 1 ∈ ℂ → ( 1 / 2 ) ∈ ℂ )
51	49 50	mp1i	⊢ ( 𝜑 → ( 1 / 2 ) ∈ ℂ )
52		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
53		eqid	⊢ ( +𝑣 ‘ 𝑊 ) = ( +𝑣 ‘ 𝑊 )
54	4 52 53 40	sspgval	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) ∧ ( 𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌 ) ) → ( 𝐾 ( +𝑣 ‘ 𝑊 ) 𝐿 ) = ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) )
55	35 39 14 15 54	syl22anc	⊢ ( 𝜑 → ( 𝐾 ( +𝑣 ‘ 𝑊 ) 𝐿 ) = ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) )
56	40	sspnv	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) → 𝑊 ∈ NrmCVec )
57	35 39 56	syl2anc	⊢ ( 𝜑 → 𝑊 ∈ NrmCVec )
58	4 53	nvgcl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝐾 ∈ 𝑌 ∧ 𝐿 ∈ 𝑌 ) → ( 𝐾 ( +𝑣 ‘ 𝑊 ) 𝐿 ) ∈ 𝑌 )
59	57 14 15 58	syl3anc	⊢ ( 𝜑 → ( 𝐾 ( +𝑣 ‘ 𝑊 ) 𝐿 ) ∈ 𝑌 )
60	55 59	eqeltrrd	⊢ ( 𝜑 → ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ∈ 𝑌 )
61		eqid	⊢ ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ 𝑈 )
62		eqid	⊢ ( ·𝑠OLD ‘ 𝑊 ) = ( ·𝑠OLD ‘ 𝑊 )
63	4 61 62 40	sspsval	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ ( SubSp ‘ 𝑈 ) ) ∧ ( ( 1 / 2 ) ∈ ℂ ∧ ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ∈ 𝑌 ) ) → ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) )
64	35 39 51 60 63	syl22anc	⊢ ( 𝜑 → ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) )
65	4 62	nvscl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ∈ 𝑌 ) → ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑌 )
66	57 51 60 65	syl3anc	⊢ ( 𝜑 → ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑊 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑌 )
67	64 66	eqeltrrd	⊢ ( 𝜑 → ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑌 )
68	42 67	sseldd	⊢ ( 𝜑 → ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑋 )
69	1 2	nvmcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑋 ) → ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ∈ 𝑋 )
70	35 7 68 69	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ∈ 𝑋 )
71	1 3	nvcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℝ )
72	35 70 71	syl2anc	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℝ )
73	72	resqcld	⊢ ( 𝜑 → ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ )
74		remulcl	⊢ ( ( 4 ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ ) → ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ∈ ℝ )
75	18 73 74	sylancr	⊢ ( 𝜑 → ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ∈ ℝ )
76	75 47	readdcld	⊢ ( 𝜑 → ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ )
77	31 12	readdcld	⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) + 𝐵 ) ∈ ℝ )
78		remulcl	⊢ ( ( 4 ∈ ℝ ∧ ( ( 𝑆 ↑ 2 ) + 𝐵 ) ∈ ℝ ) → ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ )
79	18 77 78	sylancr	⊢ ( 𝜑 → ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ )
80	22	a1i	⊢ ( 𝜑 → 0 ∈ ℝ )
81		infregelb	⊢ ( ( ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ) ∧ 0 ∈ ℝ ) → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
82	20 21 27 80 81	syl31anc	⊢ ( 𝜑 → ( 0 ≤ inf ( 𝑅 , ℝ , < ) ↔ ∀ 𝑤 ∈ 𝑅 0 ≤ 𝑤 ) )
83	23 82	mpbird	⊢ ( 𝜑 → 0 ≤ inf ( 𝑅 , ℝ , < ) )
84	83 11	breqtrrdi	⊢ ( 𝜑 → 0 ≤ 𝑆 )
85		eqid	⊢ ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) )
86		oveq2	⊢ ( 𝑦 = ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) → ( 𝐴 𝑀 𝑦 ) = ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) )
87	86	fveq2d	⊢ ( 𝑦 = ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) → ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) )
88	87	rspceeqv	⊢ ( ( ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑌 ∧ ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) → ∃ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
89	67 85 88	sylancl	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
90		eqid	⊢ ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) = ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
91		fvex	⊢ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ∈ V
92	90 91	elrnmpti	⊢ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) ↔ ∃ 𝑦 ∈ 𝑌 ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) )
93	89 92	sylibr	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ran ( 𝑦 ∈ 𝑌 ↦ ( 𝑁 ‘ ( 𝐴 𝑀 𝑦 ) ) ) )
94	93 10	eleqtrrdi	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ 𝑅 )
95		infrelb	⊢ ( ( 𝑅 ⊆ ℝ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑥 ≤ 𝑤 ∧ ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ 𝑅 ) → inf ( 𝑅 , ℝ , < ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) )
96	20 27 94 95	syl3anc	⊢ ( 𝜑 → inf ( 𝑅 , ℝ , < ) ≤ ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) )
97	11 96	eqbrtrid	⊢ ( 𝜑 → 𝑆 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) )
98		le2sq2	⊢ ( ( ( 𝑆 ∈ ℝ ∧ 0 ≤ 𝑆 ) ∧ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℝ ∧ 𝑆 ≤ ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) ) → ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) )
99	30 84 72 97 98	syl22anc	⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) )
100		4pos	⊢ 0 < 4
101	18 100	pm3.2i	⊢ ( 4 ∈ ℝ ∧ 0 < 4 )
102		lemul2	⊢ ( ( ( 𝑆 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) → ( ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ↔ ( 4 · ( 𝑆 ↑ 2 ) ) ≤ ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ) )
103	101 102	mp3an3	⊢ ( ( ( 𝑆 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ ) → ( ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ↔ ( 4 · ( 𝑆 ↑ 2 ) ) ≤ ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ) )
104	31 73 103	syl2anc	⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) ≤ ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ↔ ( 4 · ( 𝑆 ↑ 2 ) ) ≤ ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) ) )
105	99 104	mpbid	⊢ ( 𝜑 → ( 4 · ( 𝑆 ↑ 2 ) ) ≤ ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) )
106	33 75 47 105	leadd1dd	⊢ ( 𝜑 → ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) )
107		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐾 ) ∈ ℝ )
108	37 7 43 107	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝐷 𝐾 ) ∈ ℝ )
109	108	resqcld	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) ∈ ℝ )
110		metcl	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐿 ) ∈ ℝ )
111	37 7 44 110	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝐷 𝐿 ) ∈ ℝ )
112	111	resqcld	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ∈ ℝ )
113	109 112 77 77 16 17	le2addd	⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( ( ( 𝑆 ↑ 2 ) + 𝐵 ) + ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
114	77	recnd	⊢ ( 𝜑 → ( ( 𝑆 ↑ 2 ) + 𝐵 ) ∈ ℂ )
115	114	2timesd	⊢ ( 𝜑 → ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( ( ( 𝑆 ↑ 2 ) + 𝐵 ) + ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
116	113 115	breqtrrd	⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
117	109 112	readdcld	⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ )
118		2re	⊢ 2 ∈ ℝ
119		remulcl	⊢ ( ( 2 ∈ ℝ ∧ ( ( 𝑆 ↑ 2 ) + 𝐵 ) ∈ ℝ ) → ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ )
120	118 77 119	sylancr	⊢ ( 𝜑 → ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ )
121		2pos	⊢ 0 < 2
122	118 121	pm3.2i	⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
123		lemul2	⊢ ( ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ ∧ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ↔ ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) ≤ ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) ) )
124	122 123	mp3an3	⊢ ( ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ ∧ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ∈ ℝ ) → ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ↔ ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) ≤ ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) ) )
125	117 120 124	syl2anc	⊢ ( 𝜑 → ( ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ↔ ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) ≤ ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) ) )
126	116 125	mpbid	⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) ≤ ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) )
127	1 2	nvmcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐾 ) ∈ 𝑋 )
128	35 7 43 127	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝑀 𝐾 ) ∈ 𝑋 )
129	1 2	nvmcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐿 ) ∈ 𝑋 )
130	35 7 44 129	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝑀 𝐿 ) ∈ 𝑋 )
131	1 52 2 3	phpar2	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 𝑀 𝐾 ) ∈ 𝑋 ∧ ( 𝐴 𝑀 𝐿 ) ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) 𝑀 ( 𝐴 𝑀 𝐿 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐿 ) ) ↑ 2 ) ) ) )
132	5 128 130 131	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) 𝑀 ( 𝐴 𝑀 𝐿 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐿 ) ) ↑ 2 ) ) ) )
133		2cn	⊢ 2 ∈ ℂ
134	72	recnd	⊢ ( 𝜑 → ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℂ )
135		sqmul	⊢ ( ( 2 ∈ ℂ ∧ ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ∈ ℂ ) → ( ( 2 · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) )
136	133 134 135	sylancr	⊢ ( 𝜑 → ( ( 2 · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) )
137		sq2	⊢ ( 2 ↑ 2 ) = 4
138	137	oveq1i	⊢ ( ( 2 ↑ 2 ) · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) = ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) )
139	136 138	eqtrdi	⊢ ( 𝜑 → ( ( 2 · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) )
140	133	a1i	⊢ ( 𝜑 → 2 ∈ ℂ )
141	1 61 3	nvs	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ∈ 𝑋 ) → ( 𝑁 ‘ ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( ( abs ‘ 2 ) · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) )
142	35 140 70 141	syl3anc	⊢ ( 𝜑 → ( 𝑁 ‘ ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( ( abs ‘ 2 ) · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) )
143		0le2	⊢ 0 ≤ 2
144		absid	⊢ ( ( 2 ∈ ℝ ∧ 0 ≤ 2 ) → ( abs ‘ 2 ) = 2 )
145	118 143 144	mp2an	⊢ ( abs ‘ 2 ) = 2
146	145	oveq1i	⊢ ( ( abs ‘ 2 ) · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( 2 · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) )
147	142 146	eqtrdi	⊢ ( 𝜑 → ( 𝑁 ‘ ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( 2 · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) )
148	1 2 61	nvmdi	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 2 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ∈ 𝑋 ) ) → ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) = ( ( 2 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) 𝑀 ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) )
149	35 140 7 68 148	syl13anc	⊢ ( 𝜑 → ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) = ( ( 2 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) 𝑀 ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) )
150	1 52 61	nv2	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐴 ) = ( 2 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) )
151	35 7 150	syl2anc	⊢ ( 𝜑 → ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐴 ) = ( 2 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) )
152		2ne0	⊢ 2 ≠ 0
153	133 152	recidi	⊢ ( 2 · ( 1 / 2 ) ) = 1
154	153	oveq1i	⊢ ( ( 2 · ( 1 / 2 ) ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( 1 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) )
155	1 52	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ∈ 𝑋 )
156	35 43 44 155	syl3anc	⊢ ( 𝜑 → ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ∈ 𝑋 )
157	1 61	nvsid	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ∈ 𝑋 ) → ( 1 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) )
158	35 156 157	syl2anc	⊢ ( 𝜑 → ( 1 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) )
159	154 158	eqtrid	⊢ ( 𝜑 → ( ( 2 · ( 1 / 2 ) ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) )
160	1 61	nvsass	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 2 ∈ ℂ ∧ ( 1 / 2 ) ∈ ℂ ∧ ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ∈ 𝑋 ) ) → ( ( 2 · ( 1 / 2 ) ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) )
161	35 140 51 156 160	syl13anc	⊢ ( 𝜑 → ( ( 2 · ( 1 / 2 ) ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) )
162	159 161	eqtr3d	⊢ ( 𝜑 → ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) = ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) )
163	151 162	oveq12d	⊢ ( 𝜑 → ( ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐴 ) 𝑀 ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( ( 2 ( ·𝑠OLD ‘ 𝑈 ) 𝐴 ) 𝑀 ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) )
164	1 52 2	nvaddsub4	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) ) → ( ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐴 ) 𝑀 ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) )
165	35 7 7 43 44 164	syl122anc	⊢ ( 𝜑 → ( ( 𝐴 ( +𝑣 ‘ 𝑈 ) 𝐴 ) 𝑀 ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) = ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) )
166	149 163 165	3eqtr2d	⊢ ( 𝜑 → ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) = ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) )
167	166	fveq2d	⊢ ( 𝜑 → ( 𝑁 ‘ ( 2 ( ·𝑠OLD ‘ 𝑈 ) ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) ) )
168	147 167	eqtr3d	⊢ ( 𝜑 → ( 2 · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) ) )
169	168	oveq1d	⊢ ( 𝜑 → ( ( 2 · ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) ) ↑ 2 ) )
170	139 169	eqtr3d	⊢ ( 𝜑 → ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) = ( ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) ) ↑ 2 ) )
171	1 2 3 8	imsdval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐿 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) → ( 𝐿 𝐷 𝐾 ) = ( 𝑁 ‘ ( 𝐿 𝑀 𝐾 ) ) )
172	35 44 43 171	syl3anc	⊢ ( 𝜑 → ( 𝐿 𝐷 𝐾 ) = ( 𝑁 ‘ ( 𝐿 𝑀 𝐾 ) ) )
173		metsym	⊢ ( ( 𝐷 ∈ ( Met ‘ 𝑋 ) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐾 𝐷 𝐿 ) = ( 𝐿 𝐷 𝐾 ) )
174	37 43 44 173	syl3anc	⊢ ( 𝜑 → ( 𝐾 𝐷 𝐿 ) = ( 𝐿 𝐷 𝐾 ) )
175	1 2	nvnnncan1	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) ) → ( ( 𝐴 𝑀 𝐾 ) 𝑀 ( 𝐴 𝑀 𝐿 ) ) = ( 𝐿 𝑀 𝐾 ) )
176	35 7 43 44 175	syl13anc	⊢ ( 𝜑 → ( ( 𝐴 𝑀 𝐾 ) 𝑀 ( 𝐴 𝑀 𝐿 ) ) = ( 𝐿 𝑀 𝐾 ) )
177	176	fveq2d	⊢ ( 𝜑 → ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) 𝑀 ( 𝐴 𝑀 𝐿 ) ) ) = ( 𝑁 ‘ ( 𝐿 𝑀 𝐾 ) ) )
178	172 174 177	3eqtr4d	⊢ ( 𝜑 → ( 𝐾 𝐷 𝐿 ) = ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) 𝑀 ( 𝐴 𝑀 𝐿 ) ) ) )
179	178	oveq1d	⊢ ( 𝜑 → ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) 𝑀 ( 𝐴 𝑀 𝐿 ) ) ) ↑ 2 ) )
180	170 179	oveq12d	⊢ ( 𝜑 → ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) ( +𝑣 ‘ 𝑈 ) ( 𝐴 𝑀 𝐿 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝑀 𝐾 ) 𝑀 ( 𝐴 𝑀 𝐿 ) ) ) ↑ 2 ) ) )
181	1 2 3 8	imsdval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐾 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐾 ) ) )
182	35 7 43 181	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝐷 𝐾 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐾 ) ) )
183	182	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐾 ) ) ↑ 2 ) )
184	1 2 3 8	imsdval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐿 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐿 ) ) )
185	35 7 44 184	syl3anc	⊢ ( 𝜑 → ( 𝐴 𝐷 𝐿 ) = ( 𝑁 ‘ ( 𝐴 𝑀 𝐿 ) ) )
186	185	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) = ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐿 ) ) ↑ 2 ) )
187	183 186	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐿 ) ) ↑ 2 ) ) )
188	187	oveq2d	⊢ ( 𝜑 → ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( 𝐴 𝑀 𝐿 ) ) ↑ 2 ) ) ) )
189	132 180 188	3eqtr4d	⊢ ( 𝜑 → ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) = ( 2 · ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) )
190		2t2e4	⊢ ( 2 · 2 ) = 4
191	190	oveq1i	⊢ ( ( 2 · 2 ) · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) )
192	140 140 114	mulassd	⊢ ( 𝜑 → ( ( 2 · 2 ) · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) )
193	191 192	eqtr3id	⊢ ( 𝜑 → ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( 2 · ( 2 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) ) )
194	126 189 193	3brtr4d	⊢ ( 𝜑 → ( ( 4 · ( ( 𝑁 ‘ ( 𝐴 𝑀 ( ( 1 / 2 ) ( ·𝑠OLD ‘ 𝑈 ) ( 𝐾 ( +𝑣 ‘ 𝑈 ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
195	48 76 79 106 194	letrd	⊢ ( 𝜑 → ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) )
196		4cn	⊢ 4 ∈ ℂ
197	196	a1i	⊢ ( 𝜑 → 4 ∈ ℂ )
198	31	recnd	⊢ ( 𝜑 → ( 𝑆 ↑ 2 ) ∈ ℂ )
199	12	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
200	197 198 199	adddid	⊢ ( 𝜑 → ( 4 · ( ( 𝑆 ↑ 2 ) + 𝐵 ) ) = ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( 4 · 𝐵 ) ) )
201	195 200	breqtrd	⊢ ( 𝜑 → ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( 4 · 𝐵 ) ) )
202		remulcl	⊢ ( ( 4 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 4 · 𝐵 ) ∈ ℝ )
203	18 12 202	sylancr	⊢ ( 𝜑 → ( 4 · 𝐵 ) ∈ ℝ )
204	47 203 33	leadd2d	⊢ ( 𝜑 → ( ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ≤ ( 4 · 𝐵 ) ↔ ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≤ ( ( 4 · ( 𝑆 ↑ 2 ) ) + ( 4 · 𝐵 ) ) ) )
205	201 204	mpbird	⊢ ( 𝜑 → ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ≤ ( 4 · 𝐵 ) )