### Nuprl Lemma : extracted-rroot_wf

`∀[i:{2...}]. ∀[x:{x:ℝ| (↑isEven(i)) `` (r0 ≤ x)} ].`
`  (extracted-rroot(i;x) ∈ {y:ℝ| ((↑isEven(i)) `` (r0 ≤ y)) ∧ (y^i = x)} )`

Proof

Definitions occuring in Statement :  extracted-rroot: `extracted-rroot(i;x)` rleq: `x ≤ y` rnexp: `x^k1` req: `x = y` int-to-real: `r(n)` real: `ℝ` isEven: `isEven(n)` int_upper: `{i...}` assert: `↑b` uall: `∀[x:A]. B[x]` implies: `P `` Q` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` natural_number: `\$n`
Definitions unfolded in proof :  not: `¬A` false: `False` less_than': `less_than'(a;b)` le: `A ≤ B` uimplies: `b supposing a` sq_exists: `∃x:A [B[x]]` so_apply: `x[s]` and: `P ∧ Q` so_lambda: `λ2x.t[x]` prop: `ℙ` int_upper: `{i...}` implies: `P `` Q` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` extracted-rroot: `extracted-rroot(i;x)` member: `t ∈ T` uall: `∀[x:A]. B[x]`
Lemmas referenced :  set_wf false_wf upper_subtype_nat rnexp_wf req_wf sq_exists_wf int-to-real_wf rleq_wf isEven_wf assert_wf real_wf all_wf int_upper_wf subtype_rel_self rroot-exists-ext
Rules used in proof :  isect_memberEquality equalitySymmetry equalityTransitivity axiomEquality lambdaFormation independent_pairFormation independent_isectElimination dependent_set_memberEquality productEquality lambdaEquality hypothesisEquality because_Cache setEquality natural_numberEquality functionEquality isectElimination sqequalHypSubstitution hypothesis extract_by_obid instantiate applyEquality sqequalRule rename thin setElimination cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[i:\{2...\}].  \mforall{}[x:\{x:\mBbbR{}|  (\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  x)\}  ].
(extracted-rroot(i;x)  \mmember{}  \{y:\mBbbR{}|  ((\muparrow{}isEven(i))  {}\mRightarrow{}  (r0  \mleq{}  y))  \mwedge{}  (y\^{}i  =  x)\}  )

Date html generated: 2018_05_22-PM-02_22_57
Last ObjectModification: 2018_05_21-AM-00_45_41

Theory : reals

Home Index