---

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


1. a : ℝ^2
2. b : ℝ^2
3. |a⋅b| < (||a|| * ||b||)
4. |a⋅b|^2 < ||a|| * ||b||^2
⊢ (((b 0) * (a 1)) - (a 0) * (b 1)) * (((b 0) * (a 1)) - (a 0) * (b 1)) ≠ r0
BY
{ ((RWW "rnexp-rmul real-vec-norm-squared rabs-rnexp<" (-1) THENA Auto)
   THEN (RWO "rabs-of-nonneg" (-1) THENA Auto)
   THEN (RWO "rnexp2" (-1) THENA Auto)) }

1
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

---

Latex:

---

Latex:

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


By

---

Latex:
((RWW  "rnexp-rmul  real-vec-norm-squared  rabs-rnexp<"  (-1)  THENA  Auto)
  THEN  (RWO  "rabs-of-nonneg"  (-1)  THENA  Auto)
  THEN  (RWO  "rnexp2"  (-1)  THENA  Auto))

---

Home Index