MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  minvecolem2 Structured version   Visualization version   GIF version

Theorem minvecolem2 28654
Description: Lemma for minveco 28663. 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 𝑁 = (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
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.
StepHypRef Expression
1 4re 11714 . . . . . 6 4 ∈ ℝ
2 minveco.s . . . . . . . 8 𝑆 = inf(𝑅, ℝ, < )
3 minveco.x . . . . . . . . . . 11 𝑋 = (BaseSet‘𝑈)
4 minveco.m . . . . . . . . . . 11 𝑀 = ( −𝑣𝑈)
5 minveco.n . . . . . . . . . . 11 𝑁 = (normCV𝑈)
6 minveco.y . . . . . . . . . . 11 𝑌 = (BaseSet‘𝑊)
7 minveco.u . . . . . . . . . . 11 (𝜑𝑈 ∈ CPreHilOLD)
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 (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
133, 4, 5, 6, 7, 8, 9, 10, 11, 12minvecolem1 28653 . . . . . . . . . 10 (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤𝑅 0 ≤ 𝑤))
1413simp1d 1139 . . . . . . . . 9 (𝜑𝑅 ⊆ ℝ)
1513simp2d 1140 . . . . . . . . 9 (𝜑𝑅 ≠ ∅)
16 0re 10635 . . . . . . . . . 10 0 ∈ ℝ
1713simp3d 1141 . . . . . . . . . 10 (𝜑 → ∀𝑤𝑅 0 ≤ 𝑤)
18 breq1 5055 . . . . . . . . . . . 12 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
1918ralbidv 3192 . . . . . . . . . . 11 (𝑥 = 0 → (∀𝑤𝑅 𝑥𝑤 ↔ ∀𝑤𝑅 0 ≤ 𝑤))
2019rspcev 3609 . . . . . . . . . 10 ((0 ∈ ℝ ∧ ∀𝑤𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
2116, 17, 20sylancr 590 . . . . . . . . 9 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
22 infrecl 11615 . . . . . . . . 9 ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) → inf(𝑅, ℝ, < ) ∈ ℝ)
2314, 15, 21, 22syl3anc 1368 . . . . . . . 8 (𝜑 → inf(𝑅, ℝ, < ) ∈ ℝ)
242, 23eqeltrid 2920 . . . . . . 7 (𝜑𝑆 ∈ ℝ)
2524resqcld 13612 . . . . . 6 (𝜑 → (𝑆↑2) ∈ ℝ)
26 remulcl 10614 . . . . . 6 ((4 ∈ ℝ ∧ (𝑆↑2) ∈ ℝ) → (4 · (𝑆↑2)) ∈ ℝ)
271, 25, 26sylancr 590 . . . . 5 (𝜑 → (4 · (𝑆↑2)) ∈ ℝ)
28 phnv 28593 . . . . . . . . 9 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
297, 28syl 17 . . . . . . . 8 (𝜑𝑈 ∈ NrmCVec)
303, 10imsmet 28470 . . . . . . . 8 (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
3129, 30syl 17 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
32 inss1 4189 . . . . . . . . . 10 ((SubSp‘𝑈) ∩ CBan) ⊆ (SubSp‘𝑈)
3332, 8sseldi 3950 . . . . . . . . 9 (𝜑𝑊 ∈ (SubSp‘𝑈))
34 eqid 2824 . . . . . . . . . 10 (SubSp‘𝑈) = (SubSp‘𝑈)
353, 6, 34sspba 28506 . . . . . . . . 9 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌𝑋)
3629, 33, 35syl2anc 587 . . . . . . . 8 (𝜑𝑌𝑋)
37 minvecolem2.3 . . . . . . . 8 (𝜑𝐾𝑌)
3836, 37sseldd 3953 . . . . . . 7 (𝜑𝐾𝑋)
39 minvecolem2.4 . . . . . . . 8 (𝜑𝐿𝑌)
4036, 39sseldd 3953 . . . . . . 7 (𝜑𝐿𝑋)
41 metcl 22935 . . . . . . 7 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾𝑋𝐿𝑋) → (𝐾𝐷𝐿) ∈ ℝ)
4231, 38, 40, 41syl3anc 1368 . . . . . 6 (𝜑 → (𝐾𝐷𝐿) ∈ ℝ)
4342resqcld 13612 . . . . 5 (𝜑 → ((𝐾𝐷𝐿)↑2) ∈ ℝ)
4427, 43readdcld 10662 . . . 4 (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
45 ax-1cn 10587 . . . . . . . . . . . . 13 1 ∈ ℂ
46 halfcl 11855 . . . . . . . . . . . . 13 (1 ∈ ℂ → (1 / 2) ∈ ℂ)
4745, 46mp1i 13 . . . . . . . . . . . 12 (𝜑 → (1 / 2) ∈ ℂ)
48 eqid 2824 . . . . . . . . . . . . . . 15 ( +𝑣𝑈) = ( +𝑣𝑈)
49 eqid 2824 . . . . . . . . . . . . . . 15 ( +𝑣𝑊) = ( +𝑣𝑊)
506, 48, 49, 34sspgval 28508 . . . . . . . . . . . . . 14 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ (𝐾𝑌𝐿𝑌)) → (𝐾( +𝑣𝑊)𝐿) = (𝐾( +𝑣𝑈)𝐿))
5129, 33, 37, 39, 50syl22anc 837 . . . . . . . . . . . . 13 (𝜑 → (𝐾( +𝑣𝑊)𝐿) = (𝐾( +𝑣𝑈)𝐿))
5234sspnv 28505 . . . . . . . . . . . . . . 15 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑊 ∈ NrmCVec)
5329, 33, 52syl2anc 587 . . . . . . . . . . . . . 14 (𝜑𝑊 ∈ NrmCVec)
546, 49nvgcl 28399 . . . . . . . . . . . . . 14 ((𝑊 ∈ NrmCVec ∧ 𝐾𝑌𝐿𝑌) → (𝐾( +𝑣𝑊)𝐿) ∈ 𝑌)
5553, 37, 39, 54syl3anc 1368 . . . . . . . . . . . . 13 (𝜑 → (𝐾( +𝑣𝑊)𝐿) ∈ 𝑌)
5651, 55eqeltrrd 2917 . . . . . . . . . . . 12 (𝜑 → (𝐾( +𝑣𝑈)𝐿) ∈ 𝑌)
57 eqid 2824 . . . . . . . . . . . . 13 ( ·𝑠OLD𝑈) = ( ·𝑠OLD𝑈)
58 eqid 2824 . . . . . . . . . . . . 13 ( ·𝑠OLD𝑊) = ( ·𝑠OLD𝑊)
596, 57, 58, 34sspsval 28510 . . . . . . . . . . . 12 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ ((1 / 2) ∈ ℂ ∧ (𝐾( +𝑣𝑈)𝐿) ∈ 𝑌)) → ((1 / 2)( ·𝑠OLD𝑊)(𝐾( +𝑣𝑈)𝐿)) = ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))
6029, 33, 47, 56, 59syl22anc 837 . . . . . . . . . . 11 (𝜑 → ((1 / 2)( ·𝑠OLD𝑊)(𝐾( +𝑣𝑈)𝐿)) = ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))
616, 58nvscl 28405 . . . . . . . . . . . 12 ((𝑊 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +𝑣𝑈)𝐿) ∈ 𝑌) → ((1 / 2)( ·𝑠OLD𝑊)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑌)
6253, 47, 56, 61syl3anc 1368 . . . . . . . . . . 11 (𝜑 → ((1 / 2)( ·𝑠OLD𝑊)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑌)
6360, 62eqeltrrd 2917 . . . . . . . . . 10 (𝜑 → ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑌)
6436, 63sseldd 3953 . . . . . . . . 9 (𝜑 → ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑋)
653, 4nvmcl 28425 . . . . . . . . 9 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑋) → (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))) ∈ 𝑋)
6629, 9, 64, 65syl3anc 1368 . . . . . . . 8 (𝜑 → (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))) ∈ 𝑋)
673, 5nvcl 28440 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℝ)
6829, 66, 67syl2anc 587 . . . . . . 7 (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℝ)
6968resqcld 13612 . . . . . 6 (𝜑 → ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ∈ ℝ)
70 remulcl 10614 . . . . . 6 ((4 ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ∈ ℝ) → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) ∈ ℝ)
711, 69, 70sylancr 590 . . . . 5 (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) ∈ ℝ)
7271, 43readdcld 10662 . . . 4 (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
73 minvecolem2.1 . . . . . 6 (𝜑𝐵 ∈ ℝ)
7425, 73readdcld 10662 . . . . 5 (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℝ)
75 remulcl 10614 . . . . 5 ((4 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
761, 74, 75sylancr 590 . . . 4 (𝜑 → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
7716a1i 11 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
78 infregelb 11617 . . . . . . . . . 10 (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
7914, 15, 21, 77, 78syl31anc 1370 . . . . . . . . 9 (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
8017, 79mpbird 260 . . . . . . . 8 (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
8180, 2breqtrrdi 5094 . . . . . . 7 (𝜑 → 0 ≤ 𝑆)
82 eqid 2824 . . . . . . . . . . . 12 (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
83 oveq2 7153 . . . . . . . . . . . . . 14 (𝑦 = ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) → (𝐴𝑀𝑦) = (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
8483fveq2d 6662 . . . . . . . . . . . . 13 (𝑦 = ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) → (𝑁‘(𝐴𝑀𝑦)) = (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
8584rspceeqv 3624 . . . . . . . . . . . 12 ((((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑌 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) → ∃𝑦𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
8663, 82, 85sylancl 589 . . . . . . . . . . 11 (𝜑 → ∃𝑦𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
87 eqid 2824 . . . . . . . . . . . 12 (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
88 fvex 6671 . . . . . . . . . . . 12 (𝑁‘(𝐴𝑀𝑦)) ∈ V
8987, 88elrnmpti 5819 . . . . . . . . . . 11 ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) ↔ ∃𝑦𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
9086, 89sylibr 237 . . . . . . . . . 10 (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
9190, 12eleqtrrdi 2927 . . . . . . . . 9 (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ 𝑅)
92 infrelb 11618 . . . . . . . . 9 ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
9314, 21, 91, 92syl3anc 1368 . . . . . . . 8 (𝜑 → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
942, 93eqbrtrid 5087 . . . . . . 7 (𝜑𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
95 le2sq2 13501 . . . . . . 7 (((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℝ ∧ 𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))) → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))
9624, 81, 68, 94, 95syl22anc 837 . . . . . 6 (𝜑 → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))
97 4pos 11737 . . . . . . . . 9 0 < 4
981, 97pm3.2i 474 . . . . . . . 8 (4 ∈ ℝ ∧ 0 < 4)
99 lemul2 11485 . . . . . . . 8 (((𝑆↑2) ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))))
10098, 99mp3an3 1447 . . . . . . 7 (((𝑆↑2) ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ∈ ℝ) → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))))
10125, 69, 100syl2anc 587 . . . . . 6 (𝜑 → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))))
10296, 101mpbid 235 . . . . 5 (𝜑 → (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)))
10327, 71, 43, 102leadd1dd 11246 . . . 4 (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)))
104 metcl 22935 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋𝐾𝑋) → (𝐴𝐷𝐾) ∈ ℝ)
10531, 9, 38, 104syl3anc 1368 . . . . . . . . 9 (𝜑 → (𝐴𝐷𝐾) ∈ ℝ)
106105resqcld 13612 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐾)↑2) ∈ ℝ)
107 metcl 22935 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋𝐿𝑋) → (𝐴𝐷𝐿) ∈ ℝ)
10831, 9, 40, 107syl3anc 1368 . . . . . . . . 9 (𝜑 → (𝐴𝐷𝐿) ∈ ℝ)
109108resqcld 13612 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐿)↑2) ∈ ℝ)
110 minvecolem2.5 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))
111 minvecolem2.6 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))
112106, 109, 74, 74, 110, 111le2addd 11251 . . . . . . 7 (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
11374recnd 10661 . . . . . . . 8 (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℂ)
1141132timesd 11873 . . . . . . 7 (𝜑 → (2 · ((𝑆↑2) + 𝐵)) = (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
115112, 114breqtrrd 5080 . . . . . 6 (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)))
116106, 109readdcld 10662 . . . . . . 7 (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ)
117 2re 11704 . . . . . . . 8 2 ∈ ℝ
118 remulcl 10614 . . . . . . . 8 ((2 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
119117, 74, 118sylancr 590 . . . . . . 7 (𝜑 → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
120 2pos 11733 . . . . . . . . 9 0 < 2
121117, 120pm3.2i 474 . . . . . . . 8 (2 ∈ ℝ ∧ 0 < 2)
122 lemul2 11485 . . . . . . . 8 (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
123121, 122mp3an3 1447 . . . . . . 7 (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
124116, 119, 123syl2anc 587 . . . . . 6 (𝜑 → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
125115, 124mpbid 235 . . . . 5 (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵))))
1263, 4nvmcl 28425 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐾𝑋) → (𝐴𝑀𝐾) ∈ 𝑋)
12729, 9, 38, 126syl3anc 1368 . . . . . . 7 (𝜑 → (𝐴𝑀𝐾) ∈ 𝑋)
1283, 4nvmcl 28425 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐿𝑋) → (𝐴𝑀𝐿) ∈ 𝑋)
12929, 9, 40, 128syl3anc 1368 . . . . . . 7 (𝜑 → (𝐴𝑀𝐿) ∈ 𝑋)
1303, 48, 4, 5phpar2 28602 . . . . . . 7 ((𝑈 ∈ CPreHilOLD ∧ (𝐴𝑀𝐾) ∈ 𝑋 ∧ (𝐴𝑀𝐿) ∈ 𝑋) → (((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
1317, 127, 129, 130syl3anc 1368 . . . . . 6 (𝜑 → (((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
132 2cn 11705 . . . . . . . . . 10 2 ∈ ℂ
13368recnd 10661 . . . . . . . . . 10 (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℂ)
134 sqmul 13486 . . . . . . . . . 10 ((2 ∈ ℂ ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℂ) → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)))
135132, 133, 134sylancr 590 . . . . . . . . 9 (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)))
136 sq2 13561 . . . . . . . . . 10 (2↑2) = 4
137136oveq1i 7155 . . . . . . . . 9 ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))
138135, 137syl6eq 2875 . . . . . . . 8 (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))↑2) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)))
139132a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℂ)
1403, 57, 5nvs 28442 . . . . . . . . . . . 12 ((𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))))
14129, 139, 66, 140syl3anc 1368 . . . . . . . . . . 11 (𝜑 → (𝑁‘(2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))))
142 0le2 11732 . . . . . . . . . . . . 13 0 ≤ 2
143 absid 14652 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
144117, 142, 143mp2an 691 . . . . . . . . . . . 12 (abs‘2) = 2
145144oveq1i 7155 . . . . . . . . . . 11 ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
146141, 145syl6eq 2875 . . . . . . . . . 10 (𝜑 → (𝑁‘(2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))))
1473, 4, 57nvmdi 28427 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ 𝐴𝑋 ∧ ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑋)) → (2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = ((2( ·𝑠OLD𝑈)𝐴)𝑀(2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
14829, 139, 9, 64, 147syl13anc 1369 . . . . . . . . . . . 12 (𝜑 → (2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = ((2( ·𝑠OLD𝑈)𝐴)𝑀(2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
1493, 48, 57nv2 28411 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋) → (𝐴( +𝑣𝑈)𝐴) = (2( ·𝑠OLD𝑈)𝐴))
15029, 9, 149syl2anc 587 . . . . . . . . . . . . 13 (𝜑 → (𝐴( +𝑣𝑈)𝐴) = (2( ·𝑠OLD𝑈)𝐴))
151 2ne0 11734 . . . . . . . . . . . . . . . . 17 2 ≠ 0
152132, 151recidi 11363 . . . . . . . . . . . . . . . 16 (2 · (1 / 2)) = 1
153152oveq1i 7155 . . . . . . . . . . . . . . 15 ((2 · (1 / 2))( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (1( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))
1543, 48nvgcl 28399 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ NrmCVec ∧ 𝐾𝑋𝐿𝑋) → (𝐾( +𝑣𝑈)𝐿) ∈ 𝑋)
15529, 38, 40, 154syl3anc 1368 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾( +𝑣𝑈)𝐿) ∈ 𝑋)
1563, 57nvsid 28406 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ NrmCVec ∧ (𝐾( +𝑣𝑈)𝐿) ∈ 𝑋) → (1( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (𝐾( +𝑣𝑈)𝐿))
15729, 155, 156syl2anc 587 . . . . . . . . . . . . . . 15 (𝜑 → (1( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (𝐾( +𝑣𝑈)𝐿))
158153, 157syl5eq 2871 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (1 / 2))( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (𝐾( +𝑣𝑈)𝐿))
1593, 57nvsass 28407 . . . . . . . . . . . . . . 15 ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +𝑣𝑈)𝐿) ∈ 𝑋)) → ((2 · (1 / 2))( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
16029, 139, 47, 155, 159syl13anc 1369 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (1 / 2))( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
161158, 160eqtr3d 2861 . . . . . . . . . . . . 13 (𝜑 → (𝐾( +𝑣𝑈)𝐿) = (2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
162150, 161oveq12d 7163 . . . . . . . . . . . 12 (𝜑 → ((𝐴( +𝑣𝑈)𝐴)𝑀(𝐾( +𝑣𝑈)𝐿)) = ((2( ·𝑠OLD𝑈)𝐴)𝑀(2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
1633, 48, 4nvaddsub4 28436 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑋𝐴𝑋) ∧ (𝐾𝑋𝐿𝑋)) → ((𝐴( +𝑣𝑈)𝐴)𝑀(𝐾( +𝑣𝑈)𝐿)) = ((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))
16429, 9, 9, 38, 40, 163syl122anc 1376 . . . . . . . . . . . 12 (𝜑 → ((𝐴( +𝑣𝑈)𝐴)𝑀(𝐾( +𝑣𝑈)𝐿)) = ((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))
165148, 162, 1643eqtr2d 2865 . . . . . . . . . . 11 (𝜑 → (2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = ((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))
166165fveq2d 6662 . . . . . . . . . 10 (𝜑 → (𝑁‘(2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿))))
167146, 166eqtr3d 2861 . . . . . . . . 9 (𝜑 → (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿))))
168167oveq1d 7160 . . . . . . . 8 (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))↑2) = ((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2))
169138, 168eqtr3d 2861 . . . . . . 7 (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) = ((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2))
1703, 4, 5, 10imsdval 28465 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝐿𝑋𝐾𝑋) → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
17129, 40, 38, 170syl3anc 1368 . . . . . . . . 9 (𝜑 → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
172 metsym 22953 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾𝑋𝐿𝑋) → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
17331, 38, 40, 172syl3anc 1368 . . . . . . . . 9 (𝜑 → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
1743, 4nvnnncan1 28426 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑋𝐾𝑋𝐿𝑋)) → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
17529, 9, 38, 40, 174syl13anc 1369 . . . . . . . . . 10 (𝜑 → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
176175fveq2d 6662 . . . . . . . . 9 (𝜑 → (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))) = (𝑁‘(𝐿𝑀𝐾)))
177171, 173, 1763eqtr4d 2869 . . . . . . . 8 (𝜑 → (𝐾𝐷𝐿) = (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))))
178177oveq1d 7160 . . . . . . 7 (𝜑 → ((𝐾𝐷𝐿)↑2) = ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2))
179169, 178oveq12d 7163 . . . . . 6 (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)))
1803, 4, 5, 10imsdval 28465 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐾𝑋) → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
18129, 9, 38, 180syl3anc 1368 . . . . . . . . 9 (𝜑 → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
182181oveq1d 7160 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐾)↑2) = ((𝑁‘(𝐴𝑀𝐾))↑2))
1833, 4, 5, 10imsdval 28465 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐿𝑋) → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
18429, 9, 40, 183syl3anc 1368 . . . . . . . . 9 (𝜑 → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
185184oveq1d 7160 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐿)↑2) = ((𝑁‘(𝐴𝑀𝐿))↑2))
186182, 185oveq12d 7163 . . . . . . 7 (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) = (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2)))
187186oveq2d 7161 . . . . . 6 (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
188131, 179, 1873eqtr4d 2869 . . . . 5 (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))))
189 2t2e4 11794 . . . . . . 7 (2 · 2) = 4
190189oveq1i 7155 . . . . . 6 ((2 · 2) · ((𝑆↑2) + 𝐵)) = (4 · ((𝑆↑2) + 𝐵))
191139, 139, 113mulassd 10656 . . . . . 6 (𝜑 → ((2 · 2) · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
192190, 191syl5eqr 2873 . . . . 5 (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
193125, 188, 1923brtr4d 5084 . . . 4 (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
19444, 72, 76, 103, 193letrd 10789 . . 3 (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
195 4cn 11715 . . . . 5 4 ∈ ℂ
196195a1i 11 . . . 4 (𝜑 → 4 ∈ ℂ)
19725recnd 10661 . . . 4 (𝜑 → (𝑆↑2) ∈ ℂ)
19873recnd 10661 . . . 4 (𝜑𝐵 ∈ ℂ)
199196, 197, 198adddid 10657 . . 3 (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = ((4 · (𝑆↑2)) + (4 · 𝐵)))
200194, 199breqtrd 5078 . 2 (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵)))
201 remulcl 10614 . . . 4 ((4 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (4 · 𝐵) ∈ ℝ)
2021, 73, 201sylancr 590 . . 3 (𝜑 → (4 · 𝐵) ∈ ℝ)
20343, 202, 27leadd2d 11227 . 2 (𝜑 → (((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵) ↔ ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵))))
204200, 203mpbird 260 1 (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wne 3014  wral 3133  wrex 3134  cin 3918  wss 3919  c0 4275   class class class wbr 5052  cmpt 5132  ran crn 5543  cfv 6343  (class class class)co 7145  infcinf 8896  cc 10527  cr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   < clt 10667  cle 10668   / cdiv 11289  2c2 11685  4c4 11687  cexp 13430  abscabs 14589  Metcmet 20524  MetOpencmopn 20528  NrmCVeccnv 28363   +𝑣 cpv 28364  BaseSetcba 28365   ·𝑠OLD cns 28366  𝑣 cnsb 28368  normCVcnmcv 28369  IndMetcims 28370  SubSpcss 28500  CPreHilOLDccphlo 28591  CBanccbn 28641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7451  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4276  df-if 4450  df-pw 4523  df-sn 4550  df-pr 4552  df-tp 4554  df-op 4556  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7571  df-1st 7679  df-2nd 7680  df-wrecs 7937  df-recs 7998  df-rdg 8036  df-er 8279  df-map 8398  df-en 8500  df-dom 8501  df-sdom 8502  df-sup 8897  df-inf 8898  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11693  df-3 11694  df-4 11695  df-n0 11891  df-z 11975  df-uz 12237  df-rp 12383  df-xadd 12501  df-seq 13370  df-exp 13431  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-xmet 20531  df-met 20532  df-grpo 28272  df-gid 28273  df-ginv 28274  df-gdiv 28275  df-ablo 28324  df-vc 28338  df-nv 28371  df-va 28374  df-ba 28375  df-sm 28376  df-0v 28377  df-vs 28378  df-nmcv 28379  df-ims 28380  df-ssp 28501  df-ph 28592  df-cbn 28642
This theorem is referenced by:  minvecolem3  28655  minvecolem7  28662
  Copyright terms: Public domain W3C validator