Nuprl Lemma : three-cubes-mod-9

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


Proof




Definitions occuring in Statement :  eqmod: a ≡ mod m exp: i^n all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q add: m 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} subtype_rel: A ⊆B or: P ∨ Q and: P ∧ Q not: ¬A modulus: mod n remainder: rem m true: True false: False nat_plus: + decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top prop: iff: ⇐⇒ Q rev_implies:  Q nat: absval: |i|
Lemmas referenced :  subtype_base_sq int_subtype_base istype-int cube-mod-9 modulus-equal-iff-eqmod decidable__lt full-omega-unsat intformnot_wf intformless_wf itermConstant_wf int_formula_prop_not_lemma istype-void int_formula_prop_less_lemma int_term_value_constant_lemma int_formula_prop_wf istype-less_than eqmod_wf exp_wf2 decidable__le intformle_wf int_formula_prop_le_lemma istype-le 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 Error :equalityIstype,  because_Cache sqequalRule baseApply closedConclusion baseClosed applyEquality sqequalBase Error :inhabitedIsType,  unionElimination independent_pairFormation natural_numberEquality voidElimination productElimination Error :dependent_set_memberEquality_alt,  approximateComputation Error :dependent_pairFormation_alt,  Error :lambdaEquality_alt,  Error :isect_memberEquality_alt,  Error :universeIsType,  promote_hyp addEquality minusEquality

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



Date html generated: 2019_06_20-PM-02_26_14
Last ObjectModification: 2019_03_18-PM-00_04_05

Theory : num_thy_1


Home Index