---

Step * of Lemma ball-slice-radius_wf

∀[r:{r:ℝ| r0 ≤ r} ]. ∀[t:{t:ℝ| t ∈ [-(r), r]} ].  (ball-slice-radius(r;t) ∈ {r':ℝ| (r0 ≤ r') ∧ ((r'^2 + t^2) = r^2)} )
BY
{ (Intros
   THEN Unhide
   THEN (Assert r0 ≤ (r^2 - t^2) BY
               ((nRAdd ⌜t^2⌝ 0⋅ THENA Auto)
                THEN (Assert t^2 = |t|^2 BY
                            (RWO "rabs-rnexp2" 0 THEN Auto))
                THEN RWO "-1" 0
                THEN Auto
                THEN (BLemma `rnexp_functionality_wrt_rleq` THEN Auto)
                THEN DSetVars
                THEN Unhide
                THEN Auto
                THEN RWO "rabs-rleq-iff" 0
                THEN Auto))
   THEN ProveWfLemma
   THEN (MemTypeCD THEN Auto)
   THEN RWO "rsqrt-rnexp-2" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[r:\{r:\mBbbR{}|  r0  \mleq{}  r\}  ].  \mforall{}[t:\{t:\mBbbR{}|  t  \mmember{}  [-(r),  r]\}  ].
    (ball-slice-radius(r;t)  \mmember{}  \{r':\mBbbR{}|  (r0  \mleq{}  r')  \mwedge{}  ((r'\^{}2  +  t\^{}2)  =  r\^{}2)\}  )


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  (Assert  r0  \mleq{}  (r\^{}2  -  t\^{}2)  BY
                          ((nRAdd  \mkleeneopen{}t\^{}2\mkleeneclose{}  0\mcdot{}  THENA  Auto)
                            THEN  (Assert  t\^{}2  =  |t|\^{}2  BY
                                                    (RWO  "rabs-rnexp2"  0  THEN  Auto))
                            THEN  RWO  "-1"  0
                            THEN  Auto
                            THEN  (BLemma  `rnexp\_functionality\_wrt\_rleq`  THEN  Auto)
                            THEN  DSetVars
                            THEN  Unhide
                            THEN  Auto
                            THEN  RWO  "rabs-rleq-iff"  0
                            THEN  Auto))
  THEN  ProveWfLemma
  THEN  (MemTypeCD  THEN  Auto)
  THEN  RWO  "rsqrt-rnexp-2"  0
  THEN  Auto)

---

Home Index