Nuprl Lemma : rminus-int
∀[n:ℤ]. (-(r(n)) = r(-n) ∈ ℝ)
Proof
Definitions occuring in Statement :
rminus: -(x),
int-to-real: r(n),
real: ℝ,
uall: ∀[x:A]. B[x],
minus: -n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
real: ℝ,
squash: ↓T,
prop: ℙ,
int-to-real: r(n),
rminus: -(x),
nat_plus: ℕ+,
all: ∀x:A. B[x],
decidable: Dec(P),
or: P ∨ Q,
uimplies: b supposing a,
satisfiable_int_formula: satisfiable_int_formula(fmla),
exists: ∃x:A. B[x],
false: False,
implies: P ⇒ Q,
not: ¬A,
top: Top
Lemmas referenced :
int_formula_prop_wf,
int_term_value_var_lemma,
int_term_value_constant_lemma,
int_term_value_mul_lemma,
int_term_value_minus_lemma,
int_formula_prop_eq_lemma,
int_formula_prop_not_lemma,
itermVar_wf,
itermConstant_wf,
itermMultiply_wf,
itermMinus_wf,
intformeq_wf,
intformnot_wf,
satisfiable-full-omega-tt,
decidable__equal_int,
nat_plus_properties,
regular-int-seq_wf,
nat_plus_wf,
int-to-real_wf,
rminus_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
applyEquality,
lambdaEquality,
setElimination,
rename,
sqequalRule,
imageMemberEquality,
baseClosed,
setEquality,
functionEquality,
intEquality,
natural_numberEquality,
introduction,
imageElimination,
dependent_set_memberEquality,
functionExtensionality,
dependent_functionElimination,
because_Cache,
unionElimination,
independent_isectElimination,
dependent_pairFormation,
int_eqEquality,
isect_memberEquality,
voidElimination,
voidEquality,
computeAll
Latex:
\mforall{}[n:\mBbbZ{}]. (-(r(n)) = r(-n))
Date html generated:
2016_05_18-AM-06_48_49
Last ObjectModification:
2016_01_17-AM-01_45_37
Theory : reals
Home
Index