---

Step * of Lemma modulus_wf

∀[a:ℤ]. ∀[n:ℤ-o].  (a mod n ∈ ℕ)
BY
{ TACTIC:(ProveWfLemma THEN Assert ⌜-|n| < a rem n⌝⋅) }

1
.....assertion..... 
1. a : ℤ
2. n : ℤ-o
3. a rem n ∈ ℤ
4. 0 ∈ ℤ
5. a rem n < 0
⊢ -|n| < a rem n

2
1. a : ℤ
2. n : ℤ-o
3. a rem n ∈ ℤ
4. 0 ∈ ℤ
5. a rem n < 0
6. -|n| < a rem n
⊢ |n| + (a rem n) ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[n:\mBbbZ{}\msupminus{}\msupzero{}].    (a  mod  n  \mmember{}  \mBbbN{})


By

---

Latex:
TACTIC:(ProveWfLemma  THEN  Assert  \mkleeneopen{}-|n|  <  a  rem  n\mkleeneclose{}\mcdot{})

---

Home Index