Metamath Proof Explorer

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 · 𝐵 ) )