---

Step * 1 of Lemma assert-is-qrep


1. p : ℤ × ℕ+
2. ↑is-qrep(p)
⊢ ∃q:ℚ. (qrep(q) = p ∈ (ℤ × ℕ+))
BY
{ With ⌜p⌝ (D 0)⋅ }

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

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
With  \mkleeneopen{}p\mkleeneclose{}  (D  0)\mcdot{}

---

Home Index