### Nuprl Lemma : sum-consecutive-squares

`∀[n:ℕ]. (Σ(i * i | i < n) = (((n - 1) * n * ((2 * n) - 1)) ÷ 6) ∈ ℤ)`

Proof

Definitions occuring in Statement :  sum: `Σ(f[x] | x < k)` nat: `ℕ` uall: `∀[x:A]. B[x]` divide: `n ÷ m` multiply: `n * m` subtract: `n - m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` sq_type: `SQType(T)` all: `∀x:A. B[x]` implies: `P `` 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 ∈ T ` not: `¬A` false: `False` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q`
Lemmas referenced :  sum-of-consecutive-squares 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  <  n)  =  (((n  -  1)  *  n  *  ((2  *  n)  -  1))  \mdiv{}  6))

Date html generated: 2017_04_14-AM-09_21_34
Last ObjectModification: 2017_02_27-PM-03_57_20

Theory : int_2

Home Index