### Nuprl Lemma : rng_minus_sum

`∀[r:Rng]. ∀[a,b:ℤ].`
`  ∀[F:{a..b-} ⟶ |r|]. ((-r (Σ(r) a ≤ i < b. F[i])) = (Σ(r) a ≤ i < b. -r F[i]) ∈ |r|) supposing a ≤ b`

Proof

Definitions occuring in Statement :  rng_sum: rng_sum rng: `Rng` rng_minus: `-r` rng_car: `|r|` int_seg: `{i..j-}` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` so_apply: `x[s]` le: `A ≤ B` apply: `f a` function: `x:A ⟶ B[x]` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  true: `True` squash: `↓T` prop: `ℙ` rng: `Rng` uimplies: `b supposing a` member: `t ∈ T` uall: `∀[x:A]. B[x]` so_apply: `x[s]` so_lambda: `λ2x.t[x]` and: `P ∧ Q` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  rng_wf le_wf int_seg_wf rng_car_wf equal_wf rng_one_wf rng_minus_wf rng_times_sum_l rng_sum_wf squash_wf true_wf rng_times_over_minus rng_times_one iff_weakening_equal
Rules used in proof :  intEquality equalityTransitivity axiomEquality isect_memberEquality functionEquality baseClosed imageMemberEquality natural_numberEquality imageElimination lambdaEquality sqequalRule equalitySymmetry hyp_replacement because_Cache rename setElimination applyEquality hypothesis independent_isectElimination hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution functionExtensionality universeEquality productElimination independent_functionElimination

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b:\mBbbZ{}].
\mforall{}[F:\{a..b\msupminus{}\}  {}\mrightarrow{}  |r|].  ((-r  (\mSigma{}(r)  a  \mleq{}  i  <  b.  F[i]))  =  (\mSigma{}(r)  a  \mleq{}  i  <  b.  -r  F[i]))  supposing  a  \mleq{}  b

Date html generated: 2018_05_21-PM-03_15_12
Last ObjectModification: 2017_12_14-AM-10_03_39

Theory : rings_1

Home Index