---

Step * 1 2 1 of Lemma chrem_exists


1. r : ℕ+
2. s : ℕ+
3. CoPrime(r,s)
4. a : ℤ
5. b : ℤ
6. p : ℤ
7. p ≡ 1 mod r
8. p ≡ 0 mod s
9. q : ℤ
10. q ≡ 1 mod s
11. q ≡ 0 mod r
⊢ ((a * p) + (b * q)) ≡ a mod r
BY
{ (((RWWHyps [7;11] 0 THENM RW IntNormC 0) THEN Auto) THEN RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  \mBbbN{}\msupplus{}
2.  s  :  \mBbbN{}\msupplus{}
3.  CoPrime(r,s)
4.  a  :  \mBbbZ{}
5.  b  :  \mBbbZ{}
6.  p  :  \mBbbZ{}
7.  p  \mequiv{}  1  mod  r
8.  p  \mequiv{}  0  mod  s
9.  q  :  \mBbbZ{}
10.  q  \mequiv{}  1  mod  s
11.  q  \mequiv{}  0  mod  r
\mvdash{}  ((a  *  p)  +  (b  *  q))  \mequiv{}  a  mod  r


By

---

Latex:
(((RWWHyps  [7;11]  0  THENM  RW  IntNormC  0)  THEN  Auto)  THEN  RelRST  THEN  Auto)

---

Home Index