Step
*
2
1
of Lemma
divisibility-by-5-rule
1. v : ℤ
2. v1 : ℤ
⊢ (v ≡ 0 mod 5
⇐⇒ v1 ≡ 0 mod 5)
⇒ (5 | v
⇐⇒ 5 | v1)
BY
{ xxx(RepUR ``eqmod`` 0 THEN RW IntNormC 0 THEN Auto)xxx }
Latex:
Latex:
1. v : \mBbbZ{}
2. v1 : \mBbbZ{}
\mvdash{} (v \mequiv{} 0 mod 5 \mLeftarrow{}{}\mRightarrow{} v1 \mequiv{} 0 mod 5) {}\mRightarrow{} (5 | v \mLeftarrow{}{}\mRightarrow{} 5 | v1)
By
Latex:
xxx(RepUR ``eqmod`` 0 THEN RW IntNormC 0 THEN Auto)xxx
Home
Index