Step * of Lemma r2-det-convex2

[p,q,r,t,s:ℝ^2]. ∀[a,b,c:ℝ].
  |a*p b*q c*rts| ((a |pts|) (b |qts|) (c |rts|)) supposing ((a c) r1) ∧ r1 a ≠ r0
BY
Auto }

1
1. : ℝ^2
2. : ℝ^2
3. : ℝ^2
4. : ℝ^2
5. : ℝ^2
6. : ℝ
7. : ℝ
8. : ℝ
9. (a c) r1
10. r1 a ≠ r0
⊢ |a*p b*q c*rts| ((a |pts|) (b |qts|) (c |rts|))


Latex:


Latex:
\mforall{}[p,q,r,t,s:\mBbbR{}\^{}2].  \mforall{}[a,b,c:\mBbbR{}].
    |a*p  +  b*q  +  c*rts|  =  ((a  *  |pts|)  +  (b  *  |qts|)  +  (c  *  |rts|)) 
    supposing  ((a  +  b  +  c)  =  r1)  \mwedge{}  r1  -  a  \mneq{}  r0


By


Latex:
Auto




Home Index