---

Step * 1 1 1 2 2 1 1 1 of Lemma rv-compass-compass-lemma


1. r1 : ℝ
2. r2 : ℝ
3. dd : ℝ
4. r0 ≤ (r1 + dd^2 + -(r2^2))
5. r0 ≤ (-(r1 + -(dd)^2) + r2^2)
⊢ (r1^2 - r2^2) + dd^2^2 ≤ (r(4) * dd^2 * r1^2)
BY
{ ((RWO  "rnexp2" (-2) THENM nRNorm (-2)) THENA Auto) }

1
1. r1 : ℝ
2. r2 : ℝ
3. dd : ℝ
4. r0 ≤ ((dd * dd) + (r(2) * dd * r1) + (r1 * r1) + -(r2 * r2))
5. r0 ≤ (-(r1 + -(dd)^2) + r2^2)
⊢ (r1^2 - r2^2) + dd^2^2 ≤ (r(4) * dd^2 * r1^2)

---

Latex:

---

Latex:

1.  r1  :  \mBbbR{}
2.  r2  :  \mBbbR{}
3.  dd  :  \mBbbR{}
4.  r0  \mleq{}  (r1  +  dd\^{}2  +  -(r2\^{}2))
5.  r0  \mleq{}  (-(r1  +  -(dd)\^{}2)  +  r2\^{}2)
\mvdash{}  (r1\^{}2  -  r2\^{}2)  +  dd\^{}2\^{}2  \mleq{}  (r(4)  *  dd\^{}2  *  r1\^{}2)


By

---

Latex:
((RWO    "rnexp2"  (-2)  THENM  nRNorm  (-2))  THENA  Auto)

---

Home Index