---

Step * of Lemma int-to-ring-minus

∀[r:Rng]. ∀[y:ℤ].  (int-to-ring(r;-y) = (-r int-to-ring(r;y)) ∈ |r|)
BY
{ (Auto THEN (InstLemma `int-to-ring-add` [⌜r⌝;⌜y⌝;⌜-y⌝]⋅ THENA Auto)) }

1
1. r : Rng
2. y : ℤ
3. int-to-ring(r;y + (-y)) = (int-to-ring(r;y) +r int-to-ring(r;-y)) ∈ |r|
⊢ int-to-ring(r;-y) = (-r int-to-ring(r;y)) ∈ |r|

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (InstLemma  `int-to-ring-add`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}-y\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index