---

Step * 1 2 1 of Lemma coprime-equiv-unique


1. p : ℤ
2. q : ℤ
3. a : ℤ
4. b : ℤ
5. CoPrime(p,q)
6. CoPrime(a,b)
7. (p * b) = (a * q) ∈ ℤ
8. (p = a ∈ ℤ) ∨ (p = (-a) ∈ ℤ)
9. (q = b ∈ ℤ) ∨ (q = (-b) ∈ ℤ)
10. p < 0 ⇒ a < 0
11. p < 0 ⇐ a < 0
12. q < 0 ⇒ b < 0
13. q < 0 ⇐ b < 0
14. (p = (-a) ∈ ℤ) ⇒ (a = 0 ∈ ℤ)
15. (q = (-b) ∈ ℤ) ⇒ (b = 0 ∈ ℤ)
⊢ (p = a ∈ ℤ) ∧ (q = b ∈ ℤ)
BY
{ xxx(SplitOrHyps THEN Auto THEN ThinTrivial THEN Auto')xxx }

---

Latex:

---

Latex:

1.  p  :  \mBbbZ{}
2.  q  :  \mBbbZ{}
3.  a  :  \mBbbZ{}
4.  b  :  \mBbbZ{}
5.  CoPrime(p,q)
6.  CoPrime(a,b)
7.  (p  *  b)  =  (a  *  q)
8.  (p  =  a)  \mvee{}  (p  =  (-a))
9.  (q  =  b)  \mvee{}  (q  =  (-b))
10.  p  <  0  {}\mRightarrow{}  a  <  0
11.  p  <  0  \mLeftarrow{}{}  a  <  0
12.  q  <  0  {}\mRightarrow{}  b  <  0
13.  q  <  0  \mLeftarrow{}{}  b  <  0
14.  (p  =  (-a))  {}\mRightarrow{}  (a  =  0)
15.  (q  =  (-b))  {}\mRightarrow{}  (b  =  0)
\mvdash{}  (p  =  a)  \mwedge{}  (q  =  b)


By

---

Latex:
xxx(SplitOrHyps  THEN  Auto  THEN  ThinTrivial  THEN  Auto')xxx

---

Home Index