Nuprl Lemma : int-rmul-one
∀[a:ℝ]. (1 * a = a)
Proof
Definitions occuring in Statement :
int-rmul: k1 * a,
req: x = y,
real: ℝ,
uall: ∀[x:A]. B[x],
natural_number: $n
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
uiff: uiff(P;Q),
and: P ∧ Q,
rev_uimplies: rev_uimplies(P;Q)
Lemmas referenced :
real_wf,
int-rmul_wf,
rmul_wf,
int-to-real_wf,
rmul-identity1,
req_functionality,
int-rmul-req,
req_weakening
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
cut,
introduction,
extract_by_obid,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
natural_numberEquality,
hypothesisEquality,
because_Cache,
independent_isectElimination,
productElimination
Latex:
\mforall{}[a:\mBbbR{}]. (1 * a = a)
Date html generated:
2019_10_29-AM-09_32_32
Last ObjectModification:
2018_08_27-PM-00_12_12
Theory : reals
Home
Index