---

Step * 1 of Lemma qinv_wf


1. r : ℚ
2. ¬↑qeq(r;0)
⊢ 1/r ∈ ℚ
BY
{ TACTIC:TACTIC:(TACTIC:(newQuotD 1 THEN Try ((InstLemma `qeq-functionality` [⌜a⌝;⌜b⌝;⌜0⌝]⋅ THENA Auto)))
                 THEN Try (Unfold `member` 0)
                 THEN EqTypeCDRational
                 THEN Auto
                 THEN Try (BLemma `qeq_refl`)
                 THEN Try ((BLemma `qinv-wf` THEN Auto))) }

1
.....antecedent..... 
1. istype(ℤ ⋃ (ℤ × ℤ-o))
2. ∀r1,s:ℤ ⋃ (ℤ × ℤ-o).  istype(qeq(r1;s) = tt)
3. ∀r1:ℤ ⋃ (ℤ × ℤ-o). qeq(r1;r1) = tt
4. a : Base
5. b : Base
6. c : a = b ∈ pertype(λr,s. ((r ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ (s ∈ ℤ ⋃ (ℤ × ℤ-o)) ∧ qeq(r;s) = tt))
7. a ∈ ℤ ⋃ (ℤ × ℤ-o)
8. b ∈ ℤ ⋃ (ℤ × ℤ-o)
9. qeq(a;b) = tt
10. ¬↑qeq(a;0)
11. qeq(a;0) = qeq(b;0)
⊢ qeq(1/a;1/b) = tt

---

Latex:

---

Latex:

1.  r  :  \mBbbQ{}
2.  \mneg{}\muparrow{}qeq(r;0)
\mvdash{}  1/r  \mmember{}  \mBbbQ{}


By

---

Latex:
TACTIC:TACTIC:(TACTIC:(newQuotD  1
                                              THEN  Try  ((InstLemma  `qeq-functionality`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{}  THENA  Auto))
                                              )
                              THEN  Try  (Unfold  `member`  0)
                              THEN  EqTypeCDRational
                              THEN  Auto
                              THEN  Try  (BLemma  `qeq\_refl`)
                              THEN  Try  ((BLemma  `qinv-wf`  THEN  Auto)))

---

Home Index