Nuprl Lemma : odd-implies-succ-two-times

n:ℕ((↑isOdd(n))  (∃k:ℕ(n ((2 k) 1) ∈ ℤ)))


Proof




Definitions occuring in Statement :  isOdd: isOdd(n) nat: assert: b all: x:A. B[x] exists: x:A. B[x] implies:  Q multiply: m add: m natural_number: $n int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] nat: iff: ⇐⇒ Q and: P ∧ Q exists: x:A. B[x] ge: i ≥  decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top
Lemmas referenced :  equal_wf le_wf int_formula_prop_wf int_term_value_mul_lemma int_term_value_add_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermMultiply_wf itermAdd_wf intformeq_wf itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties assert-isOdd nat_wf isOdd_wf assert_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis dependent_functionElimination productElimination independent_functionElimination dependent_pairFormation dependent_set_memberEquality natural_numberEquality unionElimination independent_isectElimination lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation computeAll addEquality multiplyEquality

Latex:
\mforall{}n:\mBbbN{}.  ((\muparrow{}isOdd(n))  {}\mRightarrow{}  (\mexists{}k:\mBbbN{}.  (n  =  ((2  *  k)  +  1))))



Date html generated: 2016_05_14-PM-04_23_50
Last ObjectModification: 2016_01_14-PM-11_38_52

Theory : num_thy_1


Home Index