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

Theorem minvecolem2 29369
Description: Lemma for minveco 29378. 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 12136 . . . . . 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 29368 . . . . . . . . . 10 (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤𝑅 0 ≤ 𝑤))
1413simp1d 1141 . . . . . . . . 9 (𝜑𝑅 ⊆ ℝ)
1513simp2d 1142 . . . . . . . . 9 (𝜑𝑅 ≠ ∅)
16 0re 11056 . . . . . . . . . 10 0 ∈ ℝ
1713simp3d 1143 . . . . . . . . . 10 (𝜑 → ∀𝑤𝑅 0 ≤ 𝑤)
18 breq1 5089 . . . . . . . . . . . 12 (𝑥 = 0 → (𝑥𝑤 ↔ 0 ≤ 𝑤))
1918ralbidv 3170 . . . . . . . . . . 11 (𝑥 = 0 → (∀𝑤𝑅 𝑥𝑤 ↔ ∀𝑤𝑅 0 ≤ 𝑤))
2019rspcev 3569 . . . . . . . . . 10 ((0 ∈ ℝ ∧ ∀𝑤𝑅 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
2116, 17, 20sylancr 587 . . . . . . . . 9 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤)
22 infrecl 12036 . . . . . . . . 9 ((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) → inf(𝑅, ℝ, < ) ∈ ℝ)
2314, 15, 21, 22syl3anc 1370 . . . . . . . 8 (𝜑 → inf(𝑅, ℝ, < ) ∈ ℝ)
242, 23eqeltrid 2841 . . . . . . 7 (𝜑𝑆 ∈ ℝ)
2524resqcld 14044 . . . . . 6 (𝜑 → (𝑆↑2) ∈ ℝ)
26 remulcl 11035 . . . . . 6 ((4 ∈ ℝ ∧ (𝑆↑2) ∈ ℝ) → (4 · (𝑆↑2)) ∈ ℝ)
271, 25, 26sylancr 587 . . . . 5 (𝜑 → (4 · (𝑆↑2)) ∈ ℝ)
28 phnv 29308 . . . . . . . . 9 (𝑈 ∈ CPreHilOLD𝑈 ∈ NrmCVec)
297, 28syl 17 . . . . . . . 8 (𝜑𝑈 ∈ NrmCVec)
303, 10imsmet 29185 . . . . . . . 8 (𝑈 ∈ NrmCVec → 𝐷 ∈ (Met‘𝑋))
3129, 30syl 17 . . . . . . 7 (𝜑𝐷 ∈ (Met‘𝑋))
32 inss1 4172 . . . . . . . . . 10 ((SubSp‘𝑈) ∩ CBan) ⊆ (SubSp‘𝑈)
3332, 8sselid 3928 . . . . . . . . 9 (𝜑𝑊 ∈ (SubSp‘𝑈))
34 eqid 2736 . . . . . . . . . 10 (SubSp‘𝑈) = (SubSp‘𝑈)
353, 6, 34sspba 29221 . . . . . . . . 9 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑌𝑋)
3629, 33, 35syl2anc 584 . . . . . . . 8 (𝜑𝑌𝑋)
37 minvecolem2.3 . . . . . . . 8 (𝜑𝐾𝑌)
3836, 37sseldd 3931 . . . . . . 7 (𝜑𝐾𝑋)
39 minvecolem2.4 . . . . . . . 8 (𝜑𝐿𝑌)
4036, 39sseldd 3931 . . . . . . 7 (𝜑𝐿𝑋)
41 metcl 23565 . . . . . . 7 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾𝑋𝐿𝑋) → (𝐾𝐷𝐿) ∈ ℝ)
4231, 38, 40, 41syl3anc 1370 . . . . . 6 (𝜑 → (𝐾𝐷𝐿) ∈ ℝ)
4342resqcld 14044 . . . . 5 (𝜑 → ((𝐾𝐷𝐿)↑2) ∈ ℝ)
4427, 43readdcld 11083 . . . 4 (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
45 ax-1cn 11008 . . . . . . . . . . . . 13 1 ∈ ℂ
46 halfcl 12277 . . . . . . . . . . . . 13 (1 ∈ ℂ → (1 / 2) ∈ ℂ)
4745, 46mp1i 13 . . . . . . . . . . . 12 (𝜑 → (1 / 2) ∈ ℂ)
48 eqid 2736 . . . . . . . . . . . . . . 15 ( +𝑣𝑈) = ( +𝑣𝑈)
49 eqid 2736 . . . . . . . . . . . . . . 15 ( +𝑣𝑊) = ( +𝑣𝑊)
506, 48, 49, 34sspgval 29223 . . . . . . . . . . . . . 14 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ (𝐾𝑌𝐿𝑌)) → (𝐾( +𝑣𝑊)𝐿) = (𝐾( +𝑣𝑈)𝐿))
5129, 33, 37, 39, 50syl22anc 836 . . . . . . . . . . . . 13 (𝜑 → (𝐾( +𝑣𝑊)𝐿) = (𝐾( +𝑣𝑈)𝐿))
5234sspnv 29220 . . . . . . . . . . . . . . 15 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) → 𝑊 ∈ NrmCVec)
5329, 33, 52syl2anc 584 . . . . . . . . . . . . . 14 (𝜑𝑊 ∈ NrmCVec)
546, 49nvgcl 29114 . . . . . . . . . . . . . 14 ((𝑊 ∈ NrmCVec ∧ 𝐾𝑌𝐿𝑌) → (𝐾( +𝑣𝑊)𝐿) ∈ 𝑌)
5553, 37, 39, 54syl3anc 1370 . . . . . . . . . . . . 13 (𝜑 → (𝐾( +𝑣𝑊)𝐿) ∈ 𝑌)
5651, 55eqeltrrd 2838 . . . . . . . . . . . 12 (𝜑 → (𝐾( +𝑣𝑈)𝐿) ∈ 𝑌)
57 eqid 2736 . . . . . . . . . . . . 13 ( ·𝑠OLD𝑈) = ( ·𝑠OLD𝑈)
58 eqid 2736 . . . . . . . . . . . . 13 ( ·𝑠OLD𝑊) = ( ·𝑠OLD𝑊)
596, 57, 58, 34sspsval 29225 . . . . . . . . . . . 12 (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ (SubSp‘𝑈)) ∧ ((1 / 2) ∈ ℂ ∧ (𝐾( +𝑣𝑈)𝐿) ∈ 𝑌)) → ((1 / 2)( ·𝑠OLD𝑊)(𝐾( +𝑣𝑈)𝐿)) = ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))
6029, 33, 47, 56, 59syl22anc 836 . . . . . . . . . . 11 (𝜑 → ((1 / 2)( ·𝑠OLD𝑊)(𝐾( +𝑣𝑈)𝐿)) = ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))
616, 58nvscl 29120 . . . . . . . . . . . 12 ((𝑊 ∈ NrmCVec ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +𝑣𝑈)𝐿) ∈ 𝑌) → ((1 / 2)( ·𝑠OLD𝑊)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑌)
6253, 47, 56, 61syl3anc 1370 . . . . . . . . . . 11 (𝜑 → ((1 / 2)( ·𝑠OLD𝑊)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑌)
6360, 62eqeltrrd 2838 . . . . . . . . . 10 (𝜑 → ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑌)
6436, 63sseldd 3931 . . . . . . . . 9 (𝜑 → ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑋)
653, 4nvmcl 29140 . . . . . . . . 9 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑋) → (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))) ∈ 𝑋)
6629, 9, 64, 65syl3anc 1370 . . . . . . . 8 (𝜑 → (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))) ∈ 𝑋)
673, 5nvcl 29155 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℝ)
6829, 66, 67syl2anc 584 . . . . . . 7 (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℝ)
6968resqcld 14044 . . . . . 6 (𝜑 → ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ∈ ℝ)
70 remulcl 11035 . . . . . 6 ((4 ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ∈ ℝ) → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) ∈ ℝ)
711, 69, 70sylancr 587 . . . . 5 (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) ∈ ℝ)
7271, 43readdcld 11083 . . . 4 (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ∈ ℝ)
73 minvecolem2.1 . . . . . 6 (𝜑𝐵 ∈ ℝ)
7425, 73readdcld 11083 . . . . 5 (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℝ)
75 remulcl 11035 . . . . 5 ((4 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
761, 74, 75sylancr 587 . . . 4 (𝜑 → (4 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
7716a1i 11 . . . . . . . . . 10 (𝜑 → 0 ∈ ℝ)
78 infregelb 12038 . . . . . . . . . 10 (((𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤) ∧ 0 ∈ ℝ) → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
7914, 15, 21, 77, 78syl31anc 1372 . . . . . . . . 9 (𝜑 → (0 ≤ inf(𝑅, ℝ, < ) ↔ ∀𝑤𝑅 0 ≤ 𝑤))
8017, 79mpbird 256 . . . . . . . 8 (𝜑 → 0 ≤ inf(𝑅, ℝ, < ))
8180, 2breqtrrdi 5128 . . . . . . 7 (𝜑 → 0 ≤ 𝑆)
82 eqid 2736 . . . . . . . . . . . 12 (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
83 oveq2 7324 . . . . . . . . . . . . . 14 (𝑦 = ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) → (𝐴𝑀𝑦) = (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
8483fveq2d 6815 . . . . . . . . . . . . 13 (𝑦 = ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) → (𝑁‘(𝐴𝑀𝑦)) = (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
8584rspceeqv 3583 . . . . . . . . . . . 12 ((((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑌 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) → ∃𝑦𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
8663, 82, 85sylancl 586 . . . . . . . . . . 11 (𝜑 → ∃𝑦𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
87 eqid 2736 . . . . . . . . . . . 12 (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) = (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦)))
88 fvex 6824 . . . . . . . . . . . 12 (𝑁‘(𝐴𝑀𝑦)) ∈ V
8987, 88elrnmpti 5888 . . . . . . . . . . 11 ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) ↔ ∃𝑦𝑌 (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = (𝑁‘(𝐴𝑀𝑦)))
9086, 89sylibr 233 . . . . . . . . . 10 (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ran (𝑦𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))))
9190, 12eleqtrrdi 2848 . . . . . . . . 9 (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ 𝑅)
92 infrelb 12039 . . . . . . . . 9 ((𝑅 ⊆ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑤𝑅 𝑥𝑤 ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ 𝑅) → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
9314, 21, 91, 92syl3anc 1370 . . . . . . . 8 (𝜑 → inf(𝑅, ℝ, < ) ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
942, 93eqbrtrid 5121 . . . . . . 7 (𝜑𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
95 le2sq2 13933 . . . . . . 7 (((𝑆 ∈ ℝ ∧ 0 ≤ 𝑆) ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℝ ∧ 𝑆 ≤ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))) → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))
9624, 81, 68, 94, 95syl22anc 836 . . . . . 6 (𝜑 → (𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))
97 4pos 12159 . . . . . . . . 9 0 < 4
981, 97pm3.2i 471 . . . . . . . 8 (4 ∈ ℝ ∧ 0 < 4)
99 lemul2 11907 . . . . . . . 8 (((𝑆↑2) ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ∈ ℝ ∧ (4 ∈ ℝ ∧ 0 < 4)) → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))))
10098, 99mp3an3 1449 . . . . . . 7 (((𝑆↑2) ∈ ℝ ∧ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ∈ ℝ) → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))))
10125, 69, 100syl2anc 584 . . . . . 6 (𝜑 → ((𝑆↑2) ≤ ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2) ↔ (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))))
10296, 101mpbid 231 . . . . 5 (𝜑 → (4 · (𝑆↑2)) ≤ (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)))
10327, 71, 43, 102leadd1dd 11668 . . . 4 (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)))
104 metcl 23565 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋𝐾𝑋) → (𝐴𝐷𝐾) ∈ ℝ)
10531, 9, 38, 104syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝐴𝐷𝐾) ∈ ℝ)
106105resqcld 14044 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐾)↑2) ∈ ℝ)
107 metcl 23565 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐴𝑋𝐿𝑋) → (𝐴𝐷𝐿) ∈ ℝ)
10831, 9, 40, 107syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝐴𝐷𝐿) ∈ ℝ)
109108resqcld 14044 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐿)↑2) ∈ ℝ)
110 minvecolem2.5 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))
111 minvecolem2.6 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))
112106, 109, 74, 74, 110, 111le2addd 11673 . . . . . . 7 (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
11374recnd 11082 . . . . . . . 8 (𝜑 → ((𝑆↑2) + 𝐵) ∈ ℂ)
1141132timesd 12295 . . . . . . 7 (𝜑 → (2 · ((𝑆↑2) + 𝐵)) = (((𝑆↑2) + 𝐵) + ((𝑆↑2) + 𝐵)))
115112, 114breqtrrd 5114 . . . . . 6 (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)))
116106, 109readdcld 11083 . . . . . . 7 (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ)
117 2re 12126 . . . . . . . 8 2 ∈ ℝ
118 remulcl 11035 . . . . . . . 8 ((2 ∈ ℝ ∧ ((𝑆↑2) + 𝐵) ∈ ℝ) → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
119117, 74, 118sylancr 587 . . . . . . 7 (𝜑 → (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ)
120 2pos 12155 . . . . . . . . 9 0 < 2
121117, 120pm3.2i 471 . . . . . . . 8 (2 ∈ ℝ ∧ 0 < 2)
122 lemul2 11907 . . . . . . . 8 (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
123121, 122mp3an3 1449 . . . . . . 7 (((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ∈ ℝ ∧ (2 · ((𝑆↑2) + 𝐵)) ∈ ℝ) → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
124116, 119, 123syl2anc 584 . . . . . 6 (𝜑 → ((((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) ≤ (2 · ((𝑆↑2) + 𝐵)) ↔ (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵)))))
125115, 124mpbid 231 . . . . 5 (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) ≤ (2 · (2 · ((𝑆↑2) + 𝐵))))
1263, 4nvmcl 29140 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐾𝑋) → (𝐴𝑀𝐾) ∈ 𝑋)
12729, 9, 38, 126syl3anc 1370 . . . . . . 7 (𝜑 → (𝐴𝑀𝐾) ∈ 𝑋)
1283, 4nvmcl 29140 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐿𝑋) → (𝐴𝑀𝐿) ∈ 𝑋)
12929, 9, 40, 128syl3anc 1370 . . . . . . 7 (𝜑 → (𝐴𝑀𝐿) ∈ 𝑋)
1303, 48, 4, 5phpar2 29317 . . . . . . 7 ((𝑈 ∈ CPreHilOLD ∧ (𝐴𝑀𝐾) ∈ 𝑋 ∧ (𝐴𝑀𝐿) ∈ 𝑋) → (((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
1317, 127, 129, 130syl3anc 1370 . . . . . 6 (𝜑 → (((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
132 2cn 12127 . . . . . . . . . 10 2 ∈ ℂ
13368recnd 11082 . . . . . . . . . 10 (𝜑 → (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℂ)
134 sqmul 13918 . . . . . . . . . 10 ((2 ∈ ℂ ∧ (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) ∈ ℂ) → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)))
135132, 133, 134sylancr 587 . . . . . . . . 9 (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))↑2) = ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)))
136 sq2 13993 . . . . . . . . . 10 (2↑2) = 4
137136oveq1i 7326 . . . . . . . . 9 ((2↑2) · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2))
138135, 137eqtrdi 2792 . . . . . . . 8 (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))↑2) = (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)))
139132a1i 11 . . . . . . . . . . . 12 (𝜑 → 2 ∈ ℂ)
1403, 57, 5nvs 29157 . . . . . . . . . . . 12 ((𝑈 ∈ NrmCVec ∧ 2 ∈ ℂ ∧ (𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))) ∈ 𝑋) → (𝑁‘(2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))))
14129, 139, 66, 140syl3anc 1370 . . . . . . . . . . 11 (𝜑 → (𝑁‘(2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))))
142 0le2 12154 . . . . . . . . . . . . 13 0 ≤ 2
143 absid 15084 . . . . . . . . . . . . 13 ((2 ∈ ℝ ∧ 0 ≤ 2) → (abs‘2) = 2)
144117, 142, 143mp2an 689 . . . . . . . . . . . 12 (abs‘2) = 2
145144oveq1i 7326 . . . . . . . . . . 11 ((abs‘2) · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
146141, 145eqtrdi 2792 . . . . . . . . . 10 (𝜑 → (𝑁‘(2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))))
1473, 4, 57nvmdi 29142 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ 𝐴𝑋 ∧ ((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) ∈ 𝑋)) → (2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = ((2( ·𝑠OLD𝑈)𝐴)𝑀(2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
14829, 139, 9, 64, 147syl13anc 1371 . . . . . . . . . . . 12 (𝜑 → (2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = ((2( ·𝑠OLD𝑈)𝐴)𝑀(2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
1493, 48, 57nv2 29126 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋) → (𝐴( +𝑣𝑈)𝐴) = (2( ·𝑠OLD𝑈)𝐴))
15029, 9, 149syl2anc 584 . . . . . . . . . . . . 13 (𝜑 → (𝐴( +𝑣𝑈)𝐴) = (2( ·𝑠OLD𝑈)𝐴))
151 2ne0 12156 . . . . . . . . . . . . . . . . 17 2 ≠ 0
152132, 151recidi 11785 . . . . . . . . . . . . . . . 16 (2 · (1 / 2)) = 1
153152oveq1i 7326 . . . . . . . . . . . . . . 15 ((2 · (1 / 2))( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (1( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))
1543, 48nvgcl 29114 . . . . . . . . . . . . . . . . 17 ((𝑈 ∈ NrmCVec ∧ 𝐾𝑋𝐿𝑋) → (𝐾( +𝑣𝑈)𝐿) ∈ 𝑋)
15529, 38, 40, 154syl3anc 1370 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾( +𝑣𝑈)𝐿) ∈ 𝑋)
1563, 57nvsid 29121 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ NrmCVec ∧ (𝐾( +𝑣𝑈)𝐿) ∈ 𝑋) → (1( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (𝐾( +𝑣𝑈)𝐿))
15729, 155, 156syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → (1( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (𝐾( +𝑣𝑈)𝐿))
158153, 157eqtrid 2788 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (1 / 2))( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (𝐾( +𝑣𝑈)𝐿))
1593, 57nvsass 29122 . . . . . . . . . . . . . . 15 ((𝑈 ∈ NrmCVec ∧ (2 ∈ ℂ ∧ (1 / 2) ∈ ℂ ∧ (𝐾( +𝑣𝑈)𝐿) ∈ 𝑋)) → ((2 · (1 / 2))( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
16029, 139, 47, 155, 159syl13anc 1371 . . . . . . . . . . . . . 14 (𝜑 → ((2 · (1 / 2))( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)) = (2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
161158, 160eqtr3d 2778 . . . . . . . . . . . . 13 (𝜑 → (𝐾( +𝑣𝑈)𝐿) = (2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))
162150, 161oveq12d 7334 . . . . . . . . . . . 12 (𝜑 → ((𝐴( +𝑣𝑈)𝐴)𝑀(𝐾( +𝑣𝑈)𝐿)) = ((2( ·𝑠OLD𝑈)𝐴)𝑀(2( ·𝑠OLD𝑈)((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))
1633, 48, 4nvaddsub4 29151 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑋𝐴𝑋) ∧ (𝐾𝑋𝐿𝑋)) → ((𝐴( +𝑣𝑈)𝐴)𝑀(𝐾( +𝑣𝑈)𝐿)) = ((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))
16429, 9, 9, 38, 40, 163syl122anc 1378 . . . . . . . . . . . 12 (𝜑 → ((𝐴( +𝑣𝑈)𝐴)𝑀(𝐾( +𝑣𝑈)𝐿)) = ((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))
165148, 162, 1643eqtr2d 2782 . . . . . . . . . . 11 (𝜑 → (2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))) = ((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))
166165fveq2d 6815 . . . . . . . . . 10 (𝜑 → (𝑁‘(2( ·𝑠OLD𝑈)(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿))))
167146, 166eqtr3d 2778 . . . . . . . . 9 (𝜑 → (2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))) = (𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿))))
168167oveq1d 7331 . . . . . . . 8 (𝜑 → ((2 · (𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿)))))↑2) = ((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2))
169138, 168eqtr3d 2778 . . . . . . 7 (𝜑 → (4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) = ((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2))
1703, 4, 5, 10imsdval 29180 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝐿𝑋𝐾𝑋) → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
17129, 40, 38, 170syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝐿𝐷𝐾) = (𝑁‘(𝐿𝑀𝐾)))
172 metsym 23583 . . . . . . . . . 10 ((𝐷 ∈ (Met‘𝑋) ∧ 𝐾𝑋𝐿𝑋) → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
17331, 38, 40, 172syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝐾𝐷𝐿) = (𝐿𝐷𝐾))
1743, 4nvnnncan1 29141 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝐴𝑋𝐾𝑋𝐿𝑋)) → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
17529, 9, 38, 40, 174syl13anc 1371 . . . . . . . . . 10 (𝜑 → ((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)) = (𝐿𝑀𝐾))
176175fveq2d 6815 . . . . . . . . 9 (𝜑 → (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))) = (𝑁‘(𝐿𝑀𝐾)))
177171, 173, 1763eqtr4d 2786 . . . . . . . 8 (𝜑 → (𝐾𝐷𝐿) = (𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿))))
178177oveq1d 7331 . . . . . . 7 (𝜑 → ((𝐾𝐷𝐿)↑2) = ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2))
179169, 178oveq12d 7334 . . . . . 6 (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (((𝑁‘((𝐴𝑀𝐾)( +𝑣𝑈)(𝐴𝑀𝐿)))↑2) + ((𝑁‘((𝐴𝑀𝐾)𝑀(𝐴𝑀𝐿)))↑2)))
1803, 4, 5, 10imsdval 29180 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐾𝑋) → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
18129, 9, 38, 180syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝐴𝐷𝐾) = (𝑁‘(𝐴𝑀𝐾)))
182181oveq1d 7331 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐾)↑2) = ((𝑁‘(𝐴𝑀𝐾))↑2))
1833, 4, 5, 10imsdval 29180 . . . . . . . . . 10 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐿𝑋) → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
18429, 9, 40, 183syl3anc 1370 . . . . . . . . 9 (𝜑 → (𝐴𝐷𝐿) = (𝑁‘(𝐴𝑀𝐿)))
185184oveq1d 7331 . . . . . . . 8 (𝜑 → ((𝐴𝐷𝐿)↑2) = ((𝑁‘(𝐴𝑀𝐿))↑2))
186182, 185oveq12d 7334 . . . . . . 7 (𝜑 → (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2)) = (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2)))
187186oveq2d 7332 . . . . . 6 (𝜑 → (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))) = (2 · (((𝑁‘(𝐴𝑀𝐾))↑2) + ((𝑁‘(𝐴𝑀𝐿))↑2))))
188131, 179, 1873eqtr4d 2786 . . . . 5 (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) = (2 · (((𝐴𝐷𝐾)↑2) + ((𝐴𝐷𝐿)↑2))))
189 2t2e4 12216 . . . . . . 7 (2 · 2) = 4
190189oveq1i 7326 . . . . . 6 ((2 · 2) · ((𝑆↑2) + 𝐵)) = (4 · ((𝑆↑2) + 𝐵))
191139, 139, 113mulassd 11077 . . . . . 6 (𝜑 → ((2 · 2) · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
192190, 191eqtr3id 2790 . . . . 5 (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = (2 · (2 · ((𝑆↑2) + 𝐵))))
193125, 188, 1923brtr4d 5118 . . . 4 (𝜑 → ((4 · ((𝑁‘(𝐴𝑀((1 / 2)( ·𝑠OLD𝑈)(𝐾( +𝑣𝑈)𝐿))))↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
19444, 72, 76, 103, 193letrd 11211 . . 3 (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ (4 · ((𝑆↑2) + 𝐵)))
195 4cn 12137 . . . . 5 4 ∈ ℂ
196195a1i 11 . . . 4 (𝜑 → 4 ∈ ℂ)
19725recnd 11082 . . . 4 (𝜑 → (𝑆↑2) ∈ ℂ)
19873recnd 11082 . . . 4 (𝜑𝐵 ∈ ℂ)
199196, 197, 198adddid 11078 . . 3 (𝜑 → (4 · ((𝑆↑2) + 𝐵)) = ((4 · (𝑆↑2)) + (4 · 𝐵)))
200194, 199breqtrd 5112 . 2 (𝜑 → ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵)))
201 remulcl 11035 . . . 4 ((4 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (4 · 𝐵) ∈ ℝ)
2021, 73, 201sylancr 587 . . 3 (𝜑 → (4 · 𝐵) ∈ ℝ)
20343, 202, 27leadd2d 11649 . 2 (𝜑 → (((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵) ↔ ((4 · (𝑆↑2)) + ((𝐾𝐷𝐿)↑2)) ≤ ((4 · (𝑆↑2)) + (4 · 𝐵))))
204200, 203mpbird 256 1 (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  wne 2940  wral 3061  wrex 3070  cin 3895  wss 3896  c0 4266   class class class wbr 5086  cmpt 5169  ran crn 5608  cfv 6465  (class class class)co 7316  infcinf 9276  cc 10948  cr 10949  0cc0 10950  1c1 10951   + caddc 10953   · cmul 10955   < clt 11088  cle 11089   / cdiv 11711  2c2 12107  4c4 12109  cexp 13861  abscabs 15021  Metcmet 20663  MetOpencmopn 20667  NrmCVeccnv 29078   +𝑣 cpv 29079  BaseSetcba 29080   ·𝑠OLD cns 29081  𝑣 cnsb 29083  normCVcnmcv 29084  IndMetcims 29085  SubSpcss 29215  CPreHilOLDccphlo 29306  CBanccbn 29356
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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5223  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-cnex 11006  ax-resscn 11007  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-addrcl 11011  ax-mulcl 11012  ax-mulrcl 11013  ax-mulcom 11014  ax-addass 11015  ax-mulass 11016  ax-distr 11017  ax-i2m1 11018  ax-1ne0 11019  ax-1rid 11020  ax-rnegex 11021  ax-rrecex 11022  ax-cnre 11023  ax-pre-lttri 11024  ax-pre-lttrn 11025  ax-pre-ltadd 11026  ax-pre-mulgt0 11027  ax-pre-sup 11028  ax-addf 11029  ax-mulf 11030
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-pss 3915  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-iun 4938  df-br 5087  df-opab 5149  df-mpt 5170  df-tr 5204  df-id 5506  df-eprel 5512  df-po 5520  df-so 5521  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7273  df-ov 7319  df-oprab 7320  df-mpo 7321  df-om 7759  df-1st 7877  df-2nd 7878  df-frecs 8145  df-wrecs 8176  df-recs 8250  df-rdg 8289  df-er 8547  df-map 8666  df-en 8783  df-dom 8784  df-sdom 8785  df-sup 9277  df-inf 9278  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093  df-le 11094  df-sub 11286  df-neg 11287  df-div 11712  df-nn 12053  df-2 12115  df-3 12116  df-4 12117  df-n0 12313  df-z 12399  df-uz 12662  df-rp 12810  df-xadd 12928  df-seq 13801  df-exp 13862  df-cj 14886  df-re 14887  df-im 14888  df-sqrt 15022  df-abs 15023  df-xmet 20670  df-met 20671  df-grpo 28987  df-gid 28988  df-ginv 28989  df-gdiv 28990  df-ablo 29039  df-vc 29053  df-nv 29086  df-va 29089  df-ba 29090  df-sm 29091  df-0v 29092  df-vs 29093  df-nmcv 29094  df-ims 29095  df-ssp 29216  df-ph 29307  df-cbn 29357
This theorem is referenced by:  minvecolem3  29370  minvecolem7  29377
  Copyright terms: Public domain W3C validator