Nuprl Lemma : rexp-rminus
∀[x:ℝ]. (e^-(x) = (r1/e^x))
Proof
Definitions occuring in Statement : 
rexp: e^x
, 
rdiv: (x/y)
, 
req: x = y
, 
rminus: -(x)
, 
int-to-real: r(n)
, 
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
, 
rneq: x ≠ y
, 
guard: {T}
, 
or: P ∨ Q
, 
all: ∀x:A. B[x]
, 
prop: ℙ
, 
uiff: uiff(P;Q)
, 
and: P ∧ Q
, 
rev_uimplies: rev_uimplies(P;Q)
, 
implies: P 
⇒ Q
Lemmas referenced : 
rmul_preserves_req, 
rexp_wf, 
rminus_wf, 
rdiv_wf, 
rexp-positive, 
req_witness, 
int-to-real_wf, 
rless_wf, 
real_wf, 
rmul_wf, 
req_functionality, 
req_weakening, 
rmul-rdiv-cancel2, 
radd_wf, 
req_wf, 
req_inversion, 
rexp-radd, 
uiff_transitivity, 
rexp_functionality, 
req_transitivity, 
radd_functionality, 
rminus-as-rmul, 
rmul-identity1, 
rmul-distrib2, 
rmul_functionality, 
radd-int, 
rmul-zero-both, 
rexp0
Rules used in proof : 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
introduction, 
cut, 
extract_by_obid, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
hypothesis, 
because_Cache, 
independent_isectElimination, 
sqequalRule, 
inrFormation, 
dependent_functionElimination, 
productElimination, 
natural_numberEquality, 
independent_functionElimination, 
minusEquality, 
addEquality
Latex:
\mforall{}[x:\mBbbR{}].  (e\^{}-(x)  =  (r1/e\^{}x))
Date html generated:
2016_10_26-PM-00_12_23
Last ObjectModification:
2016_09_12-PM-05_39_32
Theory : reals_2
Home
Index