Nuprl Lemma : div_unique

[a:ℕ]. ∀[n:ℕ+]. ∀[p,q:ℕ].  (p q ∈ ℤsupposing (Div(a;n;q) and Div(a;n;p))


Definitions occuring in Statement :  div_nrel: Div(a;n;q) nat_plus: + nat: uimplies: supposing a uall: [x:A]. B[x] int: equal: t ∈ T
Definitions unfolded in proof :  top: Top false: False exists: x:A. B[x] satisfiable_int_formula: satisfiable_int_formula(fmla) implies:  Q not: ¬A or: P ∨ Q decidable: Dec(P) all: x:A. B[x] ge: i ≥  nat: nat_plus: + and: P ∧ Q lelt: i ≤ j < k div_nrel: Div(a;n;q) uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop:
Lemmas referenced :  int_formula_prop_wf int_term_value_constant_lemma int_term_value_add_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma istype-void int_formula_prop_and_lemma istype-int itermConstant_wf itermAdd_wf intformless_wf itermVar_wf intformeq_wf intformnot_wf intformand_wf full-omega-unsat decidable__equal_int nat_plus_properties nat_properties mul_cancel_in_lt lt_transitivity_2 div_nrel_wf nat_wf nat_plus_wf
Rules used in proof :  independent_pairFormation voidElimination isect_memberEquality_alt int_eqEquality lambdaEquality_alt dependent_pairFormation_alt independent_functionElimination approximateComputation unionElimination dependent_functionElimination independent_isectElimination natural_numberEquality addEquality rename setElimination multiplyEquality productElimination sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut hypothesis universeIsType extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality sqequalRule isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry because_Cache inhabitedIsType

\mforall{}[a:\mBbbN{}].  \mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[p,q:\mBbbN{}].    (p  =  q)  supposing  (Div(a;n;q)  and  Div(a;n;p))

Date html generated: 2019_10_15-AM-10_21_17
Last ObjectModification: 2019_09_21-AM-11_47_28

Theory : int_2

Home Index