Nuprl Lemma : lcm-property

x,y:ℤ.  ∃a,b:ℤ(CoPrime(a,b) ∧ ((x b) lcm(x;y) ∈ ℤ) ∧ ((y a) lcm(x;y) ∈ ℤ))


Proof




Definitions occuring in Statement :  lcm: lcm(a;b) coprime: CoPrime(a,b) all: x:A. B[x] exists: x:A. B[x] and: P ∧ Q multiply: m int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T exists: x:A. B[x] decidable: Dec(P) or: P ∨ Q and: P ∧ Q cand: c∧ B uall: [x:A]. B[x] prop: subtype_rel: A ⊆B nequal: a ≠ b ∈  assert: b bnot: ¬bb bfalse: ff top: Top false: False satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A ifthenelse: if then else fi  uiff: uiff(P;Q) btrue: tt it: unit: Unit bool: 𝔹 guard: {T} implies:  Q sq_type: SQType(T) uimplies: supposing a lcm: lcm(a;b) has-value: (a)↓ true: True squash: T gcd: gcd(a;b) iff: ⇐⇒ Q rev_implies:  Q int_nzero: -o eq_int: (i =z j)
Lemmas referenced :  gcd-property decidable__equal_int gcd_wf coprime_wf int_subtype_base istype-int neg_assert_of_eq_int assert-bnot bool_subtype_base bool_wf bool_cases_sqequal eqff_to_assert int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_formula_prop_eq_lemma istype-void int_formula_prop_not_lemma itermVar_wf itermConstant_wf itermMultiply_wf intformeq_wf intformnot_wf full-omega-unsat assert_of_eq_int eqtt_to_assert eq_int_wf int-value-type value-type-has-value subtype_base_sq istype-universe true_wf squash_wf equal_wf int_formula_prop_and_lemma intformand_wf subtype_rel_self iff_weakening_equal mul-associates mul-commutes div-cancel-1 nequal_wf zero-div-rem btrue_wf
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt hypothesis sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality productElimination dependent_pairFormation_alt natural_numberEquality unionElimination sqequalRule productIsType universeIsType isectElimination equalityIstype inhabitedIsType baseApply closedConclusion baseClosed applyEquality sqequalBase equalitySymmetry because_Cache voidElimination isect_memberEquality_alt int_eqEquality lambdaEquality_alt approximateComputation independent_pairFormation equalityElimination multiplyEquality promote_hyp independent_functionElimination equalityTransitivity independent_isectElimination intEquality cumulativity instantiate callbyvalueReduce Error :memTop,  imageMemberEquality universeEquality imageElimination hyp_replacement dependent_set_memberEquality_alt

Latex:
\mforall{}x,y:\mBbbZ{}.    \mexists{}a,b:\mBbbZ{}.  (CoPrime(a,b)  \mwedge{}  ((x  *  b)  =  lcm(x;y))  \mwedge{}  ((y  *  a)  =  lcm(x;y)))



Date html generated: 2020_05_19-PM-10_02_19
Last ObjectModification: 2019_12_31-AM-10_56_45

Theory : num_thy_1


Home Index