---

Step * 2 of Lemma int_mod_2_union_int_mod_3


1. EquivRel(ℤ;x,y.True)
⊢ ℤ_1 ≡ ⇃(ℤ)
BY
{ (D 0 THEN D 0 THEN Auto THEN D (-1) THEN Auto THEN Try (EqTypeCD) THEN EAuto 1) }

1
.....antecedent..... 
1. EquivRel(ℤ;x,y.True)
2. x : Base
3. x1 : Base
4. x = x1 ∈ pertype(λx,y. ((x ∈ ℤ) ∧ (y ∈ ℤ) ∧ True))
5. x ∈ ℤ
6. x1 ∈ ℤ
7. True
⊢ x ≡ x1 mod 1

---

Latex:

---

Latex:

1.  EquivRel(\mBbbZ{};x,y.True)
\mvdash{}  \mBbbZ{}\_1  \mequiv{}  \00D9(\mBbbZ{})


By

---

Latex:
(D  0  THEN  D  0  THEN  Auto  THEN  D  (-1)  THEN  Auto  THEN  Try  (EqTypeCD)  THEN  EAuto  1)

---

Home Index