Nuprl Lemma : gcd_reduce_property

p,q:ℤ.  let g,a,b gcd_reduce(p;q) in (p (a g) ∈ ℤ) ∧ (q (b g) ∈ ℤ) ∧ CoPrime(a,b) ∧ ((p b) (a q) ∈ ℤ)

This theorem is one of freek's list of 100 theorems


Definitions occuring in Statement :  gcd_reduce: gcd_reduce(p;q) coprime: CoPrime(a,b) spreadn: spread3 all: x:A. B[x] and: P ∧ Q multiply: m int: equal: t ∈ T
Definitions unfolded in proof :  guard: {T} true: True squash: T top: Top false: False satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A or: P ∨ Q decidable: Dec(P) ge: i ≥  rev_implies:  Q iff: ⇐⇒ Q cand: c∧ B spreadn: spread3 spreadn: spread4 implies:  Q prop: uimplies: supposing a so_apply: x[s] so_lambda: λ2x.t[x] nat: and: P ∧ Q exists: x:A. B[x] uall: [x:A]. B[x] subtype_rel: A ⊆B member: t ∈ T gcd_reduce: gcd_reduce(p;q) all: x:A. B[x]
Lemmas referenced :  iff_weakening_equal istype-universe true_wf squash_wf equal_wf int_formula_prop_wf int_term_value_constant_lemma int_term_value_var_lemma int_term_value_mul_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma istype-void int_formula_prop_and_lemma itermConstant_wf itermVar_wf itermMultiply_wf itermAdd_wf intformeq_wf intformnot_wf intformand_wf full-omega-unsat decidable__equal_int nat_properties coprime_bezout_id istype-int le_wf set_subtype_base int_subtype_base equal-wf-base nat_wf subtype_rel_self gcd-reduce-ext
Rules used in proof :  imageMemberEquality multiplyEquality universeEquality imageElimination Error :productIsType,  sqequalBase Error :universeIsType,  voidElimination Error :isect_memberEquality_alt,  int_eqEquality approximateComputation unionElimination rename setElimination Error :dependent_pairFormation_alt,  independent_functionElimination dependent_functionElimination equalitySymmetry equalityTransitivity Error :equalityIstype,  independent_pairFormation productElimination because_Cache independent_isectElimination Error :inhabitedIsType,  natural_numberEquality Error :lambdaEquality_alt,  baseClosed closedConclusion baseApply hypothesisEquality productEquality intEquality functionEquality isectElimination sqequalHypSubstitution introduction sqequalRule hypothesis extract_by_obid instantiate thin applyEquality cut Error :lambdaFormation_alt,  sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

    let  g,a,b  =  gcd\_reduce(p;q)  in 
    (p  =  (a  *  g))  \mwedge{}  (q  =  (b  *  g))  \mwedge{}  CoPrime(a,b)  \mwedge{}  ((p  *  b)  =  (a  *  q))

Date html generated: 2019_06_20-PM-02_27_19
Last ObjectModification: 2019_06_19-PM-02_32_40

Theory : num_thy_1

Home Index