---

Step * of Lemma rem_3_to_1

∀[a:{...0}]. ∀[n:{...-1}].  ((a rem n) = (-(-a rem -n)) ∈ ℤ)
BY
{ ((UnivCD THENA Auto) THEN (D 2 THENA Auto) THEN (D 1 THENA Auto)) }

1
1. a : ℤ
2. a ≤ 0
3. n : ℤ
4. n ≤ (-1)
⊢ (a rem n) = (-(-a rem -n)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a:\{...0\}].  \mforall{}[n:\{...-1\}].    ((a  rem  n)  =  (-(-a  rem  -n)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (D  2  THENA  Auto)  THEN  (D  1  THENA  Auto))

---

Home Index