---

Step * 3 of Lemma geometric-series-one-half


1. n : ℕ
⊢ (r1/r(2))^n = (r1/r(2)^n)
BY
{ (RWO  "rnexp-rdiv<" 0 THENA (Auto THEN OrRight THEN EAuto 1)) }

1
1. n : ℕ
⊢ (r1^n/r(2)^n) = (r1/r(2)^n)

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
\mvdash{}  (r1/r(2))\^{}n  =  (r1/r(2)\^{}n)


By

---

Latex:
(RWO    "rnexp-rdiv<"  0  THENA  (Auto  THEN  OrRight  THEN  EAuto  1))

---

Home Index