---

Step * of Lemma Minkowski-equality

∀n:ℕ. ∀x,y:ℝ^n.
  ((r0 < ||y||) ⇒ (||x + y|| = (||x|| + ||y||)) ⇒ (∃t:ℝ. ((r0 ≤ t) ∧ req-vec(n;x;t*y) ∧ ((r0 < ||x||) ⇒ (r0 < t)))))
BY
{ (Auto
   THEN (Assert r0 < ||y||^2 BY
               (BLemma `rnexp-positive` THEN Auto))
   THEN (Assert ||x + y||^2 = (||x||^2 + ||y||^2 + (r(2) * x⋅y)) BY
               ((RWW "real-vec-norm-squared dot-product-linearity1.1 dot-product-linearity1.2" 0⋅ THENA Auto)
                THEN (RWW "dot-product-linearity2.1 dot-product-linearity2.2" 0⋅ THENA Auto)
                THEN ((Assert x⋅y = y⋅x BY (BLemma `dot-product-comm` THEN Auto)) THEN RWO "-1" 0 THEN Auto)
                THEN nRNorm 0
                THEN Auto))) }

1
1. n : ℕ
2. x : ℝ^n
3. y : ℝ^n
4. r0 < ||y||
5. ||x + y|| = (||x|| + ||y||)
6. r0 < ||y||^2
7. ||x + y||^2 = (||x||^2 + ||y||^2 + (r(2) * x⋅y))
⊢ ∃t:ℝ. ((r0 ≤ t) ∧ req-vec(n;x;t*y) ∧ ((r0 < ||x||) ⇒ (r0 < t)))

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}x,y:\mBbbR{}\^{}n.
    ((r0  <  ||y||)
    {}\mRightarrow{}  (||x  +  y||  =  (||x||  +  ||y||))
    {}\mRightarrow{}  (\mexists{}t:\mBbbR{}.  ((r0  \mleq{}  t)  \mwedge{}  req-vec(n;x;t*y)  \mwedge{}  ((r0  <  ||x||)  {}\mRightarrow{}  (r0  <  t)))))


By

---

Latex:
(Auto
  THEN  (Assert  r0  <  ||y||\^{}2  BY
                          (BLemma  `rnexp-positive`  THEN  Auto))
  THEN  (Assert  ||x  +  y||\^{}2  =  (||x||\^{}2  +  ||y||\^{}2  +  (r(2)  *  x\mcdot{}y))  BY
                          ((RWW  "real-vec-norm-squared  dot-product-linearity1.1  dot-product-linearity1.2"  0\mcdot{}
                              THENA  Auto
                              )
                            THEN  (RWW  "dot-product-linearity2.1  dot-product-linearity2.2"  0\mcdot{}  THENA  Auto)
                            THEN  ((Assert  x\mcdot{}y  =  y\mcdot{}x  BY
                                                      (BLemma  `dot-product-comm`  THEN  Auto))
                                        THEN  RWO  "-1"  0
                                        THEN  Auto)
                            THEN  nRNorm  0
                            THEN  Auto)))

---

Home Index