Metamath Proof Explorer

Theorem minveclem2

Description: Lemma for minvec . 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 Mario Carneiro, 15-Oct-2015) (Revised by AV, 3-Oct-2020)

Ref Expression
Hypotheses minvec.x ⊒ 𝑋 = ( Base β€˜ π‘ˆ )
minvec.m ⊒ βˆ’ = ( -g β€˜ π‘ˆ )
minvec.n ⊒ 𝑁 = ( norm β€˜ π‘ˆ )
minvec.u ⊒ ( πœ‘ β†’ π‘ˆ ∈ β„‚PreHil )
minvec.y ⊒ ( πœ‘ β†’ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) )
minvec.w ⊒ ( πœ‘ β†’ ( π‘ˆ β†Ύs π‘Œ ) ∈ CMetSp )
minvec.a ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
minvec.j ⊒ 𝐽 = ( TopOpen β€˜ π‘ˆ )
minvec.r ⊒ 𝑅 = ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
minvec.s ⊒ 𝑆 = inf ( 𝑅 , ℝ , < )
minvec.d ⊒ 𝐷 = ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) )
minveclem2.1 ⊒ ( πœ‘ β†’ 𝐡 ∈ ℝ )
minveclem2.2 ⊒ ( πœ‘ β†’ 0 ≀ 𝐡 )
minveclem2.3 ⊒ ( πœ‘ β†’ 𝐾 ∈ π‘Œ )
minveclem2.4 ⊒ ( πœ‘ β†’ 𝐿 ∈ π‘Œ )
minveclem2.5 ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + 𝐡 ) )
minveclem2.6 ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + 𝐡 ) )
Assertion minveclem2 ( πœ‘ β†’ ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ≀ ( 4 Β· 𝐡 ) )

Proof

Step Hyp Ref Expression
1 minvec.x ⊒ 𝑋 = ( Base β€˜ π‘ˆ )
2 minvec.m ⊒ βˆ’ = ( -g β€˜ π‘ˆ )
3 minvec.n ⊒ 𝑁 = ( norm β€˜ π‘ˆ )
4 minvec.u ⊒ ( πœ‘ β†’ π‘ˆ ∈ β„‚PreHil )
5 minvec.y ⊒ ( πœ‘ β†’ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) )
6 minvec.w ⊒ ( πœ‘ β†’ ( π‘ˆ β†Ύs π‘Œ ) ∈ CMetSp )
7 minvec.a ⊒ ( πœ‘ β†’ 𝐴 ∈ 𝑋 )
8 minvec.j ⊒ 𝐽 = ( TopOpen β€˜ π‘ˆ )
9 minvec.r ⊒ 𝑅 = ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
10 minvec.s ⊒ 𝑆 = inf ( 𝑅 , ℝ , < )
11 minvec.d ⊒ 𝐷 = ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) )
12 minveclem2.1 ⊒ ( πœ‘ β†’ 𝐡 ∈ ℝ )
13 minveclem2.2 ⊒ ( πœ‘ β†’ 0 ≀ 𝐡 )
14 minveclem2.3 ⊒ ( πœ‘ β†’ 𝐾 ∈ π‘Œ )
15 minveclem2.4 ⊒ ( πœ‘ β†’ 𝐿 ∈ π‘Œ )
16 minveclem2.5 ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + 𝐡 ) )
17 minveclem2.6 ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ≀ ( ( 𝑆 ↑ 2 ) + 𝐡 ) )
18 4re ⊒ 4 ∈ ℝ
19 1 2 3 4 5 6 7 8 9 10 minveclem4c ⊒ ( πœ‘ β†’ 𝑆 ∈ ℝ )
20 19 resqcld ⊒ ( πœ‘ β†’ ( 𝑆 ↑ 2 ) ∈ ℝ )
21 remulcl ⊒ ( ( 4 ∈ ℝ ∧ ( 𝑆 ↑ 2 ) ∈ ℝ ) β†’ ( 4 Β· ( 𝑆 ↑ 2 ) ) ∈ ℝ )
22 18 20 21 sylancr ⊒ ( πœ‘ β†’ ( 4 Β· ( 𝑆 ↑ 2 ) ) ∈ ℝ )
23 cphngp ⊒ ( π‘ˆ ∈ β„‚PreHil β†’ π‘ˆ ∈ NrmGrp )
24 4 23 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ NrmGrp )
25 ngpms ⊒ ( π‘ˆ ∈ NrmGrp β†’ π‘ˆ ∈ MetSp )
26 24 25 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ MetSp )
27 1 11 msmet ⊒ ( π‘ˆ ∈ MetSp β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
28 26 27 syl ⊒ ( πœ‘ β†’ 𝐷 ∈ ( Met β€˜ 𝑋 ) )
29 eqid ⊒ ( LSubSp β€˜ π‘ˆ ) = ( LSubSp β€˜ π‘ˆ )
30 1 29 lssss ⊒ ( π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) β†’ π‘Œ βŠ† 𝑋 )
31 5 30 syl ⊒ ( πœ‘ β†’ π‘Œ βŠ† 𝑋 )
32 31 14 sseldd ⊒ ( πœ‘ β†’ 𝐾 ∈ 𝑋 )
33 31 15 sseldd ⊒ ( πœ‘ β†’ 𝐿 ∈ 𝑋 )
34 metcl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) β†’ ( 𝐾 𝐷 𝐿 ) ∈ ℝ )
35 28 32 33 34 syl3anc ⊒ ( πœ‘ β†’ ( 𝐾 𝐷 𝐿 ) ∈ ℝ )
36 35 resqcld ⊒ ( πœ‘ β†’ ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ∈ ℝ )
37 22 36 readdcld ⊒ ( πœ‘ β†’ ( ( 4 Β· ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ )
38 cphlmod ⊒ ( π‘ˆ ∈ β„‚PreHil β†’ π‘ˆ ∈ LMod )
39 4 38 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ LMod )
40 cphclm ⊒ ( π‘ˆ ∈ β„‚PreHil β†’ π‘ˆ ∈ β„‚Mod )
41 4 40 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ β„‚Mod )
42 eqid ⊒ ( Scalar β€˜ π‘ˆ ) = ( Scalar β€˜ π‘ˆ )
43 eqid ⊒ ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) = ( Base β€˜ ( Scalar β€˜ π‘ˆ ) )
44 42 43 clmzss ⊒ ( π‘ˆ ∈ β„‚Mod β†’ β„€ βŠ† ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) )
45 41 44 syl ⊒ ( πœ‘ β†’ β„€ βŠ† ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) )
46 2z ⊒ 2 ∈ β„€
47 46 a1i ⊒ ( πœ‘ β†’ 2 ∈ β„€ )
48 45 47 sseldd ⊒ ( πœ‘ β†’ 2 ∈ ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) )
49 2ne0 ⊒ 2 β‰  0
50 49 a1i ⊒ ( πœ‘ β†’ 2 β‰  0 )
51 42 43 cphreccl ⊒ ( ( π‘ˆ ∈ β„‚PreHil ∧ 2 ∈ ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) ∧ 2 β‰  0 ) β†’ ( 1 / 2 ) ∈ ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) )
52 4 48 50 51 syl3anc ⊒ ( πœ‘ β†’ ( 1 / 2 ) ∈ ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) )
53 eqid ⊒ ( +g β€˜ π‘ˆ ) = ( +g β€˜ π‘ˆ )
54 53 29 lssvacl ⊒ ( ( ( π‘ˆ ∈ LMod ∧ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) ) ∧ ( 𝐾 ∈ π‘Œ ∧ 𝐿 ∈ π‘Œ ) ) β†’ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ∈ π‘Œ )
55 39 5 14 15 54 syl22anc ⊒ ( πœ‘ β†’ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ∈ π‘Œ )
56 eqid ⊒ ( ·𝑠 β€˜ π‘ˆ ) = ( ·𝑠 β€˜ π‘ˆ )
57 42 56 43 29 lssvscl ⊒ ( ( ( π‘ˆ ∈ LMod ∧ π‘Œ ∈ ( LSubSp β€˜ π‘ˆ ) ) ∧ ( ( 1 / 2 ) ∈ ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) ∧ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ∈ π‘Œ ) ) β†’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ∈ π‘Œ )
58 39 5 52 55 57 syl22anc ⊒ ( πœ‘ β†’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ∈ π‘Œ )
59 31 58 sseldd ⊒ ( πœ‘ β†’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ∈ 𝑋 )
60 1 2 lmodvsubcl ⊒ ( ( π‘ˆ ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ∈ 𝑋 ) β†’ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ∈ 𝑋 )
61 39 7 59 60 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ∈ 𝑋 )
62 1 3 nmcl ⊒ ( ( π‘ˆ ∈ NrmGrp ∧ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ∈ ℝ )
63 24 61 62 syl2anc ⊒ ( πœ‘ β†’ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ∈ ℝ )
64 63 resqcld ⊒ ( πœ‘ β†’ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ )
65 remulcl ⊒ ( ( 4 ∈ ℝ ∧ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ ) β†’ ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) ∈ ℝ )
66 18 64 65 sylancr ⊒ ( πœ‘ β†’ ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) ∈ ℝ )
67 66 36 readdcld ⊒ ( πœ‘ β†’ ( ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ∈ ℝ )
68 20 12 readdcld ⊒ ( πœ‘ β†’ ( ( 𝑆 ↑ 2 ) + 𝐡 ) ∈ ℝ )
69 remulcl ⊒ ( ( 4 ∈ ℝ ∧ ( ( 𝑆 ↑ 2 ) + 𝐡 ) ∈ ℝ ) β†’ ( 4 Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) ∈ ℝ )
70 18 68 69 sylancr ⊒ ( πœ‘ β†’ ( 4 Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) ∈ ℝ )
71 1 2 3 4 5 6 7 8 9 minveclem1 ⊒ ( πœ‘ β†’ ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
72 71 simp3d ⊒ ( πœ‘ β†’ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 )
73 71 simp1d ⊒ ( πœ‘ β†’ 𝑅 βŠ† ℝ )
74 71 simp2d ⊒ ( πœ‘ β†’ 𝑅 β‰  βˆ… )
75 0re ⊒ 0 ∈ ℝ
76 breq1 ⊒ ( π‘₯ = 0 β†’ ( π‘₯ ≀ 𝑀 ↔ 0 ≀ 𝑀 ) )
77 76 ralbidv ⊒ ( π‘₯ = 0 β†’ ( βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 ↔ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
78 77 rspcev ⊒ ( ( 0 ∈ ℝ ∧ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) β†’ βˆƒ π‘₯ ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 )
79 75 72 78 sylancr ⊒ ( πœ‘ β†’ βˆƒ π‘₯ ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 )
80 75 a1i ⊒ ( πœ‘ β†’ 0 ∈ ℝ )
81 infregelb ⊒ ( ( ( 𝑅 βŠ† ℝ ∧ 𝑅 β‰  βˆ… ∧ βˆƒ π‘₯ ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 ) ∧ 0 ∈ ℝ ) β†’ ( 0 ≀ inf ( 𝑅 , ℝ , < ) ↔ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
82 73 74 79 80 81 syl31anc ⊒ ( πœ‘ β†’ ( 0 ≀ inf ( 𝑅 , ℝ , < ) ↔ βˆ€ 𝑀 ∈ 𝑅 0 ≀ 𝑀 ) )
83 72 82 mpbird ⊒ ( πœ‘ β†’ 0 ≀ inf ( 𝑅 , ℝ , < ) )
84 83 10 breqtrrdi ⊒ ( πœ‘ β†’ 0 ≀ 𝑆 )
85 eqid ⊒ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) )
86 oveq2 ⊒ ( 𝑦 = ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) β†’ ( 𝐴 βˆ’ 𝑦 ) = ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) )
87 86 fveq2d ⊒ ( 𝑦 = ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) β†’ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) )
88 87 rspceeqv ⊒ ( ( ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ∈ π‘Œ ∧ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) β†’ βˆƒ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
89 58 85 88 sylancl ⊒ ( πœ‘ β†’ βˆƒ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
90 eqid ⊒ ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) = ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
91 fvex ⊒ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ∈ V
92 90 91 elrnmpti ⊒ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) ↔ βˆƒ 𝑦 ∈ π‘Œ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) )
93 89 92 sylibr ⊒ ( πœ‘ β†’ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ∈ ran ( 𝑦 ∈ π‘Œ ↦ ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝑦 ) ) ) )
94 93 9 eleqtrrdi ⊒ ( πœ‘ β†’ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ∈ 𝑅 )
95 infrelb ⊒ ( ( 𝑅 βŠ† ℝ ∧ βˆƒ π‘₯ ∈ ℝ βˆ€ 𝑀 ∈ 𝑅 π‘₯ ≀ 𝑀 ∧ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ∈ 𝑅 ) β†’ inf ( 𝑅 , ℝ , < ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) )
96 73 79 94 95 syl3anc ⊒ ( πœ‘ β†’ inf ( 𝑅 , ℝ , < ) ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) )
97 10 96 eqbrtrid ⊒ ( πœ‘ β†’ 𝑆 ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) )
98 le2sq2 ⊒ ( ( ( 𝑆 ∈ ℝ ∧ 0 ≀ 𝑆 ) ∧ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ∈ ℝ ∧ 𝑆 ≀ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) ) β†’ ( 𝑆 ↑ 2 ) ≀ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) )
99 19 84 63 97 98 syl22anc ⊒ ( πœ‘ β†’ ( 𝑆 ↑ 2 ) ≀ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) )
100 4pos ⊒ 0 < 4
101 18 100 pm3.2i ⊒ ( 4 ∈ ℝ ∧ 0 < 4 )
102 lemul2 ⊒ ( ( ( 𝑆 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ ∧ ( 4 ∈ ℝ ∧ 0 < 4 ) ) β†’ ( ( 𝑆 ↑ 2 ) ≀ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ↔ ( 4 Β· ( 𝑆 ↑ 2 ) ) ≀ ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) ) )
103 101 102 mp3an3 ⊒ ( ( ( 𝑆 ↑ 2 ) ∈ ℝ ∧ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ∈ ℝ ) β†’ ( ( 𝑆 ↑ 2 ) ≀ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ↔ ( 4 Β· ( 𝑆 ↑ 2 ) ) ≀ ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) ) )
104 20 64 103 syl2anc ⊒ ( πœ‘ β†’ ( ( 𝑆 ↑ 2 ) ≀ ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ↔ ( 4 Β· ( 𝑆 ↑ 2 ) ) ≀ ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) ) )
105 99 104 mpbid ⊒ ( πœ‘ β†’ ( 4 Β· ( 𝑆 ↑ 2 ) ) ≀ ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) )
106 22 66 36 105 leadd1dd ⊒ ( πœ‘ β†’ ( ( 4 Β· ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≀ ( ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) )
107 metcl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) β†’ ( 𝐴 𝐷 𝐾 ) ∈ ℝ )
108 28 7 32 107 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝐾 ) ∈ ℝ )
109 108 resqcld ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) ∈ ℝ )
110 metcl ⊒ ( ( 𝐷 ∈ ( Met β€˜ 𝑋 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) β†’ ( 𝐴 𝐷 𝐿 ) ∈ ℝ )
111 28 7 33 110 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝐿 ) ∈ ℝ )
112 111 resqcld ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ∈ ℝ )
113 109 112 68 68 16 17 le2addd ⊒ ( πœ‘ β†’ ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ≀ ( ( ( 𝑆 ↑ 2 ) + 𝐡 ) + ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) )
114 68 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 68 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 lmodvsubcl ⊒ ( ( π‘ˆ ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) β†’ ( 𝐴 βˆ’ 𝐾 ) ∈ 𝑋 )
128 39 7 32 127 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 βˆ’ 𝐾 ) ∈ 𝑋 )
129 1 2 lmodvsubcl ⊒ ( ( π‘ˆ ∈ LMod ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) β†’ ( 𝐴 βˆ’ 𝐿 ) ∈ 𝑋 )
130 39 7 33 129 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 βˆ’ 𝐿 ) ∈ 𝑋 )
131 1 53 2 3 nmpar ⊒ ( ( π‘ˆ ∈ β„‚PreHil ∧ ( 𝐴 βˆ’ 𝐾 ) ∈ 𝑋 ∧ ( 𝐴 βˆ’ 𝐿 ) ∈ 𝑋 ) β†’ ( ( ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) ) ↑ 2 ) + ( ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) βˆ’ ( 𝐴 βˆ’ 𝐿 ) ) ) ↑ 2 ) ) = ( 2 Β· ( ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐿 ) ) ↑ 2 ) ) ) )
132 4 128 130 131 syl3anc ⊒ ( πœ‘ β†’ ( ( ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) ) ↑ 2 ) + ( ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) βˆ’ ( 𝐴 βˆ’ 𝐿 ) ) ) ↑ 2 ) ) = ( 2 Β· ( ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐿 ) ) ↑ 2 ) ) ) )
133 2cn ⊒ 2 ∈ β„‚
134 63 recnd ⊒ ( πœ‘ β†’ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ∈ β„‚ )
135 sqmul ⊒ ( ( 2 ∈ β„‚ ∧ ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ∈ β„‚ ) β†’ ( ( 2 Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) )
136 133 134 135 sylancr ⊒ ( πœ‘ β†’ ( ( 2 Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( ( 2 ↑ 2 ) Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) )
137 sq2 ⊒ ( 2 ↑ 2 ) = 4
138 137 oveq1i ⊒ ( ( 2 ↑ 2 ) Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) = ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) )
139 136 138 eqtrdi ⊒ ( πœ‘ β†’ ( ( 2 Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) )
140 1 3 56 42 43 cphnmvs ⊒ ( ( π‘ˆ ∈ β„‚PreHil ∧ 2 ∈ ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) ∧ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ∈ 𝑋 ) β†’ ( 𝑁 β€˜ ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) = ( ( abs β€˜ 2 ) Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) )
141 4 48 61 140 syl3anc ⊒ ( πœ‘ β†’ ( 𝑁 β€˜ ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) = ( ( abs β€˜ 2 ) Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) )
142 0le2 ⊒ 0 ≀ 2
143 absid ⊒ ( ( 2 ∈ ℝ ∧ 0 ≀ 2 ) β†’ ( abs β€˜ 2 ) = 2 )
144 118 142 143 mp2an ⊒ ( abs β€˜ 2 ) = 2
145 144 oveq1i ⊒ ( ( abs β€˜ 2 ) Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) = ( 2 Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) )
146 141 145 eqtrdi ⊒ ( πœ‘ β†’ ( 𝑁 β€˜ ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) = ( 2 Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) )
147 1 56 42 43 2 39 48 7 59 lmodsubdi ⊒ ( πœ‘ β†’ ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) = ( ( 2 ( ·𝑠 β€˜ π‘ˆ ) 𝐴 ) βˆ’ ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) )
148 eqid ⊒ ( .g β€˜ π‘ˆ ) = ( .g β€˜ π‘ˆ )
149 1 148 53 mulg2 ⊒ ( 𝐴 ∈ 𝑋 β†’ ( 2 ( .g β€˜ π‘ˆ ) 𝐴 ) = ( 𝐴 ( +g β€˜ π‘ˆ ) 𝐴 ) )
150 7 149 syl ⊒ ( πœ‘ β†’ ( 2 ( .g β€˜ π‘ˆ ) 𝐴 ) = ( 𝐴 ( +g β€˜ π‘ˆ ) 𝐴 ) )
151 1 148 56 clmmulg ⊒ ( ( π‘ˆ ∈ β„‚Mod ∧ 2 ∈ β„€ ∧ 𝐴 ∈ 𝑋 ) β†’ ( 2 ( .g β€˜ π‘ˆ ) 𝐴 ) = ( 2 ( ·𝑠 β€˜ π‘ˆ ) 𝐴 ) )
152 41 47 7 151 syl3anc ⊒ ( πœ‘ β†’ ( 2 ( .g β€˜ π‘ˆ ) 𝐴 ) = ( 2 ( ·𝑠 β€˜ π‘ˆ ) 𝐴 ) )
153 150 152 eqtr3d ⊒ ( πœ‘ β†’ ( 𝐴 ( +g β€˜ π‘ˆ ) 𝐴 ) = ( 2 ( ·𝑠 β€˜ π‘ˆ ) 𝐴 ) )
154 1 53 lmodvacl ⊒ ( ( π‘ˆ ∈ LMod ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) β†’ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ∈ 𝑋 )
155 39 32 33 154 syl3anc ⊒ ( πœ‘ β†’ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ∈ 𝑋 )
156 1 56 clmvs1 ⊒ ( ( π‘ˆ ∈ β„‚Mod ∧ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ∈ 𝑋 ) β†’ ( 1 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) = ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) )
157 41 155 156 syl2anc ⊒ ( πœ‘ β†’ ( 1 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) = ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) )
158 133 49 recidi ⊒ ( 2 · ( 1 / 2 ) ) = 1
159 158 oveq1i ⊒ ( ( 2 Β· ( 1 / 2 ) ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) = ( 1 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) )
160 1 42 56 43 clmvsass ⊒ ( ( π‘ˆ ∈ β„‚Mod ∧ ( 2 ∈ ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) ∧ ( 1 / 2 ) ∈ ( Base β€˜ ( Scalar β€˜ π‘ˆ ) ) ∧ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ∈ 𝑋 ) ) β†’ ( ( 2 Β· ( 1 / 2 ) ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) = ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) )
161 41 48 52 155 160 syl13anc ⊒ ( πœ‘ β†’ ( ( 2 Β· ( 1 / 2 ) ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) = ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) )
162 159 161 eqtr3id ⊒ ( πœ‘ β†’ ( 1 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) = ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) )
163 157 162 eqtr3d ⊒ ( πœ‘ β†’ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) = ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) )
164 153 163 oveq12d ⊒ ( πœ‘ β†’ ( ( 𝐴 ( +g β€˜ π‘ˆ ) 𝐴 ) βˆ’ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) = ( ( 2 ( ·𝑠 β€˜ π‘ˆ ) 𝐴 ) βˆ’ ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) )
165 lmodabl ⊒ ( π‘ˆ ∈ LMod β†’ π‘ˆ ∈ Abel )
166 39 165 syl ⊒ ( πœ‘ β†’ π‘ˆ ∈ Abel )
167 1 53 2 ablsub4 ⊒ ( ( π‘ˆ ∈ Abel ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ∧ ( 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) ) β†’ ( ( 𝐴 ( +g β€˜ π‘ˆ ) 𝐴 ) βˆ’ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) = ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) )
168 166 7 7 32 33 167 syl122anc ⊒ ( πœ‘ β†’ ( ( 𝐴 ( +g β€˜ π‘ˆ ) 𝐴 ) βˆ’ ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) = ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) )
169 147 164 168 3eqtr2d ⊒ ( πœ‘ β†’ ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) = ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) )
170 169 fveq2d ⊒ ( πœ‘ β†’ ( 𝑁 β€˜ ( 2 ( ·𝑠 β€˜ π‘ˆ ) ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) = ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) ) )
171 146 170 eqtr3d ⊒ ( πœ‘ β†’ ( 2 Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) = ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) ) )
172 171 oveq1d ⊒ ( πœ‘ β†’ ( ( 2 Β· ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ) ↑ 2 ) = ( ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) ) ↑ 2 ) )
173 139 172 eqtr3d ⊒ ( πœ‘ β†’ ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) = ( ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) ) ↑ 2 ) )
174 eqid ⊒ ( dist β€˜ π‘ˆ ) = ( dist β€˜ π‘ˆ )
175 3 1 2 174 ngpdsr ⊒ ( ( π‘ˆ ∈ NrmGrp ∧ 𝐾 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) β†’ ( 𝐾 ( dist β€˜ π‘ˆ ) 𝐿 ) = ( 𝑁 β€˜ ( 𝐿 βˆ’ 𝐾 ) ) )
176 24 32 33 175 syl3anc ⊒ ( πœ‘ β†’ ( 𝐾 ( dist β€˜ π‘ˆ ) 𝐿 ) = ( 𝑁 β€˜ ( 𝐿 βˆ’ 𝐾 ) ) )
177 11 oveqi ⊒ ( 𝐾 𝐷 𝐿 ) = ( 𝐾 ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) ) 𝐿 )
178 32 33 ovresd ⊒ ( πœ‘ β†’ ( 𝐾 ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) ) 𝐿 ) = ( 𝐾 ( dist β€˜ π‘ˆ ) 𝐿 ) )
179 177 178 eqtrid ⊒ ( πœ‘ β†’ ( 𝐾 𝐷 𝐿 ) = ( 𝐾 ( dist β€˜ π‘ˆ ) 𝐿 ) )
180 1 2 166 7 32 33 ablnnncan1 ⊒ ( πœ‘ β†’ ( ( 𝐴 βˆ’ 𝐾 ) βˆ’ ( 𝐴 βˆ’ 𝐿 ) ) = ( 𝐿 βˆ’ 𝐾 ) )
181 180 fveq2d ⊒ ( πœ‘ β†’ ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) βˆ’ ( 𝐴 βˆ’ 𝐿 ) ) ) = ( 𝑁 β€˜ ( 𝐿 βˆ’ 𝐾 ) ) )
182 176 179 181 3eqtr4d ⊒ ( πœ‘ β†’ ( 𝐾 𝐷 𝐿 ) = ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) βˆ’ ( 𝐴 βˆ’ 𝐿 ) ) ) )
183 182 oveq1d ⊒ ( πœ‘ β†’ ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) = ( ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) βˆ’ ( 𝐴 βˆ’ 𝐿 ) ) ) ↑ 2 ) )
184 173 183 oveq12d ⊒ ( πœ‘ β†’ ( ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) = ( ( ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) ( +g β€˜ π‘ˆ ) ( 𝐴 βˆ’ 𝐿 ) ) ) ↑ 2 ) + ( ( 𝑁 β€˜ ( ( 𝐴 βˆ’ 𝐾 ) βˆ’ ( 𝐴 βˆ’ 𝐿 ) ) ) ↑ 2 ) ) )
185 11 oveqi ⊒ ( 𝐴 𝐷 𝐾 ) = ( 𝐴 ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) ) 𝐾 )
186 7 32 ovresd ⊒ ( πœ‘ β†’ ( 𝐴 ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) ) 𝐾 ) = ( 𝐴 ( dist β€˜ π‘ˆ ) 𝐾 ) )
187 185 186 eqtrid ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝐾 ) = ( 𝐴 ( dist β€˜ π‘ˆ ) 𝐾 ) )
188 3 1 2 174 ngpds ⊒ ( ( π‘ˆ ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐾 ∈ 𝑋 ) β†’ ( 𝐴 ( dist β€˜ π‘ˆ ) 𝐾 ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐾 ) ) )
189 24 7 32 188 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 ( dist β€˜ π‘ˆ ) 𝐾 ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐾 ) ) )
190 187 189 eqtrd ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝐾 ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐾 ) ) )
191 190 oveq1d ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) = ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐾 ) ) ↑ 2 ) )
192 11 oveqi ⊒ ( 𝐴 𝐷 𝐿 ) = ( 𝐴 ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) ) 𝐿 )
193 7 33 ovresd ⊒ ( πœ‘ β†’ ( 𝐴 ( ( dist β€˜ π‘ˆ ) β†Ύ ( 𝑋 Γ— 𝑋 ) ) 𝐿 ) = ( 𝐴 ( dist β€˜ π‘ˆ ) 𝐿 ) )
194 192 193 eqtrid ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝐿 ) = ( 𝐴 ( dist β€˜ π‘ˆ ) 𝐿 ) )
195 3 1 2 174 ngpds ⊒ ( ( π‘ˆ ∈ NrmGrp ∧ 𝐴 ∈ 𝑋 ∧ 𝐿 ∈ 𝑋 ) β†’ ( 𝐴 ( dist β€˜ π‘ˆ ) 𝐿 ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐿 ) ) )
196 24 7 33 195 syl3anc ⊒ ( πœ‘ β†’ ( 𝐴 ( dist β€˜ π‘ˆ ) 𝐿 ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐿 ) ) )
197 194 196 eqtrd ⊒ ( πœ‘ β†’ ( 𝐴 𝐷 𝐿 ) = ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐿 ) ) )
198 197 oveq1d ⊒ ( πœ‘ β†’ ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) = ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐿 ) ) ↑ 2 ) )
199 191 198 oveq12d ⊒ ( πœ‘ β†’ ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) = ( ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐿 ) ) ↑ 2 ) ) )
200 199 oveq2d ⊒ ( πœ‘ β†’ ( 2 Β· ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) = ( 2 Β· ( ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐾 ) ) ↑ 2 ) + ( ( 𝑁 β€˜ ( 𝐴 βˆ’ 𝐿 ) ) ↑ 2 ) ) ) )
201 132 184 200 3eqtr4d ⊒ ( πœ‘ β†’ ( ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) = ( 2 Β· ( ( ( 𝐴 𝐷 𝐾 ) ↑ 2 ) + ( ( 𝐴 𝐷 𝐿 ) ↑ 2 ) ) ) )
202 2t2e4 ⊒ ( 2 · 2 ) = 4
203 202 oveq1i ⊒ ( ( 2 Β· 2 ) Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) = ( 4 Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) )
204 2cnd ⊒ ( πœ‘ β†’ 2 ∈ β„‚ )
205 204 204 114 mulassd ⊒ ( πœ‘ β†’ ( ( 2 Β· 2 ) Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) = ( 2 Β· ( 2 Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) ) )
206 203 205 eqtr3id ⊒ ( πœ‘ β†’ ( 4 Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) = ( 2 Β· ( 2 Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) ) )
207 126 201 206 3brtr4d ⊒ ( πœ‘ β†’ ( ( 4 Β· ( ( 𝑁 β€˜ ( 𝐴 βˆ’ ( ( 1 / 2 ) ( ·𝑠 β€˜ π‘ˆ ) ( 𝐾 ( +g β€˜ π‘ˆ ) 𝐿 ) ) ) ) ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≀ ( 4 Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) )
208 37 67 70 106 207 letrd ⊒ ( πœ‘ β†’ ( ( 4 Β· ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≀ ( 4 Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) )
209 4cn ⊒ 4 ∈ β„‚
210 209 a1i ⊒ ( πœ‘ β†’ 4 ∈ β„‚ )
211 20 recnd ⊒ ( πœ‘ β†’ ( 𝑆 ↑ 2 ) ∈ β„‚ )
212 12 recnd ⊒ ( πœ‘ β†’ 𝐡 ∈ β„‚ )
213 210 211 212 adddid ⊒ ( πœ‘ β†’ ( 4 Β· ( ( 𝑆 ↑ 2 ) + 𝐡 ) ) = ( ( 4 Β· ( 𝑆 ↑ 2 ) ) + ( 4 Β· 𝐡 ) ) )
214 208 213 breqtrd ⊒ ( πœ‘ β†’ ( ( 4 Β· ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≀ ( ( 4 Β· ( 𝑆 ↑ 2 ) ) + ( 4 Β· 𝐡 ) ) )
215 remulcl ⊒ ( ( 4 ∈ ℝ ∧ 𝐡 ∈ ℝ ) β†’ ( 4 Β· 𝐡 ) ∈ ℝ )
216 18 12 215 sylancr ⊒ ( πœ‘ β†’ ( 4 Β· 𝐡 ) ∈ ℝ )
217 36 216 22 leadd2d ⊒ ( πœ‘ β†’ ( ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ≀ ( 4 Β· 𝐡 ) ↔ ( ( 4 Β· ( 𝑆 ↑ 2 ) ) + ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ) ≀ ( ( 4 Β· ( 𝑆 ↑ 2 ) ) + ( 4 Β· 𝐡 ) ) ) )
218 214 217 mpbird ⊒ ( πœ‘ β†’ ( ( 𝐾 𝐷 𝐿 ) ↑ 2 ) ≀ ( 4 Β· 𝐡 ) )