---

Step * 2 1 of Lemma equipollent-int_mod


1. m : ℕ+
2. ∀x:ℤ_m. (x mod m ∈ ℕm)
⊢ Bij(ℤ_m;ℕm;λx.(x mod m))
BY
{ (RepeatFor 2 (D 0) THEN Reduce 0 THEN Auto) }

1
1. m : ℕ+
2. ∀x:ℤ_m. (x mod m ∈ ℕm)
3. a1 : ℤ_m
4. a2 : ℤ_m
5. (a1 mod m) = (a2 mod m) ∈ ℕm
⊢ a1 = a2 ∈ ℤ_m

2
1. m : ℕ+
2. ∀x:ℤ_m. (x mod m ∈ ℕm)
3. b : ℕm
⊢ ∃a:ℤ_m. ((a mod m) = b ∈ ℕm)

---

Latex:

---

Latex:

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


By

---

Latex:
(RepeatFor  2  (D  0)  THEN  Reduce  0  THEN  Auto)

---

Home Index