---

Step * of Lemma chrem_exists_a

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index