---

Step * of Lemma int_pi_det_fun_wf

∀[i:ℤ]. ((i)ℤ-det-fun ∈ detach_fun(|ℤ-rng|;(i)ℤ-rng))
BY
{ (Auto
   THEN RepUR ``int_pi_det_fun detach_fun princ_ideal`` 0
   THEN MemTypeCD
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN AutoSplit) }

1
1. i : ℤ
2. i = 0 ∈ ℤ
⊢ ∀x@0:ℤ. (∃b:ℤ. (x@0 = (i * b) ∈ ℤ) ⇐⇒ ↑(x@0 =z 0))

2
1. i : ℤ
2. i ≠ 0
⊢ ∀x:ℤ. (∃b:ℤ. (x = (i * b) ∈ ℤ) ⇐⇒ ↑(x rem i =z 0))

---

Latex:

---

Latex:
\mforall{}[i:\mBbbZ{}].  ((i)\mBbbZ{}-det-fun  \mmember{}  detach\_fun(|\mBbbZ{}-rng|;(i)\mBbbZ{}-rng))


By

---

Latex:
(Auto
  THEN  RepUR  ``int\_pi\_det\_fun  detach\_fun  princ\_ideal``  0
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  AutoSplit)

---

Home Index