### 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

Proof

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: `n * m` int: `ℤ` equal: `s = 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 ≥ j ` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` cand: `A c∧ B` spreadn: spread3 spreadn: spread4 implies: `P `` Q` prop: `ℙ` uimplies: `b 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 ⊆r 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

Latex:
\mforall{}p,q:\mBbbZ{}.
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