---

Step * of Lemma int-eq-constraint-factor

∀[a:ℤ]. ∀[g:ℤ-o]. ∀[xs,L:ℤ List].
  uiff([1 / xs] ⋅ [a / g * L] = 0 ∈ ℤ;((a rem g) = 0 ∈ ℤ) ∧ ([1 / xs] ⋅ [a ÷ g / L] = 0 ∈ ℤ))
BY
{ (Auto THEN All Reduce) }

1
1. a : ℤ
2. g : ℤ-o
3. xs : ℤ List
4. L : ℤ List
5. ((1 * a) + xs ⋅ g * L) = 0 ∈ ℤ
⊢ (a rem g) = 0 ∈ ℤ

2
1. a : ℤ
2. g : ℤ-o
3. xs : ℤ List
4. L : ℤ List
5. ((1 * a) + xs ⋅ g * L) = 0 ∈ ℤ
⊢ ((1 * (a ÷ g)) + xs ⋅ L) = 0 ∈ ℤ

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  All  Reduce)

---

Home Index