---

Step * of Lemma int-prod-isolate

∀[n:ℕ]. ∀[m:ℕn]. ∀[f:ℕn ⟶ ℤ].  (Π(f[x] | x < n) = (Π(if (x =z m) then 1 else f[x] fi  | x < n) * f[m]) ∈ ℤ)
BY
{ (Auto
   THEN ((InstLemma `int-prod-split` [⌜n⌝;⌜f⌝;⌜m⌝]⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN Thin (-1))
   THEN (InstLemma `int-prod-split` [⌜n⌝;⌜λ2x.if (x =z m) then 1 else f[x] fi ⌝;⌜m⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Thin (-1)
   THEN ((InstLemma `int-prod-split` [⌜n - m⌝;⌜λ2x.f[x + m]⌝;⌜1⌝]⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN Thin (-1))
   THEN (InstLemma `int-prod-split` [⌜n - m⌝;⌜λ2x.if (x + m =z m) then 1 else f[x + m] fi ⌝;⌜1⌝]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Thin (-1)) }

1
1. n : ℕ
2. m : ℕn
3. f : ℕn ⟶ ℤ
⊢ (Π(f[x] | x < m) * Π(f[x + m] | x < 1) * Π(f[(x + 1) + m] | x < n - m - 1))
= ((Π(if (x =z m) then 1 else f[x] fi  | x < m)
  * Π(if (x + m =z m) then 1 else f[x + m] fi  | x < 1)
  * Π(if ((x + 1) + m =z m) then 1 else f[(x + 1) + m] fi  | x < n - m - 1))
  * f[m])
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[m:\mBbbN{}n].  \mforall{}[f:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].
    (\mPi{}(f[x]  |  x  <  n)  =  (\mPi{}(if  (x  =\msubz{}  m)  then  1  else  f[x]  fi    |  x  <  n)  *  f[m]))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `int-prod-split`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  HypSubst'  (-1)  0  THEN  Thin  (-1))
  THEN  (InstLemma  `int-prod-split`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.if  (x  =\msubz{}  m)  then  1  else  f[x]  fi  \mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Thin  (-1)
  THEN  ((InstLemma  `int-prod-split`  [\mkleeneopen{}n  -  m\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.f[x  +  m]\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  HypSubst'  (-1)  0
              THEN  Thin  (-1))
  THEN  (InstLemma  `int-prod-split`  [\mkleeneopen{}n  -  m\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.if  (x  +  m  =\msubz{}  m)  then  1  else  f[x  +  m]  fi  \mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  HypSubst'  (-1)  0
  THEN  Thin  (-1))

---

Home Index