---

Step * of Lemma chinese-remainder1

No Annotations
∀r:ℤ. ∀s:{s':ℤ| CoPrime(r,s')} . ∀a,b:ℤ.  (∃x:ℤ [((x ≡ a mod r) ∧ (x ≡ b mod s))])
BY
{ (Auto THEN (InstLemma `gcd-reduce` [⌜r⌝;⌜s⌝]⋅ THENA Auto) THEN ExRepD) }

1
1. r : ℤ
2. s : {s':ℤ| CoPrime(r,s')} 
3. a : ℤ
4. b : ℤ
5. g : ℕ
6. a1 : ℤ
7. b1 : ℤ
8. x : ℤ
9. y : ℤ
10. r = (a1 * g) ∈ ℤ
11. s = (b1 * g) ∈ ℤ
12. ((x * a1) + (y * b1)) = 1 ∈ ℤ
⊢ ∃x:ℤ [((x ≡ a mod r) ∧ (x ≡ b mod s))]

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (InstLemma  `gcd-reduce`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}s\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index