Step
*
of Lemma
residue-mul-assoc
∀[n:ℕ+]. ∀[a,b,c:{i:ℤ| CoPrime(n,i)} ]. (((ab mod n)c mod n) = (a(bc mod n) mod n) ∈ ℤ)
BY
{ (Auto THEN RepUR ``residue-mul`` 0 THEN BLemma `modulus-equal-iff-eqmod` THEN Auto) }
1
1. n : ℕ+
2. a : {i:ℤ| CoPrime(n,i)}
3. b : {i:ℤ| CoPrime(n,i)}
4. c : {i:ℤ| CoPrime(n,i)}
⊢ (((a * b) mod n) * c) ≡ (a * ((b * c) mod n)) mod n
Latex:
Latex:
\mforall{}[n:\mBbbN{}\msupplus{}]. \mforall{}[a,b,c:\{i:\mBbbZ{}| CoPrime(n,i)\} ]. (((ab mod n)c mod n) = (a(bc mod n) mod n))
By
Latex:
(Auto THEN RepUR ``residue-mul`` 0 THEN BLemma `modulus-equal-iff-eqmod` THEN Auto)
Home
Index