---

Step * of Lemma coprime-equiv-unique

∀[p,q,a,b:ℤ].
  ({(p = a ∈ ℤ) ∧ (q = b ∈ ℤ)}) supposing 
     ((q < 0 ⇐⇒ b < 0) and 
     (p < 0 ⇐⇒ a < 0) and 
     ((p * b) = (a * q) ∈ ℤ) and 
     CoPrime(a,b) and 
     CoPrime(p,q))
BY
{ xxxRepeatFor 7 ((D 0 THENA Auto))xxx }

1
1. p : ℤ
2. q : ℤ
3. a : ℤ
4. b : ℤ
5. CoPrime(p,q)
6. CoPrime(a,b)
7. (p * b) = (a * q) ∈ ℤ
⊢ ({(p = a ∈ ℤ) ∧ (q = b ∈ ℤ)}) supposing ((q < 0 ⇐⇒ b < 0) and (p < 0 ⇐⇒ a < 0))

---

Latex:

---

Latex:
\mforall{}[p,q,a,b:\mBbbZ{}].
    (\{(p  =  a)  \mwedge{}  (q  =  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:
xxxRepeatFor  7  ((D  0  THENA  Auto))xxx

---

Home Index