---

Step * of Lemma rem-minus-1

No Annotations
∀a:ℤ. (a rem -1 ~ 0)
BY
{ ((Auto THEN (InstLemma `rem_bounds_absval` [⌜-1⌝;⌜a⌝]⋅ THENA Auto))
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜a rem -1⌝⋅ THENA Auto)) }

1
1. a : ℤ
2. v : ℤ
3. (a rem -1) = v ∈ ℤ
⊢ |v| < |-1| ⇒ (v = 0 ∈ ℤ)

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:\mBbbZ{}.  (a  rem  -1  \msim{}  0)


By

---

Latex:
((Auto  THEN  (InstLemma  `rem\_bounds\_absval`  [\mkleeneopen{}-1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}a  rem  -1\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index