---

Step * of Lemma rem-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