Nuprl Lemma : sinh-inv-sinh

[x:ℝ]. (sinh(inv-sinh(x)) x)


Proof




Definitions occuring in Statement :  inv-sinh: inv-sinh(x) sinh: sinh(x) req: y real: uall: [x:A]. B[x]
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] inv-sinh: inv-sinh(x) sinh: sinh(x) implies:  Q and: P ∧ Q prop: subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] int_nzero: -o true: True nequal: a ≠ b ∈  not: ¬A uimplies: supposing a sq_type: SQType(T) guard: {T} false: False rneq: x ≠ y or: P ∨ Q iff: ⇐⇒ Q rev_implies:  Q less_than: a < b squash: T less_than': less_than'(a;b) uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) rdiv: (x/y) req_int_terms: t1 ≡ t2 top: Top sq_stable: SqStable(P)
Lemmas referenced :  inv-sinh-domain req_witness sinh_wf inv-sinh_wf real_wf ln_wf radd_wf rsqrt_wf rmul_wf int-to-real_wf rleq_wf req_wf rless_wf set_wf rlog_wf expr_wf rexp_wf rminus_wf equal_wf int-rdiv_wf subtype_base_sq int_subtype_base equal-wf-base true_wf nequal_wf rsub_wf rdiv_wf rless-int rmul_preserves_req rinv_wf2 itermSubtract_wf itermMultiply_wf itermVar_wf itermConstant_wf itermAdd_wf req-iff-rsub-is-0 minus-one-mul itermMinus_wf rmul_comm req_functionality int-rdiv-req req_weakening req_transitivity radd_functionality int-rinv-cancel rmul-rinv3 real_polynomial_null real_term_value_sub_lemma real_term_value_mul_lemma real_term_value_var_lemma real_term_value_const_lemma real_term_value_add_lemma real_term_value_minus_lemma sq_stable__req rexp-positive uiff_transitivity rexp_functionality rexp-rlog rexp-rminus rdiv_functionality req_inversion rless_transitivity1 rleq_weakening rminus_functionality rmul-rinv rmul_functionality radd-preserves-req
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination hypothesis independent_functionElimination dependent_set_memberEquality natural_numberEquality productElimination applyEquality lambdaEquality setElimination rename setEquality productEquality sqequalRule because_Cache lambdaFormation equalityTransitivity equalitySymmetry addLevel instantiate cumulativity intEquality independent_isectElimination voidElimination baseClosed inrFormation independent_pairFormation imageMemberEquality minusEquality approximateComputation int_eqEquality isect_memberEquality voidEquality imageElimination

Latex:
\mforall{}[x:\mBbbR{}].  (sinh(inv-sinh(x))  =  x)



Date html generated: 2017_10_04-PM-10_44_44
Last ObjectModification: 2017_06_24-AM-10_48_57

Theory : reals_2


Home Index