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

This solution to the problem of writing 33 as the sum of three cubes
was found around March 9, 2019 by Andrew Booker using 15 core-years
computation time (over three weeks real time) on a super-computer in Bristol.

The smallest number for which it is unknown whether it is the sum of three
cubes is now 42 (and the next is 114).⋅

∀k:ℕ
  (∃a,b,c:ℤ. (((a * a * a) + (b * b * b) + (c * c * c)) = k ∈ ℤ)
  ⇐⇒ ∃c:ℤ
       (((c * c * c) = k ∈ ℤ)
       ∨ (∃d:ℕ
           ((¬(d = 0 ∈ ℤ))
           ∧ ((k - c * c * c rem d) = 0 ∈ ℤ)

           ∧ (∃n:ℕ. (((4 * ((k - c * c * c) ÷ d)) - d * d) = (3 * n * n) ∈ ℤ))))))

Proof

Definitions occuring in Statement : nat: ℕ, all: ∀x:A. B[x], exists: ∃x:A. B[x], iff: P ⇐⇒ Q, not: ¬A, or: P ∨ Q, and: P ∧ Q, remainder: n rem m, divide: n ÷ m, multiply: n * m, subtract: n - m, add: n + m, natural_number: $n, int: ℤ, equal: s = t ∈ T
Definitions unfolded in proof : all: ∀x:A. B[x], iff: P ⇐⇒ Q, and: P ∧ Q, implies: P ⇒ Q, exists: ∃x:A. B[x], member: t ∈ T, subtype_rel: A ⊆r B, nat: ℕ, uall: ∀[x:A]. B[x], so_lambda: λ₂x.t[x], so_apply: x[s], uimplies: b supposing a, rev_implies: P ⇐ Q, or: P ∨ Q, not: ¬A, false: False, decidable: Dec(P), cand: A c∧ B, ge: i ≥ j , satisfiable_int_formula: satisfiable_int_formula(fmla), top: Top, prop: ℙ, gt: i > j, nat_plus: ℕ⁺, subtract: n - m, squash: ↓T, true: True, guard: {T}, int_nzero: ℤ^-^o, nequal: a ≠ b ∈ T
Lemmas referenced : istype-int, int_subtype_base, set_subtype_base, le_wf, istype-void, istype-nat, decidable__le, nat_properties, full-omega-unsat, intformand_wf, intformnot_wf, intformle_wf, itermConstant_wf, itermAdd_wf, itermVar_wf, int_formula_prop_and_lemma, int_formula_prop_not_lemma, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_add_lemma, int_term_value_var_lemma, int_formula_prop_wf, decidable__equal_int, intformeq_wf, itermMultiply_wf, int_formula_prop_eq_lemma, int_term_value_mul_lemma, istype-le, decidable__lt, intformless_wf, int_formula_prop_less_lemma, neg_mul_arg_bounds, pos_mul_arg_bounds, gt_wf, itermMinus_wf, int_term_value_minus_lemma, exp_preserves_lt, istype-less_than, less_than_wf, squash_wf, true_wf, exp2, subtype_rel_self, iff_weakening_equal, exp_step, sum-of-three-cubes-iff-1, three-cubes-lemma, divide_wfa, subtract_wf, nequal_wf, itermSubtract_wf, int_term_value_subtract_lemma
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, Error :lambdaFormation_alt, independent_pairFormation, sqequalRule, Error :productIsType, cut, introduction, extract_by_obid, hypothesis, because_Cache, Error :equalityIstype, baseApply, closedConclusion, baseClosed, hypothesisEquality, applyEquality, sqequalHypSubstitution, isectElimination, thin, intEquality, Error :lambdaEquality_alt, natural_numberEquality, Error :inhabitedIsType, independent_isectElimination, sqequalBase, equalitySymmetry, Error :unionIsType, Error :functionIsType, equalityTransitivity, productElimination, dependent_functionElimination, addEquality, unionElimination, Error :dependent_pairFormation_alt, setElimination, rename, approximateComputation, independent_functionElimination, int_eqEquality, Error :isect_memberEquality_alt, voidElimination, Error :universeIsType, multiplyEquality, Error :inlFormation_alt, Error :inrFormation_alt, minusEquality, Error :dependent_set_memberEquality_alt, imageElimination, imageMemberEquality, instantiate, universeEquality

Latex:
\mforall{}k:\mBbbN{} (\mexists{}a,b,c:\mBbbZ{}. (((a * a * a) + (b * b * b) + (c * c * c)) = k) \mLeftarrow{}{}\mRightarrow{} \mexists{}c:\mBbbZ{} (((c * c * c) = k) \mvee{} (\mexists{}d:\mBbbN{} ((\mneg{}(d = 0)) \mwedge{} ((k - c * c * c rem d) = 0) \mwedge{} (\mexists{}n:\mBbbN{}. (((4 * ((k - c * c * c) \mdiv{} d)) - d * d) = (3 * n * n))))))) Date html generated: 2019_06_20-PM-02_42_17 Last ObjectModification: 2019_03_16-PM-01_00_54 Theory : num_thy_1 Home Index