---

Step * of Lemma chrem_wf

No Annotations
∀r,s,a,b:ℤ.  (chrem(a;r;b;s) ∈ {x:ℤ| (x ≡ a mod r) ∧ (x ≡ b mod s)}  + (¬(∃x:ℤ [((x ≡ a mod r) ∧ (x ≡ b mod s))])))
BY
{ (Intros
   THEN (Subst' chrem(a;r;b;s) ~ TERMOF{chinese-remainder2-extract:o, 1:l} r s a b 0 THENA Computation)
   THEN DoSubsume
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}r,s,a,b:\mBbbZ{}.
    (chrem(a;r;b;s)
      \mmember{}  \{x:\mBbbZ{}|  (x  \mequiv{}  a  mod  r)  \mwedge{}  (x  \mequiv{}  b  mod  s)\}    +  (\mneg{}(\mexists{}x:\mBbbZ{}  [((x  \mequiv{}  a  mod  r)  \mwedge{}  (x  \mequiv{}  b  mod  s))])))


By

---

Latex:
(Intros
  THEN  (Subst'  chrem(a;r;b;s)  \msim{}  TERMOF\{chinese-remainder2-extract:o,  1:l\}  r  s  a  b  0
              THENA  Computation
              )
  THEN  DoSubsume
  THEN  Auto)

---

Home Index