---

Step * of Lemma fps-geometric-slice1

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[m:ℕ]. ∀[g:PowerSeries(X;r)].  ([(1÷(1-[g]_1))]_m = ([g]_1)^(m) ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ (xxxxxxInstLemma `fps-geometric-slice` []xxxxxx
   THEN RepeatFor 5 (ParallelLast')
   THEN InstHyp [⌜1⌝] (-1)⋅
   THEN Auto
   THEN RWW "-2 div-one rem-one" 0
   THEN Auto) }

1
.....rewrite subgoal..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. m : ℕ
6. ∀[n:ℕ+]. ∀[g:PowerSeries(X;r)].
     [(1÷(1-g))]_m = if (m rem n =z 0) then (g)^(m ÷ n) else 0 fi  ∈ PowerSeries(X;r) 
     supposing g = [g]_n ∈ PowerSeries(X;r)
7. ∀[g:PowerSeries(X;r)]
     [(1÷(1-g))]_m = if (m rem 1 =z 0) then (g)^(m ÷ 1) else 0 fi  ∈ PowerSeries(X;r) 
     supposing g = [g]_1 ∈ PowerSeries(X;r)
8. g : PowerSeries(X;r)
⊢ [g]_1 = [[g]_1]_1 ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[m:\mBbbN{}].  \mforall{}[g:PowerSeries(X;r)].    ([(1\mdiv{}(1-[g]\_1))]\_m  =  ([g]\_1)\^{}(m)) 
    supposing  valueall-type(X)


By

---

Latex:
(xxxxxxInstLemma  `fps-geometric-slice`  []xxxxxx
  THEN  RepeatFor  5  (ParallelLast')
  THEN  InstHyp  [\mkleeneopen{}1\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto
  THEN  RWW  "-2  div-one  rem-one"  0
  THEN  Auto)

---

Home Index