---

Step * of Lemma qinv_wf

∀[r:ℚ]. 1/r ∈ ℚ supposing ¬↑qeq(r;0)
BY
{ TACTIC:TACTIC:(BasicUniformUnivCD Auto THEN D 0) }

1
1. r : ℚ
2. ¬↑qeq(r;0)
⊢ 1/r ∈ ℚ

2
.....wf..... 
1. r : ℚ
⊢ istype(¬↑qeq(r;0))

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  1/r  \mmember{}  \mBbbQ{}  supposing  \mneg{}\muparrow{}qeq(r;0)


By

---

Latex:
TACTIC:TACTIC:(BasicUniformUnivCD  Auto  THEN  D  0)

---

Home Index