---

Step * of Lemma modulus-int_mod-nonzero

∀[n:ℕ+]. ∀[x:ℤ_n].  x mod n ∈ ℕ+n supposing x ≠ 0 ∈ ℤ_n 
BY
{ (InstLemma `modulus_wf_int_mod` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (Assert ⌜¬((x mod n) = 0 ∈ ℤ)⌝⋅ THENM Auto)) }

1
.....assertion..... 
1. n : ℕ+
2. x : ℤ_n
3. x mod n ∈ ℕn
4. x ≠ 0 ∈ ℤ_n 
⊢ ¬((x mod n) = 0 ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[x:\mBbbZ{}\_n].    x  mod  n  \mmember{}  \mBbbN{}\msupplus{}n  supposing  x  \mneq{}  0  \mmember{}  \mBbbZ{}\_n 


By

---

Latex:
(InstLemma  `modulus\_wf\_int\_mod`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mneg{}((x  mod  n)  =  0)\mkleeneclose{}\mcdot{}  THENM  Auto))

---

Home Index