---

Step * 1 of Lemma int-prod-split


1. n : ℤ
2. f : ℕ0 ⟶ ℤ
3. m : ℕ1
⊢ 1 = (Π(f[x] | x < m) * Π(f[x + m] | x < 0 - m)) ∈ ℤ
BY
{ ((IntSegCases (-1) THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((IntSegCases  (-1)  THEN  Reduce  0)  THEN  Auto)

---

Home Index