---

Step * 1 2 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) ∧ (q ~ b)
⊢ ({(p = a ∈ ℤ) ∧ (q = b ∈ ℤ)}) supposing ((q < 0 ⇐⇒ b < 0) and (p < 0 ⇐⇒ a < 0))
BY
{ xxx((RWO "assoced_elim" (-1))
      THEN Auto
      THEN Unfold `guard` 0
      THEN (Assert ⌜(p = (-a) ∈ ℤ) ⇒ (a = 0 ∈ ℤ)⌝ BY
                  (xxx((Decide p < 0 THENA Auto) THEN ThinTrivial THEN Auto')xxx
                   THEN (Decide a < 0 THENA Auto)
                   THEN ThinTrivial
                   THEN Auto'))
      THEN (Assert ⌜(q = (-b) ∈ ℤ) ⇒ (b = 0 ∈ ℤ)⌝ BY
                  (xxx((Decide q < 0 THENA Auto) THEN ThinTrivial THEN Auto')xxx
                   THEN (Decide b < 0 THENA Auto)
                   THEN ThinTrivial
                   THEN Auto')))xxx }

1
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 ∈ ℤ)

---

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  \msim{}  a)  \mwedge{}  (q  \msim{}  b)
\mvdash{}  (\{(p  =  a)  \mwedge{}  (q  =  b)\})  supposing  ((q  <  0  \mLeftarrow{}{}\mRightarrow{}  b  <  0)  and  (p  <  0  \mLeftarrow{}{}\mRightarrow{}  a  <  0))


By

---

Latex:
xxx((RWO  "assoced\_elim"  (-1))
        THEN  Auto
        THEN  Unfold  `guard`  0
        THEN  (Assert  \mkleeneopen{}(p  =  (-a))  {}\mRightarrow{}  (a  =  0)\mkleeneclose{}  BY
                                (xxx((Decide  p  <  0  THENA  Auto)  THEN  ThinTrivial  THEN  Auto')xxx
                                  THEN  (Decide  a  <  0  THENA  Auto)
                                  THEN  ThinTrivial
                                  THEN  Auto'))
        THEN  (Assert  \mkleeneopen{}(q  =  (-b))  {}\mRightarrow{}  (b  =  0)\mkleeneclose{}  BY
                                (xxx((Decide  q  <  0  THENA  Auto)  THEN  ThinTrivial  THEN  Auto')xxx
                                  THEN  (Decide  b  <  0  THENA  Auto)
                                  THEN  ThinTrivial
                                  THEN  Auto')))xxx

---

Home Index