Step * of Lemma chrem_exists

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

1
1. : ℕ+
2. : ℕ+
3. CoPrime(r,s)
4. : ℤ
5. : ℤ
⊢ ∃x:ℤ((x ≡ mod r) ∧ (x ≡ 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