Step * 2 1 1 1 1 of Lemma not-proj-sep-iff-proj-eq


1. : ℕ
2. : ℙ^n
3. : ℙ^n
4. : ℝ
5. ||a|| (|m| ||b||)
6. m < r0
7. ∀i:ℕ1. ((a i) (m (b i)))
8. : ℕ1
9. (a i) (m (b i))
⊢ ((b i) ||b|| m) -((b i) |m| ||b||)
BY
(RWO "rabs-of-nonpos" THEN Auto) }


Latex:


Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbP{}\^{}n
3.  b  :  \mBbbP{}\^{}n
4.  m  :  \mBbbR{}
5.  ||a||  =  (|m|  *  ||b||)
6.  m  <  r0
7.  \mforall{}i:\mBbbN{}n  +  1.  ((a  i)  =  (m  *  (b  i)))
8.  i  :  \mBbbN{}n  +  1
9.  (a  i)  =  (m  *  (b  i))
\mvdash{}  ((b  i)  *  ||b||  *  m)  =  -((b  i)  *  |m|  *  ||b||)


By


Latex:
(RWO  "rabs-of-nonpos"  0  THEN  Auto)




Home Index