Nuprl Lemma : sum-consecutive-cubes

[n:ℕ]. ((i i) i < n) ((((n 1) (n 1)) n) ÷ 4) ∈ ℤ)


Proof




Definitions occuring in Statement :  sum: Σ(f[x] x < k) nat: uall: [x:A]. B[x] divide: n ÷ m multiply: m subtract: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sq_type: SQType(T) all: x:A. B[x] implies:  Q guard: {T} squash: T prop: so_lambda: λ2x.t[x] int_seg: {i..j-} nat: so_apply: x[s] int_nzero: -o true: True nequal: a ≠ b ∈  not: ¬A false: False subtype_rel: A ⊆B iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q
Lemmas referenced :  sum-of-consecutive-cubes subtype_base_sq int_subtype_base equal_wf squash_wf true_wf sum_wf int_seg_wf divide-exact equal-wf-base nequal_wf iff_weakening_equal nat_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality instantiate cumulativity intEquality independent_isectElimination dependent_functionElimination equalityTransitivity equalitySymmetry independent_functionElimination applyEquality lambdaEquality imageElimination universeEquality sqequalRule multiplyEquality setElimination rename because_Cache natural_numberEquality dependent_set_memberEquality addLevel lambdaFormation voidElimination baseClosed imageMemberEquality productElimination

Latex:
\mforall{}[n:\mBbbN{}].  (\mSigma{}((i  *  i)  *  i  |  i  <  n)  =  ((((n  -  1)  *  (n  -  1))  *  n  *  n)  \mdiv{}  4))



Date html generated: 2017_04_14-AM-09_21_43
Last ObjectModification: 2017_02_27-PM-03_57_17

Theory : int_2


Home Index