Nuprl Lemma : lcm-assoc-nat
∀[n,m,k:ℕ]. (lcm(n;lcm(m;k)) = lcm(lcm(n;m);k) ∈ ℤ)
Proof
Definitions occuring in Statement :
lcm: lcm(a;b),
nat: ℕ,
uall: ∀[x:A]. B[x],
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
cand: A c∧ B,
prop: ℙ,
nat: ℕ
Lemmas referenced :
nat_wf,
lcm-unique-nat,
lcm_wf_nat,
divides_wf,
lcm_wf,
lcm-is-lcm-nat,
divides_transitivity
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
hypothesis,
lemma_by_obid,
sqequalRule,
sqequalHypSubstitution,
isect_memberEquality,
isectElimination,
thin,
hypothesisEquality,
axiomEquality,
because_Cache,
dependent_functionElimination,
independent_functionElimination,
independent_pairFormation,
productElimination,
lambdaFormation,
setElimination,
rename,
intEquality
Latex:
\mforall{}[n,m,k:\mBbbN{}]. (lcm(n;lcm(m;k)) = lcm(lcm(n;m);k))
Date html generated:
2016_05_14-PM-09_25_40
Last ObjectModification:
2015_12_26-PM-08_03_00
Theory : num_thy_1
Home
Index