---

Step * of Lemma equipollent-int_mod

No Annotations
∀m:ℕ+. ℤ_m ~ ℕm
BY
{ (Auto THEN Assert ⌜∀x:ℤ_m. (x mod m ∈ ℕm)⌝⋅) }

1
.....assertion..... 
1. m : ℕ+
⊢ ∀x:ℤ_m. (x mod m ∈ ℕm)

2
1. m : ℕ+
2. ∀x:ℤ_m. (x mod m ∈ ℕm)
⊢ ℤ_m ~ ℕm

---

Latex:

---

Latex:
No  Annotations
\mforall{}m:\mBbbN{}\msupplus{}.  \mBbbZ{}\_m  \msim{}  \mBbbN{}m


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}x:\mBbbZ{}\_m.  (x  mod  m  \mmember{}  \mBbbN{}m)\mkleeneclose{}\mcdot{})

---

Home Index