---

Step * of Lemma int-eq-constraint-factor-sym

∀[a:ℤ]. ∀[g:ℤ-o]. ∀[xs,L:ℤ List].
  uiff([a / g * L] ⋅ [1 / xs] = 0 ∈ ℤ;((a rem g) = 0 ∈ ℤ) ∧ ([a ÷ g / L] ⋅ [1 / xs] = 0 ∈ ℤ))
BY
{ (InstLemma  `int-eq-constraint-factor` [] THEN RepeatFor 6 (ParallelLast')) }

1
1. a : ℤ
2. g : ℤ-o
3. xs : ℤ List
4. L : ℤ List
5. [a / g * L] ⋅ [1 / xs] = 0 ∈ ℤ
6. (a rem g) = 0 ∈ ℤ
7. [1 / xs] ⋅ [a ÷ g / L] = 0 ∈ ℤ
⊢ [a ÷ g / L] ⋅ [1 / xs] = 0 ∈ ℤ

2
1. a : ℤ
2. g : ℤ-o
3. xs : ℤ List
4. L : ℤ List
5. (a rem g) = 0 ∈ ℤ
6. [a ÷ g / L] ⋅ [1 / xs] = 0 ∈ ℤ
⊢ [1 / xs] ⋅ [a ÷ g / L] = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[a:\mBbbZ{}].  \mforall{}[g:\mBbbZ{}\msupminus{}\msupzero{}].  \mforall{}[xs,L:\mBbbZ{}  List].
    uiff([a  /  g  *  L]  \mcdot{}  [1  /  xs]  =  0;((a  rem  g)  =  0)  \mwedge{}  ([a  \mdiv{}  g  /  L]  \mcdot{}  [1  /  xs]  =  0))


By

---

Latex:
(InstLemma    `int-eq-constraint-factor`  []  THEN  RepeatFor  6  (ParallelLast'))

---

Home Index