---

Step * 1 of Lemma qinv-wf


1. r : ℤ ⋃ (ℤ × ℤ-o)
2. ¬↑qeq(r;0)
⊢ 1/r ∈ ℤ ⋃ (ℤ × ℤ-o)
BY
{ (Unfold `qinv` 0
   THEN All D_rational_form
   THEN ((Reduce 0 THENA Auto) THEN ((CallByValueReduce 0 THENA Auto) THEN Reduce 0 THEN Auto)⋅)
   THEN BUnionRight
   THEN Auto
   THEN MemTypeCD
   THEN Auto
   THEN D 0
   THEN Auto
   THEN D -2
   THEN HypSubst' (-1) 0) }

1
1. a1 : ℤ
2. a1 = 0 ∈ ℤ@i
⊢ ↑qeq(0;0)

2
1. a2 : ℤ
2. a3 : ℤ-o
3. a2 = 0 ∈ ℤ@i
⊢ ↑qeq(<0, a3>;0)

---

Latex:

---

Latex:

1.  r  :  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})
2.  \mneg{}\muparrow{}qeq(r;0)
\mvdash{}  1/r  \mmember{}  \mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{})


By

---

Latex:
(Unfold  `qinv`  0
  THEN  All  D\_rational\_form
  THEN  ((Reduce  0  THENA  Auto)  THEN  ((CallByValueReduce  0  THENA  Auto)  THEN  Reduce  0  THEN  Auto)\mcdot{})
  THEN  BUnionRight
  THEN  Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  D  -2
  THEN  HypSubst'  (-1)  0)

---

Home Index