### Nuprl Lemma : not-same-parity-implies-even-odd

`∀n,m:ℤ.  ((¬↑same-parity(n;m)) `` (((↑isEven(n)) ∧ (↑isOdd(m))) ∨ ((↑isOdd(n)) ∧ (↑isEven(m)))))`

Proof

Definitions occuring in Statement :  same-parity: `same-parity(n;m)` isEven: `isEven(n)` isOdd: `isOdd(n)` assert: `↑b` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` or: `P ∨ Q` and: `P ∧ Q` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` implies: `P `` Q` same-parity: `same-parity(n;m)` member: `t ∈ T` uall: `∀[x:A]. B[x]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` prop: `ℙ` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` false: `False` cand: `A c∧ B` true: `True` not: `¬A`
Lemmas referenced :  isEven_wf bool_wf eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot odd-iff-not-even even-iff-not-odd false_wf assert_wf isOdd_wf not_wf same-parity_wf bool_cases assert_of_bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation sqequalHypSubstitution cut introduction extract_by_obid isectElimination thin hypothesisEquality hypothesis unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule dependent_pairFormation promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination because_Cache voidElimination inrFormation independent_pairFormation productEquality intEquality inlFormation natural_numberEquality

Latex:
\mforall{}n,m:\mBbbZ{}.    ((\mneg{}\muparrow{}same-parity(n;m))  {}\mRightarrow{}  (((\muparrow{}isEven(n))  \mwedge{}  (\muparrow{}isOdd(m)))  \mvee{}  ((\muparrow{}isOdd(n))  \mwedge{}  (\muparrow{}isEven(m)))))

Date html generated: 2017_04_17-AM-09_43_40
Last ObjectModification: 2017_02_27-PM-05_38_16

Theory : num_thy_1

Home Index