Nuprl Lemma : isEven-add
∀[n,m:ℤ].  uiff(↑isEven(n + m);↑same-parity(n;m))
Proof
Definitions occuring in Statement : 
same-parity: same-parity(n;m)
, 
isEven: isEven(n)
, 
assert: ↑b
, 
uiff: uiff(P;Q)
, 
uall: ∀[x:A]. B[x]
, 
add: n + m
, 
int: ℤ
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
and: P ∧ Q
, 
uiff: uiff(P;Q)
, 
uimplies: b supposing a
, 
implies: P 
⇒ Q
, 
prop: ℙ
Lemmas referenced : 
isOdd-isEven-add, 
assert_witness, 
same-parity_wf, 
assert_wf, 
isEven_wf
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
lemma_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
productElimination, 
hypothesis, 
sqequalRule, 
independent_pairEquality, 
isect_memberEquality, 
because_Cache, 
independent_functionElimination, 
equalityTransitivity, 
equalitySymmetry, 
intEquality, 
addEquality
Latex:
\mforall{}[n,m:\mBbbZ{}].    uiff(\muparrow{}isEven(n  +  m);\muparrow{}same-parity(n;m))
Date html generated:
2016_05_14-PM-04_24_39
Last ObjectModification:
2015_12_26-PM-08_19_50
Theory : num_thy_1
Home
Index