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