---

Step * of Lemma fps-geometric-slice_lemma2

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[n:ℕ+]. ∀[m:ℕn]. ∀[g:PowerSeries(X;r)].
    [(1÷(1-g))]_m = if (m =z 0) then 1 else 0 fi  ∈ PowerSeries(X;r) supposing g = [g]_n ∈ PowerSeries(X;r) 
  supposing valueall-type(X)
BY
{ (Auto
   THEN (Assert IsRing(|fps-rng(r)|;+fps-rng(r);0;-fps-rng(r);*;1) BY
               ((InstLemma `fps-rng_wf` [⌜X⌝;⌜eq⌝;⌜r⌝]⋅ THENA Auto)
                THEN (MemTypeD (-1) THENA Auto)
                THEN Fold `member` (-2)
                THEN MemTypeD (-2)
                THEN Auto))
   THEN RepUR ``fps-rng`` -1
   THEN (InstLemma `fps-mul-slice` [⌜X⌝;⌜eq⌝;⌜r⌝;⌜m⌝;⌜(1-g)⌝;⌜(1÷(1-g))⌝]⋅ THENA Auto)
   THEN (InstLemma `fps-div-property` [⌜X⌝;⌜eq⌝;⌜r⌝;⌜1⌝;⌜(1-g)⌝;⌜1⌝]⋅
         THENA (Auto
                THEN RepUR ``fps-sub fps-neg fps-coeff fps-add fps-one bag-null empty-bag`` 0
                THEN Fold `empty-bag` 0
                THEN Subst' (g {}) = 0 ∈ |r| 0
                THEN Auto
                THEN RW RngNormC 0
                THEN Auto
                THEN (Fold `fps-coeff` 0 THEN Subst ⌜g[{}] = [g]_n[{}] ∈ |r|⌝ 0⋅ THEN Auto)⋅
                THEN RepUR ``fps-coeff fps-slice`` 0
                THEN AutoSplit)
         )
   THEN HypSubst' (-1) (-2)
   THEN Auto
   THEN Thin (-1)
   THEN (InstLemma `fps-one-slice` [⌜X⌝;⌜r⌝;⌜m⌝]⋅ THENA Auto)
   THEN (HypSubst' (-1) (-2) THENA Auto)
   THEN Thin (-1)
   THEN SplitOnHypITE -1 
   THEN Auto) }

1
.....truecase..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. n : ℕ+
6. m : ℕn
7. g : PowerSeries(X;r)
8. g = [g]_n ∈ PowerSeries(X;r)
9. IsRing(PowerSeries(X;r);λf,g. (f+g);0;λf.-(f);λf,g. (f*g);1)
10. 1 = fps-summation(r;upto(m + 1);k.([(1-g)]_k*[(1÷(1-g))]_m - k)) ∈ PowerSeries(X;r)
11. m = 0 ∈ ℤ
⊢ [(1÷(1-g))]_m = if (m =z 0) then 1 else 0 fi  ∈ PowerSeries(X;r)

2
.....falsecase..... 
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. n : ℕ+
6. m : ℕn
7. g : PowerSeries(X;r)
8. g = [g]_n ∈ PowerSeries(X;r)
9. IsRing(PowerSeries(X;r);λf,g. (f+g);0;λf.-(f);λf,g. (f*g);1)
10. 0 = fps-summation(r;upto(m + 1);k.([(1-g)]_k*[(1÷(1-g))]_m - k)) ∈ PowerSeries(X;r)
11. ¬(m = 0 ∈ ℤ)
⊢ [(1÷(1-g))]_m = if (m =z 0) then 1 else 0 fi  ∈ PowerSeries(X;r)

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[m:\mBbbN{}n].  \mforall{}[g:PowerSeries(X;r)].
        [(1\mdiv{}(1-g))]\_m  =  if  (m  =\msubz{}  0)  then  1  else  0  fi    supposing  g  =  [g]\_n 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  (Assert  IsRing(|fps-rng(r)|;+fps-rng(r);0;-fps-rng(r);*;1)  BY
                          ((InstLemma  `fps-rng\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (MemTypeD  (-1)  THENA  Auto)
                            THEN  Fold  `member`  (-2)
                            THEN  MemTypeD  (-2)
                            THEN  Auto))
  THEN  RepUR  ``fps-rng``  -1
  THEN  (InstLemma  `fps-mul-slice`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}(1-g)\mkleeneclose{};\mkleeneopen{}(1\mdiv{}(1-g))\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `fps-div-property`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}(1-g)\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  RepUR  ``fps-sub  fps-neg  fps-coeff  fps-add  fps-one  bag-null  empty-bag``  0
                            THEN  Fold  `empty-bag`  0
                            THEN  Subst'  (g  \{\})  =  0  0
                            THEN  Auto
                            THEN  RW  RngNormC  0
                            THEN  Auto
                            THEN  (Fold  `fps-coeff`  0  THEN  Subst  \mkleeneopen{}g[\{\}]  =  [g]\_n[\{\}]\mkleeneclose{}  0\mcdot{}  THEN  Auto)\mcdot{}
                            THEN  RepUR  ``fps-coeff  fps-slice``  0
                            THEN  AutoSplit)
              )
  THEN  HypSubst'  (-1)  (-2)
  THEN  Auto
  THEN  Thin  (-1)
  THEN  (InstLemma  `fps-one-slice`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-1)  (-2)  THENA  Auto)
  THEN  Thin  (-1)
  THEN  SplitOnHypITE  -1 
  THEN  Auto)

---

Home Index