### Nuprl Lemma : near-root-rational

`∀k:{2...}. ∀p:{p:ℤ| (0 ≤ p) ∨ (↑isOdd(k))} . ∀q,n:ℕ+.`
`  (∃r:ℤ × ℕ+ [let a,b = r `
`              in (0 ≤ p `⇐⇒` 0 ≤ a) ∧ (|(r(a))/b^k - (r(p)/r(q))| < (r1/r(n)))])`

Proof

Definitions occuring in Statement :  rdiv: `(x/y)` rless: `x < y` rabs: `|x|` rnexp: `x^k1` int-rdiv: `(a)/k1` rsub: `x - y` int-to-real: `r(n)` isOdd: `isOdd(n)` int_upper: `{i...}` nat_plus: `ℕ+` assert: `↑b` le: `A ≤ B` all: `∀x:A. B[x]` sq_exists: `∃x:A [B[x]]` iff: `P `⇐⇒` Q` or: `P ∨ Q` and: `P ∧ Q` set: `{x:A| B[x]} ` spread: spread def product: `x:A × B[x]` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` prop: `ℙ` or: `P ∨ Q` int_upper: `{i...}` implies: `P `` Q` sq_stable: `SqStable(P)` squash: `↓T` nat_plus: `ℕ+` uimplies: `b supposing a` sq_type: `SQType(T)` guard: `{T}` uiff: `uiff(P;Q)` and: `P ∧ Q` bfalse: `ff` band: `p ∧b q` ifthenelse: `if b then t else f fi ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` bool: `𝔹` decidable: `Dec(P)` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` nat: `ℕ` unit: `Unit` it: `⋅` btrue: `tt` bnot: `¬bb` assert: `↑b` eq_int: `(i =z j)` nequal: `a ≠ b ∈ T ` top: `Top` subtype_rel: `A ⊆r B` subtract: `n - m` ge: `i ≥ j ` le: `A ≤ B` less_than': `less_than'(a;b)` exp: `i^n` primrec: `primrec(n;b;c)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` true: `True` sq_exists: `∃x:A [B[x]]` rneq: `x ≠ y` cand: `A c∧ B` less_than: `a < b` rless: `x < y` isOdd: `isOdd(n)` rev_uimplies: `rev_uimplies(P;Q)` rge: `x ≥ y` req_int_terms: `t1 ≡ t2` rdiv: `(x/y)`

Latex:
\mforall{}k:\{2...\}.  \mforall{}p:\{p:\mBbbZ{}|  (0  \mleq{}  p)  \mvee{}  (\muparrow{}isOdd(k))\}  .  \mforall{}q,n:\mBbbN{}\msupplus{}.
(\mexists{}r:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  [let  a,b  =  r
in  (0  \mleq{}  p  \mLeftarrow{}{}\mRightarrow{}  0  \mleq{}  a)  \mwedge{}  (|(r(a))/b\^{}k  -  (r(p)/r(q))|  <  (r1/r(n)))])

Date html generated: 2020_05_20-PM-00_29_17
Last ObjectModification: 2020_01_06-PM-00_55_43

Theory : reals

Home Index