### Nuprl Lemma : rroot-abs-property

`∀i:{2...}. ∀x:ℝ.  (rroot-abs(i;x)^i = |x|)`

Proof

Definitions occuring in Statement :  rroot-abs: `rroot-abs(i;x)` rabs: `|x|` rnexp: `x^k1` req: `x = y` real: `ℝ` int_upper: `{i...}` all: `∀x:A. B[x]` natural_number: `\$n`
Definitions unfolded in proof :  member: `t ∈ T` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` nat: `ℕ` int_upper: `{i...}` nequal: `a ≠ b ∈ T ` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` and: `P ∧ Q` prop: `ℙ` nat_plus: `ℕ+` int_nzero: `ℤ-o` true: `True` sq_type: `SQType(T)` guard: `{T}` so_lambda: `λ2x.t[x]` real: `ℝ` so_apply: `x[s]` le: `A ≤ B` less_than': `less_than'(a;b)` uiff: `uiff(P;Q)` rnexp: `x^k1` has-value: `(a)↓` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` bnot: `¬bb` assert: `↑b` reg-seq-nexp: `reg-seq-nexp(x;k)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bdd-diff: `bdd-diff(f;g)` ge: `i ≥ j ` rroot-abs: `rroot-abs(i;x)` squash: `↓T` sq_stable: `SqStable(P)` regular-int-seq: `k-regular-seq(f)` less_than: `a < b` label: `...\$L... t` rev_uimplies: `rev_uimplies(P;Q)` subtract: `n - m` cand: `A c∧ B`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesisEquality hypothesis applyEquality because_Cache sqequalRule dependent_set_memberEquality_alt setElimination rename natural_numberEquality unionElimination independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality isect_memberEquality_alt voidElimination independent_pairFormation universeIsType addEquality multiplyEquality lambdaFormation_alt instantiate cumulativity intEquality equalityTransitivity equalitySymmetry equalityIstype baseClosed sqequalBase functionEquality inhabitedIsType applyLambdaEquality pointwiseFunctionality promote_hyp baseApply closedConclusion productElimination callbyvalueReduce equalityElimination setEquality functionIsType imageElimination imageMemberEquality universeEquality productIsType minusEquality lessCases isect_memberFormation_alt axiomSqEquality isectIsTypeImplies divideEquality equalityIsType4 remainderEquality hyp_replacement equalityIsType1

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\mBbbR{}.    (rroot-abs(i;x)\^{}i  =  |x|)

Date html generated: 2019_10_30-AM-07_56_17
Last ObjectModification: 2019_10_10-AM-10_22_50

Theory : reals

Home Index