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:  Q and: P ∧ Q subtract: m add: m natural_number: $n int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T implies:  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: supposing a ifthenelse: if then else fi  or: P ∨ Q sq_type: SQType(T) bfalse: ff not: ¬A false: False subtype_rel: A ⊆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