---

Step * 1 1 1 1 1 1 of Lemma r2-det-nonzero


1. a : ℝ^2
2. b : ℝ^2
3. |a⋅b| < (||a|| * ||b||)
4. (a⋅b * a⋅b) < (a⋅a * b⋅b)
⊢ (((b 0) * (a 1)) - (a 0) * (b 1)) * (((b 0) * (a 1)) - (a 0) * (b 1)) ≠ r0
BY
{ ((RepUR ``dot-product`` -1
    THEN (RWO "rsum_unroll" (-1) THENA Auto)
    THEN Reduce -1
    THEN (RWO "rsum_single" (-1) THENA Auto))
   THEN MoveToConcl (-1)
   THEN GenConclTerms Auto [⌜a 0⌝;⌜a 1⌝;⌜b 0⌝;⌜b 1⌝]⋅
   THEN All Thin) }

1
1. v : ℝ
2. v1 : ℝ
3. v2 : ℝ
4. v3 : ℝ
⊢ ((((v * v2) + (v1 * v3)) * ((v * v2) + (v1 * v3))) < (((v * v) + (v1 * v1)) * ((v2 * v2) + (v3 * v3))))
⇒ ((v2 * v1) - v * v3) * ((v2 * v1) - v * v3) ≠ r0

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  |a\mcdot{}b|  <  (||a||  *  ||b||)
4.  (a\mcdot{}b  *  a\mcdot{}b)  <  (a\mcdot{}a  *  b\mcdot{}b)
\mvdash{}  (((b  0)  *  (a  1))  -  (a  0)  *  (b  1))  *  (((b  0)  *  (a  1))  -  (a  0)  *  (b  1))  \mneq{}  r0


By

---

Latex:
((RepUR  ``dot-product``  -1
    THEN  (RWO  "rsum\_unroll"  (-1)  THENA  Auto)
    THEN  Reduce  -1
    THEN  (RWO  "rsum\_single"  (-1)  THENA  Auto))
  THEN  MoveToConcl  (-1)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}a  0\mkleeneclose{};\mkleeneopen{}a  1\mkleeneclose{};\mkleeneopen{}b  0\mkleeneclose{};\mkleeneopen{}b  1\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index