Nuprl Lemma : odd-implies

n:ℤ((↑isOdd(n))  {((↑isEven(n 1)) ∧ (¬↑isEven(n))) ∧ (↑isEven(n 1))})


Proof




Definitions occuring in Statement :  isEven: isEven(n) isOdd: isOdd(n) assert: b guard: {T} all: x:A. B[x] not: ¬A implies:  Q and: P ∧ Q subtract: m add: m natural_number: $n int:
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q guard: {T} and: P ∧ Q cand: c∧ B member: t ∈ T prop: uall: [x:A]. B[x] iff: ⇐⇒ Q rev_implies:  Q exists: x:A. B[x] decidable: Dec(P) or: P ∨ Q uimplies: supposing a satisfiable_int_formula: satisfiable_int_formula(fmla) false: False not: ¬A top: Top isOdd: isOdd(n) int_nzero: -o true: True nequal: a ≠ b ∈  sq_type: SQType(T) subtype_rel: A ⊆B uiff: uiff(P;Q) isEven: isEven(n) eq_int: (i =z j) assert: b ifthenelse: if then else fi  bfalse: ff
Lemmas referenced :  false_wf nequal_wf true_wf int_subtype_base subtype_base_sq modulus_wf assert_of_eq_int equal_wf int_formula_prop_wf int_term_value_add_lemma int_term_value_mul_lemma int_term_value_constant_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermAdd_wf itermMultiply_wf itermConstant_wf itermVar_wf itermSubtract_wf intformeq_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__equal_int subtract_wf assert-isEven assert-isOdd isOdd_wf assert_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation independent_pairFormation cut hypothesis lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality intEquality dependent_functionElimination productElimination independent_functionElimination natural_numberEquality dependent_pairFormation because_Cache unionElimination independent_isectElimination lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality sqequalRule computeAll multiplyEquality dependent_set_memberEquality addLevel instantiate cumulativity equalityTransitivity equalitySymmetry applyEquality addEquality

Latex:
\mforall{}n:\mBbbZ{}.  ((\muparrow{}isOdd(n))  {}\mRightarrow{}  \{((\muparrow{}isEven(n  -  1))  \mwedge{}  (\mneg{}\muparrow{}isEven(n)))  \mwedge{}  (\muparrow{}isEven(n  +  1))\})



Date html generated: 2016_05_14-PM-04_23_57
Last ObjectModification: 2016_01_14-PM-11_38_08

Theory : num_thy_1


Home Index