---

Step * of Lemma coprime-equiv-unique-pair

∀[p:ℤ]. ∀[q:ℤ-o]. ∀[a,b:ℤ].
  (<p, q> = <a, b> ∈ (ℤ × ℤ-o)) supposing 
     ((q < 0 ⇐⇒ b < 0) and 
     (p < 0 ⇐⇒ a < 0) and 
     ((p * b) = (a * q) ∈ ℤ) and 
     CoPrime(a,b) and 
     CoPrime(p,q))
BY
{ (Auto THEN (Assert (p = a ∈ ℤ) ∧ (q = b ∈ ℤ) BY (BLemma `coprime-equiv-unique` THEN Auto)) THEN EqCD THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:\mBbbZ{}].  \mforall{}[q:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[a,b:\mBbbZ{}].
    (<p,  q>  =  <a,  b>)  supposing 
          ((q  <  0  \mLeftarrow{}{}\mRightarrow{}  b  <  0)  and 
          (p  <  0  \mLeftarrow{}{}\mRightarrow{}  a  <  0)  and 
          ((p  *  b)  =  (a  *  q))  and 
          CoPrime(a,b)  and 
          CoPrime(p,q))


By

---

Latex:
(Auto
  THEN  (Assert  (p  =  a)  \mwedge{}  (q  =  b)  BY
                          (BLemma  `coprime-equiv-unique`  THEN  Auto))
  THEN  EqCD
  THEN  Auto)

---

Home Index