---

Step * of Lemma equals-qrep

∀[r:ℚ]. (qrep(r) = r ∈ ℚ)
BY
{ ((Intro THEN InstLemma `qeq_wf` [])
   THEN (Assert ∀a:ℤ ⋃ (ℤ × ℤ-o). (qrep(a) = a ∈ ℚ) BY
               ((D 0 THENA Auto)
                THEN ((InstLemma `qeq-qrep` [⌜a⌝])⋅ THENA (DoSubsume THEN Auto))
                THEN ((InstLemma `qrep_wf` [⌜a⌝])⋅ THENA (DoSubsume THEN Auto))⋅
                THEN (Symmetry THEN (EqTypeCD THEN Try (QuickAuto))⋅)⋅))
   ) }

1
.....aux..... 
1. r : ℚ
2. ∀[r,s:ℤ ⋃ (ℤ × ℤ-o)].  (qeq(r;s) ∈ 𝔹)
3. a : ℤ ⋃ (ℤ × ℤ-o)
4. qeq(a;qrep(a)) = tt
5. qrep(a) ∈ ℤ × ℕ+
⊢ qrep(a) ∈ ℤ ⋃ (ℤ × ℤ-o)

2
1. r : ℚ
2. ∀[r,s:ℤ ⋃ (ℤ × ℤ-o)].  (qeq(r;s) ∈ 𝔹)
3. ∀a:ℤ ⋃ (ℤ × ℤ-o). (qrep(a) = a ∈ ℚ)
⊢ qrep(r) = r ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  (qrep(r)  =  r)


By

---

Latex:
((Intro  THEN  InstLemma  `qeq\_wf`  [])
  THEN  (Assert  \mforall{}a:\mBbbZ{}  \mcup{}  (\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{}).  (qrep(a)  =  a)  BY
                          ((D  0  THENA  Auto)
                            THEN  ((InstLemma  `qeq-qrep`  [\mkleeneopen{}a\mkleeneclose{}])\mcdot{}  THENA  (DoSubsume  THEN  Auto))
                            THEN  ((InstLemma  `qrep\_wf`  [\mkleeneopen{}a\mkleeneclose{}])\mcdot{}  THENA  (DoSubsume  THEN  Auto))\mcdot{}
                            THEN  (Symmetry  THEN  (EqTypeCD  THEN  Try  (QuickAuto))\mcdot{})\mcdot{}))
  )

---

Home Index