### Nuprl Lemma : rnexp-rminus

`∀x:ℝ. ∀n:ℕ.  (-(x)^n = if isOdd(n) then -(x^n) else x^n fi )`

Proof

Definitions occuring in Statement :  rnexp: `x^k1` req: `x = y` rminus: `-(x)` real: `ℝ` isOdd: `isOdd(n)` nat: `ℕ` ifthenelse: `if b then t else f fi ` all: `∀x:A. B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` nat: `ℕ` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` prop: `ℙ` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T` less_than': `less_than'(a;b)` true: `True` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` isEven: `isEven(n)` rev_uimplies: `rev_uimplies(P;Q)` not: `¬A`
Lemmas referenced :  isOdd_wf bool_wf eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot nat_wf real_wf req_wf rnexp_wf rminus_wf rmul_wf int-to-real_wf eq_int_wf modulus_wf_int_mod less_than_wf subtype_rel_set int_mod_wf le_wf int-subtype-int_mod assert_of_eq_int neg_assert_of_eq_int exp_wf2 isEven_wf req_weakening rmul-identity1 uiff_transitivity req_functionality rnexp_functionality rminus-as-rmul rnexp-rmul rmul_functionality req_transitivity rnexp-int squash_wf true_wf exp-minusone even-iff-not-odd
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin setElimination rename hypothesisEquality hypothesis unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule dependent_pairFormation promote_hyp dependent_functionElimination instantiate because_Cache independent_functionElimination voidElimination minusEquality natural_numberEquality dependent_set_memberEquality independent_pairFormation imageMemberEquality baseClosed applyEquality intEquality lambdaEquality cumulativity imageElimination

Latex:
\mforall{}x:\mBbbR{}.  \mforall{}n:\mBbbN{}.    (-(x)\^{}n  =  if  isOdd(n)  then  -(x\^{}n)  else  x\^{}n  fi  )

Date html generated: 2017_10_03-AM-08_39_52
Last ObjectModification: 2017_07_28-AM-07_31_00

Theory : reals

Home Index