---

Step * 1 of Lemma q-elim


1. r : ℚ
2. qrep(r) = r ∈ ℚ
⊢ ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (qrep(r) = (p/q) ∈ ℚ))
BY
{ ((GenConclAtAddrType ⌜ℤ × ℕ+⌝ [2;2;2;2]⋅ THENA (Auto THEN BLemma `qrep-denom` THEN Auto))
   THEN (Thin (-1))
   THEN D -1) }

1
1. r : ℚ
2. qrep(r) = r ∈ ℚ
3. v1 : ℤ
4. v2 : ℕ+
⊢ ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (<v1, v2> = (p/q) ∈ ℚ))

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  qrep(r)  =  r
\mvdash{}  \mexists{}p:\mBbbZ{}.  \mexists{}q:\mBbbN{}\msupplus{}.  ((\mneg{}(q  =  0))  c\mwedge{}  (qrep(r)  =  (p/q)))


By

---

Latex:
((GenConclAtAddrType  \mkleeneopen{}\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}\mkleeneclose{}  [2;2;2;2]\mcdot{}  THENA  (Auto  THEN  BLemma  `qrep-denom`  THEN  Auto))
  THEN  (Thin  (-1))
  THEN  D  -1)

---

Home Index