---

Step * 1 1 of Lemma r2-left-separated

.....assertion..... 
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. r0 < |acd|
6. r0 < |bdc|
7. r0 < (|acd| + |bdc|)
⊢ (|acd| + |bdc|) = a - b⋅λi.if (i =z 0) then (c 1) - d 1 else (d 0) - c 0 fi 
BY
{ ((RWO "r2-dot-product" 0 THENA Auto) THEN RepUR ``real-vec-sub r2-det`` 0 THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  c  :  \mBbbR{}\^{}2
4.  d  :  \mBbbR{}\^{}2
5.  r0  <  |acd|
6.  r0  <  |bdc|
7.  r0  <  (|acd|  +  |bdc|)
\mvdash{}  (|acd|  +  |bdc|)  =  a  -  b\mcdot{}\mlambda{}i.if  (i  =\msubz{}  0)  then  (c  1)  -  d  1  else  (d  0)  -  c  0  fi 


By

---

Latex:
((RWO  "r2-dot-product"  0  THENA  Auto)  THEN  RepUR  ``real-vec-sub  r2-det``  0  THEN  Auto)

---

Home Index