Nuprl Lemma : three-cubes-6-mod-9

a,b,c,k:ℤ.
  (((a^3 b^3 c^3) k ∈ ℤ (k ≡ mod 9)  ((a^3 ≡ (-1) mod 9) ∧ (b^3 ≡ (-1) mod 9) ∧ (c^3 ≡ (-1) mod 9)))


Proof




Definitions occuring in Statement :  eqmod: a ≡ mod m exp: i^n all: x:A. B[x] implies:  Q and: P ∧ Q add: m minus: -n natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a sq_type: SQType(T) guard: {T} or: P ∨ Q prop: subtype_rel: A ⊆B nat: decidable: Dec(P) not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top false: False nat_plus: + iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q modulus: mod n remainder: rem m true: True absval: |i| cand: c∧ B
Lemmas referenced :  subtype_base_sq int_subtype_base cube-mod-9 eqmod_wf istype-int exp_wf2 decidable__le full-omega-unsat intformnot_wf intformle_wf itermConstant_wf int_formula_prop_not_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_formula_prop_wf istype-le modulus-equal-iff-eqmod decidable__lt intformless_wf int_formula_prop_less_lemma istype-less_than eqmod_functionality_wrt_eqmod add_functionality_wrt_eqmod eqmod_weakening
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :lambdaFormation_alt,  cut thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity intEquality independent_isectElimination hypothesis dependent_functionElimination equalityTransitivity equalitySymmetry hypothesisEquality independent_functionElimination unionElimination Error :universeIsType,  natural_numberEquality Error :equalityIstype,  because_Cache sqequalRule baseApply closedConclusion baseClosed applyEquality sqequalBase Error :inhabitedIsType,  addEquality Error :dependent_set_memberEquality_alt,  approximateComputation Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  Error :isect_memberEquality_alt,  voidElimination productElimination independent_pairFormation minusEquality

Latex:
\mforall{}a,b,c,k:\mBbbZ{}.
    (((a\^{}3  +  b\^{}3  +  c\^{}3)  =  k)
    {}\mRightarrow{}  (k  \mequiv{}  6  mod  9)
    {}\mRightarrow{}  ((a\^{}3  \mequiv{}  (-1)  mod  9)  \mwedge{}  (b\^{}3  \mequiv{}  (-1)  mod  9)  \mwedge{}  (c\^{}3  \mequiv{}  (-1)  mod  9)))



Date html generated: 2019_06_20-PM-02_26_23
Last ObjectModification: 2019_03_18-PM-00_14_26

Theory : num_thy_1


Home Index