Nuprl Lemma : not-same-parity-implies

`∀[n,m:ℤ].  ((¬↑same-parity(n;m)) `` {(↑same-parity(n;m - 1)) ∧ (↑same-parity(n;m + 1))})`

Proof

Definitions occuring in Statement :  same-parity: `same-parity(n;m)` assert: `↑b` uall: `∀[x:A]. B[x]` guard: `{T}` not: `¬A` implies: `P `` Q` and: `P ∧ Q` subtract: `n - m` add: `n + m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` guard: `{T}` and: `P ∧ Q` same-parity: `same-parity(n;m)` all: `∀x:A. B[x]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` or: `P ∨ Q` sq_type: `SQType(T)` bfalse: `ff` not: `¬A` false: `False` subtype_rel: `A ⊆r B` prop: `ℙ`
Lemmas referenced :  isEven_wf bool_wf eqtt_to_assert bool_cases subtype_base_sq bool_subtype_base eqff_to_assert assert_of_bnot uiff_transitivity equal-wf-base int_subtype_base assert_wf bnot_wf not_wf equal_wf same-parity_wf assert_witness subtract_wf odd-iff-not-even odd-implies even-iff-not-odd even-implies
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation independent_pairFormation sqequalHypSubstitution extract_by_obid isectElimination thin hypothesisEquality hypothesis unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule because_Cache dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination baseApply closedConclusion baseClosed applyEquality lambdaEquality independent_pairEquality natural_numberEquality addEquality intEquality isect_memberEquality

Latex:
\mforall{}[n,m:\mBbbZ{}].    ((\mneg{}\muparrow{}same-parity(n;m))  {}\mRightarrow{}  \{(\muparrow{}same-parity(n;m  -  1))  \mwedge{}  (\muparrow{}same-parity(n;m  +  1))\})

Date html generated: 2017_04_17-AM-09_43_33
Last ObjectModification: 2017_02_27-PM-05_38_19

Theory : num_thy_1

Home Index