### Nuprl Lemma : gcd-reduce

`∀p,q:ℤ.  ∃g:ℕ. ∃a,b,x,y:ℤ. ((p = (a * g) ∈ ℤ) ∧ (q = (b * g) ∈ ℤ) ∧ (((x * a) + (y * b)) = 1 ∈ ℤ))`

Proof

Definitions occuring in Statement :  nat: `ℕ` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` and: `P ∧ Q` multiply: `n * m` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  absval: `|i|` sign: `sign(x)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` less_than': `less_than'(a;b)` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` label: `...\$L... t` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` true: `True` nat_plus: `ℕ+` nequal: `a ≠ b ∈ T ` int_nzero: `ℤ-o` top: `Top` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` ge: `i ≥ j ` cand: `A c∧ B` guard: `{T}` sq_type: `SQType(T)` or: `P ∨ Q` decidable: `Dec(P)` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` prop: `ℙ` uimplies: `b supposing a` so_apply: `x[s]` squash: `↓T` less_than: `a < b` le: `A ≤ B` lelt: `i ≤ j < k` so_lambda: `λ2x.t[x]` int_seg: `{i..j-}` subtype_rel: `A ⊆r B` and: `P ∧ Q` exists: `∃x:A. B[x]` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]`
Lemmas referenced :  bnot_of_le_int assert_functionality_wrt_uiff uiff_transitivity assert_wf bnot_wf absval_unfold lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf le_int_wf assert_of_le_int satisfiable-full-omega-tt eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot itermMinus_wf int_term_value_minus_lemma sign_wf equal-wf-base-T absval_wf int_term_value_subtract_lemma itermSubtract_wf mul_assoc int_nzero_wf mul-commutes iff_weakening_equal mul_add_distrib istype-universe true_wf squash_wf div_rem_sum subtract_wf divide_wfa istype-le decidable__le istype-less_than int_formula_prop_le_lemma int_formula_prop_less_lemma int_formula_prop_and_lemma intformle_wf intformless_wf intformand_wf decidable__lt rem_bounds_1 int-value-type equal_wf set-value-type nequal_wf remainder_wfa int_term_value_add_lemma itermAdd_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_mul_lemma int_term_value_constant_lemma int_formula_prop_eq_lemma istype-void int_formula_prop_not_lemma itermVar_wf itermMultiply_wf itermConstant_wf intformeq_wf intformnot_wf full-omega-unsat nat_properties subtype_base_sq decidable__equal_int subtype_rel_self subtype_rel_function equal-wf-base exists_wf nat_wf all_wf natrec_wf istype-nat le_wf int_subtype_base lelt_wf set_subtype_base istype-int int_seg_wf
Rules used in proof :  minusEquality equalityElimination lessCases isect_memberFormation axiomSqEquality isect_memberEquality voidEquality dependent_pairFormation computeAll promote_hyp dependent_pairEquality independent_pairEquality axiomEquality lambdaEquality lambdaFormation imageMemberEquality universeEquality hyp_replacement multiplyEquality addEquality cutEval Error :dependent_set_memberEquality_alt,  independent_pairFormation voidElimination Error :isect_memberEquality_alt,  int_eqEquality Error :dependent_pairFormation_alt,  approximateComputation independent_functionElimination cumulativity instantiate unionElimination dependent_functionElimination functionEquality functionExtensionality productEquality equalityTransitivity equalitySymmetry sqequalBase baseClosed closedConclusion baseApply independent_isectElimination imageElimination productElimination Error :lambdaEquality_alt,  intEquality applyEquality Error :equalityIstype,  because_Cache Error :productIsType,  hypothesis rename setElimination natural_numberEquality thin isectElimination sqequalHypSubstitution extract_by_obid introduction Error :universeIsType,  Error :functionIsType,  sqequalRule hypothesisEquality Error :inhabitedIsType,  Error :lambdaFormation_alt,  sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution cut

Latex:
\mforall{}p,q:\mBbbZ{}.    \mexists{}g:\mBbbN{}.  \mexists{}a,b,x,y:\mBbbZ{}.  ((p  =  (a  *  g))  \mwedge{}  (q  =  (b  *  g))  \mwedge{}  (((x  *  a)  +  (y  *  b))  =  1))

Date html generated: 2019_06_20-PM-02_27_10
Last ObjectModification: 2019_06_19-PM-02_31_44

Theory : num_thy_1

Home Index