Nuprl Lemma : not-even-succ-implies-even

n:ℤ((¬↑isEven(n 1))  (↑isEven(n)))


Proof




Definitions occuring in Statement :  isEven: isEven(n) assert: b all: x:A. B[x] not: ¬A implies:  Q add: m natural_number: $n int:
Definitions unfolded in proof :  isEven: isEven(n) all: x:A. B[x] implies:  Q uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a rev_uimplies: rev_uimplies(P;Q) squash: T prop: true: True guard: {T} iff: ⇐⇒ Q nat_plus: + less_than: a < b less_than': less_than'(a;b) nequal: a ≠ b ∈  decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top int_nzero: -o sq_type: SQType(T)
Lemmas referenced :  equal_wf int_subtype_base subtype_base_sq eq_int_wf assert_wf not_wf int_formula_prop_wf int_term_value_subtract_lemma int_formula_prop_le_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_eq_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermSubtract_wf intformle_wf intformless_wf itermConstant_wf itermVar_wf intformeq_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__equal_int less_than_wf mod_bounds iff_weakening_equal add-one-mod-2 true_wf squash_wf nequal_wf assert_of_eq_int modulus_wf neg_assert_of_eq_int
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesis applyEquality natural_numberEquality productElimination independent_isectElimination lambdaEquality imageElimination hypothesisEquality equalityTransitivity equalitySymmetry universeEquality intEquality imageMemberEquality baseClosed independent_functionElimination dependent_set_memberEquality independent_pairFormation introduction dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality computeAll addEquality addLevel instantiate cumulativity

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



Date html generated: 2016_05_14-PM-04_23_40
Last ObjectModification: 2016_01_14-PM-11_38_11

Theory : num_thy_1


Home Index