---

Step * of Lemma assert-is-qrep

∀p:ℤ × ℕ+. (↑is-qrep(p) ⇐⇒ ∃q:ℚ. (qrep(q) = p ∈ (ℤ × ℕ+)))
BY
{ xxx(Auto THEN ExRepD)xxx }

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

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

---

Latex:

---

Latex:
\mforall{}p:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}.  (\muparrow{}is-qrep(p)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}q:\mBbbQ{}.  (qrep(q)  =  p))


By

---

Latex:
xxx(Auto  THEN  ExRepD)xxx

---

Home Index