Nuprl Lemma : negerse_fps

[X:Type]. ∀[r:CRng]. ∀[a:PowerSeries(X;r)].  (((a+-(a)) 0 ∈ PowerSeries(X;r)) ∧ ((-(a)+a) 0 ∈ PowerSeries(X;r)))


Proof




Definitions occuring in Statement :  fps-neg: -(f) fps-add: (f+g) fps-zero: 0 power-series: PowerSeries(X;r) uall: [x:A]. B[x] and: P ∧ Q universe: Type equal: t ∈ T crng: CRng
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q cand: c∧ B squash: T prop: true: True subtype_rel: A ⊆B uimplies: supposing a guard: {T} iff: ⇐⇒ Q rev_implies:  Q implies:  Q fps-zero: 0 fps-neg: -(f) fps-add: (f+g) power-series: PowerSeries(X;r) fps-coeff: f[b] crng: CRng rng: Rng infix_ap: y
Lemmas referenced :  equal_wf squash_wf true_wf power-series_wf fps-add-comm fps-neg_wf iff_weakening_equal crng_wf bag_wf rng_car_wf rng_zero_wf rng_plus_inv
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut independent_pairFormation hypothesis applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity equalitySymmetry universeEquality cumulativity natural_numberEquality sqequalRule imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination independent_pairEquality axiomEquality isect_memberEquality because_Cache functionExtensionality setElimination rename

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[a:PowerSeries(X;r)].    (((a+-(a))  =  0)  \mwedge{}  ((-(a)+a)  =  0))



Date html generated: 2018_05_21-PM-09_56_35
Last ObjectModification: 2017_07_26-PM-06_32_59

Theory : power!series


Home Index