---

Step * 2 1 1 of Lemma q-geometric-series


1. v : ℚ
2. v1 : ℚ
3. v2 : ℚ
4. (v * v1) = v2 ∈ ℚ
5. ¬(v = 0 ∈ ℚ)
⊢ v1 = (v2/v) ∈ ℚ
BY
{ ((RWO "-2<" 0 THEN Auto) THEN QMul ⌜v⌝ 0⋅) }

---

Latex:

---

Latex:

1.  v  :  \mBbbQ{}
2.  v1  :  \mBbbQ{}
3.  v2  :  \mBbbQ{}
4.  (v  *  v1)  =  v2
5.  \mneg{}(v  =  0)
\mvdash{}  v1  =  (v2/v)


By

---

Latex:
((RWO  "-2<"  0  THEN  Auto)  THEN  QMul  \mkleeneopen{}v\mkleeneclose{}  0\mcdot{})

---

Home Index