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