Nuprl Lemma : gcd_functionality_wrt_eqmod

a,a',m:ℤ.  ((a' ≡ mod m)  (gcd(a';m) gcd(a;m)))


Proof




Definitions occuring in Statement :  eqmod: a ≡ mod m assoced: b gcd: gcd(a;b) all: x:A. B[x] implies:  Q int:
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q eqmod: a ≡ mod m divides: a exists: x:A. B[x] member: t ∈ T and: P ∧ Q gcd_p: GCD(a;b;y) assoced: b cand: c∧ B prop: uall: [x:A]. B[x] uimplies: supposing a decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top sq_type: SQType(T) guard: {T}
Lemmas referenced :  gcd_elim assoced_wf gcd_wf eqmod_wf subtype_base_sq int_subtype_base decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf itermAdd_wf itermMultiply_wf itermMinus_wf itermSubtract_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_add_lemma int_term_value_mul_lemma int_term_value_minus_lemma int_term_value_subtract_lemma int_formula_prop_wf divisor_of_sum divisor_of_mul
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution productElimination thin cut introduction extract_by_obid dependent_functionElimination hypothesisEquality because_Cache hypothesis independent_pairFormation independent_functionElimination hyp_replacement equalitySymmetry Error :applyLambdaEquality,  isectElimination sqequalRule intEquality instantiate cumulativity independent_isectElimination unionElimination natural_numberEquality dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality computeAll multiplyEquality minusEquality equalityTransitivity

Latex:
\mforall{}a,a',m:\mBbbZ{}.    ((a'  \mequiv{}  a  mod  m)  {}\mRightarrow{}  (gcd(a';m)  \msim{}  gcd(a;m)))



Date html generated: 2016_10_21-AM-11_09_12
Last ObjectModification: 2016_07_12-AM-06_01_44

Theory : num_thy_1


Home Index