### Nuprl Lemma : int-prod-split2

`∀[n:ℕ]. ∀[m:ℕn + 1]. ∀[f:ℕn ⟶ ℤ].  (Π(f[x] | x < n) = (Π(f[x] | x < m) * Π(f[x + m] | x < n - m)) ∈ ℤ)`

Proof

Definitions occuring in Statement :  int-prod: `Π(f[x] | x < k)` int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` multiply: `n * m` subtract: `n - m` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  nat: `ℕ` so_apply: `x[s]` so_lambda: `λ2x.t[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  nat_wf int_seg_wf int-prod-split
Rules used in proof :  addEquality because_Cache axiomEquality isect_memberEquality intEquality functionEquality hypothesis rename setElimination natural_numberEquality functionExtensionality applyEquality lambdaEquality sqequalRule hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

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

Date html generated: 2018_05_21-PM-00_29_14
Last ObjectModification: 2017_12_10-PM-01_45_16

Theory : int_2

Home Index