Nuprl Lemma : add_is_int_counterexample
∀[n:ℤ]. ∀[x:ℤ_n]. (x + (-x) ∈ ℤ)
Proof
Definitions occuring in Statement :
int_mod: ℤ_n,
uall: ∀[x:A]. B[x],
member: t ∈ T,
add: n + m,
minus: -n,
int: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
int_mod: ℤ_n,
quotient: x,y:A//B[x; y],
and: P ∧ Q,
all: ∀x:A. B[x],
implies: P ⇒ Q,
prop: ℙ,
top: Top
Lemmas referenced :
eqmod_wf,
equal_wf,
equal-wf-base,
int_mod_wf,
minus-one-mul,
add-mul-special,
zero-mul
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
sqequalHypSubstitution,
pointwiseFunctionalityForEquality,
intEquality,
sqequalRule,
pertypeElimination,
productElimination,
thin,
equalityTransitivity,
hypothesis,
equalitySymmetry,
lambdaFormation,
because_Cache,
rename,
extract_by_obid,
isectElimination,
hypothesisEquality,
dependent_functionElimination,
independent_functionElimination,
productEquality,
axiomEquality,
isect_memberEquality,
voidElimination,
voidEquality,
natural_numberEquality
Latex:
\mforall{}[n:\mBbbZ{}]. \mforall{}[x:\mBbbZ{}\_n]. (x + (-x) \mmember{} \mBbbZ{})
Date html generated:
2017_04_17-AM-09_47_26
Last ObjectModification:
2017_02_27-PM-05_44_46
Theory : num_thy_1
Home
Index