---

Step * of Lemma chrem_exists_aux

∀r,s:ℕ+.  (CoPrime(r,s) ⇒ (∃x:ℤ. ((x ≡ 1 mod r) ∧ (x ≡ 0 mod s))))
BY
{ (Unfold `eqmod` 0 THEN Auto) }

1
1. r : ℕ+
2. s : ℕ+
3. CoPrime(r,s)
⊢ ∃x:ℤ. ((r | (x - 1)) ∧ (s | (x - 0)))

---

Latex:

---

Latex:
\mforall{}r,s:\mBbbN{}\msupplus{}.    (CoPrime(r,s)  {}\mRightarrow{}  (\mexists{}x:\mBbbZ{}.  ((x  \mequiv{}  1  mod  r)  \mwedge{}  (x  \mequiv{}  0  mod  s))))


By

---

Latex:
(Unfold  `eqmod`  0  THEN  Auto)

---

Home Index