Nuprl Lemma : special-mod4-decomp_wf
∀[m:ℤ]
(special-mod4-decomp(m) ∈ {p:ℤ × {-2..3-}| let k,b = p in (m = ((4 * k) + b) ∈ ℤ) ∧ ((|b| = 2 ∈ ℤ) ⇒ (↑isEven(k)))} )
Proof
Definitions occuring in Statement :
special-mod4-decomp: special-mod4-decomp(m),
isEven: isEven(n),
absval: |i|,
int_seg: {i..j-},
assert: ↑b,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
member: t ∈ T,
set: {x:A| B[x]} ,
spread: spread def,
product: x:A × B[x],
multiply: n * m,
add: n + m,
minus: -n,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
special-mod4-decomp: special-mod4-decomp(m),
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
so_lambda: λ2x.t[x],
prop: ℙ,
and: P ∧ Q,
int_seg: {i..j-},
implies: P ⇒ Q,
so_apply: x[s],
sq_exists: ∃x:A [B[x]],
nat: ℕ
Lemmas referenced :
sparse-signed-rep-lemma1-ext,
subtype_rel_self,
sq_exists_wf,
int_seg_wf,
equal-wf-base-T,
int_subtype_base,
equal-wf-T-base,
absval_wf,
assert_wf,
isEven_wf,
nat_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalRule,
applyEquality,
thin,
instantiate,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
isectElimination,
functionEquality,
intEquality,
productEquality,
minusEquality,
natural_numberEquality,
lambdaEquality,
spreadEquality,
hypothesisEquality,
addEquality,
multiplyEquality,
setElimination,
rename,
because_Cache,
baseClosed,
setEquality,
axiomEquality,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}[m:\mBbbZ{}]
(special-mod4-decomp(m) \mmember{} \{p:\mBbbZ{} \mtimes{} \{-2..3\msupminus{}\}|
let k,b = p
in (m = ((4 * k) + b)) \mwedge{} ((|b| = 2) {}\mRightarrow{} (\muparrow{}isEven(k)))\} )
Date html generated:
2018_05_21-PM-08_33_55
Last ObjectModification:
2018_05_19-PM-05_05_26
Theory : general
Home
Index