Nuprl Lemma : 2-is-sum-of-three-cubes

According to wikipedia, as of 2018 these are the only
known ways of writing 2 as the sum of three cubes .⋅
(∀x:ℤ
   let a = 1 + (6 * x * x * x) in
    let b = 1 - 6 * x * x * x in
    let c = -(6 * x * x) in
    ((a * a * a) + (b * b * b) + (c * c * c)) = 2 ∈ ℤ)
∧ let a = 1214928 in
   let b = 3480205 in
   let c = -3528875 in
   ((a * a * a) + (b * b * b) + (c * c * c)) = 2 ∈ ℤ


Proof



Definitions occuring in Statement :  let: let,  all: ∀x:A. B[x],  and: P ∧ Q,  multiply: n * m,  subtract: n - m,  add: n + m,  minus: -n,  natural_number: $n,  int: ℤ,  equal: s = t ∈ T
Definitions unfolded in proof :  let: let,  and: P ∧ Q,  cand: A c∧ B,  all: ∀x:A. B[x],  uall: ∀[x:A]. B[x],  member: t ∈ T,  top: Top,  subtract: n - m
Lemmas referenced :  mul-distributes-right,  istype-void,  mul-distributes,  mul-associates,  add-associates,  minus-one-mul,  mul-commutes,  mul-swap,  minus-one-mul-top,  add-swap,  add-commutes,  zero-mul,  zero-add,  add-zero,  istype-int
Rules used in proof :  sqequalSubstitution,  sqequalRule,  sqequalReflexivity,  sqequalTransitivity,  computationStep,  cut,  Error :lambdaFormation_alt,  introduction,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  thin,  multiplyEquality,  addEquality,  natural_numberEquality,  hypothesisEquality,  Error :isect_memberEquality_alt,  voidElimination,  hypothesis,  minusEquality,  independent_pairFormation
Latex:
(\mforall{}x:\mBbbZ{}
      let  a  =  1  +  (6  *  x  *  x  *  x)  in
        let  b  =  1  -  6  *  x  *  x  *  x  in
        let  c  =  -(6  *  x  *  x)  in
        ((a  *  a  *  a)  +  (b  *  b  *  b)  +  (c  *  c  *  c))  =  2)
\mwedge{}  let  a  =  1214928  in
      let  b  =  3480205  in
      let  c  =  -3528875  in
      ((a  *  a  *  a)  +  (b  *  b  *  b)  +  (c  *  c  *  c))  =  2


Date html generated: 2019_06_20-PM-02_43_00
Last ObjectModification: 2019_03_16-AM-11_04_23

Theory : num_thy_1


Home Index