---

Step * 2 1 of Lemma equipollent-rationals


1. a1 : ℚ
2. a2 : ℚ
3. qrep(a1) = qrep(a2) ∈ {p:ℤ × ℕ+| ↑is-qrep(p)} 
⊢ a1 = a2 ∈ ℚ
BY
{ ((InstLemma `equals-qrep` [⌜a1⌝]⋅ THENA Auto) THEN (InstLemma `equals-qrep` [⌜a2⌝]⋅ THENA Auto)) }

1
1. a1 : ℚ
2. a2 : ℚ
3. qrep(a1) = qrep(a2) ∈ {p:ℤ × ℕ+| ↑is-qrep(p)} 
4. qrep(a1) = a1 ∈ ℚ
5. qrep(a2) = a2 ∈ ℚ
⊢ a1 = a2 ∈ ℚ

---

Latex:

---

Latex:

1.  a1  :  \mBbbQ{}
2.  a2  :  \mBbbQ{}
3.  qrep(a1)  =  qrep(a2)
\mvdash{}  a1  =  a2


By

---

Latex:
((InstLemma  `equals-qrep`  [\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  (InstLemma  `equals-qrep`  [\mkleeneopen{}a2\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index