### Nuprl Lemma : rroot-odd-2-regular

`∀i:{2...}. ∀x:ℝ.  2-regular-seq(rroot-odd(i;x))`

Proof

Definitions occuring in Statement :  rroot-odd: `rroot-odd(i;x)` real: `ℝ` regular-int-seq: `k-regular-seq(f)` int_upper: `{i...}` all: `∀x:A. B[x]` natural_number: `\$n`
Definitions unfolded in proof :  has-value: `(a)↓` sq_type: `SQType(T)` so_apply: `x[s]` so_lambda: `λ2x.t[x]` less_than': `less_than'(a;b)` le: `A ≤ B` nat: `ℕ` rroot-odd: `rroot-odd(i;x)` rroot-abs: `rroot-abs(i;x)` regular-int-seq: `k-regular-seq(f)` rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` guard: `{T}` subtype_rel: `A ⊆r B` true: `True` squash: `↓T` sq_stable: `SqStable(P)` false: `False` prop: `ℙ` top: `Top` exists: `∃x:A. B[x]` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` uimplies: `b supposing a` or: `P ∨ Q` decidable: `Dec(P)` int_upper: `{i...}` nat_plus: `ℕ+` uall: `∀[x:A]. B[x]` real: `ℝ` implies: `P `` Q` member: `t ∈ T` all: `∀x:A. B[x]` ge: `i ≥ j ` assert: `↑b` bnot: `¬bb` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` less_than: `a < b` subtract: `n - m` cand: `A c∧ B` rev_uimplies: `rev_uimplies(P;Q)`

Latex:
\mforall{}i:\{2...\}.  \mforall{}x:\mBbbR{}.    2-regular-seq(rroot-odd(i;x))

Date html generated: 2020_05_20-PM-00_30_38
Last ObjectModification: 2020_03_20-AM-11_01_25

Theory : reals

Home Index