---

Step * 2 of Lemma equals-qrep


1. r : ℚ
2. ∀[r,s:ℤ ⋃ (ℤ × ℤ-o)].  (qeq(r;s) ∈ 𝔹)
3. ∀a:ℤ ⋃ (ℤ × ℤ-o). (qrep(a) = a ∈ ℚ)
⊢ qrep(r) = r ∈ ℚ
BY
{ (newQuotD 1⋅
   THEN ((BHyp -1 THEN Auto) ORELSE (RWO "-1" 0 THEN Auto) ORELSE (Intros THEN D 0 THEN Auto) ORELSE Auto)
   ) }

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  \mforall{}[r,s:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})].    (qeq(r;s)  \mmember{}  \mBbbB{})
3.  \mforall{}a:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{}).  (qrep(a)  =  a)
\mvdash{}  qrep(r)  =  r


By

---

Latex:
(newQuotD  1\mcdot{}
  THEN  ((BHyp  -1  THEN  Auto)
              ORELSE  (RWO  "-1"  0  THEN  Auto)
              ORELSE  (Intros  THEN  D  0  THEN  Auto)
              ORELSE  Auto)
  )

---

Home Index