---

Step * 1 of Lemma int_mod_2_union_int_mod_3


1. EquivRel(ℤ;x,y.True)
⊢ ℤ_2 ⋃ ℤ_3 ≡ ℤ_1
BY
{ (InstLemma `int_mod_union_int_mod` [⌜2⌝;⌜3⌝]⋅ THEN Auto THEN NthHypEq (-1) THEN Repeat (EqCD) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  EquivRel(\mBbbZ{};x,y.True)
\mvdash{}  \mBbbZ{}\_2  \mcup{}  \mBbbZ{}\_3  \mequiv{}  \mBbbZ{}\_1


By

---

Latex:
(InstLemma  `int\_mod\_union\_int\_mod`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}3\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  NthHypEq  (-1)
  THEN  Repeat  (EqCD)
  THEN  Auto)\mcdot{}

---

Home Index