Nuprl Lemma : even-plus-odd

[n,m:ℤ].  ↑isOdd(n m) supposing (↑isOdd(m)) ∧ (↑isEven(n))


Proof




Definitions occuring in Statement :  isEven: isEven(n) isOdd: isOdd(n) assert: b uimplies: supposing a uall: [x:A]. B[x] and: P ∧ Q add: m int:
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a not: ¬A implies:  Q false: False and: P ∧ Q same-parity: same-parity(n;m) all: x:A. B[x] bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b rev_implies:  Q iff: ⇐⇒ Q
Lemmas referenced :  eqtt_to_assert odd-iff-not-even eqff_to_assert bool_cases_sqequal subtype_base_sq bool_wf bool_subtype_base istype-assert same-parity_wf isOdd_wf isEven_wf istype-int iff_weakening_uiff assert_wf not_wf isOdd-add
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction lambdaFormation_alt thin sqequalHypSubstitution productElimination because_Cache inhabitedIsType hypothesis unionElimination equalityElimination extract_by_obid isectElimination independent_isectElimination sqequalRule hypothesisEquality dependent_pairFormation_alt equalityTransitivity equalitySymmetry equalityIstype promote_hyp dependent_functionElimination instantiate cumulativity independent_functionElimination voidElimination lambdaEquality_alt functionIsTypeImplies productIsType isect_memberEquality_alt isectIsTypeImplies addEquality

Latex:
\mforall{}[n,m:\mBbbZ{}].    \muparrow{}isOdd(n  +  m)  supposing  (\muparrow{}isOdd(m))  \mwedge{}  (\muparrow{}isEven(n))



Date html generated: 2020_05_19-PM-10_01_18
Last ObjectModification: 2019_11_12-PM-03_47_24

Theory : num_thy_1


Home Index