---

Step * 2 1 1 1 of Lemma r2-left-right


1. x : ℝ^2
2. y : ℝ^2
3. x⋅λi.if (i =z 0) then -(y 1) else y 0 fi  = r0
⊢ ¬(|x⋅y| < (||x|| * ||y||))
BY
{ ((RWO "r2-dot-product" (-1) THENA Auto) THEN Reduce -1) }

1
1. x : ℝ^2
2. y : ℝ^2
3. (((x 0) * -(y 1)) + ((x 1) * (y 0))) = r0
⊢ ¬(|x⋅y| < (||x|| * ||y||))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}\^{}2
2.  y  :  \mBbbR{}\^{}2
3.  x\mcdot{}\mlambda{}i.if  (i  =\msubz{}  0)  then  -(y  1)  else  y  0  fi    =  r0
\mvdash{}  \mneg{}(|x\mcdot{}y|  <  (||x||  *  ||y||))


By

---

Latex:
((RWO  "r2-dot-product"  (-1)  THENA  Auto)  THEN  Reduce  -1)

---

Home Index