Step 
*
 of Lemma 
coprime_symmetry
∀a,b:ℤ.  (CoPrime(a,b) ⇒ CoPrime(b,a))
BY
 
{ (Unfold `coprime` 0 THEN Auto) }
1
1. a : ℤ
2. b : ℤ
3. GCD(a;b;1)
⊢ GCD(b;a;1)
 
Latex: 
Latex:
\mforall{}a,b:\mBbbZ{}.    (CoPrime(a,b)  {}\mRightarrow{}  CoPrime(b,a))
 By 
Latex:
(Unfold  `coprime`  0  THEN  Auto)
Home
Index