Step * 1 1 of Lemma rv-pos-angle-symmetry


1. : ℕ
2. : ℝ^n
3. : ℝ^n
4. : ℝ^n
5. |a b⋅b| < (||a b|| ||c b||)
6. (||c b|| ||a b||) (||a b|| ||c b||)
⊢ |c b⋅b| < (||a b|| ||c b||)
BY
(RWO "dot-product-comm" THEN Auto) }


Latex:


Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  c  :  \mBbbR{}\^{}n
5.  |a  -  b\mcdot{}c  -  b|  <  (||a  -  b||  *  ||c  -  b||)
6.  (||c  -  b||  *  ||a  -  b||)  =  (||a  -  b||  *  ||c  -  b||)
\mvdash{}  |c  -  b\mcdot{}a  -  b|  <  (||a  -  b||  *  ||c  -  b||)


By


Latex:
(RWO  "dot-product-comm"  0  THEN  Auto)




Home Index