---

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


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)
BY
{ ((Assert (-(r1 + -(dd)^2) + r2^2) = ((r(2) * dd * r1) - (dd * dd) + (r1 * r1) + -(r2 * r2)) BY
          ((RWO  "rnexp2" 0 THENM nRNorm 0) THENA Auto))
   THEN (RWO "-1" (-2) THENA Auto)
   ) }

1
1. r1 : ℝ
2. r2 : ℝ
3. dd : ℝ
4. r0 ≤ ((dd * dd) + (r(2) * dd * r1) + (r1 * r1) + -(r2 * r2))
5. r0 ≤ ((r(2) * dd * r1) - (dd * dd) + (r1 * r1) + -(r2 * r2))
6. (-(r1 + -(dd)^2) + r2^2) = ((r(2) * dd * r1) - (dd * dd) + (r1 * r1) + -(r2 * r2))
⊢ (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{}  ((dd  *  dd)  +  (r(2)  *  dd  *  r1)  +  (r1  *  r1)  +  -(r2  *  r2))
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:
((Assert  (-(r1  +  -(dd)\^{}2)  +  r2\^{}2)  =  ((r(2)  *  dd  *  r1)  -  (dd  *  dd)  +  (r1  *  r1)  +  -(r2  *  r2))  BY
                ((RWO    "rnexp2"  0  THENM  nRNorm  0)  THENA  Auto))
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  )

---

Home Index