---

Step * of Lemma int_mod_2_union_int_mod_3

ℤ_2 ⋃ ℤ_3 ≡ ⇃(ℤ)
BY
{ ((Assert EquivRel(ℤ;x,y.True) BY
          Repeat ((D 0 THEN Auto)))
   THEN (Using [`B',⌜ℤ_1⌝] (BLemma `ext-eq_transitivity`)⋅ THEN Auto)
   ) }

1
1. EquivRel(ℤ;x,y.True)
⊢ ℤ_2 ⋃ ℤ_3 ≡ ℤ_1

2
1. EquivRel(ℤ;x,y.True)
⊢ ℤ_1 ≡ ⇃(ℤ)

---

Latex:

---

Latex:
\mBbbZ{}\_2  \mcup{}  \mBbbZ{}\_3  \mequiv{}  \00D9(\mBbbZ{})


By

---

Latex:
((Assert  EquivRel(\mBbbZ{};x,y.True)  BY
                Repeat  ((D  0  THEN  Auto)))
  THEN  (Using  [`B',\mkleeneopen{}\mBbbZ{}\_1\mkleeneclose{}]  (BLemma  `ext-eq\_transitivity`)\mcdot{}  THEN  Auto)
  )

---

Home Index