Step * of Lemma chrem_exists

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

1
1. r : ℕ+
2. s : ℕ+
3. CoPrime(r,s)
4. a : ℤ
5. b : ℤ
⊢ ∃x:ℤ. ((x ≡ a mod r) ∧ (x ≡ b mod s))


Latex:


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


By


Latex:
Auto




Home Index