---

Step * of Lemma qinv-wf

∀[r:ℤ ⋃ (ℤ × ℤ-o)]. 1/r ∈ ℤ ⋃ (ℤ × ℤ-o) supposing ¬↑qeq(r;0)
BY
{ Auto }

1
1. r : ℤ ⋃ (ℤ × ℤ-o)
2. ¬↑qeq(r;0)
⊢ 1/r ∈ ℤ ⋃ (ℤ × ℤ-o)

---

Latex:

---

Latex:
\mforall{}[r:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})].  1/r  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})  supposing  \mneg{}\muparrow{}qeq(r;0)


By

---

Latex:
Auto

---

Home Index