---

Step * 1 1 1 1 of Lemma chrem_exists_aux_a


1. r : ℕ+
2. s : ℕ+
3. CoPrime(r,s)
4. x : ℤ
5. y : ℤ
6. ((r * x) + (s * y)) = 1 ∈ ℤ
⊢ ((s * y) ≡ 1 mod r) ∧ ((s * y) ≡ 0 mod s)
BY
{ (RevHypSubst 6 0 THENA Auto) }

1
1. r : ℕ+
2. s : ℕ+
3. CoPrime(r,s)
4. x : ℤ
5. y : ℤ
6. ((r * x) + (s * y)) = 1 ∈ ℤ
⊢ ((s * y) ≡ ((r * x) + (s * y)) mod r) ∧ ((s * y) ≡ 0 mod s)

---

Latex:

---

Latex:

1.  r  :  \mBbbN{}\msupplus{}
2.  s  :  \mBbbN{}\msupplus{}
3.  CoPrime(r,s)
4.  x  :  \mBbbZ{}
5.  y  :  \mBbbZ{}
6.  ((r  *  x)  +  (s  *  y))  =  1
\mvdash{}  ((s  *  y)  \mequiv{}  1  mod  r)  \mwedge{}  ((s  *  y)  \mequiv{}  0  mod  s)


By

---

Latex:
(RevHypSubst  6  0  THENA  Auto)

---

Home Index