---

Step * of Lemma coprime_functionality_wrt_eqmod2

∀a,a',m:ℤ.  ((a' ≡ a mod m) ⇒ (CoPrime(m,a') ⇐⇒ CoPrime(m,a)))
BY
{ ((UnivCD THENA Auto) THEN (RWO "coprime_inversion" 0 THENA Auto)) }

1
1. a : ℤ@i
2. a' : ℤ@i
3. m : ℤ@i
4. a' ≡ a mod m@i
⊢ CoPrime(a',m) ⇐⇒ CoPrime(a,m)

---

Latex:

---

Latex:
\mforall{}a,a',m:\mBbbZ{}.    ((a'  \mequiv{}  a  mod  m)  {}\mRightarrow{}  (CoPrime(m,a')  \mLeftarrow{}{}\mRightarrow{}  CoPrime(m,a)))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "coprime\_inversion"  0  THENA  Auto))

---

Home Index