---

Step * 1 3 of Lemma assert-is-qrep

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index