---

Step * 2 of Lemma assert-is-qrep


1. p : ℤ × ℕ+
2. q : ℚ
3. qrep(q) = p ∈ (ℤ × ℕ+)
⊢ ↑is-qrep(p)
BY
{ RevHypSubst' (-1) 0 }

1
1. p : ℤ × ℕ+
2. q : ℚ
3. qrep(q) = p ∈ (ℤ × ℕ+)
⊢ ↑is-qrep(qrep(q))

---

Latex:

---

Latex:

1.  p  :  \mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}
2.  q  :  \mBbbQ{}
3.  qrep(q)  =  p
\mvdash{}  \muparrow{}is-qrep(p)


By

---

Latex:
RevHypSubst'  (-1)  0

---

Home Index