### Nuprl Lemma : int-to-ring-minus

`∀[r:Rng]. ∀[y:ℤ].  (int-to-ring(r;-y) = (-r int-to-ring(r;y)) ∈ |r|)`

Proof

Definitions occuring in Statement :  int-to-ring: `int-to-ring(r;n)` rng: `Rng` rng_minus: `-r` rng_car: `|r|` uall: `∀[x:A]. B[x]` apply: `f a` minus: `-n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` top: `Top` squash: `↓T` prop: `ℙ` rng: `Rng` infix_ap: `x f y` true: `True` subtype_rel: `A ⊆r B` uimplies: `b supposing a` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q`
Lemmas referenced :  int-to-ring-add rng_wf int-to-ring-zero minus-one-mul add-mul-special zero-mul equal_wf squash_wf true_wf rng_car_wf rng_plus_wf rng_minus_wf int-to-ring_wf infix_ap_wf iff_weakening_equal rng_plus_ac_1 rng_plus_comm rng_plus_inv rng_plus_zero
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality minusEquality hypothesis intEquality sqequalRule isect_memberEquality axiomEquality because_Cache voidElimination voidEquality applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry universeEquality setElimination rename natural_numberEquality imageMemberEquality baseClosed independent_isectElimination productElimination independent_functionElimination multiplyEquality

Latex:
\mforall{}[r:Rng].  \mforall{}[y:\mBbbZ{}].    (int-to-ring(r;-y)  =  (-r  int-to-ring(r;y)))

Date html generated: 2017_10_01-AM-08_19_14
Last ObjectModification: 2017_02_28-PM-02_03_48

Theory : rings_1

Home Index