Nuprl Lemma : three-cubes-lemma

∀d,e:ℤ.
  (∃a,b:ℤ. ((((a * a) + ((b * b) - a * b)) = e ∈ ℤ) ∧ ((a + b) = d ∈ ℤ))
  ⇐⇒ ∃n:ℕ. (((4 * e) - d * d) = (3 * n * n) ∈ ℤ))


Proof



Definitions occuring in Statement :  nat: ℕ,  all: ∀x:A. B[x],  exists: ∃x:A. B[x],  iff: P ⇐⇒ Q,  and: P ∧ Q,  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,  rev_implies: P ⇐ Q,  nat: ℕ,  uall: ∀[x:A]. B[x],  so_lambda: λ2x.t[x],  so_apply: x[s],  uimplies: b supposing a,  squash: ↓T,  prop: ℙ,  true: True,  guard: {T},  sq_type: SQType(T),  decidable: Dec(P),  or: P ∨ Q,  not: ¬A,  satisfiable_int_formula: satisfiable_int_formula(fmla),  false: False,  top: Top,  subtract: n - m,  ge: i ≥ j ,  cand: A c∧ B,  int_nzero: ℤ-o,  nequal: a ≠ b ∈ T 
Lemmas referenced :  int_subtype_base,  istype-nat,  set_subtype_base,  le_wf,  istype-int,  absval_wf,  subtract_wf,  equal_wf,  squash_wf,  true_wf,  istype-universe,  absval_squared,  subtype_rel_self,  iff_weakening_equal,  subtype_base_sq,  add-subtract-cancel,  decidable__equal_int,  full-omega-unsat,  intformnot_wf,  intformeq_wf,  itermVar_wf,  int_formula_prop_not_lemma,  istype-void,  int_formula_prop_eq_lemma,  int_term_value_var_lemma,  int_formula_prop_wf,  mul-distributes,  mul-distributes-right,  add-associates,  minus-add,  mul-associates,  minus-one-mul,  mul-swap,  mul-commutes,  add-swap,  add-commutes,  nat_properties,  intformand_wf,  itermAdd_wf,  itermMultiply_wf,  itermConstant_wf,  itermSubtract_wf,  int_formula_prop_and_lemma,  int_term_value_add_lemma,  int_term_value_mul_lemma,  int_term_value_constant_lemma,  int_term_value_subtract_lemma,  mod2-cases,  mod2-is-zero,  mod2-is-one,  add_functionality_wrt_eq,  minus-one-mul-top,  add-mul-special,  zero-mul,  add-zero,  mul_cancel_in_eq,  nequal_wf,  one-mul
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation_alt,  independent_pairFormation,  sqequalHypSubstitution,  productElimination,  thin,  sqequalRule,  productIsType,  because_Cache,  equalityIstype,  baseApply,  closedConclusion,  baseClosed,  cut,  hypothesisEquality,  applyEquality,  introduction,  extract_by_obid,  hypothesis,  sqequalBase,  equalitySymmetry,  isectElimination,  intEquality,  lambdaEquality_alt,  natural_numberEquality,  inhabitedIsType,  independent_isectElimination,  dependent_pairFormation_alt,  multiplyEquality,  imageElimination,  equalityTransitivity,  universeIsType,  instantiate,  universeEquality,  imageMemberEquality,  independent_functionElimination,  promote_hyp,  cumulativity,  dependent_functionElimination,  unionElimination,  approximateComputation,  int_eqEquality,  isect_memberEquality_alt,  voidElimination,  minusEquality,  addEquality,  setElimination,  rename,  inlFormation_alt,  inrFormation_alt,  dependent_set_memberEquality_alt
Latex:
\mforall{}d,e:\mBbbZ{}.
    (\mexists{}a,b:\mBbbZ{}.  ((((a  *  a)  +  ((b  *  b)  -  a  *  b))  =  e)  \mwedge{}  ((a  +  b)  =  d))
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}.  (((4  *  e)  -  d  *  d)  =  (3  *  n  *  n)))


Date html generated: 2020_05_19-PM-10_04_16
Last ObjectModification: 2019_11_22-AM-10_51_31

Theory : num_thy_1


Home Index