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