Nuprl Lemma : small-eqmod-odd

m:ℕ+((↑isOdd(m))  (∀a:ℤ. ∃b:ℤ(2 |b| < m ∧ (b ≡ mod m))))


Proof




Definitions occuring in Statement :  isOdd: isOdd(n) eqmod: a ≡ mod m absval: |i| nat_plus: + assert: b less_than: a < b all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q multiply: m natural_number: $n int:
Definitions unfolded in proof :  sq_type: SQType(T) guard: {T} prop: top: Top satisfiable_int_formula: satisfiable_int_formula(fmla) not: ¬A uimplies: supposing a nat: le: A ≤ B false: False or: P ∨ Q decidable: Dec(P) nat_plus: + subtype_rel: A ⊆B uall: [x:A]. B[x] cand: c∧ B and: P ∧ Q exists: x:A. B[x] member: t ∈ T implies:  Q all: x:A. B[x] rev_implies:  Q iff: ⇐⇒ Q
Lemmas referenced :  nat_plus_wf isOdd_wf assert_wf eqmod_wf less_than_wf int_subtype_base subtype_base_sq odd-implies false_wf int_formula_prop_wf int_formula_prop_le_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_mul_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformle_wf intformless_wf itermConstant_wf itermMultiply_wf itermVar_wf intformeq_wf intformnot_wf intformand_wf full-omega-unsat nat_wf decidable__equal_int nat_plus_properties absval_wf decidable__lt small-eqmod equal-wf-base assert-isEven
Rules used in proof :  productEquality cumulativity instantiate independent_pairFormation voidEquality voidElimination isect_memberEquality intEquality int_eqEquality independent_functionElimination approximateComputation independent_isectElimination lambdaEquality promote_hyp equalitySymmetry equalityTransitivity pointwiseFunctionality unionElimination rename setElimination sqequalRule because_Cache applyEquality hypothesis isectElimination natural_numberEquality multiplyEquality dependent_pairFormation productElimination hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution extract_by_obid introduction cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution baseClosed closedConclusion baseApply

Latex:
\mforall{}m:\mBbbN{}\msupplus{}.  ((\muparrow{}isOdd(m))  {}\mRightarrow{}  (\mforall{}a:\mBbbZ{}.  \mexists{}b:\mBbbZ{}.  (2  *  |b|  <  m  \mwedge{}  (b  \mequiv{}  a  mod  m))))



Date html generated: 2018_05_21-PM-00_56_07
Last ObjectModification: 2017_12_31-PM-07_41_57

Theory : num_thy_1


Home Index