---

Step * 2 1 2 2 1 of Lemma int-prod-split


1. n : ℤ
2. 0 < n
3. ∀[f:ℕn - 1 ⟶ ℤ]. ∀[m:ℕ(n - 1) + 1].  (Π(f[x] | x < n - 1) = (Π(f[x] | x < m) * Π(f[x + m] | x < n - 1 - m)) ∈ ℤ)
4. f : ℕn ⟶ ℤ
5. m : ℕn + 1
6. ¬n - m < 1
7. ¬(m = (n - 1) ∈ ℤ)
8. ¬(m = n ∈ ℤ)
⊢ (Π(f[x] | x < n - 1) * f[n - 1]) = (Π(f[x] | x < m) * Π(f[x + m] | x < n - m - 1) * f[(n - m - 1) + m]) ∈ ℤ
BY
{ ((InstHyp [⌜f⌝;⌜m⌝] 3⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN Thin (-1) THEN Thin (-3)) }

1
1. n : ℤ
2. 0 < n
3. ∀[f:ℕn - 1 ⟶ ℤ]. ∀[m:ℕ(n - 1) + 1].  (Π(f[x] | x < n - 1) = (Π(f[x] | x < m) * Π(f[x + m] | x < n - 1 - m)) ∈ ℤ)
4. f : ℕn ⟶ ℤ
5. m : ℕn + 1
6. ¬(m = (n - 1) ∈ ℤ)
7. ¬(m = n ∈ ℤ)
⊢ ((Π(f[x] | x < m) * Π(f[x + m] | x < n - 1 - m)) * f[n - 1])
= (Π(f[x] | x < m) * Π(f[x + m] | x < n - m - 1) * f[(n - m - 1) + m])
∈ ℤ

---

Latex:

---

Latex:

1.  n  :  \mBbbZ{}
2.  0  <  n
3.  \mforall{}[f:\mBbbN{}n  -  1  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[m:\mBbbN{}(n  -  1)  +  1].
          (\mPi{}(f[x]  |  x  <  n  -  1)  =  (\mPi{}(f[x]  |  x  <  m)  *  \mPi{}(f[x  +  m]  |  x  <  n  -  1  -  m)))
4.  f  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}
5.  m  :  \mBbbN{}n  +  1
6.  \mneg{}n  -  m  <  1
7.  \mneg{}(m  =  (n  -  1))
8.  \mneg{}(m  =  n)
\mvdash{}  (\mPi{}(f[x]  |  x  <  n  -  1)  *  f[n  -  1])
=  (\mPi{}(f[x]  |  x  <  m)  *  \mPi{}(f[x  +  m]  |  x  <  n  -  m  -  1)  *  f[(n  -  m  -  1)  +  m])


By

---

Latex:
((InstHyp  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]  3\mcdot{}  THENA  Auto)  THEN  HypSubst'  (-1)  0  THEN  Thin  (-1)  THEN  Thin  (-3))

---

Home Index