---

Step * 1 of Lemma coprime_functionality_wrt_eqmod2


1. a : ℤ@i
2. a' : ℤ@i
3. m : ℤ@i
4. a' ≡ a mod m@i
⊢ CoPrime(a',m) ⇐⇒ CoPrime(a,m)
BY
{ (InstLemma `coprime_functionality_wrt_eqmod` [⌜a⌝;⌜a'⌝;⌜m⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  a'  :  \mBbbZ{}@i
3.  m  :  \mBbbZ{}@i
4.  a'  \mequiv{}  a  mod  m@i
\mvdash{}  CoPrime(a',m)  \mLeftarrow{}{}\mRightarrow{}  CoPrime(a,m)


By

---

Latex:
(InstLemma  `coprime\_functionality\_wrt\_eqmod`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index