---

Step * 1 1 1 of Lemma q-elim


1. r : ℚ
2. qrep(r) = r ∈ ℚ
3. v1 : ℤ
4. v2 : ℕ+
5. <v1, v2> ~ (v1/v2)
⊢ ∃p:ℤ. ∃q:ℕ+. ((¬(q = 0 ∈ ℚ)) c∧ (<v1, v2> = (p/q) ∈ ℚ))
BY
{ (HypSubst' -1 0⋅ THEN InstConcl [⌜v1⌝;⌜v2⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  qrep(r)  =  r
3.  v1  :  \mBbbZ{}
4.  v2  :  \mBbbN{}\msupplus{}
5.  <v1,  v2>  \msim{}  (v1/v2)
\mvdash{}  \mexists{}p:\mBbbZ{}.  \mexists{}q:\mBbbN{}\msupplus{}.  ((\mneg{}(q  =  0))  c\mwedge{}  (<v1,  v2>  =  (p/q)))


By

---

Latex:
(HypSubst'  -1  0\mcdot{}  THEN  InstConcl  [\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}v2\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index