Nuprl Lemma : gcd-mod

x:ℕ+. ∀y:ℕ.  (gcd(x;y mod x) gcd(x;y) ∈ ℤ)


Proof




Definitions occuring in Statement :  modulus: mod n gcd: gcd(a;b) nat_plus: + nat: all: x:A. B[x] int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T nat: decidable: Dec(P) or: P ∨ Q uall: [x:A]. B[x] uimplies: supposing a sq_type: SQType(T) implies:  Q guard: {T} squash: T prop: nat_plus: + int_seg: {i..j-} lelt: i ≤ j < k and: P ∧ Q le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top true: True subtype_rel: A ⊆B iff: ⇐⇒ Q int_nzero: -o so_lambda: λ2x.t[x] so_apply: x[s] nequal: a ≠ b ∈  gcd: gcd(a;b) int_upper: {i...} bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b
Lemmas referenced :  decidable__equal_int subtype_base_sq int_subtype_base nat_wf nat_plus_wf gcd_wf squash_wf true_wf modulus_base false_wf nat_properties nat_plus_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformnot_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf lelt_wf equal_wf iff_weakening_equal modulus-is-rem subtype_rel_sets less_than_wf nequal_wf intformeq_wf int_formula_prop_eq_lemma equal-wf-base gcd_com nat_plus_subtype_nat int_upper_subtype_nat le_wf nequal-le-implies zero-add eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int int_upper_properties eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_int
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin setElimination rename hypothesisEquality hypothesis natural_numberEquality unionElimination instantiate isectElimination cumulativity intEquality independent_isectElimination because_Cache independent_functionElimination applyEquality lambdaEquality imageElimination equalityTransitivity equalitySymmetry sqequalRule dependent_set_memberEquality independent_pairFormation dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality computeAll universeEquality imageMemberEquality baseClosed productElimination setEquality applyLambdaEquality hypothesis_subsumption equalityElimination promote_hyp remainderEquality

Latex:
\mforall{}x:\mBbbN{}\msupplus{}.  \mforall{}y:\mBbbN{}.    (gcd(x;y  mod  x)  =  gcd(x;y))



Date html generated: 2018_05_21-PM-08_57_29
Last ObjectModification: 2017_07_26-PM-06_21_15

Theory : general


Home Index