---

Step * 1 1 of Lemma residue-mul-assoc


1. n : ℕ+
2. a : {i:ℤ| CoPrime(n,i)} 
3. b : {i:ℤ| CoPrime(n,i)} 
4. c : {i:ℤ| CoPrime(n,i)} 
5. (a mod n) ≡ a mod n
6. (b mod n) ≡ b mod n
7. (c mod n) ≡ c mod n
⊢ (((a * b) mod n) * c) ≡ (a * ((b * c) mod n)) mod n
BY
{ ((Assert ((a * b) mod n) ≡ ((a mod n) * (b mod n)) mod n BY
          ((RWO "5 6 7" 0 THENA Auto) THEN BLemma `mod-eqmod` THEN Auto))
   THEN (Assert ((b * c) mod n) ≡ ((b mod n) * (c mod n)) mod n BY
               ((RWO "5 6 7" 0 THENA Auto) THEN BLemma `mod-eqmod` THEN Auto))
   ) }

1
1. n : ℕ+
2. a : {i:ℤ| CoPrime(n,i)} 
3. b : {i:ℤ| CoPrime(n,i)} 
4. c : {i:ℤ| CoPrime(n,i)} 
5. (a mod n) ≡ a mod n
6. (b mod n) ≡ b mod n
7. (c mod n) ≡ c mod n
8. ((a * b) mod n) ≡ ((a mod n) * (b mod n)) mod n
9. ((b * c) mod n) ≡ ((b mod n) * (c mod n)) mod n
⊢ (((a * b) mod n) * c) ≡ (a * ((b * c) mod n)) mod n

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  a  :  \{i:\mBbbZ{}|  CoPrime(n,i)\} 
3.  b  :  \{i:\mBbbZ{}|  CoPrime(n,i)\} 
4.  c  :  \{i:\mBbbZ{}|  CoPrime(n,i)\} 
5.  (a  mod  n)  \mequiv{}  a  mod  n
6.  (b  mod  n)  \mequiv{}  b  mod  n
7.  (c  mod  n)  \mequiv{}  c  mod  n
\mvdash{}  (((a  *  b)  mod  n)  *  c)  \mequiv{}  (a  *  ((b  *  c)  mod  n))  mod  n


By

---

Latex:
((Assert  ((a  *  b)  mod  n)  \mequiv{}  ((a  mod  n)  *  (b  mod  n))  mod  n  BY
                ((RWO  "5  6  7"  0  THENA  Auto)  THEN  BLemma  `mod-eqmod`  THEN  Auto))
  THEN  (Assert  ((b  *  c)  mod  n)  \mequiv{}  ((b  mod  n)  *  (c  mod  n))  mod  n  BY
                          ((RWO  "5  6  7"  0  THENA  Auto)  THEN  BLemma  `mod-eqmod`  THEN  Auto))
  )

---

Home Index