---

Step * of Lemma chrem_exists_aux_a

∀r:ℕ+. ∀s:{s':ℕ+| CoPrime(r,s')} .  (∃x:ℤ [((x ≡ 1 mod r) ∧ (x ≡ 0 mod s))])
BY
{ Auto }

1
1. r : ℕ+
2. s : {s':ℕ+| CoPrime(r,s')} 
⊢ ∃x:ℤ [((x ≡ 1 mod r) ∧ (x ≡ 0 mod s))]

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index