---

Step * 2 of Lemma equipollent-int_mod


1. m : ℕ+
2. ∀x:ℤ_m. (x mod m ∈ ℕm)
⊢ ℤ_m ~ ℕm
BY
{ (With ⌜λx.(x mod m)⌝ (D 0)⋅ THEN Try (Complete (Auto)))⋅ }

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

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}\msupplus{}
2.  \mforall{}x:\mBbbZ{}\_m.  (x  mod  m  \mmember{}  \mBbbN{}m)
\mvdash{}  \mBbbZ{}\_m  \msim{}  \mBbbN{}m


By

---

Latex:
(With  \mkleeneopen{}\mlambda{}x.(x  mod  m)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Try  (Complete  (Auto)))\mcdot{}

---

Home Index