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