Nuprl Lemma : fps-exp-unroll
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[n:ℕ+]. ∀[f:PowerSeries(X;r)].  ((f)^(n) = ((f)^(n - 1)*f) ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
Proof
Definitions occuring in Statement : 
fps-exp: (f)^(n)
, 
fps-mul: (f*g)
, 
power-series: PowerSeries(X;r)
, 
deq: EqDecider(T)
, 
nat_plus: ℕ+
, 
valueall-type: valueall-type(T)
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
subtract: n - m
, 
natural_number: $n
, 
universe: Type
, 
equal: s = t ∈ T
, 
crng: CRng
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
uimplies: b supposing a
, 
subtype_rel: A ⊆r B
, 
fps-rng: fps-rng(r)
, 
rng_car: |r|
, 
pi1: fst(t)
, 
rng_times: *
, 
pi2: snd(t)
, 
infix_ap: x f y
, 
fps-exp: (f)^(n)
Lemmas referenced : 
rng_nexp_unroll, 
fps-rng_wf, 
crng_subtype_rng, 
crng_wf, 
deq_wf, 
valueall-type_wf, 
istype-universe
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation_alt, 
introduction, 
cut, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
independent_isectElimination, 
hypothesis, 
applyEquality, 
sqequalRule, 
isect_memberEquality_alt, 
axiomEquality, 
isectIsTypeImplies, 
inhabitedIsType, 
universeIsType, 
instantiate, 
universeEquality
Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[f:PowerSeries(X;r)].    ((f)\^{}(n)  =  ((f)\^{}(n  -  1)*f)) 
    supposing  valueall-type(X)
Date html generated:
2020_05_20-AM-09_05_45
Last ObjectModification:
2020_02_04-PM-01_54_43
Theory : power!series
Home
Index