Step
*
1
of Lemma
int-to-ring-minus
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|
BY
{ ((RW IntNormC (-1) THENM RWO "int-to-ring-zero" (-1)) THENA Auto) }
1
1. r : Rng
2. y : ℤ
3. 0 = (int-to-ring(r;y) +r int-to-ring(r;(-1) * y)) ∈ |r|
⊢ int-to-ring(r;-y) = (-r int-to-ring(r;y)) ∈ |r|
Latex:
Latex:
1. r : Rng
2. y : \mBbbZ{}
3. int-to-ring(r;y + (-y)) = (int-to-ring(r;y) +r int-to-ring(r;-y))
\mvdash{} int-to-ring(r;-y) = (-r int-to-ring(r;y))
By
Latex:
((RW IntNormC (-1) THENM RWO "int-to-ring-zero" (-1)) THENA Auto)
Home
Index