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