---

Step * 2 of Lemma real-vec-angle-lemma


1. n : ℕ
2. x : ℝ^n
3. z : ℝ^n
4. z⋅x = x⋅z
5. r0 < x⋅z
⊢ (x⋅x + (r(-2) * x⋅z) + z⋅z) < (x⋅x + (r(2) * x⋅z) + z⋅z)
BY
{ nRAdd ⌜(r(2) * x⋅z) - z⋅z + x⋅x⌝ 0⋅ }

1
1. n : ℕ
2. x : ℝ^n
3. z : ℝ^n
4. z⋅x = x⋅z
5. r0 < x⋅z
⊢ r0 < (r(4) * x⋅z)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  x  :  \mBbbR{}\^{}n
3.  z  :  \mBbbR{}\^{}n
4.  z\mcdot{}x  =  x\mcdot{}z
5.  r0  <  x\mcdot{}z
\mvdash{}  (x\mcdot{}x  +  (r(-2)  *  x\mcdot{}z)  +  z\mcdot{}z)  <  (x\mcdot{}x  +  (r(2)  *  x\mcdot{}z)  +  z\mcdot{}z)


By

---

Latex:
nRAdd  \mkleeneopen{}(r(2)  *  x\mcdot{}z)  -  z\mcdot{}z  +  x\mcdot{}x\mkleeneclose{}  0\mcdot{}

---

Home Index